Analyzing the CRF Java Memory Model

The current Java Memory Model [1] is flawed and has many unintended implications [2]. 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 Murϕ verification system is applied to study the Commit/Reconcile/Fence (CRF) memory model [3], one of the proposed thread semantics to replace the present Java Memory Model. The CRF proposal is formally specified using the Murϕ description language. A suite of test programs is designed to reveal pivotal 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. 1