C S+locked+mb {} P0(int* y,spinlock_t* lo,int* x) { spin_lock(lo); WRITE_ONCE(*x,2); spin_unlock(lo); spin_lock(lo); WRITE_ONCE(*y,1); spin_unlock(lo); } P1(int* y,int* x) { int r0 = READ_ONCE(*y); smp_mb(); WRITE_ONCE(*x,1); } Observed x=2; 1:r0=1;