**Next message:**Bill Pugh: "Re: JavaMemoryModel: Reopen Case 18?"**Previous message:**Jeremy Manson: "JavaMemoryModel: Experimental Memory Model Without Forbidden Executions"**Next in thread:**Bill Pugh: "Re: JavaMemoryModel: Reopen Case 18?"**Reply:**Bill Pugh: "Re: JavaMemoryModel: Reopen Case 18?"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

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

**Next message:**Bill Pugh: "Re: JavaMemoryModel: Reopen Case 18?"**Previous message:**Jeremy Manson: "JavaMemoryModel: Experimental Memory Model Without Forbidden Executions"**Next in thread:**Bill Pugh: "Re: JavaMemoryModel: Reopen Case 18?"**Reply:**Bill Pugh: "Re: JavaMemoryModel: Reopen Case 18?"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

*
This archive was generated by hypermail 2b29
: Thu Oct 13 2005 - 07:00:58 EDT
*