Test MP+dmb.st+dsb.st-tlbi-dsb-isb

AArch64 MP+dmb.st+dsb.st-tlbi-dsb-isb
{
pte_x=(valid:1);

0:X1=(oa:phy_x,valid:0);
0:X2=pte_x;
0:X8=y;

1:X8=y;
1:X3=x;
}
P0           | P1;
STR X1,[X2]  | LDR W7,[X8]     ;
DMB ST       | DSB ST          ;
MOV W7,#1    | LSR X9,X3,#12   ;
STR W7,[X8]  | TLBI VAAE1IS,X9 ;
             | DSB ISH         ;
             | ISB             ;
             |L0:              ;
             | LDR W4,[X3]     ;
exists (1:X7=1 /\ ~fault(P1:L0,x))