Causality Test Cases

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.

Proposed causal loop semantics for JMM

• Correctly synchronized, non-SC behavior forbidden: test cases 4, 12, 13, 14, 15
• Forbidden behaviors of incorrectly synchronized programs: test cases 5, 10
• Allowed behaviors: test cases 1-3, 6-9, 11, 16 - 20

Causality test case 1

```Initially, x = y = 0

r1 = x
if r1 >= 0
y = 1

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.
```

Justification

```r1 = x
y = 1		# to be committed
r2 = y
x = r2
```

Commit y = 1:

```y = 1  		# committed
r2 = y (0)	# to be committed, can see y = 1
r1 = x (0)
x = r2 (0)
```

Commit r2 = y (1)

```y = 1
r2 = y (1) 	# committed
x = r2 (1)	# to be committed
r1 = x (0)
```

Commit x = r2 (1)

```y = 1
r2 = y (1)
x = r2 (1)	# committed
r1 = x (0)	# to be committed, can see x = 1
```

Commit r1 = x (1):

```y = 1
r2 = y (1)
x = r2 (1)
r1 = x (1)	# committed
```

Causality test case 2

```Initially, x = y = 0

r1 = x
r2 = x
if r1 == r2
y = 1

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.
```

Justification:

```r1 = x
r2 = x
y = 1		# to be committed
r3 = y
x = r3
```

Commit y = 1:

```y = 1 		# committed
r1 = x (0)
r2 = x (0)
r3 = y (0)	# to be committed, can see y = 1
x = r3
```

Commit r3 = y (1):

```y = 1
r3 = y (1)  	# committed
r1 = x (0)
r2 = x (0)
x = r3 (1)	# to be committed
```

Commit x = r3 (1):

```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
```

Commit both remaining actions.

```y = 1
r3 = y (1)
x = r3 (1)
r1 = x (1)
r2 = x (1)	# committed
```

Causality test case 3

```Initially, x = y = 0

r1 = x
r2 = x
if r1 == r2
y = 1

r3 = y
x = r3

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
```

Justification:

Same as test case 2

Causality test case 4

```Initially, x = y = 0

r1 = x
y = r1

r2 = y
x = r2

Behavior in question: r1 == r2 == 1

Decision: Forbidden: values are not allowed to come out of thin air
```

Causality test case 5

```Initially, x = y = z = 0

r1 = x
y = r1

r2 = y
x = r2

z = 1

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.

Causality test case 6

```Initially A = B = 0

r1 = A
if (r1 == 1)
B = 1

r2=B
if (r2 == 1)
A = 1
if (r2 == 0)
A = 1

Behavior in question: r1 == r2 == 1 allowed?

1 to A and hoist the write to the beginning of thread 2.
```

Justification:

```r2 = B (0)
A = 1  		# to be committed
r1 = A
B = 1
```

Commit A=1:

```A = 1  		# committed
r1 = A (0)	# to be committed, can see A = 1
r2 = B (0)
```

Commit r1 = A:

```A = 1
r1 = A (1)	# committed
B = 1		# to be committed
r2 = B (1)
```

Commit B = 1:

```A = 1
r1 = A (1)
B = 1		# committed
r2 = B (0)	# to be committed, can see B = 1
```

Commit remaining actions.

```A = 1
r1 = A (1)
B = 1
r2 = B (1)	# committed
```

Causality test case 7

```Initially, x = y = z = 0

r1 = z
r2 = x
y = r2

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
```

Justification::

```r3 = y (0)
z = r3
x = 1
r1 = z (0)
r2 = x (0)	# to be committed
y = r2
```

Commit x = 1:

```x = 1		# committed
r3 = y (0)
z = r3
r1 = z (0)
r2 = x (0)	# to be committed, can see x=1
y = r2
```

Commit r2 = x (1):

```x = 1
r2 = x (1)	# committed
r3 = y (0)
z = r3
r1 = z (0)
y = r2		# to be committed
```

Commit y = r2 (1):

```x = 1
r2 = x (1)
y = r2 		# committed
r3 = y (0)	# to be committed, can see y = r2 (1)
z = r3
r1 = z (0)
```

Commit r3 = y (1):

```x = 1
r2 = x (1)
y = r2
r3 = y (1)	# committed
z = r3		# to be committed
r1 = z (0)
```

Commit z = r3:

```x = 1
r2 = x (1)
y = r2
r3 = y (1)
z = r3		# committed
r1 = z (0)	# to be committed, can see z = r3 (1)
```

Commit r1 = x (1):

```x = 1
r2 = x (1)
y = r2
r3 = y (1)
z = r3
r1 = z (1)	# committed
```

Causality test case 8

```Initially, x = y = 0

