基于模型检验的共享内存多处理机时序一致性研究
Verifying Sequential Consistency on Shared-Memory Multiprocessors by Model Checking
摘要：
共享内存多处理器的内存模型是多处理器设计者和程序员之间的契约。顺序一致性存储器模型指定在每个处理器处执行的存储器（读取和写入）事件之间的总顺序。如果在跟踪中存在所有存储器事件的总顺序，则存储器系统的跟踪满足顺序一致性，该总顺序既与每个处理器处的总顺序一致，又具有对位置的每个读取事件返回对该位置的最后写入的值的属性。共享内存系统的描述通常由处理器的数量、内存位置的数量和数据值的数量来参数化。它已被证明，即使是有限的参数值，验证一般共享存储器系统的顺序一致性是不可判定的。我们观察到，在实践中，共享内存系统满足因果关系和数据独立性的属性。因果关系是读事件的值从写事件的值流出的属性。数据独立性是所有跟踪都可以通过重命名来自其中写入的值彼此不同的跟踪的数据值来生成的属性。如果因果和数据独立的系统也具有这样的属性，即每个位置的写入事件的逻辑顺序与它们的时间顺序相同，则可以在算法上验证顺序一致性。具体来说，我们提出了一种模型检验算法来验证此类系统在有限数量的处理器和存储器位置以及任意数量的数据值的序列一致性。
英文摘要：
The memory model of a shared-memory multiprocessor is a contract between the designer and programmer of the multiprocessor. The sequential consistency memory model specifies a total order among the memory (read and write) events performed at each processor. A trace of a memory system satisfies sequential consistency if there exists a total order of all memory events in the trace that is both consistent with the total order at each processor and has the property that every read event to a location returns the value of the last write to that location. Descriptions of shared-memory systems are typically parameterized by the number of processors, the number of memory locations, and the number of data values. It has been shown that even for finite parameter values, verifying sequential consistency on general shared-memory systems is undecidable. We observe that, in practice, shared-memory systems 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 distinct from each other. 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 can be verified algorithmically. Specifically, we present a 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
