AArch64 SWP-RpteW+RR+DMBLD+DMBLD-P0HD TTHM=HD { 0:X3=pte_x; pte_x=(valid:0); 0:X1=(oa:phy_x,af:1); 0:X2=(oa:phy_x,af:0); 0:X6=y; 1:X6=y; 1:X7=x; } P0 | P1; SWP X1,X2,[X3] | LDR W5,[X6] ; LDR X4,[X3] | DMB LD ; DMB LD | L0: LDR W8,[X7]; MOV W5,#1 | ; STR W5,[X6] | ; exists (0:X4=(oa:PA(x)) /\ 1:X5=1 /\ fault(P1:L0,x,MMU:Translation))