Shared memory is a mechanism used for inter-process communication in distributed systems which is considered a feasible alternative to the traditional communication model. However, most of the work on shared memory has not paid enough attention to the way memory operations behave, leading to some degree of confusion. In this paper, we describe a framework for specifying the behavior of memory operations. That framework has been used to formally specify some of the most significant memory models. In this framework, to characterize a memory model it is enough to specify the executions that it allows. We use a dual approach. First, we provide axiomatic definitions of those memory models; then, we provide operational ones. Whereas axiomatic definitions are simple and intuitive, operational definitions are more convenient for being used in correctness proofs. We show that both approaches are equivalent.
Using Shared Memory Abstractions to Design Eager Sequentializations for Weak Memory Models
