Given the growing interest in multithreaded Java programming, it is essential to have a sound framework that would allow formal reasoning about the JMM. In our research, we have adapted the CRF JMM to an executable specification using guarded commands. A model checking tool based on Murphi is integrated with the memory model specification. This enables us to exercise the underlying model with a suite of test programs to reveal pivotal properties and verify common programming idioms. Our formal analysis of the CRF JMM has demonstrated that formal methods, such as model checking, are feasible and effective techniques for understanding a language level memory model. This work is presented in our paper Analyzing the CRF Java Memory Model.
A memory model specification framework should be generic instead of being constrained by any specific architectural designs. It is also useful to have a common memory model specification interface that allows one to easily compare and understand different models. Based on these observations, we have designed the Uniform Memory Model (UMM). UMM is a simple and flexible specification framework with the built-in support for formal verification. It defines memory operations as events controlled by a carefully designed abstract machine. This provides an abstraction mechanism to capture different memory model properties into an executable specification. In addition, UMM also provides additional supports for a language level memory model by including state information of local variables. Thread local data dependency can be precisely specified as explicit conditions in the transition system which is desired to reduce the gap between program and memory semantics. The UMM prototype has been developed in Murphi. An alternative formal specification of the JMM, primarily based on the semantics proposed by Manson and Pugh, is implemented in UMM. Interesting results have been revealed by the systematic analysis using idiom-driven test programs. This work is summerized in our paper Specifying Java Thread Semantics Using a Uniform Memory Model.
This work has also been presented at the Workshop on Software Model Checking (SWMC01) and the Java Verification Workshop (JVW02).
Yue Yang, Ganesh Gopalakrishnan, and Gary Lindstrom, Specifying Java Thread Semantics Using a Uniform Memory Model, in Joint ACM Java Grande/ISCOPE Conference, November 2002. (PDF, Presentation, Murphi Implementation)