RISCV ISA-LB-DEP-ADDR3-SUCCESS (* Addr+Success dependency on P1, variation on an idea by D. Lustig, In the LR/SC pair on P1, only the write addr depends on initial load, As a result: Forbid (where SC succeeds), following rule3 addr;po \in ppo. { int z; int x; int y; int *p = &z; int *1:a0; 1:s0=p; 1:s1=y; 1:s2=x; 0:s0=p; 0:s1=y; 0:s2=x; } P0 | P1 ; lw a0,0(s1) | ld a0,0(s0) ; andi t1,a0,8| lr.w a1,0(s2) ; add s2,s2,t1| li t1,1 ; sd s2,0(s0) | sc.w a2,t1,0(a0) ; | ori t2,a2,1 ; | sw t2,0(s1) ; Observed 1:x12=0; 1:x10=z; 0:x10=1; and 1:x12=0; 1:x10=z; 0:x10=0;