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

　　在CMP中，多個處理器核心對單一內存空間的共享使得處理器和主存儲器之間的速度差距的矛盾更加突出，因此CMP設計必須采用多級高速緩存Cache，通過層次化的存儲結構來緩解這一矛盾。圖1給出了共享內存的CMP系統模型" title="系統模型">系統模型。與常規SMP系統類似，CMP系統必須解決由此而引發的Cache一致性問題以及一致性驗證問題。采用什么樣的Cache一致性模型與它的驗證方法都將對CMP的整體設計與開發產生重要影響。
　　從CMP中Cache一致性協議的驗證技術的發展來看，目前應用比較廣的驗證方法有狀態列舉法^[1]、模型檢驗法^[2][3]、符號狀態模型法^[4]三種。本文結合CMP的特點，建立了基于MESI一致性協議的CMP驗證模型，并在此模型基礎上分析了這三種驗證方法的基本原理，每一種方法的復雜性分析及優缺點。
1 Cache一致性協議的建模
　　從本質上看Cache一致性協議是由一些過程組成的，這些過程包括Cache與內存控制器之間交換信息以及對處理器事件做出的反應。因此用有限狀態機" title="有限狀態機">有限狀態機模型來描述Cache一致性協議是一件很自然的事情。Cache一致性協議可以在三種不同的層次上建立驗證建模。最高層次是對整個協議行為的抽象，中間層次是在系統/消息傳遞一級進行抽象，最低層次則是在結構模型一級進行抽象，表1給出了這三個層次的抽象模型的特點^[5]。

　　目前對Cache一致性協議驗證研究中，主要是對一致性協議在系統級" title="系統級">系統級進行模型抽象。這主要有三方面的原因：首先，在行為級的抽象中把所有的狀態轉換操作都看作是原子操作是不切合實際的。其次，在行為級層次上進行的驗證實際作用不大。最后，由于系統復雜性的急劇增加，在結構模型的層次上驗證一個Cache一致性協議是不可行的。
　　在系統級上對Cache一致性協議進行驗證具有相對適中的復雜性。在這個層次上，可以通過有限狀態機之間的消息傳遞來描述各個組件間的操作，加深對系統各個組件間相互作用的理解。此外，基于有限狀態機的模型使得我們可以應用層次性驗證的方法。即首先在系統級的層次上驗證協議的正確性，之后就可以進入到更加低級的層次去驗證具體的實現了。
2 Cache一致性協議的驗證方法
2.1 系統模型
　　為了重點說明驗證方法原理，減少具體驗證過程的復雜性，本文所用的驗證分析模型由兩個相同的處理器組成，每個處理器有一個Cache；每個Cache有一個Cache行，應用MESI一致性協議。Cache的有限狀態機具有四個狀態^[6]：M：修改狀態，E：獨占狀態，S：共享狀態， I：無效狀態。圖2給出了驗證模型，圖3給出了MESI一致性協議的有限狀態機。

?

　　應該指出，建立只有一個Cache行的系統模型對于大多數的Cache協議驗證都是足夠的。這是由于協議執行的粒度是Cache行。而對于執行粒度是word的Cache協議，就必須建立起每一個Cache行有幾個word的模型，但是驗證的基本原理都是相同的。
2.2 狀態列舉法(State Enumeration)
　　狀態列舉法^[1][7]研究整個系統的狀態空間。首先用有限狀態機來描述協議中組件的模型，并定義全局狀態由所有組件的狀態組成。然后推導系統所有的可達狀態，推導過程從一個初始的全局狀態出發，進行每一種可能的轉換，這將產生出一些新的狀態。新的狀態如果是第一次出現，將被插入到工作隊列，重復這個過程直到再沒有新的狀態產生為止。在得到所有的可達狀態集合后，需要驗證對于每一個可達的全局狀態。若所有Cache中的數據都是一致的，即可說明要驗證的協議的正確性。在我們的驗證模型中，全局狀態用(s₁,s₂)表示，其中s₁,s₂∈[M E S I]。可以從初始狀態(I，I)出發，逐步得到全部可達狀態集合。表2給出了所有全局狀態，其中有下劃線的為不可達狀態。在所有可達狀態下，Cache間的數據都是一致的，從而驗證了在本文模型下MESI一致性協議的正確性。

