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