A Theory of Memory Models (Extended Abstract)

A memory model for a concurrent imperative programming lan-guage specifies which writes to shared variables may be seen by reads performed by other threads. We present a simple mathemat-ical framework for relaxed memory models for programming lan-guages. To instantiate this framework for a specific language, the designer must choose the notion of atomic steps supported by the language (e.g. 32-bit reads and writes) and specify how a composite step may be broken into a sequence of atomic steps (the decompo-sition rule). This rule determines which sequence of intermediate writes (if any) are visible to concurrent reads by other threads. Dif-ferent choices of the rule lead to models which permit a read to re-turn any value if there is a concurrent write (race), or models which satisfy a “No Thin Air Read ” property. The former is suitable for languages such as C++ (programs with races have undefined behav-ior), and the latter for Java. Other intermediate models are possible, useful and interesting. We establish that all models in the framework satisfy the Fun-damental Property of relaxed memory models: programs whose se-quentially consistent (SC) executions have no races must have have only SC executions. We show how to define synchronization con-structs (such as volatiles of various kinds) in the framework, and discuss the causality test cases from the Java Memory Model