At 9:35 AM -0400 9/8/03, victor.luchangco@sun.com wrote:
>(Apologies if you get this more than once--I got a bounced mail the first
>time I sent it.)
>
>Hi Bill and Jeremy (and others),
>
>Thanks for the new description and the proofs.
>
>Generally, I like the switch to using forbidden prefixes rather than forbidden
>executions. I don't entirely understand the second restriction on the set of
>forbidden prefixes (and in any case, is it possible to state this restriction
>in terms of prefixes rather than executions?). Could you give some intuition
>about what constitutes a valid forbidden set? Consider, for example, the
>following program:
>
> r1 = v v = 1
> r2 = x x = 2
> r3 = v
> r4 = x
>
>Could the following prefixes be the only forbidden prefixes?
>
> v=1; r1=v; r2=x; r3=v; x=2;
> v=1; r1=v; r2=x; x=2;
No, for the reasons you state below.
>
>That is, the compiler determines that if it reads 1 from v the first
>time, then
>it is safe to merge the two reads of x, so no write to x can be occur between
>them. This set does not forbid the following execution, in which r4=x is
>prescient:
>
> E: v=1; r1=v; r2=x; r4=x; x=2; r3=v;
>
>It does, however, forbid the following prescient relaxation of E:
>
> E': v=1; r1=v; r2=x; x=2; r4=x; r3=v.
Although I don't think there is any technical problem with the
existing proposal, it does make it rather difficult to determine
whether a set of forbidden prefixes is valid.
So instead have having the rule for whether a set of forbidden
prefixes is valid depend upon prescient relaxation, I'd like to
propose that we say an execution E is forbidden if any prescient
relaxation of E starts with a forbidden prefix.
At 9:35 AM -0400 9/8/03, victor.luchangco@sun.com wrote:
>Also, my informal understanding of the intuition behind
>justification says that
>any "unconditional action" (i.e., one that occurs in any execution) does not
>need to be justified (formally, the definition of justification should always
>cover such actions).
I assume we are talking about a prescient action, since non-prescient
actions can be trivially justified.
An unconditional action may need a non-trivial justification to occur
presciently. If you have an unconditional write w, you need to
justify that there are no conflicting reads r such that r hb w and r
is not in the justification order prefix before w.
See causality test case 14 in
http://www.cs.umd.edu/~pugh/java/memoryModel/CausalityTestCases.html
The write a=1, although it occurs in all fair executions, may not
occur in the justification order before the read of a by thread 1.
(Note that for this example, we use forbidden execution prefixes to
forbid non-fair executions in which thread 1 isn't allowed to make
progress).
At 9:35 AM -0400 9/8/03, victor.luchangco@sun.com wrote:
>I also want to reiterate my plea that the "causal order" be renamed.
>I suggest
>the term "justification order", as that is what it is used for.
Google gives 156 hits for "memory model" + "causal order", and only a
few of those are ours, so we'll rename it to justification order.
>
>
>In your proof that correctly synchronized programs exhibit only SC behaviors,
>and I believe your definition for correctly synchronized programs is too
>strong.
We clarified it to:
>A program is {\bf correctly synchronized} if and only if in all sequentially
>consistent executions, all conflicting accesses to non-volatile variables are
>ordered by happens-before edges.
>
>In the proof sketch that your model allows reordering, you define
>reordering on
>adjacent statements in a program, and restrict which pairs of
>statements may be
>reordered. However, the first restriction mentions happens-before
>edges, which
>are defined for an execution, not a program. Do you mean that reordering the
>statements must not eliminate any transitive happens-before edges in any
>sequential execution?
>
Actually, it should be that the reordering will not eliminate any
transitive hb edges in any valid execution (i.e., valid according to
the memory model).
Bill & Jeremy
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:51 EDT