Test LB+ctrl+mb

C LB+ctrl+mb
"DpCtrldW Rfe FenceScdRW Rfe"
(* Hand edited -> true dependency *)
{}

P0 (int* y,int* x) {
  int r0 = READ_ONCE(*x);
  if (r0 == 1) {
    WRITE_ONCE(*y,1);
  }
}

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

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

C11 equivalent: c11-prop-src/LB+ctrl+mb.litmus