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 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 fini...