C LB+locked-diff+data
{}
P0(int* y,int* x,spinlock_t *lock_x, spinlock_t *lock_y) {
spin_lock(lock_x);
int r0 = READ_ONCE(*x);
spin_unlock(lock_x);
spin_lock(lock_y);
WRITE_ONCE(*y,1);
spin_unlock(lock_y);
}
P1(int* y,int* x) {
int r0 = READ_ONCE(*y);
WRITE_ONCE(*x,r0);
}
Observed
1:r0=1; 0:r0=1;