Verifying Sequential Consistency on Shared-Memory Multiprocessors by Model Checking
Verifying Sequential Consistency on Shared-Memory Multiprocessors by Model Checking
复制标题
通过模型检查验证共享内存多处理器上的顺序一致性
DOI：
--
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
S. Qadeer
中科院分区：
文献类型：
--
作者：
S. Qadeer
共享内存多处理器的内存模型是多处理器的设计者和程序员之间的契约。存储器模型通常通过高速缓存一致性协议来实现。该协议的设计是多处理器设计中最复杂的方面之一，因此很容易出错。但是，必须确保缓存一致性协议满足共享内存模型。我们提出了一种新的技术，基于模型检测来解决这个困难的问题的重要和著名的共享内存模型的顺序一致性。令人惊讶的是，验证顺序一致性一般是不可判定的，即使是有限状态缓存一致性协议。在实践中，缓存一致性协议满足因果关系和数据独立性的属性。因果关系是读事件的值从写事件的值流出的属性。数据独立性是所有跟踪都可以通过重命名写入值成对不同的跟踪中的数据值来生成的属性。我们表明，如果一个因果和数据独立的系统也有属性，写事件的逻辑顺序，每个位置是相同的时间顺序，然后顺序一致性是可判定的。我们提出了一种新的模型检测算法来验证有限数量的处理器和存储器位置和任意数量的数据值在这样的系统上的顺序一致性。
The memory model of a shared-memory multiprocessor is a contract between the designer and the programmer of the multiprocessor. A memory model is typically implemented by means of a cache-coherence protocol. The design of this protocol is one of the most complex aspects of multiprocessor design and is consequently quite error-prone. However, it is imperative to ensure that the cache-coherence protocol satisfies the shared-memory model. We present a novel technique based on model checking to tackle this difficult problem for the important and well-known shared-memory model of sequential consistency. Surprisingly, verifying sequential consistency is undecidable in general, even for finite-state cache-coherence protocols. In practice, cache-coherence protocols satisfy the properties of causality and data independence. Causality is the property that values of read events flow from values of write events. Data independence is the property that all traces can be generated by renaming data values from traces where the written values are pairwise distinct. We show that, if a causal and data independent system also has the property that the logical order of write events to each location is identical to their temporal order, then sequential consistency is decidable. We present a novel model checking algorithm to verify sequential consistency on such systems for a finite number of processors and memory locations and an arbitrary number of data values.