On the Verification of Memory Models of Shared-Memory Multiprocessors

The memory model of a shared-memory multiprocessor is a contract between the designer and programmer of the multiprocessor. We present a model checking algorithm to verify this contract for finite values of the parameters —number of processors and number of memory locations— for a large class of shared-memory systems and memory models. A memory model is a generalization of serial memory, which behaves as if there is a centralized memory that services read and write requests atomically such that a read to a location returns the latest value written to that location. We formalize a memory model as an {\em irreflexive partial order\/} among the memory (read and write) events performed locally at each processor. A run of a memory system satisfies a memory model if there exists a total order of all memory events that is both consistent with all the partial orders and a trace of serial memory. Sequential consistency is an example of a well-known memory model. It has been shown that even for finite parameter values, verifying sequential consistency on general memory systems is undecidable. We show that certain properties of shared-memory systems occurring in practice allow us to do better. In particular, we use the properties of {\em data independence\/} and {\em simple write ordering\/} to design a model checking algorithm which decides whether a system satisfies a memory model.