Vijay Saraswat wrote:
> I agree with your reasoning.
>
> Sarita Adve wrote:
>
> > To reason with the weaker relation, we have to know about program
> > order and
> > we have to know which synchronization read returned the value from which
> > write. To reason with the stronger relation, we need to additionally
know
> > about a total ordering on all conflicting synchronization writes.
> > Thus, the
> > stronger semantics are marginally harder to explain.
> >
> >
> Not sure you need to reason about a total order on all conflicting
> synchronization writes. The stronger semantics only requires only
> additional writer -> reader edges, but says nothing about additional
> writer -> writer edges.
I believe you effectively need a total order on conflicting writes. Consider
the earlier example:
Initially, x = y = v = 0.
v is a volatile variable.
Thread 1:
r1 = x
v = 0
r2 = v
y = 1
Thread 2:
r3 = y
v = 0
r4 = v
x = 1
Is the behavior r1 == r3 == 1 possible?
The only way to deduce that the r1==r3==1 is not possible with the stronger
semantics is for threads 1 and 2 to agree on one order between the two
writes to v=0. Otherwise, Thread 1 could place its read of v before Thread
2's write and vice versa. Thus, there would be no hb ordering between
threads and we could again get r1==r3==1.
The current presentation of the strong semantics assumes this total order.
Note that this is not an additional constraint on the system since requiring
SC synchronization already guarantees this total order. The point is that to
use code such as the above correctly, we have to reason about the total
order. And to present the hb definition to programmers in this way, we have
to introduce the total order first.
Sarita
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:01:00 EDT