A Unified Formal Specification and Analysis of the New Java Memory Models

In a multithreaded program running on a multiprocessor platform, dierent processors may observe operations in dierent 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)