# 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

    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.

## Causality test case 2

    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.

## Causality test case 3

    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

## Causality test case 4

    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

## Causality test case 5

    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.

## Causality test case 6

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

## Causality test case 7

    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.

## Causality test case 8

    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.

## Causality test case 9

    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.

## Causality test case 10

    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.

## Causality test case 11

    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.

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

## Causality test case 13

    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.

## Causality test case 14

    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.

## Causality test case 15

    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.

## Causality test case 16

    Initially, x = 0

    Thread 1:
    r1 = x
    x = 1

    Thread 2:
    r2 = x
    x = 2

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

    Decision: Allowed.

## Causality test case 17

    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.

## Causality test case 18

    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.

## Causality test case 19

    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.

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