**Next message:**Sarita Adve: "RE: JavaMemoryModel: Examples similar to tests 5 and 10"**Previous message:**Sylvia Else: "RE: JavaMemoryModel: Implications of SC-: we need your feedback"**In reply to:**Sarita Adve: "JavaMemoryModel: Examples similar to tests 5 and 10"**Next in thread:**Sarita Adve: "RE: JavaMemoryModel: Examples similar to tests 5 and 10"**Reply:**Sarita Adve: "RE: JavaMemoryModel: Examples similar to tests 5 and 10"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]**Mail actions:**[ respond to this message ] [ mail a new topic ]

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

**Next message:**Sarita Adve: "RE: JavaMemoryModel: Examples similar to tests 5 and 10"**Previous message:**Sylvia Else: "RE: JavaMemoryModel: Implications of SC-: we need your feedback"**In reply to:**Sarita Adve: "JavaMemoryModel: Examples similar to tests 5 and 10"**Next in thread:**Sarita Adve: "RE: JavaMemoryModel: Examples similar to tests 5 and 10"**Reply:**Sarita Adve: "RE: JavaMemoryModel: Examples similar to tests 5 and 10"**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:56 EDT
*