Re: JavaMemoryModel: Examples similar to tests 5 and 10

From: Bill Pugh (pugh@cs.umd.edu)
Date: Sat Jan 17 2004 - 23:39:46 EST


At 8:46 PM -0600 1/9/04, Sarita Adve wrote:
>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 Example 1, there is a story you can tell:

T3 performs Z = 2
The execution engine determines that since r2 = Z in T2 will not see
the initial value, X=1 will always be performed by T2.
T2 performs X = 1 preciently
T1 performs r1 = X, seeing 1
T1 performs Z = 1
T2 performs r2 = Z, seeing 1

In Example 2, there is no such story that can be told, without
allowing for bait-and-switch.

>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

-------------------------------
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