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)