Automatic Verification of Sequential Consistency for
Unbounded Addresses and Data Values

Jesse Bingham, Anne Condon, Alan J. Hu, Shaz Qadeer, and Zhichuan Zhang,

Computer Aided Verification:  Sixteenth International Conference,
Lecture Notes in Computer Science Vol. 3114, pp. 427-439,
Springer, 2004.

Sequential consistency is the archetypal correctness condition for the
memory protocols of shared-memory multiprocessors.  Typically, such
protocols are parameterized by the number of processors, the number of
addresses, and the number of distinguishable data values, and
typically, automatic protocol verification analyzes only concrete
instances of the protocol with small values (generally $<3$) for the
protocol parameters.  This paper presents a fully automatic method for
proving the sequential consistency of an entire parameterized family of
protocols, with the number of processors fixed, but the number of
addresses and data values being unbounded parameters.  Using some
practical, reasonable assumptions (data independence, processor
symmetry, location symmetry, simple store ordering, some syntactic
restrictions), the method automatically generates a finite-state
abstract protocol from the parameterized protocol description; proving
sequential consistency of the abstract model, via known methods,
guarantees sequential consistency of the entire protocol family.  The
method is sound, but incomplete, but we argue that it is likely to
apply to most real protocols.  We present experimental results showing
the effectiveness of our method on parameterized versions of the
Piranha shared memory protocol and an extended version of a directory
protocol from the University of Wisconsin Multifacet Project.