RISCV PPOLDSTLD02
(*
Variation on ppo rule ld->st->ld, or (addr|data);rfi
the "data" dependency is from SC success register....
*)
{
0:x6=x; 0:x8=y;
1:x5=y; 1:x9=z; 1:x13=x;
}
P0 | P1 ;
ori x5,x0,1 | lr.w x6,0(x5) ;
sw x5,0(x6) | sc.w x7,x6,0(x5) ;
fence w,w | xor x8,x7,x7 ;
ori x7,x0,1 | ori x8,x8,1 ;
sw x7,0(x8) | sw x8,0(x9) ;
| lw x10,0(x9) ;
| andi x11,x10,128 ;
| add x14,x13,x11 ;
| lw x12,0(x14) ;
exists
(y=1 /\ 1:x7=0 /\ 1:x6=1 /\ 1:x10=1 /\ 1:x12=0)