OK, well not quite. That was just to get your attention.
Jeremy and I have basically completed our work on the formal
description of a proposed memory model for Java. The proposal is
similar to what was in our Java Grande paper, with the major
extension related to better handling of the cases where a reference
to an object is stored into the heap before the object's construction
is finished. We also tied up lots of loose ends (like fairness).
The following items will be available momentarily for those interested in them:
* A revised version of our Java Grande paper, reflecting the updates
and refinements.
* An executable simulator for the memory model, which for small
program fragments can tell you what behaviors are possible.
Unpredictable prescient writes need a human to provide suggestions
about what unpredictable prescient writes might occur. However, the
rest of the system is completely automatic, and the suggestions are
checked.
To explain the suggestions, consider a long complicated computation
that always computes the value 42 and stores it into the heap. The
simulator can't predict the value of this write and automatically try
performing this write presciently, but if you suggest that 42 should
be written presciently, the simulator can check if that prescient
write is valid (it isn't valid if the prescient write effects the
value written).
The simulator is written in Haskell. We are looking at writing a
separate version in Java for use in the final version of the JMM, and
for provided the added assurance of two separate implementations we
could compare.
* A compiler transformation checker tool. We implemented a tool that
generates program transformations according to standard rules about
what compiler transformations are legal (e.g., you can reorder two
memory references if they aren't aliased or if both of them are
reads). The checker then:
- Takes an example code fragment, runs it through the simulator
- generates transformed versions of the code fragment
- for each transformed fragment, runs the simulator and checks
that the behaviors of the
transformed fragment are a subset of the behaviors of the
original code fragment
For some small code fragments, we are able to exhaustively test all
possible legal permutations of the original code fragments.
* A set of litmus tests that have been modeled by our simulator, and
most have been checked by the compiler transformation checker. We are
working on documenting the litmus tests to explain the motivation or
point of each example.
OK, now Jeremy and I still have lots of work to do to get this stuff
into the shape it would need to be official formal spec of the Java
memory model. But at this point, we really need to start getting more
feedback and involvement from the expert group and the mailing list.
If anyone wants to argue that we should use anything other than the
model that Jeremy and I are proposing, now is the time to do that.
Even assuming no one raises objections, we need to figure out how we
get from what we have to an official spec. How should the spec be
organized, what components should it contain, and so on. Is anyone
other than Jeremy and myself going to write any parts of it? Should
we do a conference call with the expert group, or handle it via email.
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:36 EDT