　　由于系統的全局狀態是由各個處理器的Cache狀態共同組成的。若一個系統有n個處理器，Cache狀態有m個，有k個與狀態轉換有關的操作，那么系統的狀態空間大小是mⁿ，有k^*mⁿ個狀態轉換操作。隨著處理器數目與Cache協議復雜性的增加，驗證工作的工作量也呈指數級增長。由于狀態列舉法是采用窮舉系統狀態的方法進行驗證，所以其實現復雜性是O(mⁿ)。即使考慮到全局狀態之間的等價關系，把等價的狀態用一個狀態表示，這雖然可以大大減少要驗證狀態的數目，但其實現復雜性依然是O(mⁿ)。
　　狀態列舉法的優點是方法的概念比較簡單，易于理解和實現；協議的模型可以隨著設計的變動而快速的修改，在協議設計初期可以快速地找出設計中的錯誤；可以方便地用程序設計語言對Cache協議進行建模，并可以應用自動化的工具進行驗證。狀態列舉法的主要不足是隨著處理器數目的增加，狀態空間會急劇地以指數級膨脹，因此它的適用性被局限在規模較小的系統中。
2.3 模型檢驗法(Model Checking)
　　模型檢驗就是驗證某個系統的設計是否滿足某種規范，系統的規范用時態邏輯公式來刻畫。而通過對系統可達狀態空間的遍歷來證明設計符合規范。驗證時的輸入是系統設計與要滿足的規范。如果給定的模型滿足給定規范，那么驗證輸出為是，否則可以找出違反了規范的反例，通過反例可以了解設計無法滿足規范的原因，精確地定位設計缺陷。
　　可以用來刻畫模型的規范化語言不是唯一的，這里以CTL(Computation Tree Logic 運算樹邏輯)^[2]為例來定義模型和進行驗證。CTL是常用的布爾命題邏輯(BPL)的擴展，除了支持常規的邏輯操作外，還支持輔助的時序操作和路徑操作符。在運算樹邏輯中，一條路徑是一個無限的狀態序列(s₀,s₁，...)，其中存在著由si到si+1的轉換。這種方法首先要得到系統的全局狀態圖，由系統所有可達的全局狀態及狀態間的轉換操作構成。圖4給出了我們的驗證模型的全局狀態圖。要證明系統滿足數據一致性的性質用AGf表示，這里f為數據保持一致性的命題。并且要求在系統中的所有路徑上的所有狀態都要滿足命題f。在本例中條件滿足，這就說明本文模型下MESI一致性協議的正確性。

　　除了上面的CTL邏輯以外，還可以用其它的時序邏輯公式來描述Cache協議^[3][8]。不同的時態邏輯公式描述方式有所不同，但一般都要先對Cache一致性協議進行抽象，得到一個簡單的模型然后再驗證。
　　早期模型檢驗工具采用顯式的方法來表示狀態空間。由于這種方法的驗證過程也是通過對于全局狀態空間的遍歷實現的，所以也存在著狀態空間膨脹的問題。其實現復雜性與狀態列舉法一樣也是O(mⁿ)。盡管后來在符號模型檢驗^[3][9]中采用了將狀態空間轉化為布爾函數的方法，應用了ORBDD(ordered reduced binary decision diagram)來表示狀態空間，存儲BDD節點所需要的空間仍然與所表達的系統的規模呈指數關系。
　　模型檢驗方法的優點在于時序邏輯強大的表達能力，與狀態列舉法相比，找到滿足Cache一致性性質的表達方式要容易得多。模型檢驗方法的一個主要缺點是建立系統模型的過程非常復雜，經常需要包括一些不必要的協議細節，而且要建立自動檢驗程序也是很困難的。另外在符號狀態檢驗中BDD的大小對布爾變量的順序敏感，不同布爾變量順序對BDD大小影響是顯著的。
2.4 符號狀態模型法(SSM Symbolic State Model)
　　SSM^[4][10][11]法與前面討論的狀態列舉法的不同在于對全局狀態的表示。SSM方法對系統的全局狀態進行了抽象，這種抽象是由以下觀察引發的：首先若系統的各個組件的狀態機是相同的，則所有處于相同狀態的有限狀態機可以集成在一起成為一個集成狀態。其次在所有協議中，不是通過寫更新，就是通過寫無效來實現數據的一致性。而處于Shared狀態拷貝的具體數目與協議正確性無關，關鍵是對某一個特定狀態存在的拷貝的數目是0、1還是多個，從而可以把全局狀態用更抽象的狀態來映射，而不深究處于某一個狀態的Cache的具體數目。定義如下表示符：
　　0：表示有0個實例；
　　1：表示有且只有一個實例；
　　*：表示0個，1個或者多個實例；
　　+：表示1個或者多個實例。
　　通過這些符號，可以構建復雜狀態的簡明表示，例如可以用(I⁺，S^*)來表示一個或多個Cache處于無效狀態，0、1或者多個Cache處于共享狀態。一個系統的全局狀態可以用(q₁^r1，q₂^r2，...，q_n^rn)來表示，這里n是Cache有限狀態機的狀態數目，rⁱ屬于[0，1，+，*]。根據其表示的內容，這些表示符號的順序為1＜+＜*，0＜*。并定義一個狀態集S₂包含另一個狀態集S₁的條件為：q^r1∈S₁，q^r2∈S₂，有q^r1≤q^r2，即r1≤r2，其中q為Cache狀態，ri屬于[0，1，+，*]。包含關系的重要性在于，如果S₂包含S₁，那么S₂所表示的狀態是S₁所表示的狀態的一個超集，只要驗證了S₂的正確性，就可以不必再去驗證S₁的正確性。這是因為對于S₁所進行的下一次的狀態轉換所形成的狀態集肯定包含在對S₂所進行的下一個的狀態轉換所形成的狀態集之中。
　　在SSM中，狀態集的產生是與狀態列舉方法相同的。首先通過當前可以進行的轉換產生新的狀態，然后是一個聚合過程，把處于相同狀態的Cache歸為一類，最后再檢查包含的情況，對于本文的系統模型，從初始的(I⁺)狀態開始的狀態擴張過程，最后形成的狀態轉換圖如圖5^[4]所示。可以看出在狀態擴張過程結束時，只產生了另外的四種狀態：(E，I^*)、(M，I^*)、(S，I⁺)和(S⁺，I^*)。在這五個狀態中，Cache都是一致的，從而驗證了MESI協議的正確性。SSM方法發現協議錯誤的方法與狀態列舉法相同。

