Jeremy and I have written up a very rough draft of a new approach to
specifying the Java Memory Model:
http://www.cs.umd.edu/~pugh/java/memoryModel/newApproach.pdf
The write up is rough, but complete enough to ask for (forgiving) feedback on.
We have changed the way we describe the semantics. 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 made the change because I think it will be easier for others to
understand. If people don't like the new way of talking about the
memory model, we can easily go back to talking about allWrites,
overwritten and previous.
The rough draft doesn't include anything about final fields, and
gives purely sequentially consistent semantics for volatiles. It also
doesn't really address causal loops.
The writeup is only 7 pages long, describes the semantics, gives an
example, and proofs that correctly synchronized programs have
sequentially consistent semantics and that standard reordering
transformations are legal.
Please try to take a quick look at it and provide feedback. This is
still rough enough that we would be willing to consider substantial
changes. However, at the moment we are pretty happy with this new
approach.
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:40 EDT