AArch64 S+dataxp+dmb.sy "based on: PosWRXP DpDatadW Rfe DMB.SYdRW WsePX" Prefetch=0:x=F,0:y=W,1:y=F,1:x=W Com=Rf Ws { ok=1; 0:X0=x; 0:X6=y; 1:X1=y; 1:X3=x; } P0 | P1 ; MOV W1,#2 | LDR W0,[X1] ; LDXR W2,[X0] | DMB SY ; STXR W3,W1,[X0] | MOV W2,#1 ; EOR W5,W3,W3 | STR W2,[X3] ; ADD W5,W5,#1 | ; STR W5,[X6] | ; exists (x=2 /\ 0:X2=1 /\ 0:X3=0 /\ 1:X0=1)