Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models
Abstract
Conforming to the underlying memory consistency rules is a fundamental requirement for implementing shared memory systems and writing 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 have developed a specification framework called Nemos (Non-operational yet Executable Memory Ordering Specifications), which employs a uniform notation based on predicate logic to define shared memory semantics in an axiomatic as well as compositional style. In this paper, we present this framework and discuss how constraint logic programming and SAT solving can be used to make these axiomatic specifications executable for memory model analysis, thus supporting precise specification and automatic execution in the same framework. To illustrate our approach, this paper formalizes a collection of well known memory models, including sequential consistency, coherence, PRAM, causal consistency, and processor consistency.