> 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.
| *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.
| Each PUR must be validated by a valid execution trace. Let r be PUR of
| variable v in execution trace E that sees the value of a later write w
| with GUID g. A PUR r is validated by an execution trace E0 in which r
| sees the same value from the same variable from the same
| write. However, in E0, the write w must occur before r and there must
| be no happens-before path in E0 from the read r to the write w (which
| means that the read is incorrectly synchronized).
The formalization of validating an execution trace seems to be an
unneeded level of indirection. Rather, can't we just say that the set
of possible values for a given read is the union of values from all
valid traces? What does that leave out that the PUR notion adds?
Now, some idle thoughts. It seems to me that if we were to introduce an
extra start action for the entire program, which happens before all
initial write actions, the happens-before edges would make a subgraph
from which all actions were reachable from this start node.
Given the happens-before graph, we can construct a dominator tree on the
graph from the start. A properly synchronized read of x, Rx, means that
(1) there is some write of x, Wx, which dominates Rx
(2) all other writes of x which dominate Rx also dominate Wx
(3) all other writes of x which are dominated by Wx are also dominated
by Rx
Possible but unsynchronized reads and impossible reads can be defined in
similar terms.
Does this make sense to anyone? Or have I wandered off into the woods?
--p
-------------------------------
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