The revised version of the paper which completely characterizes
JMM in a non-operational fasion (excluding synchronizations) is
now available from www.cs.technion.ac.il/~assaf/publications/java.ps
The revised version includes a clean operational-to-non-operational
setup, and complete proofs. The hardest of all is the inclusion
of a non-operational model for the case of prescient stores, thus
characterising the maximal weakening of consistency that can be
gained by applying this optimization.
The revised version emphasizes the way JVM memory model is interpreted,
and why no complyant JVM can be built without proper implementation
of this model. This explains why the well-known javasoft bug happened.
--- Assaf
ups: of course, we will be delighted to get feedback and comments.
we do intend to include synchronizations using the same methods,
though the proofs seems to be a lot more involved.
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:27 EDT