Verifying Sequentially Consistent Memory Using Interface Refinement

摘要

In large multiprocessor architectures the design of efficient shared memorysystems is important because the latency imposed on the processors when reading or writing should be kept at a minimum. The challenge that sequentially correct memory poses is not so much the verification of yet another complex protocol but rather the fact that sequential consistency does not comfortably fit the patterns of standard refinement strategies (trace inclusion, failure or ready trace equivalence, testing pre order, bisimulation, etc.). The aim of this paper is to show how sequential consistency can be interpreted as an instance of interface refinement and to verify a sequentially consistent memory protocol--the lazy caching protocol. Section 2 explains and defines sequential consistency. The lazy caching protocol is introduced in Section 3. The heart of the paper is formed by Section 3 and 4. The latter contains the proof of sequential correctness of the protocol. Section 3 gives an overview of the verification methodology. Investigating sequential consistency made us realize that the methodology to prove interface refinement can be considerably simplified. Accordingly, this Section is also of independent interest. In Section 5 some conclusions are drawn.