Test RCU-MP

C RCU-mp
Hash=efa84080f8fda7f085fc9a458a135c16

{}


P0(int* x,int* y) {
  rcu_read_lock();
  int r1 = READ_ONCE(*y);
  int r0 = READ_ONCE(*x);
  rcu_read_unlock();
}

P1(int* x,int* y) {
  WRITE_ONCE(*x,1);
  synchronize_rcu();
  WRITE_ONCE(*y,1);
}

exists (0:r0=0 /\ 0:r1=1)