JavaMemoryModel: Model Checking the CRF JMM

From: Yue Yang (
Date: Mon Jul 02 2001 - 13:07:21 EDT

As an effort to formally study a language level memory model, we have
developed a framework to specify and reason the CRF JMM using Model
Checking techniques.

The CRF model is implemented in Murphi as a "memory model engine" and a
suite of test programs are developed to study important properties
including the ordering rules, constructor properties, and
synchronization idioms such as the "double-checked locking" pattern.
This mechanism enables one to exhaustively exercise a language level
memory model on a particular program.

Our approach and initial results are presented in a paper entitled
"Analyzing the CRF Java Memory Model with Murphi" available at

Your comments and suggestions are very welcome.

Best Regards,

-- Jason

  Jason Yue Yang
  Computer Science Dept.
  University of Utah
  Tel: (801)733-2007 Fax: (801)733-2022

JavaMemoryModel mailing list -

This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:32 EDT