[concurrency-interest] concurrency puzzle

[Vijay Saraswat]

David Holmes wrote:

> So this means that:
>
>   class A {
>       int x;
>       ...
>   }
>
>is semantically different to:
>
>   class A {
>       int x = 0;
>       ...
>   }
>
>because the explicit write of zero to x could "appear" later (even though it
>is overwriting a zero value in main memory) just as the value 10 could
>"appear" later.
>
>Wow! That is a very subtle distinction. I'm not sure there are any practical
>consequences arising from it but I find it disconcerting to have this
>difference.
>  
>
The difference could be huge.

Question: Is there some argument for why any Java code has a race with 
the second fragment iff it has a race with the first?

That would be a very interesting global property of the Java language.

If not, then one would need some interesting results about JSR 133 rules 
to be certain that there are no practical consequences arising from this 
distinction -- since the presence of races has such a huge impact on the 
semantics. For instance one would need *at least* the following to be 
true (and in reality much more general forms of this would need to be true):

Claim: Suppose the only race in a program is between a read action and a 
write action on x that writes the same value as the hb-value of x at the 
read operation. Then all executions of the program are SC.

Unfortunately, JSR 133 rules are complex and not mathematically precise. 
So I cant figure out if this is true.

If someone can provide some precise reasoning based on JSR133 for why 
the question or the claim above is true (or false!), I would be very 
grateful.

Best,
Vijay