片上多處理器中Cache一致性協(xié)議的驗證

集成電路工藝的發(fā)展使得芯片的集成度不斷提高，一種新型體系結(jié)構(gòu)——CMP(Chip Multiprocessor ——片上多處理器)應(yīng)運而生，通過在一個芯片上集成多個微處理器核心來提高程序的并行性。多個微處理器核心可以并行地執(zhí)行程序代碼，具有較高的線程級并行。由于CMP采用了相對簡單的單線程微處理器作為處理器核心，使得CMP具有高主頻、設(shè)計和驗證周期短、控制邏輯簡單、擴展性好、易于實現(xiàn)、功耗低、子通信延遲低等優(yōu)點。此外，CMP還能充分利用不同應(yīng)用的指令級并行和線程級并行，成為處理器體系結(jié)構(gòu)發(fā)展的一個主要趨勢。

在CMP中，多個處理器核心對單一內(nèi)存空間的共享使得處理器和主存儲器之間的速度差距的矛盾更加突出，因此CMP設(shè)計必須采用多級高速緩存Cache，通過層次化的存儲結(jié)構(gòu)來緩解這一矛盾。圖1給出了共享內(nèi)存的CMP系統(tǒng)模型。與常規(guī)SMP系統(tǒng)類似，CMP系統(tǒng)必須解決由此而引發(fā)的Cache一致性問題以及一致性驗證問題。采用什么樣的Cache一致性模型與它的驗證方法都將對CMP的整體設(shè)計與開發(fā)產(chǎn)生重要影響。

　　從CMP中Cache一致性協(xié)議的驗證技術(shù)的發(fā)展來看，目前應(yīng)用比較廣的驗證方法有狀態(tài)列舉法[1]、模型檢驗法[2][3]、符號狀態(tài)模型法[4]三種。本文結(jié)合CMP的特點，建立了基于MESI一致性協(xié)議的CMP驗證模型，并在此模型基礎(chǔ)上分析了這三種驗證方法的基本原理，每一種方法的復(fù)雜性分析及優(yōu)缺點。

1 Cache一致性協(xié)議的建模

從本質(zhì)上看Cache一致性協(xié)議是由一些過程組成的，這些過程包括Cache與內(nèi)存控制器之間交換信息以及對處理器事件做出的反應(yīng)。因此用有限狀態(tài)機模型來描述Cache一致性協(xié)議是一件很自然的事情。Cache一致性協(xié)議可以在三種不同的層次上建立驗證建模。最高層次是對整個協(xié)議行為的抽象，中間層次是在系統(tǒng)/消息傳遞一級進行抽象，最低層次則是在結(jié)構(gòu)模型一級進行抽象，表1給出了這三個層次的抽象模型的特點[5]。

目前對Cache一致性協(xié)議驗證研究中，主要是對一致性協(xié)議在系統(tǒng)級進行模型抽象。這主要有三方面的原因：首先，在行為級的抽象中把所有的狀態(tài)轉(zhuǎn)換操作都看作是原子操作是不切合實際的。其次，在行為級層次上進行的驗證實際作用不大。最后，由于系統(tǒng)復(fù)雜性的急劇增加，在結(jié)構(gòu)模型的層次上驗證一個Cache一致性協(xié)議是不可行的。

在系統(tǒng)級上對Cache一致性協(xié)議進行驗證具有相對適中的復(fù)雜性。在這個層次上，可以通過有限狀態(tài)機之間的消息傳遞來描述各個組件間的操作，加深對系統(tǒng)各個組件間相互作用的理解。此外，基于有限狀態(tài)機的模型使得我們可以應(yīng)用層次性驗證的方法。即首先在系統(tǒng)級的層次上驗證協(xié)議的正確性，之后就可以進入到更加低級的層次去驗證具體的實現(xiàn)了。

2 Cache一致性協(xié)議的驗證方法

2.1 系統(tǒng)模型

為了重點說明驗證方法原理，減少具體驗證過程的復(fù)雜性，本文所用的驗證分析模型由兩個相同的處理器組成，每個處理器有一個Cache；每個Cache有一個Cache行，應(yīng)用MESI一致性協(xié)議。Cache的有限狀態(tài)機具有四個狀態(tài)[6]：M：修改狀態(tài)，E：獨占狀態(tài)，S：共享狀態(tài)， I：無效狀態(tài)。圖2給出了驗證模型，圖3給出了MESI一致性協(xié)議的有限狀態(tài)機。

