JavaMemoryModel: revised version of non-operational JMM paper

From: Assaf Schuster (
Date: Mon Sep 25 2000 - 15:42:59 EDT

The revised version of the paper which completely characterizes
JMM in a non-operational fasion (excluding synchronizations) is
now available from

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 -

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