Test S+locked+data

C S+locked+data

{}


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);
  WRITE_ONCE(*x,r0);
}

Observed
    x=2; 1:r0=1;