Here are two examples that are in the family of tests 5 and 10 that I
mentioned in the message to Sylvia. I do not understand why the M/P model
allows example 1 but not 2.
In the first example, X=1 is allowed to be prescient because in all
*non-forbidden* executions, T2's read of Z returns 2 which makes X=1
execute. However, in the execution that is finally generated, T2's read of Z
returns 1.
In the second example, the same thing happens, except that not only does
T2's read of Z return 1, but the write Z=2 also doesn't happen in the actual
execution. The M/P model does not like the fact that Z=2 doesn't happen. But
how does that matter? In both examples, the justification for doing X=1 is
the read of Z that returns 2; in both examples, in the actual execution that
happens, the read does not return 2. Why does it matter that the write did
not happen, if the net result is the same; i.e., the read did not read that
value. I find this quite arbitrary. Can anyone think of a good explanation?
Example 1: Initially all variables are 0
T1
r1=X
if (r1==1)
Z=1
T2
r2=Z
if (r2==1 || r2==2)
X=1
T3
Z=2
Result: r1=r2=1
Example 2: Initially all variables are 0
T1
r1=X
if (r1==1)
Z=1
T2
r2=Z
if (r2==1 || r2==2)
X=1
T3
Y = 1
T4
r4 = Y
if r4
Z = 2
Result: r1=r2=1, r4 = 0
Sarita
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:56 EDT