Certain kinds of causal loops, in which an event causes itself to happen, are unacceptable. Since discussions have shown that notions of causality are not intuitive or universal, it is useful to describe a series of examples of unacceptable causal loops and seemly causal loops that must be allowed by the semantics.
In the cases below where non-SC behavior can be seen, we show how the "Java Memory Model" justifies allowing these cases. The first given justification order is one where all reads see writes that happen before them - what follows uses the JMM rules to derive the non-SC behavior.
Initially, x = y = 0 Thread 1 r1 = x if r1 >= 0 y = 1 Thread 2 r2 = y x = r2 Behavior in question: r1 == r2 == 1 Decision: Allowed, since interthread compiler analysis could determine that x and y are always non-negative, allowing simplification of r1 >= 0 to true, and allowing write y = 1 to be moved early.
r1 = x y = 1 # to be committed r2 = y x = r2
y = 1 # committed r2 = y (0) # to be committed, can see y = 1 r1 = x (0) x = r2 (0)
y = 1 r2 = y (1) # committed x = r2 (1) # to be committed r1 = x (0)
y = 1 r2 = y (1) x = r2 (1) # committed r1 = x (0) # to be committed, can see x = 1
y = 1 r2 = y (1) x = r2 (1) r1 = x (1) # committed
Initially, x = y = 0 Thread 1: r1 = x r2 = x if r1 == r2 y = 1 Thread 2: r3 = y x = r3 Behavior in question: r1 == r2 == r3 == 1 Decision: Allowed, since redundant read elimination could result in simplification of r1 == r2 to true, allowing y = 1 to be moved early. Notes: In SC executions, both reads of x always return the same value (i.e., zero), so that r1 == r2 is always true in SC executions.
r1 = x r2 = x y = 1 # to be committed r3 = y x = r3
y = 1 # committed r1 = x (0) r2 = x (0) r3 = y (0) # to be committed, can see y = 1 x = r3
y = 1 r3 = y (1) # committed r1 = x (0) r2 = x (0) x = r3 (1) # to be committed
y = 1 r3 = y (1) x = r3 (1) # committed r1 = x (0) # to be committed, can see x = 1 r2 = x (0) # to be committed, can see x = 1
y = 1 r3 = y (1) x = r3 (1) r1 = x (1) r2 = x (1) # committed
Initially, x = y = 0 Thread 1: r1 = x r2 = x if r1 == r2 y = 1 Thread 2: r3 = y x = r3 Thread 3: x = 2 Behavior in question: r1 == r2 == r3 == 1 Decision: Allowed, since redundant read elimination could result in simplification of r1 == r2 to true, allowing y = 1 to be moved early. Notes: Same as test case 2, except there are SC executions in which r1 != r2
Same as test case 2
Initially, x = y = 0 Thread 1: r1 = x y = r1 Thread 2: r2 = y x = r2 Behavior in question: r1 == r2 == 1 Decision: Forbidden: values are not allowed to come out of thin air
Initially, x = y = z = 0 Thread 1: r1 = x y = r1 Thread 2 r2 = y x = r2 Thread 3 z = 1 Thread 4 r3 = z x = r3 Behavior in question: r1 == r2 == 1, r3 == 0. Decision: Forbidden: values are not allowed to come out of thin air, even if there are other executions in which the thin-air value would have been written to that variable by some not out-of-thin air means.
If reads in threads 1 and 2 only see writes that happen-before them, those threads both read and write zero. In order to commit an action where threads 1 or 2 read or write the value 1, you would first need to commit thread 4 writing 1 to x. Having done that, you could then commit thread 1 reading x and seeing 1.
But in that case, we already have r3 == 1.
Initially A = B = 0
Thread 1
r1 = A
if (r1 == 1)
B = 1
Thread 2
r2=B
if (r2 == 1)
A = 1
if (r2 == 0)
A = 1
Behavior in question: r1 == r2 == 1 allowed?
Decision: Allowed. Intrathread analysis could determine that thread 2 always writes
1 to A and hoist the write to the beginning of thread 2.
r2 = B (0) A = 1 # to be committed r1 = A B = 1
A = 1 # committed r1 = A (0) # to be committed, can see A = 1 r2 = B (0)
A = 1 r1 = A (1) # committed B = 1 # to be committed r2 = B (1)
A = 1 r1 = A (1) B = 1 # committed r2 = B (0) # to be committed, can see B = 1
A = 1 r1 = A (1) B = 1 r2 = B (1) # committed
Initially, x = y = z = 0 Thread 1: r1 = z r2 = x y = r2 Thread 2: r3 = y z = r3 x = 1 Behavior in question: r1 = r2 = r3 = 1. Decision: Allowed. Intrathread transformations could move r1 = z to after the last statement in thread 1, and x = 1 to before the first statement in thread 2.
r3 = y (0) z = r3 x = 1 r1 = z (0) r2 = x (0) # to be committed y = r2
x = 1 # committed r3 = y (0) z = r3 r1 = z (0) r2 = x (0) # to be committed, can see x=1 y = r2
x = 1 r2 = x (1) # committed r3 = y (0) z = r3 r1 = z (0) y = r2 # to be committed
x = 1 r2 = x (1) y = r2 # committed r3 = y (0) # to be committed, can see y = r2 (1) z = r3 r1 = z (0)
x = 1 r2 = x (1) y = r2 r3 = y (1) # committed z = r3 # to be committed r1 = z (0)
x = 1 r2 = x (1) y = r2 r3 = y (1) z = r3 # committed r1 = z (0) # to be committed, can see z = r3 (1)
x = 1 r2 = x (1) y = r2 r3 = y (1) z = r3 r1 = z (1) # committed
Initially, x = y = 0 Thread 1: r1 = x r2 = 1 + r1*r1 - r1 y = r2 Thread 2: r3 = y x = r3 Behavior in question: r1 = r2 = 1 Decision: Allowed. Interthread analysis could determine that x and y are always either 0 or 1, and thus determine that r2 is always 1. Once this determination is made, the write of 1 to y could be moved early in thread 1.Note that in the justification order below, r2 = 1 + r1*r1 - r1 is not included. This is because it isn't an interthread action - it only affects local variables.
r1 = x (0) y = r2 (1) # to be committed r3 = y (0) x = r3
y = r2 (1) # committed r3 = y (0) # to be committed, can see y = r2 (1) r1 = x (0) x = r3
y = r2 (1) r3 = y (1) # committed r1 = x (0) x = r3
y = r2 (1) r3 = y (1) x = r3 # committed r1 = x (0) # to be committed, can see x = r3 (1)
y = r2 (1) r3 = y (1) x = r3 r1 = x (1) # committed
Initially, x = y = 0 Thread 1: r1 = x r2 = 1 + r1*r1 - r1 y = r2 Thread 2: r3 = y x = r3 Thread 3: x = 2 Behavior in question: r1 = r2 = 1 Decision: Allowed. Similar to test case 8, except that the x is not always 0 or 1. However, a compiler might determine that the read of x by thread 2 will never see the write by thread 3 (perhaps because thread 3 will be scheduled after thread 1). Thus, the compiler can determine that r1 will always be 0 or 1.
For the purposes of justification, this is identical to test case 8.
Initially, x = 2, y = 0 Thread 1: r1 = x r2 = 1 + r1*r1 - r1 y = r1 Thread 2: r3 = y x = r3 Thread 3: x = 0 Behavior in question: r1 = r2 = 1 Decision: Allowed. Similar to test case 8, except that the x is not always 0 or 1. However, a compiler might determine that thread 3 will always execute before thread 1, and that therefore the initial value of 2 will not be visible to the read of x in thread 1. Thus, the compiler can determine that r1 will always be 0 or 1.
For the purposes of justification, this is identical to test case 8.
Initially, x = y = z = 0 Thread 1: r1 = x if (r1 == 1) y = 1 Thread 2 r2 = y if (r2 == 1) x = 1 Thread 3 z = 1 Thread 4 r3 = z if (r3 == 1) x = 1 Behavior in question: r1 == r2 == 1, r3 == 0. Decision: Forbidden. This is the same as test case 5, except using control dependences rather than data dependences.For justification information, see note on test case 5.
Initially, x = y = z = 0 Thread 1: r1 = z w = r1 r2 = x y = r2 Thread 2: r4 = w r3 = y z = r3 x = 1 Behavior in question: r1 = r2 = r3 = r4 = 1 Decision: Allowed. Reordering of independent statements can transform the code to: Thread 1: r2 = x y = r2 r1 = z w = r1 Thread 2: x = 1 r3 = y z = r3 r4 = w after which the behavior in question is SC.Justification
Similar to test case 7, but longer.
Initially, x = y = 0; a[0] = 1, a[1] = 2
Thread 1
r1 = x
a[r1] = 0
r2 = a[0]
y = r2
Thread 2
r3 = y
x = r3
Behavior in question: r1 = r2 = r3 = 1
Decision: Disallowed. Since no other thread accesses the array a,
the code for thread 1 should be equivalent to:
r1 = x
a[r1] = 0
if (r1 == 0)
r2 = 0
else
r2 = 1
y = r2
With this code, it is clear that this is the same situation as
test 4.
Initially, x = y = 0 Thread 1: r1 = x if (r1 == 1) y = 1 Thread 2: r2 = y if (r2 == 1) x = 1 Behavior in question: r1 == r2 == 1 Decision: Disallowed. In all sequentially consistent executions, no writes to x or y occur and the program is correctly synchronized. The only SC behavior is r1 == r2 == 0.Since no writes occur in any non-prescient execution, there is nothing to perform presciently. Therefore, this execution is disallowed.
Initially, a = b = y = 0, y is volatile
Thread 1:
r1 = a
if (r1 == 0)
y = 1
else
b = 1
Thread 2:
do {
r2 = y
r3 = b
} while (r2 + r3 == 0);
a = 1;
Behavior in question: r1 == r3 = 1; r2 = 0
Decision: Disallowed In all sequentially consistent executions, r1 = 0 and
the program is correctly synchronized. Since the program is correctly
synchronized in all SC executions, no non-sc behaviors are allowed.
The only execution in which each read sees a write that happen before it is:
r1 = a (0) y = 1 r2 = y (1) r3 = b (0) a = 1There are also execution in which thread 2 reads y and b multiple times before seeing the 1 written to y by thread 1. For the purposes of justification, such executions are identical to this case.
Which action do we wish to commit first? The only action that also occurs in the behavior we are trying to justify (r1 = r3 = 1, r2 = 1) is a = 1. So we can commit a=1.
With a=1 committed, in order to commit additional actions, we must demonstrate an execution in which each non-committed read sees a write that happens-before it. In all of those executions, thread 1 sees the value 0 for a; it then writes to y but does not write to b; the read of a by thread 1 therefore happens-before the write to a by thread 2 - the write is not visible to the read.
So we can't commit a write of 1 to b, or a read of a seeing 1. and thus we can't get the behavior r1 == r3 = 1; r2 = 0.
Initially, a = b = x = y = 0, x and y are volatile
Thread 1:
r0 = x
if (r0 == 1)
r1 = a
else
r1 = 0
if (r1 == 0)
y = 1
else
b = 1
Thread 2:
do {
r2 = y
r3 = b
} while (r2 + r3 == 0);
a = 1;
Thread 3:
x = 1
Behavior in question: r0 == r1 == r3 = 1; r2 == 0
Decision: Disallowed. In all sequentially consistent executions, r1 = 0 and
the program is correctly synchronized. Since the program is correctly
synchronized in all SC executions, no non-sc behaviors are allowed.
Justification note: see Causality test case 14.
Initially, x = 0 Thread 1: r1 = x x = 1 Thread 2: r2 = x x = 2 Behavior in question: r1 == 2; r2 == 1 Decision: Allowed.
r1 = x x = 1 r2 = x x = 2
x = 1 # committed r1 = x (0) r2 = x (0) x = 2 # to be committed
x = 1 x = 2 # committed r1 = x (0) # to be committed, can see x = 2 r2 = x (0) # to be committed, can see x = 1
x = 1 x = 2 r1 = x (2) # committed r2 = x (1) # committed
Initially, x = y = 0 Thread 1: r3 = x if (r3 != 42) x = 42 r1 = x y = r1 Thread 2: r2 = y x = r2 Behavior in question: r1 == r2 == r3 == 42 Decision: Allowed. A compiler could determine that at r1 = x in thread 1, is must be legal for to read x and see the value 42. Changing r1 = x to r1 = 42 would allow y = r1 to be transformed to y = 42 and performed earlier, resulting in the behavior in question.Justification note: see test case 20.
Initially, x = y = 0 Thread 1: r3 = x if (r3 == 0) x = 42 r1 = x y = r1 Thread 2: r2 = y x = r2 Behavior in question: r1 == r2 == r3 == 42 Decision: Allowed. A compiler could determine that the only legal values for x are 0 and 42. From that, the compiler could deduce that r3 != 0 implies r3 = 42. A compiler could then determine that at r1 = x in thread 1, is must be legal for to read x and see the value 42. Changing r1 = x to r1 = 42 would allow y = r1 to be transformed to y = 42 and performed earlier, resulting in the behavior in question.Justification note: see test case 20.
Initially, x = y = 0 Thread 1: join thread 3 r1 = x y = r1 Thread 2: r2 = y x = r2 Thread 3: r3 = x if (r3 != 42) x = 42 Behavior in question: r1 == r2 == r3 == 42 Decision: Allowed. This is the same as test case 17, except that thread 1 has been split into two threads.Justification note: see test case 20.
Initially, x = y = 0 Thread 1: join thread 3 r1 = x y = r1 Thread 2: r2 = y x = r2 Thread 3: r3 = x if (r3 == 0) x = 42 Behavior in question: r1 == r2 == r3 == 42 Decision: Allowed. This is the same as test case 18, except that thread 1 has been split into two threads.
r3 = x (0) x = 42 r1 = x (42) y = r1 (42) # to be committed r2 = y (0) x = r2
y = r1 (42) # committed r3 = x (0) x = 42 r1 = x (42) r2 = y (0) # to be committed, can see y = r1 (42) x = r2
y = r1 (42) r2 = y (42) # committed r3 = x (0) x = 42 r1 = x (42) x = r2 # to be committed
y = r1 (42) r2 = y (42) x = r2 # committed r3 = x (0) # to be committed, can see x = r2 (42) x = 42 r1 = x (42) # to be committed, can see x = r2 (42)
y = r1 (42) r2 = y (42) x = r2 r3 = x (42) # committed r1 = x (42) # committed