RISCV ISA-OLD+TER { 0:s0=x; 0:s1=y; 1:s0=x; 1:s1=y; } (* D. Lustig version of ISA-OLD+BIS, amoor ..,x0,.. -> lw.aq *) P0 | P1 ; li t1,1 | li t2,2 ; sw t1,0(s0) | amoswap.w a0,t2,0(s1) ; amoswap.w.rl x0,t1,0(s1) | lw.aq a1,0(s1) ; | lw a2,0(s0) ; ~exists 1:a0=1 /\ 1:a1=2 /\ 1:a2=0