RISCV ISA-MP-DEP-WW-SUCCESS (* Success dependency on P0 does not create ppo from W to W, Allow *) { 0:x6=x; 0:x8=y; 1:x6=y; 1:x9=x; } P0 | P1 ; lr.w x1,0(x6) | ; ori x5,x1,1 | lw x5,0(x6) ; sc.w x9,x5,0(x6) | andi x7,x5,128 ; ori x7,x9,1 | add x10,x9,x7 ; andi x7,x7,1 | lw x8,0(x10) ; sw x7,0(x8) | ; exists (1:x5=1 /\ 1:x8=0 /\ 0:x9=0 /\ x=1)