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

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

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

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

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

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

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

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

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

2.1 系統模型

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

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

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

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

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

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

2.3 模型檢驗法(Model Checking)

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

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

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

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

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

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

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

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

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

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

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

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

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