RISCV ISA-DEP-SUCCESS-SUCCESS (* Double success dependency, on an idea by P. Loewenstein, In case of two chained success dependency, Allow *) { uint64_t x; uint64_t y; uint64_t z; uint64_t a; 0:s0=x; 0:s1=y; 0:s2=z; 0:s3=a; 1:s0=x; 1:s2=z; } P0 | P1 ; ld a0,0(s0) | ld a3,0(s2) ; lr.d a1,0(s1) | sd a3,0(s0) ; sc.d a2,a0,0(s1) | ; addi a2,a2,2 | ; lr.d a3,0(s3) | ; sc.d a4,a2,0(s3) | ; addi a4,a4,2 | ; sd a4,0(s2) | ; exists 0:a0=2 /\ 0:a4=2 /\ 1:a3=2 /\ (0:a2=2 /\ a=2 /\ y=2 \/ 0:a2=3 /\ a=3 /\ y=0) \/ 0:a0=3 /\ 0:a4=3 /\ 1:a3=3 /\ a=0 /\ (0:a2=2 /\ y=3 \/ 0:a2=3 /\ y=0)