In this case, it is true that in all sequentially consistent
executions, r3 will always be zero. But the JMM is not SC.
I think we need to say that if a compiler uses some conservative
mechanism to determine the set of values that could be seen by a read,
the compiler can use that information. In particular, the mechanism has
to be conservative with respect to the memory model.
In this case, the compiler could use a non-standard type inference
algorithm to determine that the types of x, y, r1, r2 and r3 are {0,
42}. For this analysis, we might simply assume that any read can see
any write of that same variable; this would be conservative with
respect to the memory model. From this information, we can deduce that
if r3 != 0, then r3 == 42.
The point is that the compiler would be allowed to do this if it was
absolutely guaranteed that the only possible values for r3 were 0 and
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!
But we already know that r3 is constrained to be 0 or 42, so 41 is not
a solution.
In particular, the compiler must ensure that even if we assume that r3
!= 0 implies r3 = 42, it is still the case that the only possible
values for r3 are 0 or 42.
You should also consider this example where x and y are boolean values,
substituting false for 0 and true for 42. It should be clear in that
case that we can get r1 = r2 = r3 = true.
I'm not thrilled by this example; it killed an isolation property we
were trying to build. But it seems to be allowed by existing compiler
transformations.
Bill
-------------------------------
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