JavaMemoryModel: Model Checking the CRF JMM

From: Yue Yang (yyang@lsil.com)
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
http://www.cs.utah.edu/~yyang/research/paper.pdf.

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 - http://www.cs.umd.edu/~pugh/java/memoryModel



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