C SB-unlock-lock {} P0(int *x, int *y, spinlock_t *u) { int r0; spin_lock(u); WRITE_ONCE(*x, 1); spin_unlock(u); spin_lock(u); r0 = READ_ONCE(*y); spin_unlock(u); } P1(int *x, int *y, spinlock_t *v) { int r0; spin_lock(v); WRITE_ONCE(*y, 1); spin_unlock(v); spin_lock(v); r0 = READ_ONCE(*x); spin_unlock(v); } Observed 1:r0=0; 0:r0=0;