Specifying Java Thread Semantics Using a Uniform Memory Model
Abstract
Standardized language level support for threads is one of the most important features of Java. However, defining the Java Memory
Model (JMM) has turned out to be a major challenge. Several models produced to date are not as easily comprehensible and comparable
as first thought. Given the growing interest in multithreaded Java programming, it is essential to have a sound framework that would
allow formal specification and reasoning about the JMM.
This paper presents the Uniform Memory Model (UMM), a generic memory model specification framework. Based on guarded commands,
UMM can be easily integrated with a model checking utility, providing strong built-in support for formal verification and
program analysis. With a flexible and simple architecture, UMM is configurable to capture different memory consistency requirements
for both architectural and language level memory models. An alternative formal specification of the JMM, primarily based on
the semantics proposed by Manson and Pugh, is implemented in UMM. Systematic analysis has revealed interesting properties of the
proposed semantics. Inconsistencies from the original specification have also been uncovered.