Test MP+rel+DSB.LD-TLBI-DSB

AArch64 MP+rel+DSB.LD-TLBI-DSB
{ 
pte_x=(valid:0,oa:phy_x);
0:X2=pte_x;
0:X1=(valid:1,oa:phy_y);
0:X3=x; 1:X3=x;
y=1;
0:X8=z; 1:X8=z;
}
P0              | P1;
STR X1,[X2]     | LDR W7,[X8]    ;
                | DSB LD         ;
MOV W7,#1       | LSR X9,X3,#12  ;
STLR W7,[X8]    | TLBI VAAE1IS,X9;
                | DSB ISH        ;
                | L0:LDR W4,[X3];
exists (1:X4=0 /\ 1:X7=1 /\ fault(P1:L0,x,MMU:Translation))