Test C-cpord-obs-failure

C C-cpord-obs-failure

(* This test should be forbidden, but it isn't.

        P0        P1     P2     P3     P4     P5
        Rx1=1     Rx2=1  Wx3=2  Wx4=1  Wy2=2  Wy3=2
        data dep  mb     mb     wmb    wmb    wmb
      a:Wx2=1     Wx3=1  Rx4=0  Wy1=1  wy3=1  Wx1=1
        Ry1=1
        data dep
      b:Wy2=1   

   a: ->rfe 1:Rx2 ->mb 1:Wx3 ->co 2:Wx3 ->mb 2:Rx4 ->fre 3:Wx4 ->wmb
            3:Wy1 ->hb* b:

   b: ->co 4:Wy2 ->wmb 4:Wy3 ->co 5:Wy3 ->wmb 5:Wx1 ->hb* a:

   Since wmb is B-cumulative, if a: executes before b: then we get

        b: ->cpord* 5:Wy3 ->wmb 5:Wx1 ->hb* a: ->hb b:

   and so  b: ->cpord* b:.  If b: executes before a: then we get

       1:Wx3 ->co 2:Wx3 ->mb 2:Rx4 ->fre 3:Wx4 ->wmb 3:Wy1 ->hb*
               b: ->hb a: ->rfe 1:Rx2 ->mb 1:Wx3

   and so  1:Wx3 ->cpord* 2:Rx4 -> strong-prop 1:Wx3.

   Either way, there is a violation of the propagation check.
*)

{
}

P0(int *x1, int *x2, int *y1, int *y2)
{
 int r0;
 int r1;

 r0 = READ_ONCE(*x1);
 WRITE_ONCE(*x2, r0);

 r1 = READ_ONCE(*y1);
 WRITE_ONCE(*y2, r1);
}

P1(int *x2, int *x3)
{
 int r2;

 r2 = READ_ONCE(*x2);
 smp_mb();
 WRITE_ONCE(*x3, 1);
}

P2(int *x3, int *x4)
{
 int r4;

 WRITE_ONCE(*x3, 2);
 smp_mb();
 r4 = READ_ONCE(*x4);
}

P3(int *x4, int *y1)
{
 WRITE_ONCE(*x4, 1);
 smp_wmb();
 WRITE_ONCE(*y1, 1);
}

P4(int *y2, int *y3)
{
 WRITE_ONCE(*y2, 2);
 smp_wmb();
 WRITE_ONCE(*y3, 1);
}

P5(int *y3, int *x1)
{
 WRITE_ONCE(*y3, 2);
 smp_wmb();
 WRITE_ONCE(*x1, 1);
}

Observed
    y3=2; y2=2; x3=2; 2:r4=1; 1:r2=1; 0:r1=1; 0:r0=1;
and y3=2; y2=2; x3=1; 2:r4=1; 1:r2=1; 0:r1=1; 0:r0=1;
and y3=2; y2=2; x3=2; 2:r4=0; 1:r2=1; 0:r1=1; 0:r0=1;
and y3=2; y2=1; x3=2; 2:r4=0; 1:r2=1; 0:r1=1; 0:r0=1;
and y3=2; y2=2; x3=1; 2:r4=0; 1:r2=1; 0:r1=1; 0:r0=1;
and y3=2; y2=2; x3=2; 2:r4=1; 1:r2=0; 0:r1=1; 0:r0=1;
and y3=2; y2=2; x3=1; 2:r4=1; 1:r2=0; 0:r1=1; 0:r0=1;
and y3=2; y2=2; x3=2; 2:r4=0; 1:r2=0; 0:r1=1; 0:r0=1;
and y3=2; y2=2; x3=1; 2:r4=0; 1:r2=0; 0:r1=1; 0:r0=1;
and y3=2; y2=2; x3=2; 2:r4=1; 1:r2=1; 0:r1=0; 0:r0=1;
and y3=2; y2=2; x3=1; 2:r4=1; 1:r2=1; 0:r1=0; 0:r0=1;
and y3=2; y2=2; x3=2; 2:r4=0; 1:r2=1; 0:r1=0; 0:r0=1;
and y3=2; y2=2; x3=1; 2:r4=0; 1:r2=1; 0:r1=0; 0:r0=1;
and y3=2; y2=2; x3=2; 2:r4=1; 1:r2=0; 0:r1=0; 0:r0=1;
and y3=2; y2=2; x3=1; 2:r4=1; 1:r2=0; 0:r1=0; 0:r0=1;
and y3=2; y2=2; x3=2; 2:r4=0; 1:r2=0; 0:r1=0; 0:r0=1;
and y3=2; y2=2; x3=1; 2:r4=0; 1:r2=0; 0:r1=0; 0:r0=1;