*
Thomas A. Henzinger,
Shaz Qadeer, and Sriram K. Rajamani*

In shared-memory multiprocessors *sequential consistency* offers a
natural tradeoff between the flexibility afforded to the implementor and the
complexity of the programmer's view of the memory. Sequential consistency
requires that some interleaving of the local temporal orders of read/write
events at different processors be a trace of serial memory. We develop a
systematic methodology for proving sequential consistency for memory systems
with three parameters --number of processors, number of memory locations, and
number of data values. From the definition of sequential consistency it
suffices to construct a non-interfering observer that watches and reorders
read/write events so that a trace of serial memory is obtained. While in
general such an observer must be unbounded even for fixed values of the
parameters --checking sequential consistency is undecidable!-- we show that
for two paradigmatic protocol classes --*lazy caching* and *snoopy
cache coherence*-- there exist finite-state observers. In these cases,
sequential consistency for fixed parameter values can thus be checked by
language inclusion between finite automata.

In order to reduce the arbitrary-parameter problem to the fixed-parameter
problem, we develop a novel framework for induction over the number of
processors. Classical induction schemas, which are based on process
invariants that are inductive with respect to an implementation preorder that
preserves the temporal sequence of events, are inadequate for our purposes,
because proving sequential consistency requires the reordering of events.
Hence we introduce *merge invariants*, which permit certain reorderings
of read/write events. We show that under certain reasonable assumptions
about the memory system, it is possible to conclude sequential consistency
for any number of processors, memory locations, and data values by model
checking two finite-state lemmas about process and merge invariants: they
involve two processors each accessing a maximum of three locations, where
each location stores at most two data values. For both lazy caching and
snoopy cache coherence we are able to discharge the two lemmas using the
model checker Mocha.

*Proceedings of the
11th International Conference on Computer-Aided Verification*
(CAV),
Lecture Notes in Computer Science 1633,
Springer, 1999, pp. 301-315.

Download inofficial, sometimes updated PostScript / PDF document. © 1999 Springer.