JavaMemoryModel: OK, time to get moving again

From: Bill Pugh (pugh@cs.umd.edu)
Date: Mon Jan 13 2003 - 16:28:26 EST


OK, we've been quiet for far too long. Things still need polishing, but
if we wait until things don't need polishing, nothing would ever get done.

We have written up a draft of a new specification the Java memory
model.
        http://www.cs.umd.edu/~pugh/java/memoryModel/newest.pdf

We would like to see some feedback on this, as we believe that it
encompasses all of the necessary features for field accesses. Discussion
of final and volatile fields isn't included in this release.

This is really for the academic memory model geeks; this isn't a
version primarily intended for Java programmers or VM implementors.

The new semantics are not intended to be any different than our previous
semantics. However, the form of the new semantics is significantly different.
We made this change to allow us to formally prove the things that needed to
be proved, and also because we believe it will be easier to understand.
Our semantics is no longer operational; instead, it just allows you
to determine
whether a particular execution is legal. Also, rather than talking
about overwritten, previous and allWrite sets, we talk about
execution traces and happens-before edges and paths. It is really
just two ways of talking about the same thing.

We have changed the way we describe the semantics from our last release.
We don't talk about prescient reads anymore, but we do introduce the
notion of a "causal order" that is used to justify a read. This is how we
now get around the problems associated with causal loops.

We made this change for two reasons. First, we think it will now be
easier to understand. Second, this made it easier to understand why the
semantics exhibit the desired behavior. We are now able to show that
correctly synchronized programs have sequentially consistent semantics and
that many standard transformations are legal.

We aren't any happier than many of you that we've had to go through
so many revisions. However, we believe it is essential to have a
semantics with the required properties and be able to formally prove
that it has those properties.

Please try to take a look at it and provide feedback. We think that we
are past the point of needing substantial changes, but we would like to
hear what people have to say.

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



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