Test rcu-barrier-vs-relacq

LISA rcu-barrier-vs-relacq.litmus
(*
 * Result: Maybe
 *
 * Forbidden under the memory barrier model of RCU,
 * allowed under the write-release/read-acquire model.
 *)
{
}
 P0                 | P1            | P2            ;
 f[rcu_read_lock]   | w[once] x 1   | w[once] v 1   ;
 r[once] r1 x       | f[sync]       | f[wmb]        ;
 r[once] r2 u       | r[once] r4 y  | w[once] u 1   ;
 f[rcu_read_unlock] |               |               ;
 w[once] y 1        |               |               ;
 r[once] r3 v       |               |               ;
Observed
    1:r4=0; 0:r3=1; 0:r2=0; 0:r1=1;
and 1:r4=0; 0:r3=1; 0:r2=1; 0:r1=0;
and 1:r4=0; 0:r3=1; 0:r2=0; 0:r1=0;