The Java Memory Model: a Formal Explanation
Marieke Huisman, Gustavo Petri · 2007
This paper discusses the new Java Memory Model (JMM), introduced for Java 1.5. The JMM specifies the allowed executions of multithreaded Java programs. The new JMM fixes some security problems of the previous memory model. In addition, it gives compiler builders the possibility to apply a wide range of singlethreaded compiler optimisations (something that was nearly impossible for the old memory model). For program developers, the JMM provides the following guarantee: if a program does not contain any data races, its allowed behaviours can be described with an interleaving semantics. This paper motivates the definition of the JMM. It shows in particular the consequences of the wish to have the data race freeness guarantee and to forbid any out of thin air values to occur in an execution. The remainder of the paper then discusses a formalisation of the JMM in Coq. This formalisation has been used to prove the data race freeness guarantee. Given the complexity of the JMM definition, having a formalisation is necessary to investigate all aspects of the JMM. Keywords: Java Memory Model, formalisation, Data-Race-Freeness Guarantee