  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.
