Verifying sequential consistency on shared-memory multiprocessor systems

Abstract. In shared-memory multiprocessors sequential consistency o ers a natural tradeo between the exibility a orded to the implementor and the complexity ofthe programmer's view of the memory. Sequential consistency requires that some interleaving of the local temporal orders of read/write events at di erent processors be a trace of serial memory. Wedevelop 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 de nition of sequential consistency it su ces 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 mustbeunbounded even for xed 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 nite-state observers. In these cases, sequential consistency for xed parameter values can thus be checked by language inclusion between nite automata. In order to reduce the arbitrary-parameter problem to the xed-parameter problem