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)