JavaMemoryModel: IMPORTANT: New Unified JMM formalism, $100 reward for any flaws

From: Bill Pugh (pugh@cs.umd.edu)
Date: Tue Mar 16 2004 - 10:39:52 EST


Jeremy, Sarita and I have managed to put together a new unified proposal
for the Java Memory Model that manages to combine many of the features
of the earlier M/P and SC- proposal. Doug Lea also provided a lot
of important feedback.

Nothing really changes in terms of the behaviors we have previously
discussed. This proposal just about a way of formalizing the behaviors
we've agreed on for some time.

Obviously, we are not thrilled about introducing a new model so close
to our
deadline. But we weren't satisfied with the existing proposals, and the
new proposal seems clearly superior, both in terms of simplicity and
behavior,
to previous proposals.

We've been working very hard on this, and we are now satisfied enough
with
it that we would like feedback from the JMM and JSR-133 community.
Actually,
we are feeling pretty optimistic about this model. As Sarita noted, some
of the important proofs are "absurdly, uncomfortably too simple".

We would also like to encourage people to aggressively "Tiger Team" it,
and try
to break it. So I am personally offering a $100 reward to the first
person to
find a substantial flaw in the model. That doesn't include things like
a proof
that needs to be fixed, or something that is unclear or presently
poorly.
Instead, a flaw would be a behavior allowed by existing and reasonable
compiler
and processor optimizations but prohibited by the model, or a behavior
that
is allowed by the model that needs to be prohibited for clear and
convincing
reasons.

Information about the new model is described on a web page:
        http://www.cs.umd.edu/~pugh/java/memoryModel/unifiedProposal/

At the moment, the documents up there are:
  * An overview of the model, including a one page description of the
model
    and descriptions of some behaviors allowed and disallowed by the
model
  * Worked examples of applying the new model to causality test cases
1-20.
  * Proofs that standard compiler reordering transformations are legal,
    and that correctly synchronized programs have only sequentially
consistent
    behaviors

Sarita has also been working on a proof that an implementation of her
system-centric
model obeys the new memory model, and I'll add a link to that when it
is ready.

I should mention that we are still considering different ways of
presenting this
material that are provably equivalent, but may be easier to understand.
But right
now, we want feedback as to whether our new model has the correct
behavior.

Bill

-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



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