Under consideration for publication in Theory and Practice of Logic Programming 1 A Constraint-Based Approach for Specifying Memory Consistency Models

Conforming to the underlying memory consistency rules is a fundamental requirement for implementing shared memory systems and writing multiprocessor software. In order to promote understanding and enable rigorous analysis, it is highly desirable that a memory model specification be both declarative and executable. In this paper, we explore the practicality of analyzing memory consistency models us-ing constraint solving. By precisely defining a memory model as a set of constraints in an axiomatic and compositional style, our approach provides a generic formalism for specify-ing memory consistency models. Furthermore, this framework offers a unique advantage for program verification, i.e., it enables an accurate and exhaustive analysis of program properties which covers all execution paths for a given shared memory system. With this constraint-base approach, this paper formalizes a collection of classical memory models as well as the memory ordering rules of the Intel Itanium processor families. We also dis-cuss how logic programming and constraint solving can be used to make these axiomatic specifications executable to support automated analysis