data race example of SPECIAL POPL ISSUE The Java Memory Model confusion

Question

I am confused with Figure 3 in SPECIAL POPL ISSUE The Java Memory Model paper.

Example (page 5, Figure 3):

Initially, x == y == 0    

Thread 1 -> r1 = x; y = r1;

Thread 2 -> r2 = y; r3 = r2 | 1; x = r2;

r1 == r2 == r3 == 1 is legal behavior.

Explanation 1 (page 5, 1.2 Casual Loops): Another example of a causal loop – this time, one that describes an acceptable behavior – can be seen in Figure 3. In order to see the result r1 == r2 == r3 == 1, one of the threads must perform its write before it performs its read. But each write seems dependent upon the read above it. While this value might also seem to come out of thin air, it does not and can result from standard compiler transformations, as discussed in Section 2.2.2.

Explanation 2 (page 10, 2.2.2 Dependence Breaking Analysis and Transformations): Figure 3 shows a similar but even more surprising behavior. In this case, the compiler would have to perform a more slightly deeper analysis to determine that the values of x and y are guaranteed to be either 0 or 1. One possible such analysis would be an analysis that determines the bit width required to represent integer values in a program [Stephenson et al. 2000].

In this example r1 and r2 could be == 1 only if x or y == 1 and x or y could be == 1 only if r1 and r2 == 1. But assignment of 1 I can find only in r3 = r2 | 1; So in my opinion there is no way to get 1 to r1, r2, x or y.

So, this example is wrong or I'm mistaken?

Answer 1

You're right. The example is wrong. It should be:

Initially, x == y == 0
Thread 1 -> r1 = x; y = r1;
Thread 2 -> r2 = y; r3 = r2 | 1; x = r3;

You can see the correct example in Figure 1.3 of Jeremy Manson's PhD dissertation.