AArch64 coRR-pte6+VMALL { 0:X1=x; 0:X3=x; 1:X3=pte_x; 1:X4=(oa:phy_y); y=1; } P0 | P1 ; LDR W2,[X1] | STR X4, [X3]; DSB ISH | ; TLBI VMALLE1IS | ; DSB ISH | ; LDR W4,[X3] | ; exists (0:X2=1 /\ 0:X4=0)