RISCV ISA-DEP-WR-ADDR (* SC-W to R addr dependency through result register *) { 0:x5=x; 0:x10=y; 1:x6=y; 1:x9=x; } P0 | P1 ; ori x6,x0,1 | ori x5,x0,1 ; lr.w x7,0(x5) | sw x5,0(x6) ; sc.w x8,x6,0(x5) | fence rw,rw ; xor x9,x8,x8 | lw x8,0(x9) ; add x11,x10,x9 | ; lw x5,0(x11) | ; exists (x=1 /\ 0:x5=0 /\ 1:x8=0)