(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;
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.
For this program, the forbidden set does not affect the observable behavior,
but I think it would be possible to use it as a basis for a more complicated
example that does have observably different behaviors. (Note that a compiler
using this forbidden set cannot get r1==1, r2==0 and r4==2.)
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). Is this true?
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. If the current
form of the model is adequate, I believe we can simply call that sequence the
execution: the synchronization order can be derived from it, and the
happens-before relation can be derived from the synchronization order and the
program order. (The program is implicit, and fixed, in all these definitions,
and the program order can be derived from the program and the operations that
occur in the execution.) Such a definition (i.e., one in which the execution
is just a sequence of actions) has the added benefit that it is similar in form
to how most memory models have previously been defined.
In your proof that correctly synchronized programs exhibit only SC behaviors,
and I believe your definition for correctly synchronized programs is too
strong. In particular, a program that accesses only volatiles should be
considered correctly synchronized, but it is not by your definition (because
the happens-before relation does not totally order the operations on
volatiles). The easiest way to correct this is to only require the conflicting
accesses to nonvolatile variables to be ordered by the happens-before
relation.
Other than that, it looks mostly fine to me. I can't check it fully,
of course, because you haven't given us a full formal specification for the
latest version of the memory model.
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?
Victor
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:51 EDT