Okay, I can explain the things I punted on a little better now, I think.
> - the issue of prohibited traces seems like a hack. I do see how it
> solves the problem, but why based on a single read? I also do not
> understand the requirement: "E' is an alternate execution trace that
> contains r and the causal trace r has in E, but returns a different value
> for r." That is:
>
> -- we're talking about a variable read for r---that is, a static read
> action, and not a runtime action, right? (otherwise i don't see how it can
> return a different value---are not runtime actions associated with their
> values read?). What does it mean for E' to "contain r"---just that we
> execute that static stmt as some point? More importantly, what does it
> mean that E' contains the causal trace r has in E. Do you mean any one of
> the causal sequences of E leading to any particular runtime execution of r
> exists as a subsequence of a (any?) causal order for E'? It would probably
> help a lot to work through your example in detail, showing the actual
> <E,r,E'> triples (not just their results in terms of i,j,k).
We are talking about a run time action; this is a deficiency in our
description of causal orders. More specifically (and I'll be adding this
more concretely to the semantics), E' is an alternate execution trace for
E for a read r (i.e., there is an <E, r, E'> triple) if
a) the causal trace for r in E is C
b) there is a subtrace C' of E' such that the actions in C' have a
one-to-one correspondence with the actions in C (including GUID and value
read).
c) C' is a causal trace in E' for an action r' that is generated by the
same statement that generates r. r' sees a different value from the one r
sees.
That may need some refining, but it is the general idea.
> - The hand-waving in the very last sentence of 6.1 is not convincing. Can
> you explain exactly how the read of 2 in h2 is validated, in very explicit
> terms of valid sets and elements? I don't see any valid seq. cons.
> execution that contains h1 (reads 2) as an action. Is this done by
> constructing valid_2 after valid_1? I'm confused here; perhaps there's
> something basic i've misunderstood.
The read of 2 in h2 is validated separately from the read of 2 in h1,
using the exact same causal order, in exactly the same way. In other
words, we say exactly the same thing that we say at the end of Section
6.1, except we would end it with this:
Here is the key action: the read of 2 in h2 is allowed in every execution
that contains { h4, h5 (reads 2), h6, h1 }.
You don't need a valid SC execution that contains h1 (reads 2) as an
action, because the read of 2 for h2 is not caused by h1 seeing 2.
I hope that helps to clear up the remaining points.
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