CMP中Cache一致性协议的验证

摘要： CMP是处理器体系结构发展的一个重要方向，其中Cache一致性问题的验证是CMP设计中的一项重要课题。基于MESI一致性协议，本文建立了CMP的Cache一致性协议的验证模型，总结了三种三种验证方法验证方法——状态列举法、模型检验法和符号状态法，并给出了每一种方法的复杂性分析。关键词： CMP Cache一致性状态列举模型检验符号状态模型

集成电路工艺的发展使得芯片的集成度不断提高，一种新型体系结构——CMP(Chip Multiprocessor ——片上多处理器)应运而生，通过在一个芯片上集成多个微处理器核心来提高程序的并行性。多个微处理器核心可以并行地执行程序代码，具有较高的线程级并行。由于CMP采用了相对简单的单线程微处理器作为处理器核心，使得CMP具有高主频、设计和验证周期短、控制逻辑简单、扩展性好、易于实现、功耗低、子通信延迟低等优点。此外，CMP还能充分利用不同应用的指令级并行和线程级并行，成为处理器体系结构发展的一个主要趋势。

在CMP中，多个处理器核心对单一内存空间的共享使得处理器和主存储器之间的速度差距的矛盾更加突出，因此CMP设计必须采用多级高速缓存Cache，通过层次化的存储结构来缓解这一矛盾。图1给出了共享内存的CMP系统模型系统模型。与常规SMP系统类似，CMP 系统必须解决由此而引发的Cache一致性问题以及一致性验证问题。采用什么样的Cache一致性模型与它的验证方法都将对CMP的整体设计与开发产生重要影响。从CMP中Cache 一致性协议的验证技术的发展来看，目前应用比较广的验证方法有状态列举法[1]、模型检验法[2][3]、符号状态模型法[4]三种。本文结合CMP的特点，建立了基于MESI一致性协议的CMP验证模型，并在此模型基础上分析了这三种验证方法的基本原理，每一种方法的复杂性分析及优缺点。1 Cache一致性协议的建模从本质上看Cache一致性协议是由一些过程组成的，这些过程包括Cache与内存控制器之间交换信息以及对处理器事件做出的反应。因此用有限状态机有限状态机模型来描述Cache一致性协议是一件很自然的事情。Cache一致性协议可以在三种不同的层次上建立验证建模。最高层次是对整个协议行为的抽象，中间层次是在系统/消息传递一级进行抽象，最低层次则是在结构模型一级进行抽象，表1给出了这三个层次的抽象模型的特点[5]。

目前对Cache一致性协议验证研究中，主要是对一致性协议在系统级系统级进行模型抽象。这主要有三方面的原因：首先，在行为级的抽象中把所有的状态转换操作都看作是原子操作是不切合实际的。其次，在行为级层次上进行的验证实际作用不大。最后，由于系统复杂性的急剧增加，在结构模型的层次上验证一个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 中的数据都是一致的，即可说明要验证的协议的正确性。在我们的验证模型中，全局状态用(s1,s2)表示，其中s1,s2∈[M E S I]。可以从初始状态(I，I)出发，逐步得到全部可达状态集合。表2给出了所有全局状态，其中有下划线的为不可达状态。在所有可达状态下，Cache 间的数据都是一致的，从而验证了在本文模型下MESI一致性协议的正确性。

由于系统的全局状态是由各个处理器的Cache状态共同组成的。若一个系统有n个处理器，Cache状态有m个，有k个与状态转换有关的操作，那么系统的状态空间大小是mn，有k*mn个状态转换操作。随着处理器数目与Cache协议复杂性的增加，验证工作的工作量也呈指数级增长。由于状态列举法是采用穷举系统状态的方法进行验证，所以其实现复杂性是O(mn)。即使考虑到全局状态之间的等价关系，把等价的状态用一个状态表示，这虽然可以大大减少要验证状态的数目，但其实现复杂性依然是O(mn)。状态列举法的优点是方法的概念比较简单，易于理解和实现；协议的模型可以随着设计的变动而快速的修改，在协议设计初期可以快速地找出设计中的错误；可以方便地用程序设计语言对Cache协议进行建模，并可以应用自动化的工具进行验证。状态列举法的主要不足是随着处理器数目的增加，状态空间会急剧地以指数级膨胀，因此它的适用性被局限在规模较小的系统中。2.3 模型检验法(Model Checking) 模型检验就是验证某个系统的设计是否满足某种规范，系统的规范用时态逻辑公式来刻画。而通过对系统可达状态空间的遍历来证明设计符合规范。验证时的输入是系统设计与要满足的规范。如果给定的模型满足给定规范，那么验证输出为是，否则可以找出违反了规范的反例，通过反例可以了解设计无法满足规范的原因，精确地定位设计缺陷。可以用来刻画模型的规范化语言不是唯一的，这里以CTL(Computation Tree Logic 运算树逻辑)[2]为例来定义模型和进行验证。CTL是常用的布尔命题逻辑(BPL)的扩展，除了支持常规的逻辑操作外，还支持辅助的时序操作和路径操作符。在运算树逻辑中，一条路径是一个无限的状态序列(s0,s1，...)，其中存在着由si到si+1的转换。这种方法首先要得到系统的全局状态图，由系统所有可达的全局状态及状态间的转换操作构成。图4给出了我们的验证模型的全局状态图。要证明系统满足数据一致性的性质用AGf表示，这里f为数据保持一致性的命题。并且要求在系统中的所有路径上的所有状态都要满足命题f。在本例中条件满足，这就说明本文模型下MESI一致性协议的正确性。

除了上面的CTL逻辑以外，还可以用其它的时序逻辑公式来描述Cache协议[3][8]。不同的时态逻辑公式描述方式有所不同，但一般都要先对Cache一致性协议进行抽象，得到一个简单的模型然后再验证。早期模型检验工具采用显式的方法来表示状态空间。由于这种方法的验证过程也是通过对于全局状态空间的遍历实现的，所以也存在着状态空间膨胀的问题。其实现复杂性与状态列举法一样也是O(mn)。尽管后来在符号模型检验[3][9]中采用了将状态空间转化为布尔函数的方法，应用了ORBDD(ordered reduced binary decision diagram)来表示状态空间，存储BDD节点所需要的空间仍然与所表达的系统的规模呈指数关系。模型检验方法的优点在于时序逻辑强大的表达能力，与状态列举法相比，找到满足Cache一致性性质的表达方式要容易得多。模型检验方法的一个主要缺点是建立系统模型的过程非常复杂，经常需要包括一些不必要的协议细节，而且要建立自动检验程序也是很困难的。另外在符号状态检验中BDD的大小对布尔变量的顺序敏感，不同布尔变量顺序对BDD大小影响是显著的。2.4 符号状态模型法(SSM Symbolic State Model) SSM[4][10][11]法与前面讨论的状态列举法的不同在于对全局状态的表示。SSM方法对系统的全局状态进行了