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:
http://www.comp.nus.edu.sg/~abhik/pdf/icse02.pdf
and the slides for the conference presentation are available at:
http://www.comp.nus.edu.sg/~abhik/talks/icse02.ppt
-Abhik and Tulika.
National University of Singapore.
http://www.comp.nus.edu.sg/~abhik
http://www.comp.nus.edu.sg/~tulika
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:40 EDT