r1 = x
r2 = 1 + r1*r1 - r1
y = r2

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.

Justification:

```r1 = x (0)
y = r2 (1)	# to be committed
r3 = y (0)
x = r3
```

Commit y = r2 (1):

```y = r2 (1)	# committed
r3 = y (0)	# to be committed, can see y = r2 (1)
r1 = x (0)
x = r3
```

Commit r3 = y (1):

```y = r2 (1)
r3 = y (1)	# committed
r1 = x (0)
x = r3
```

Commit x = r3 (1):

```y = r2 (1)
r3 = y (1)
x = r3			# committed
r1 = x (0)		# to be committed, can see x = r3 (1)
```

Commit r1 = x (1):

```y = r2 (1)
r3 = y (1)
x = r3
r1 = x (1)		# committed
```

Causality test case 9

```Initially, x = y = 0

r1 = x
r2 = 1 + r1*r1 - r1
y = r2

r3 = y
x = r3

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.
```

Justification

For the purposes of justification, this is identical to test case 8.

Causality test case 9a

```Initially, x = 2, y = 0

r1 = x
r2 = 1 + r1*r1 - r1
y = r1

r3 = y
x = r3

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.
```

Justification

For the purposes of justification, this is identical to test case 8.

Causality test case 10

```Initially, x = y = z = 0

r1 = x
if (r1 == 1)
y = 1

r2 = y
if (r2 == 1)
x = 1

z = 1

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.

Causality test case 11

```Initially, x = y = z = 0

r1 = z
w = r1
r2 = x
y = r2

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:

r2 = x
y = r2
r1 = z
w = r1

x = 1
r3 = y
z = r3
r4 = w

after which the behavior in question is SC.

Justification

Similar to test case 7, but longer.
```

Causality test case 12

```Initially, x = y = 0; a[0] = 1, a[1] = 2

r1 = x
a[r1] = 0
r2 = a[0]
y = r2

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.
```

Causality test case 13

```Initially, x = y = 0

r1 = x
if (r1 == 1)
y = 1

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.

Causality test case 14

```Initially, a = b = y = 0, y is volatile

r1 = a
if (r1 == 0)
y = 1
else
b = 1

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 = 1
```
There 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.

Causality test case 15

```Initially, a = b = x = y = 0, x and y are volatile

r0 = x
if (r0 == 1)
r1 = a
else
r1 = 0
if (r1 == 0)
y = 1
else
b = 1

do {
r2 = y
r3 = b
} while (r2 + r3 == 0);
a = 1;

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.

Causality test case 16

```Initially, x = 0

r1 = x
x = 1

r2 = x
x = 2

Behavior in question: r1 == 2; r2 == 1

Decision: Allowed.
```

Justification:

```r1 = x
x = 1
r2 = x
x = 2
```

Commit x = 1:

```x = 1 		# committed
r1 = x (0)
r2 = x (0)
x = 2		# to be committed
```

Commit x = 2:

```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
```

Causality test case 17

```Initially,  x = y = 0

r3 = x
if (r3 != 42)
x = 42
r1 = x
y = r1

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.

Causality test case 18

```Initially,  x = y = 0

r3 = x
if (r3 == 0)
x = 42
r1 = x
y = r1

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.

Causality test case 19

```Initially,  x = y = 0

r1 = x
y = r1

r2 = y
x = r2

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
```
Justification note: see test case 20.

Causality test case 20

```Initially,  x = y = 0

r1 = x
y = r1

r2 = y
x = r2

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
```

Justification order:

```r3 = x (0)
x = 42
r1 = x (42)
y = r1 (42)	# to be committed
r2 = y (0)
x = r2
```

Commit y = r1 (42):

```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
```

Commit r2 = y (42):

```y = r1 (42)
r2 = y (42)	# committed
r3 = x (0)
x = 42
r1 = x (42)
x = r2		# to be committed
```

Commit x = r2:

```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)
```

Commit r3 = x (42)

```y = r1 (42)
r2 = y (42)
x = r2
r3 = x (42)	# committed
r1 = x (42)	# committed
```