AArch64 D15347-MP+shoot+DSB-ISB-RO
{
pte_x=(oa:phy_x,db:0,dbm:1);
0:X2=pte_x; 0:X3=x; 1:X2=pte_x;
0:X1=(oa:phy_y,db:0);
y=1;
0:X8=z;
1:X8=z;
}
P0 | P1 ;
STR X1,[X2] | ;
DSB ISH | LDR W7,[X8] ;
LSR X9,X3,#12 | DSB ISH ;
TLBI VAAE1IS,X9 | L0:LDR X4,[X2];
DSB ISH | ;
MOV W7,#1 | ;
STR W7,[X8] | ;
exists(1:X7=1 /\ 1:X4=(oa:phy_x,af:1,db:0,dbm:1, valid:1) /\ x=0)