AArch64 D15347-load-shoot+VMALL { pte_x=(valid:0,db:1); (*invalid*) 0:X2=pte_x; 0:X5=x; 0:X1=(oa:phy_y,db:1); 0:X3=x; y=1; } P0 ; MOV W4,#0 ; STR X1,[X2] ; DSB ISH ; TLBI VMALLE1IS ; DSB ISH ; L0:LDR W4,[X3] ; exists (0:X4=0 /\ fault(P0:L0,x,MMU:Translation))