Formal Specification of Memory Models

摘要

The authors introduce a formal framework for specifying the behavior of memorysystems for shared memory multiprocessors. Specifications in the framework are axiomatic, thereby avoiding ambiguities inherent in most existing specifications, which are informal. The framework makes it convenient to construct correctness arguments for hardware implementations and to generate proofs of critical program fragments. By providing a common language in which a range of memory models can be specified, the framework also permits comparison of existing models and facilitates exploration of the space of possible models. The framework is illustrated with three examples: the well-known Strong Consistency model, and two store ordered models Total Store Ordering (TSO) and Partial Store Ordering (PSO). (Copyright (c) 1991 Xerox Corporation. All rights reserved.)