AArch64 D15347-M-store-shoot+DMB.ST+VMALL { pte_x=(valid:0); (*invalid*) 0:X2=pte_x; 0:X4=x; 0:X1=(oa:phy_y,db:1); 1:X3=x; y=1; pte_z=(af:1,db:1); 0:X8=z; 1:X8=z; } P0 | P1; STR X1,[X2] | LDR W7,[X8] ; DSB ISH | DMB ST ; TLBI VMALLE1IS | L0:STR WZR,[X3]; DSB ISH | ; MOV W7,#1 | ; STR W7,[X8] | ; exists (1:X7=1 /\ fault(P1:L0,x,MMU:Translation))