At 10:54 PM 7/27/2003, Bill Pugh wrote:
>I want to enumerate several of the executions allowed by Sarita's model
>that I find profoundly troubling.
I don't find the first two examples below troubling. (I haven't looked at 3
in detail). In both examples I display transformations that I believe a
compiler should be allowed to make. I don't take it as our job to decide
whether these are desirable transformations. That job belongs to the
optimizer. I take our job to be to tell the optimizer whether these
transformations are allowed.
I have always taken it that the intention is to allow the optimizer to
treat code without threading constructs as if threading doesn't exist. If
these results are to be disallowed we seem to be imposing constraints on
the optimizer that are not articulated in a way that compiler writers can
understand.
>Example 1:
>
>Initially, x = y = z = 0
>
>Thread 1:
>x = 1
>
>Thread 2:
>r1 = x
>y = r1
>
>Thread 3:
>r2 = y
>z = r2
>
>Thread 4:
>r3 = z
>y = r3
>
>Troubling execution: r1 == 0, r2 == r3 == 1.
>
>This execution is troubling because, given that r1 = 0, the only way r2
>could be 1 is if thread 4 wrote 1 to y. And the only way that could be
>true is if r3 is one, which could only be true if r2 is one. So in this
>example, there is no causal way to explain how r2 and r3 became one.
That result can arise quite naturally if the compiler transforms Thread 2 to
r1=x
y=x
What do we say to disallow this outcome? Do you want to disallow redundant
loads? That is a pretty severe constraint on compilers?
>Example 2:
>Initially, x = 0, y = 0, a[0] = 1, a[1] = 2
>
> Thread 1 Thread 2
> r1 = X r3 = Y
> a[r1] = 0 X = r3
> r2 = a[0]
> Y = r2
>
>Troubling execution r1 == r2 == r3 == 1
>
>This execution is troubling because in order for r2 to be 1, r1 must
>have been 1. But r1 could be one only if thread 2 wrote 1 to X. Which
>could only be true if thread 2 read 1 from Y. Which could only be true if
>r2 is 1.
Transform Thread 1 to
Y=a[0]
r1 = X
a[r1] = 0
r2 = a[0]
if ( X == 0 ) Y = 0
It appears that to disallow this outcome we have to tell the optimizer it
can't do "speculative stores". That is, it can't store a value that might
be right and then later determine if it is. Such a prohibition is a part of
"no out of thin air", but this example illustrates that "no out of thin
air" is an independent constraint we are imposing on the optimizer and not
something that arises natually out of the semantics of java
>Example 3 (I haven't had a chance to run this one by Sarita yet):
>
>Initially, x = 1, y = 0
>
>Thread 1:
>r1 = x
>y = r1+1
>x = r1
>
>Thread 2:
>r2 = y
>x = r2+2
>
>Troubling execution r1 = 4 and r2 = 5
>
>How could this happen in Sarita's model? Basically, the read of x in
>thread 1 has to see the later write to x in thread 1. Which both involves
>seeing a read in violation of the happens-before ordering and is a
>causality violation.
>
>There is a race D1 between the read of x in thread 1 and the write of x in
>thread 2. There is a SC execution in which r1 = x comes first, the race
>occurs, and thread 2 writes 4 to x. Thus, Prefix:1 is empty, and P|D1 will
>be a program that just sets r1 = 4. Which allows r1 = 4 and r2 = 5.
>
>
>Bill
>-------------------------------
>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:46 EDT