I would like to reopen discussion on Case 18, because the reasoning
seems a bit suspicious to me.
====================================================
<H2>Causality test case 18</H2><PRE>Initially, x = y = 0
Thread 1:
1: r3 = x
2: if (r3 == 0)
3: x = 42
4: r1 = x
5: y = r1
Thread 2:
6: r2 = y
7: x = r2
Behavior in question: r1 == r2 == r3 == 42
Decision: Allowed. A compiler could determine that the only legal values
for x are 0 and 42. From that, the compiler could deduce that r3 != 0
implies
r3 = 42. A compiler could then determine that at r1 = x in thread 1,
is must be legal for to read x and see the value 42. Changing r1 = x
to r1 = 42 would allow y = r1 to be transformed to y = 42 and performed
earlier, resulting in the behavior in question.
</PRE>
<HR>
=======================================================
I agree that the only legal values for x are 0 and 42. However, it does
not follow that the compiler can deduce that r3 !=0 implies r3 = 42.
For it could be the case that r3 could be *only* 0, and could not take
on the value 42. (That is, when read at r3, x can contain only the value
0.) Therefore it is not correct to say that at Line 4 it must be legal
to read x and see 42.
The same reasoning does not apply for Case 17 (which differs from Case
18 only in that the guard is r3 != 42). Here, it is correct to say that
at Line 4 it must be legal to read x and see 42. For, either the value
read at Line 1 is 42 or not. If not, then the read at Line 4 could read
from the conditional assignment. If it is 42, then the read can reuse
that value. Hence it is correct to change r1=x at Line 4 to r1=42.
Technically the distinction between the two cases is this. Suppose we
make the same linkages in Case 17 and Case 18 between the reads and
writes. Then in Case 17 we get the equation
r3 = (r3 != 42) ? 42 : r3
which has only one solution (r3=42). Whereas in Case 18 we get the equation
r3 = (r3 = 0)? 42 : r3
which has arbitrarily many solutions (any non-zero value). So if 42 is a
solution, so is 41!
(The only constraint c(r) for which the equation
r = c(r) ? 42: r
has a unique solution is c(r) = (r != 42).)
Best,
Vijay Saraswat
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:58 EDT