1;3409;0c Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models

Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models

18th International Parallel and Distributed Processing Symposium (IPDPS 2004), 2004
DOI: 10.1109/IPDPS.2004.1302944

IPDPS

bibtex

Conforming to the underlying memory consistency rules is a fundamental requirement for implementing shared memory systems and developing multiprocessor programs. In order to promote understanding and enable automated verification, it is highly desirable that a memory model specification be both declarative and executable. We present a specification framework called Nemos (Nonoperational yet Executable Memory Ordering Specifications), which supports precise specification and automatic execution in the same framework. We employ a uniform notation based on predicate logic to define shared memory semantics in an axiomatic as well as compositional style. We also apply constraint logic programming and SAT solving to make the axiomatic speci.cations executable for memory model analysis. To illustrate our approach, this paper formalizes a collection of classical memory models, including sequential consistency, coherence, PRAM, causal consistency, and processor consistency.