Nemos: a framework for axiomatic and executable specifications of memory consistency models

Abstract

Summary form only given. 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 specifications executable for memory model analysis. To illustrate our approach, we formalize a collection of classical memory models, including sequential consistency, coherence, PRAM, causal consistency, and processor consistency.