Re: JavaMemoryModel: New approach to defining the Java Memory Model

From: Bill Pugh (pugh@cs.umd.edu)
Date: Mon Jul 22 2002 - 14:03:13 EDT


At 2:28 PM -0700 7/21/02, Paul Haahr wrote:
> > 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
>
>I like the idea of basing the sematics on execution traces rather than
>the the allWrites, etc, sets. But, I actually found this presentation
>almost as confusing as the previous one, perhaps because I'm mostly just
>a lurker on these discussions.
>
>Here's what I noted when reading the draft:
>
>
> You mention the GUIDs in a bunch of places, but they don't seem to
> serve any purpose.

They are primarily used for relating statements to actions, or
actions in one execution trace to actions in another execution trace.
The only place we use them in the memory model is to say that a PUR
must read from a write with the same GUID as seen in the race read
that validates the PUR.

>
>
> | *Happens-before edge* Within an execution trace, there is a
> | happens-before edge from each action in a thread t to each
> | previous action in t. Furthermore, there is an edge from a lock
> | action on monitor m to all previous unlock actions on m, and a
> | path from each read of a volatile variable v to all previous
> | writes to v. There is also an edge from every thread action to all
> | initial write actions.
>
> The from and to directions on this seem swapped. That is, the ``to''
> node for happens-before is the before node rather than the after node,
> as I read these descriptions. The same comment applies to the
> ``happens-before path.'' Either these should become ``happens after''
> edges and paths or you should change the to and from nodes.

OK, the way we had been referring to it is that a happens-before edge
from x to y indicates that y happens before x.

Our thinking had been that the edge indicates a relation: for each
node x, what are the nodes that happen before x?

However, I can see how this is confusing.

We could flip it, which would confuse a different group of people.

Perhaps it would be clearer if we talked about things more as a
partial order rather than a graph. We would still have to figure out
the appropriate English terminology for speaking about it while
confusing the minimal number of people.

Suggestions?

        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