應(yīng)該指出，建立只有一個Cache行的系統(tǒng)模型對于大多數(shù)的Cache協(xié)議驗證都是足夠的。這是由于協(xié)議執(zhí)行的粒度是Cache行。而對于執(zhí)行粒度是word的Cache協(xié)議，就必須建立起每一個Cache行有幾個word的模型，但是驗證的基本原理都是相同的。

2.2 狀態(tài)列舉法(State Enumeration)

狀態(tài)列舉法[1][7]研究整個系統(tǒng)的狀態(tài)空間。首先用有限狀態(tài)機來描述協(xié)議中組件的模型，并定義全局狀態(tài)由所有組件的狀態(tài)組成。然后推導(dǎo)系統(tǒng)所有的可達狀態(tài)，推導(dǎo)過程從一個初始的全局狀態(tài)出發(fā)，進行每一種可能的轉(zhuǎn)換，這將產(chǎn)生出一些新的狀態(tài)。新的狀態(tài)如果是第一次出現(xiàn)，將被插入到工作隊列，重復(fù)這個過程直到再沒有新的狀態(tài)產(chǎn)生為止。在得到所有的可達狀態(tài)集合后，需要驗證對于每一個可達的全局狀態(tài)。若所有Cache中的數(shù)據(jù)都是一致的，即可說明要驗證的協(xié)議的正確性。在我們的驗證模型中，全局狀態(tài)用(s1,s2)表示，其中s1,s2∈[M E S I]。可以從初始狀態(tài)(I，I)出發(fā)，逐步得到全部可達狀態(tài)集合。表2給出了所有全局狀態(tài)，其中有下劃線的為不可達狀態(tài)。在所有可達狀態(tài)下，Cache間的數(shù)據(jù)都是一致的，從而驗證了在本文模型下MESI一致性協(xié)議的正確性。

由于系統(tǒng)的全局狀態(tài)是由各個處理器的Cache狀態(tài)共同組成的。若一個系統(tǒng)有n個處理器，Cache狀態(tài)有m個，有k個與狀態(tài)轉(zhuǎn)換有關(guān)的操作，那么系統(tǒng)的狀態(tài)空間大小是mn，有k*mn個狀態(tài)轉(zhuǎn)換操作。隨著處理器數(shù)目與Cache協(xié)議復(fù)雜性的增加，驗證工作的工作量也呈指數(shù)級增長。由于狀態(tài)列舉法是采用窮舉系統(tǒng)狀態(tài)的方法進行驗證，所以其實現(xiàn)復(fù)雜性是O(mn)。即使考慮到全局狀態(tài)之間的等價關(guān)系，把等價的狀態(tài)用一個狀態(tài)表示，這雖然可以大大減少要驗證狀態(tài)的數(shù)目，但其實現(xiàn)復(fù)雜性依然是O(mn)。

狀態(tài)列舉法的優(yōu)點是方法的概念比較簡單，易于理解和實現(xiàn)；協(xié)議的模型可以隨著設(shè)計的變動而快速的修改，在協(xié)議設(shè)計初期可以快速地找出設(shè)計中的錯誤；可以方便地用程序設(shè)計語言對Cache協(xié)議進行建模，并可以應(yīng)用自動化的工具進行驗證。狀態(tài)列舉法的主要不足是隨著處理器數(shù)目的增加，狀態(tài)空間會急劇地以指數(shù)級膨脹，因此它的適用性被局限在規(guī)模較小的系統(tǒng)中。

2.3 模型檢驗法(Model Checking)

模型檢驗就是驗證某個系統(tǒng)的設(shè)計是否滿足某種規(guī)范，系統(tǒng)的規(guī)范用時態(tài)邏輯公式來刻畫。而通過對系統(tǒng)可達狀態(tài)空間的遍歷來證明設(shè)計符合規(guī)范。驗證時的輸入是系統(tǒng)設(shè)計與要滿足的規(guī)范。如果給定的模型滿足給定規(guī)范，那么驗證輸出為是，否則可以找出違反了規(guī)范的反例，通過反例可以了解設(shè)計無法滿足規(guī)范的原因，精確地定位設(shè)計缺陷。

