At 08:46 PM 9/01/2004 -0600, 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 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?
Particularly as in example 1, the optimiser could omit the write Z=2 as
well, so the write would not occur in either example. The difference is
that the programmer can prove that it didn't occur in example 2, but cannot
so prove in example 1. So a value is out of thin air in M/P only if there
exists a proof that a write of the value did not occur. Add the statement
r4=0 to the end of T4, and the proof of the absence of the write no longer
works, and the outcome becomes permitted, even though the write of Z=2
would still never happen. From the programmer's perspective the value
written by r4=0 would never be read, but the addition of the statement
somehow changes the outcome.
At this point not only is my brain starting to hurt, but I wonder whether
some of the reordering transformations in M/P are self-justifying - the
transformation is only allowed because it's allowed, and if it weren't
allowed, then it wouldn't be allowed. Or to put it another way, that the
permissibility of the reordering transformation is undecidable.
BTW, in the quoted code below, I've changed T4, which seemed to have been
garbled in transmission (at least in the version I received). Perhaps
Sarita could confirm that I've correctly stated it.
Sylvia.
>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 == 1)
> Z = 2
>
>Result: r1=r2=1, r4 = 0
-------------------------------
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