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

### JMM semantics

• Forbidden behaviors: test cases 4, 5, 10, 12-15
• 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.
```

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

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

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

## Causality test case 6

Earlier drafts had a bug with A and B initially 1
```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?

Decision: Allowed. Intrathread analysis could determine that thread 2 always writes
1 to A and hoist the write to the beginning of thread 2.
```

## 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
first statement in thread 2.
```

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

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

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

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

Note: This is similar to test case 7, but extended with one more
rung in the ladder
```

## Causality test case 12

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

r1 = x
a[r1] = 0
r2 = a
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.
```

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

```

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

```

## Causality test case 16

```Initially, x = 0

r1 = x
x = 1

r2 = x
x = 2

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

Decision: Allowed.
```

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

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

## 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
split into two threads.
```

## Causality test case 20

```Initially,  x = y = 0

r1 = x
y = r1