可以用來刻畫模型的規(guī)范化語言不是唯一的，這里以CTL(Computation Tree Logic 運算樹邏輯)[2]為例來定義模型和進行驗證。CTL是常用的布爾命題邏輯(BPL)的擴展，除了支持常規(guī)的邏輯操作外，還支持輔助的時序操作和路徑操作符。在運算樹邏輯中，一條路徑是一個無限的狀態(tài)序列(s0,s1，...)，其中存在著由si到si+1的轉(zhuǎn)換。這種方法首先要得到系統(tǒng)的全局狀態(tài)圖，由系統(tǒng)所有可達的全局狀態(tài)及狀態(tài)間的轉(zhuǎn)換操作構(gòu)成。圖4給出了我們的驗證模型的全局狀態(tài)圖。要證明系統(tǒng)滿足數(shù)據(jù)一致性的性質(zhì)用AGf表示，這里f為數(shù)據(jù)保持一致性的命題。并且要求在系統(tǒng)中的所有路徑上的所有狀態(tài)都要滿足命題f。在本例中條件滿足，這就說明本文模型下MESI一致性協(xié)議的正確性。

除了上面的CTL邏輯以外，還可以用其它的時序邏輯公式來描述Cache協(xié)議[3][8]。不同的時態(tài)邏輯公式描述方式有所不同，但一般都要先對Cache一致性協(xié)議進行抽象，得到一個簡單的模型然后再驗證。

早期模型檢驗工具采用顯式的方法來表示狀態(tài)空間。由于這種方法的驗證過程也是通過對于全局狀態(tài)空間的遍歷實現(xiàn)的，所以也存在著狀態(tài)空間膨脹的問題。其實現(xiàn)復(fù)雜性與狀態(tài)列舉法一樣也是O(mn)。盡管后來在符號模型檢驗[3][9]中采用了將狀態(tài)空間轉(zhuǎn)化為布爾函數(shù)的方法，應(yīng)用了ORBDD(ordered reduced binary decision diagram)來表示狀態(tài)空間，存儲BDD節(jié)點所需要的空間仍然與所表達的系統(tǒng)的規(guī)模呈指數(shù)關(guān)系。

模型檢驗方法的優(yōu)點在于時序邏輯強大的表達能力，與狀態(tài)列舉法相比，找到滿足Cache一致性性質(zhì)的表達方式要容易得多。模型檢驗方法的一個主要缺點是建立系統(tǒng)模型的過程非常復(fù)雜，經(jīng)常需要包括一些不必要的協(xié)議細節(jié)，而且要建立自動檢驗程序也是很困難的。另外在符號狀態(tài)檢驗中BDD的大小對布爾變量的順序敏感，不同布爾變量順序?qū)DD大小影響是顯著的。

2.4 符號狀態(tài)模型法(SSM Symbolic State Model)

SSM[4][10][11]法與前面討論的狀態(tài)列舉法的不同在于對全局狀態(tài)的表示。SSM方法對系統(tǒng)的全局狀態(tài)進行了抽象，這種抽象是由以下觀察引發(fā)的：首先若系統(tǒng)的各個組件的狀態(tài)機是相同的，則所有處于相同狀態(tài)的有限狀態(tài)機可以集成在一起成為一個集成狀態(tài)。其次在所有協(xié)議中，不是通過寫更新，就是通過寫無效來實現(xiàn)數(shù)據(jù)的一致性。而處于Shared狀態(tài)拷貝的具體數(shù)目與協(xié)議正確性無關(guān)，關(guān)鍵是對某一個特定狀態(tài)存在的拷貝的數(shù)目是0、1還是多個，從而可以把全局狀態(tài)用更抽象的狀態(tài)來映射，而不深究處于某一個狀態(tài)的Cache的具體數(shù)目。定義如下表示符：

0：表示有0個實例；
1：表示有且只有一個實例；
*：表示0個，1個或者多個實例；
+：表示1個或者多個實例。

