…
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;