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