RISCV ISA-Rel-Acq (* ISA, C11 problematic release-acquire sequence *) { uint64_t x; uint64_t y; 0:s0=x; 0:s1=y; 1:s0=x; 1:s1=y; } P0 | P1 ; ori x6,x0,1 | ori x6,x0,1 ; sd x6,0(s0) | amoswap.d a0,x6,0(s1) ; fence w,w | ld.aq a1,0(s1) ; sd x6,0(s1) | ld a2,0(s0) ; locations [1:a0;1:a1;1:a2;] ~exists 1:a0=1 /\ 1:a2=0