通過這些符號，可以構(gòu)建復(fù)雜狀態(tài)的簡明表示，例如可以用(I+，S*)來表示一個或多個Cache處于無效狀態(tài)，0、1或者多個Cache處于共享狀態(tài)。一個系統(tǒng)的全局狀態(tài)可以用(q1r1，q2r2，...，qnrn)來表示，這里n是Cache有限狀態(tài)機的狀態(tài)數(shù)目，ri屬于[0，1，+，*]。根據(jù)其表示的內(nèi)容，這些表示符號的順序為1＜+＜*，0＜*。并定義一個狀態(tài)集S2包含另一個狀態(tài)集S1的條件為：qr1∈S1，qr2∈S2，有qr1≤qr2，即r1≤r2，其中q為Cache狀態(tài)，ri屬于[0，1，+，*]。包含關(guān)系的重要性在于，如果S2包含S1，那么S2所表示的狀態(tài)是S1所表示的狀態(tài)的一個超集，只要驗證了S2的正確性，就可以不必再去驗證S1的正確性。這是因為對于S1所進行的下一次的狀態(tài)轉(zhuǎn)換所形成的狀態(tài)集肯定包含在對S2所進行的下一個的狀態(tài)轉(zhuǎn)換所形成的狀態(tài)集之中。

在SSM中，狀態(tài)集的產(chǎn)生是與狀態(tài)列舉方法相同的。首先通過當前可以進行的轉(zhuǎn)換產(chǎn)生新的狀態(tài)，然后是一個聚合過程，把處于相同狀態(tài)的Cache歸為一類，最后再檢查包含的情況，對于本文的系統(tǒng)模型，從初始的(I+)狀態(tài)開始的狀態(tài)擴張過程，最后形成的狀態(tài)轉(zhuǎn)換圖如圖5[4]所示。可以看出在狀態(tài)擴張過程結(jié)束時，只產(chǎn)生了另外的四種狀態(tài)：(E，I*)、(M，I*)、(S，I+)和(S+，I*)。在這五個狀態(tài)中，Cache都是一致的，從而驗證了MESI協(xié)議的正確性。SSM方法發(fā)現(xiàn)協(xié)議錯誤的方法與狀態(tài)列舉法相同。

由于SSM驗證方法產(chǎn)生的狀態(tài)空間與要驗證的系統(tǒng)的規(guī)模無關(guān)，對于協(xié)議的驗證也與系統(tǒng)的規(guī)模無關(guān)，這是SSM方法最主要的一個優(yōu)點，由于全局狀態(tài)數(shù)目比較小，相對于傳統(tǒng)的其他方法在狀態(tài)遍歷時的開銷要小得多。而且因為它對于不同規(guī)模的系統(tǒng)模型做到了100%的覆蓋率，驗證的結(jié)果也是可靠的。其主要不足在于建立的模型過于抽象，另外SSM的狀態(tài)表達方式也有可能將一些存在錯誤的狀態(tài)也引入到可達的集合中，例如(D*，...)和(D，S*)。另外一個缺點就是無法對于組件不同的系統(tǒng)進行驗證。

本文綜述了CMP系統(tǒng)中Cache一致性協(xié)議的驗證方法。其中狀態(tài)列舉法在概念上是最簡單的，但存在著狀態(tài)空間膨脹的問題。模型檢驗可以驗證任何用時序邏輯表述的性質(zhì)，但狀態(tài)空間膨脹的問題也限制了它的應(yīng)用，而且在具體的程序設(shè)計時的工作量也非常大。SSM方法把多個狀態(tài)用一個抽象后的狀態(tài)表示，從而大大地縮減了系統(tǒng)的狀態(tài)空間，而且驗證所得到的結(jié)果也是可以信賴的，但是并不是所有的協(xié)議的狀態(tài)抽象過程都是直接明了的。這些方法的主要不同在于對協(xié)議的建模方法和狀態(tài)擴張過程中的采用的縮減狀態(tài)空間的方法。

隨著CMP的研究的不斷發(fā)展，在片上集成的處理器數(shù)目將越來越多，消息的傳遞途徑也由總線發(fā)展為片上網(wǎng)絡(luò)。如何給出更加適用于CMP結(jié)構(gòu)、且高效易用的Cache一致性驗證方法，將是今后CMP的Cache一致性驗證問題的研究方向。