AArch64 ATOM00 "WsePX WseXP" Prefetch= Com=Ws Ws Orig=WsePX WseXP { ok=1; 0:X1=x; 1:X0=x; 1:X5=ok; } P0 | P1 ; MOV W0,#1 | MOV W1,#2 ; STR W0,[X1] | LDXR W2,[X0] ; | STXR W3,W1,[X0] ; | CBNZ W3,Fail1 ; | B Exit1 ; | Fail1: ; | MOV W4,#0 ; | STR W4,[X5] ; | Exit1: ; locations [ok;x;1:X2;] ~exists (ok=1 /\ x = 2 /\ 1:X2=0)