Submitted for publication.
A memory model for a concurrent imperative programming language specifies which writes to shared variables may be seen by reads performed by other threads. We present a simple mathematical framework for relaxed memory models for programming languages. 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 decomposition rule). This rule determines which sequence of intermediate writes (if any) are visible to concurrent reads by other threads. Different choices of the rule lead to models which permit a read to return 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 behavior), and the latter for Java. Other intermediate models are possible, useful and interesting.
Full paper (pdf) (Updated 9/16/2006, with some typos fixed.)