…
C C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE
{
}
P0(int *sl, int *x0, int *x1)
{
int r2;
int r1;
r2 = cmpxchg_acquire(sl, 0, 1);
WRITE_ONCE(*x0, 1);
r1 = READ_ONCE(*x1);
smp_store_release(sl, 0);
}
P1(int *sl, int *x1, int *x2)
{
int r2;
int r1;
r2 = cmpxchg_acquire(sl, 0, 1);
WRITE_ONCE(*x1, 1);
r1 = READ_ONCE(*x2);
smp_store_release(sl, 0);
}
P2(int *sl, int *x2, int *x3)
{
int r2;
int r1;
r2 = cmpxchg_acquire(sl, 0, 1);
WRITE_ONCE(*x2, 1);
r1 = READ_ONCE(*x3);
smp_store_release(sl, 0);
}
P3(int *sl, int *x3, int *x0)
{
int r2;
int r1;
r2 = cmpxchg_acquire(sl, 0, 1);
WRITE_ONCE(*x3, 1);
r1 = READ_ONCE(*x0);
smp_store_release(sl, 0);
}
Observed
3:r2=0; 3:r1=1; 2:r2=1; 2:r1=1; 1:r2=0; 1:r1=1; 0:r2=1; 0:r1=1;
and 3:r2=0; 3:r1=1; 2:r2=1; 2:r1=1; 1:r2=0; 1:r1=1; 0:r2=0; 0:r1=1;
and 3:r2=0; 3:r1=0; 2:r2=1; 2:r1=0; 1:r2=0; 1:r1=0; 0:r2=0; 0:r1=0;