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

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

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

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

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

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

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

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

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

2.1 系統(tǒng)模型

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

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

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

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

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

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

2.3 模型檢驗(yàn)法(Model Checking)

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

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

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

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

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

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

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

0：表示有0個(gè)實(shí)例；
1：表示有且只有一個(gè)實(shí)例；
*：表示0個(gè)，1個(gè)或者多個(gè)實(shí)例；
+：表示1個(gè)或者多個(gè)實(shí)例。

通過(guò)這些符號(hào)，可以構(gòu)建復(fù)雜狀態(tài)的簡(jiǎn)明表示，例如可以用(I+，S*)來(lái)表示一個(gè)或多個(gè)Cache處于無(wú)效狀態(tài)，0、1或者多個(gè)Cache處于共享狀態(tài)。一個(gè)系統(tǒng)的全局狀態(tài)可以用(q1r1，q2r2，...，qnrn)來(lái)表示，這里n是Cache有限狀態(tài)機(jī)的狀態(tài)數(shù)目，ri屬于[0，1，+，*]。根據(jù)其表示的內(nèi)容，這些表示符號(hào)的順序?yàn)?＜+＜*，0＜*。并定義一個(gè)狀態(tài)集S2包含另一個(gè)狀態(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)的一個(gè)超集，只要驗(yàn)證了S2的正確性，就可以不必再去驗(yàn)證S1的正確性。這是因?yàn)閷?duì)于S1所進(jìn)行的下一次的狀態(tài)轉(zhuǎn)換所形成的狀態(tài)集肯定包含在對(duì)S2所進(jìn)行的下一個(gè)的狀態(tài)轉(zhuǎn)換所形成的狀態(tài)集之中。

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

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

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

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