　　由于SSM驗證方法產生的狀態空間與要驗證的系統的規模無關，對于協議的驗證也與系統的規模無關，這是SSM方法最主要的一個優點，由于全局狀態數目比較小，相對于傳統的其他方法在狀態遍歷時的開銷要小得多。而且因為它對于不同規模的系統模型做到了100%的覆蓋率，驗證的結果也是可靠的。其主要不足在于建立的模型過于抽象，另外SSM的狀態表達方式也有可能將一些存在錯誤的狀態也引入到可達的集合中，例如(D^*，...)和(D，S^*)。另外一個缺點就是無法對于組件不同的系統進行驗證。
　　本文綜述了CMP系統中Cache一致性協議的驗證方法。其中狀態列舉法在概念上是最簡單的，但存在著狀態空間膨脹的問題。模型檢驗可以驗證任何用時序邏輯表述的性質，但狀態空間膨脹的問題也限制了它的應用，而且在具體的程序設計時的工作量也非常大。SSM方法把多個狀態用一個抽象后的狀態表示，從而大大地縮減了系統的狀態空間，而且驗證所得到的結果也是可以信賴的，但是并不是所有的協議的狀態抽象過程都是直接明了的。這些方法的主要不同在于對協議的建模方法和狀態擴張過程中的采用的縮減狀態空間的方法。
　　隨著CMP的研究的不斷發展，在片上集成的處理器數目將越來越多，消息的傳遞途徑也由總線發展為片上網絡。如何給出更加適用于CMP結構、且高效易用的Cache一致性驗證方法，將是今后CMP的Cache一致性驗證問題的研究方向。

參考文獻
1 COUSOT, P. AND COUSOT, R. Abstract interpretation fram-eworks.[J] Logic Comput. 2,4 (Aug) 1992.
2 J. K. Archibald The Cache Coherence Problem in Shared Memory Multiprocessors[D] PhD Dissertation Department of Computer Science University of Washington Feb 1987
3 BROWNE, M. C., CLARKE, E. M., DILL, D., MISHRA, B. Automatic verification of sequential circuits using temporal logic[J]. IEEE Transactions. Comput. (Dec.), 1986
4 K McMillan Symbolic Model Checking An Approach to the State Explosion Problem [D] Carnegie Mellon University May 1992
5 Fong Pong; Dubois, M A new approach for the verification of cache coherence protocols Parallel and Distributed Systems,[J], IEEE Transactions on Volume 6, Issue 8, Aug. 1995
6 F. Pong and M. Dubois, Verification techniques for cache coherence protocols, [C] ACM Computing Surveys, vol. 29, no. 1, Mar. 1997
7 Ivanov, L.; Nunna, R.;Modeling and verification of cache coherence protocols [C]. ISCAS 2001.The 2001 IEEE Inter-national Symposium on Volume 5, 6-9 May 2001 Page(s):129-132 vol.5
8 Azizi, M; Ait Mohamed, O.; Xiaoyu Song; Cache coherence protocol verification of a multiprocessor system with shared memory[C];Microelectronics, 1998. ICM ′98. Proceedings of the Tenth International Conference Dec. 1998
9 Qadeer, S;Verifying sequential consistency on shared-memory multiprocessors by model checking. Parallel and Distributed Systems, [J],IEEE Transactions on Volume 14, Issue 8, Aug. 2003
10 Hyeong-Ju Kang; In-Cheol Park; SAT-based unbounded symbolic model checking [J] Computer-Aided Design of In-tegrated Circuits and Systems, IEEE Transactions on Volume 24, Issue 2, Feb. 2005
11 F Pong A Nowatzyk G Aybay and M Dubois Veriying Dis-tributed Directory based Cache Coherence Protocols S3.mp a Case Study [C] European Conference on Parallel Computing 1995
12 Fong Pong; Dubois, M. Formal automatic verification of cache coherence in multiprocessors with relaxed memory models [J]Parallel and Distributed Systems, IEEE Transac-tions on Volume 11, Issue 9, Sept. 2000