AArch64 LDRx+STRx-LDRptex+af TTHM=HA { int x=0; int y=0; pte_x=(af:0); pte_y=(oa:phy_x); 0:X2=x; 1:X4=y; 1:X6=pte_x; } P0 | P1 ; LDR W1,[X2] | MOV W1,#1 ; | STR W1,[X4] ; | DSB ISH ; | LDR X3,[X6] ; exists (0:X1=0 /\ 1:X3=(oa:PA(x), af:0))