Test LR-SC-NOT-FENCE

RISCV LR-SC-NOT-FENCE

(* 
  Original test by Sizhuo Zhang:
  LR/SC with aq.rl qualifier does not suffice to implement x86 locked
  instructions (which have implied fences).
*)

{
0:x6=a; 0:x8=b; 0:x10=c;
1:x6=b; 1:x8=a; 1:x10=d;
}

 P0                       | P1                       ;
 ori x5,x0,1              | ori x5,x0,1              ;
 sw x5,0(x6)              | sw x5,0(x6)              ;
 lr.w.aq.rl x12,0(x10)    | lr.w.aq.rl x12,0(x10)    ;
 sc.w.aq.rl x11,x5,0(x10) | sc.w.aq.rl x11,x5,0(x10) ;
 lw x7,0(x8)              | lw x7,0(x8)              ;

exists (c=1 /\ d=1 /\ 0:x7=0 /\ 1:x7=0)