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