Test RCU-deferred-free

C RCU-deferred-free
Hash=df5f73fb4c6230133558c0a7beccc6be

{}


P0(int* x,int* y) {
  rcu_read_lock();
  int r0 = READ_ONCE(*x);
  int r1 = READ_ONCE(*y);
  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)