AArch64 D15347-M-store-shoot+DMB.ST
{
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 ;
LSR X3,X4,12 | L0:STR WZR,[X3];
TLBI VAAE1IS,X2 | ;
DSB ISH | ;
MOV W7,#1 | ;
STR W7,[X8] | ;
exists (1:X7=1 /\ fault(P1:L0,x,MMU:Translation))