C C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE { } P0(int *sl, int *x0, int *x1) { int r2; int r1; r2 = xchg_acquire(sl, 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 = xchg_acquire(sl, 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 = xchg_acquire(sl, 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 = xchg_acquire(sl, 1); WRITE_ONCE(*x3, 1); r1 = READ_ONCE(*x0); smp_store_release(sl, 0); } Observed 3:r2=0; 3:r1=1; 2:r2=0; 2:r1=1; 1:r2=1; 1:r1=1; 0:r2=0; 0:r1=1;