Test TC11

LISA TC11
(*
 * Result: Sometimes
 *
 * http://www.cs.umd.edu/~pugh/java/memoryModel/unifiedProposal/testcases.html
 *
 * 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: I added the initialization of w=0.
 *)
{
w = 0;
x = 0;
y = 0;
z = 0;
}
 P0           | P1           ;
 r[once] r1 z | r[once] r4 w ;
 w[once] w r1 | r[once] r3 y ;
 r[once] r2 x | w[once] z r3 ;
 w[once] y r2 | w[once] x 1  ;
Observed
    1:r4=1; 1:r3=1; 0:r2=1; 0:r1=1;
and 1:r4=0; 1:r3=1; 0:r2=1; 0:r1=1;
and 1:r4=0; 1:r3=1; 0:r2=1; 0:r1=0;