C C-MP+o-wmb-o+o-rmb-o.litmus
{
}
P0(int *a, int *b)
{
WRITE_ONCE(*a, 1);
smp_wmb();
WRITE_ONCE(*b, 1);
}
P1(int *a, int *b)
{
int r1;
int r2;
r1 = READ_ONCE(*b);
smp_rmb();
r2 = READ_ONCE(*a);
}
exists
(1:r1=1 /\ 1:r2=0)
C11 equivalent: c11-prop-src/C-MP+o-wmb-o+o-rmb-o.litmus