In a multithreaded program running on a multiprocessor platform, different processors may observe operations in different
orders. This may lead to surprising results not anticipated by the programmer. The problem is exacerbated by common compiler
and hardware optimization techniques. A memory (consistency) model provides a contract between the system designer and the
software designer that constrains the order in which operations are observed. Every memory model strikes some balance between
strictness (simplifying program behavior) and laxness (permitting greater optimization). With its emphasis on cross-platform
compatibility, the Java programming language needs a memory model that is satisfactory to language users and implementors.
Everyone in the Java community must be able to understand the Java memory model and its ramifications. The description of
the original Java memory model suffered from ambiguity and opaqueness, and attempts to interpret it revealed serious deficiencies.
Two memory models have been proposed as replacements. Unfortunately, these two new models are described at different levels
of abstraction and are represented in different formats, making it difficult to compare them. In this paper we formalize these
models and develop a unified representation of them, using Abstract State Machines. Using our formal specifications, we relate
the new Java memory models to the Location Consistency memory model and to each other.