JavaMemoryModel: A paper on JMM

From: Abhik Roychoudhury (
Date: Tue Jun 04 2002 - 03:13:32 EDT

Hi all,
We would like to bring your attention to
the following paper about Java Memory Model.

"Specifying Multithreaded Java Semantics for Program Verification"
-Abhik Roychoudhury and Tulika Mitra
In Proceedings of International Conference on Software Engineering (ICSE) 2002.

This paper is written from a formal specification/verification perspective.
In particular, it develops a formal executable specification of the old
Java Memory Model. This is achieved by modeling the different actions in
the old JMM as guarded commands. The paper illustrates (a) how the operational
specification style makes the understanding of JMM easier, and (b) how
the executable specification allows the JMM to be integrated into
invariant checking of low-level code.

The paper is available at:
and the slides for the conference presentation are available at:

-Abhik and Tulika.
National University of Singapore.

JavaMemoryModel mailing list -

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