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


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.