Analyzing the CRF Java Memory Model
Abstract
The current Java Memory Model is flawed and has many unintended implications. It is a very
challenging task to design or understand a memory model at the programming language level. As multithreaded programming becomes
increasingly popular in Java and hardware memory architectures become more aggressively parallel, it is of significant importance
to provide a framework for formally analyzing the Java Memory Model.
The Murphi verification system is applied to study the Commit/Reconcile/Fence (CRF) memory model, one of the
proposed thread semantics to replace the present Java Memory Model. The CRF proposal is formally specified using the
Murphi description language. A suite of test programs is designed to reveal interesting properties of the model. The
results demonstrate the feasibility of applying model checking techniques to language level memory model specifications. Not only
can it help the designers to debug their designs, it also provides a formal mechanism for Java programmers to understand the
subtleties of the Java Memory Model.