集成电路工艺的发展使得芯片的集成度不断提高，一种新型体系结构——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