At 11:04 AM -0700 9/14/01, Clifford Click wrote:
>I certainly agree with Jan that we need a semantics independent of
>optimizations.
I'm sorry, but that is completely impossible. Semantics define the 
set of allowed transformations/optimizations. They cannot be 
independent.
For example, here are two transformations everyone would like to 
allow: forward substitution and redundant load elimination.
If you make prescient writes dependent upon only local information, 
those transformations are illegal.
Example 1: redundant load elimination is illegal:
Initially:
x = 0 and y = 1
Thread 1:
r1 = x
r2 = x
if (r1 == r2)
   y = 2
Thread 2:
r3 = y
x = r3
The write y=2 cannot be done early; you can't determine if the write 
will always occur from purely thread local information. This 
disallows the result r1 = r2 = r3 = 2
However, if you perform redundant load elimination you get:
Initially:
x = 0 and y = 1
Thread 1:
r1 = x
r2 = r1
if (r1 == r2)
   y = 2
Thread 2:
r3 = y
x = r3
Local analysis now allows you to determine that the write y=2 is 
always performed and can be performed early, allowing r1 = r2 = r3 = 
2.
-----
Example 2 - forward substitution is illegal
Initially:
x = 0 and y = 1 and z = 0
Thread 1:
r1 = z
x = r1
r2 = x
if (r1 == r2)
   y = 2
Thread 2:
r3 = y
z = r3
The write y=2 cannot be done early; you can't determine if the write 
y=2 will always occur from purely thread local information. This 
disallows the result r1 = r2 = r3 = 2
Applying forward substitution to example 2 yields:
Initially:
x = 0 and y = 1 and z = 0
Thread 1:
r1 = z
x = r1
r2 = r1
if (r1 == r2)
   y = 2
Thread 2:
r3 = y
z = r3
For this transformed code, the write y = 2 can be done early, 
allowing r1 = r2 = r3 = 2.
This isn't to say that you can't fix the problem by adjusting the 
semantics. However, the semantics have to allow it. If the semantics 
don't allow the behavior it can produce, it isn't a legal program 
transformation.
At 10:18 AM -0400 9/14/01, Jan-Willem Maessen wrote:
>Next week, a new program transformation will be invented; Java programmers
>will be none the wiser, and the system still needs to behave explicably.
I wish things were that simple. Unfortunately, they aren't. A 
semantics has to be able to tell you whether a particular behavior is 
legal. Given a particular execution model (e.g., TSO), program 
transformations affect which behaviors can be perceived.
It turns out that in our model, we have needed to adjust the model to 
account for the interaction between forward substitution, redundant 
load elimination and prescient writes. I wasn't thrilled about having 
to do this adjustment, but I didn't see any alternative.
How can we be 100% certain that some transformation won't be invented 
later that will be ruled invalid by our model? I don't see how we 
could be 100% certain. But we spend a lot of time trying to break our 
model, and I hope the readers of this list will too. Sometimes, 99 
44/100% certain will have to do.
        Bill
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:35 EDT