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)