Test PbStar

C PbStar

{ } 

void P0(int *c, int *x) {
  rcu_read_lock();
  WRITE_ONCE(*c,1);
  int r0 = READ_ONCE(*x);
  rcu_read_unlock();
}

void P1(int *x,int *y) {
  WRITE_ONCE(*x,1);
  smp_mb();
  int r0 = READ_ONCE(*y);
}

void P2(int *y,int *z) {
  WRITE_ONCE(*y,1);
  smp_mb();
  int r0 = READ_ONCE(*z);
}

void P3(int* z,int* a) {
  WRITE_ONCE(*z,1);
  synchronize_rcu();
  int r0 = READ_ONCE(*a);
}

void P4(int *a,int *b) {
  WRITE_ONCE(*a,1);
  smp_mb();
  int r0 = READ_ONCE(*b);
}

void P5(int *b,int *c) {
  WRITE_ONCE(*b,1);
  smp_mb();
  int r0 = READ_ONCE(*c);
}

Observed
    5:r0=1; 4:r0=1; 3:r0=0; 2:r0=1; 1:r0=1; 0:r0=1;
and 5:r0=0; 4:r0=1; 3:r0=0; 2:r0=1; 1:r0=1; 0:r0=1;
and 5:r0=1; 4:r0=0; 3:r0=0; 2:r0=1; 1:r0=1; 0:r0=1;
and 5:r0=0; 4:r0=0; 3:r0=0; 2:r0=1; 1:r0=1; 0:r0=1;
and 5:r0=1; 4:r0=1; 3:r0=0; 2:r0=0; 1:r0=1; 0:r0=1;
and 5:r0=0; 4:r0=1; 3:r0=0; 2:r0=0; 1:r0=1; 0:r0=1;
and 5:r0=1; 4:r0=0; 3:r0=0; 2:r0=0; 1:r0=1; 0:r0=1;
and 5:r0=0; 4:r0=0; 3:r0=0; 2:r0=0; 1:r0=1; 0:r0=1;
and 5:r0=1; 4:r0=1; 3:r0=0; 2:r0=1; 1:r0=0; 0:r0=1;
and 5:r0=0; 4:r0=1; 3:r0=0; 2:r0=1; 1:r0=0; 0:r0=1;
and 5:r0=1; 4:r0=0; 3:r0=0; 2:r0=1; 1:r0=0; 0:r0=1;
and 5:r0=0; 4:r0=0; 3:r0=0; 2:r0=1; 1:r0=0; 0:r0=1;
and 5:r0=1; 4:r0=1; 3:r0=0; 2:r0=0; 1:r0=0; 0:r0=1;
and 5:r0=0; 4:r0=1; 3:r0=0; 2:r0=0; 1:r0=0; 0:r0=1;
and 5:r0=1; 4:r0=0; 3:r0=0; 2:r0=0; 1:r0=0; 0:r0=1;
and 5:r0=0; 4:r0=0; 3:r0=0; 2:r0=0; 1:r0=0; 0:r0=1;
and 5:r0=1; 4:r0=1; 3:r0=0; 2:r0=1; 1:r0=1; 0:r0=0;
and 5:r0=0; 4:r0=1; 3:r0=0; 2:r0=1; 1:r0=1; 0:r0=0;
and 5:r0=1; 4:r0=0; 3:r0=0; 2:r0=1; 1:r0=1; 0:r0=0;
and 5:r0=0; 4:r0=0; 3:r0=0; 2:r0=1; 1:r0=1; 0:r0=0;
and 5:r0=1; 4:r0=1; 3:r0=0; 2:r0=0; 1:r0=1; 0:r0=0;
and 5:r0=0; 4:r0=1; 3:r0=0; 2:r0=0; 1:r0=1; 0:r0=0;
and 5:r0=1; 4:r0=0; 3:r0=0; 2:r0=0; 1:r0=1; 0:r0=0;
and 5:r0=0; 4:r0=0; 3:r0=0; 2:r0=0; 1:r0=1; 0:r0=0;
and 5:r0=1; 4:r0=1; 3:r0=0; 2:r0=1; 1:r0=0; 0:r0=0;
and 5:r0=0; 4:r0=1; 3:r0=0; 2:r0=1; 1:r0=0; 0:r0=0;
and 5:r0=1; 4:r0=0; 3:r0=0; 2:r0=1; 1:r0=0; 0:r0=0;
and 5:r0=0; 4:r0=0; 3:r0=0; 2:r0=1; 1:r0=0; 0:r0=0;
and 5:r0=0; 4:r0=1; 3:r0=1; 2:r0=0; 1:r0=0; 0:r0=0;
and 5:r0=0; 4:r0=0; 3:r0=1; 2:r0=0; 1:r0=0; 0:r0=0;
and 5:r0=1; 4:r0=1; 3:r0=0; 2:r0=0; 1:r0=0; 0:r0=0;
and 5:r0=0; 4:r0=1; 3:r0=0; 2:r0=0; 1:r0=0; 0:r0=0;
and 5:r0=1; 4:r0=0; 3:r0=0; 2:r0=0; 1:r0=0; 0:r0=0;