AArch64 MP+shoot+po
{
0:X2=pte_x;
0:X1=(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 ISH |L0: ;
LSR X9,X3,#12 | LDR W4,[X3] ;
TLBI VAAE1IS,X9 | ;
DSB ISH | ;
MOV W7,#1 | ;
STR W7,[X8] | ;
exists (1:X4=0 /\ 1:X7=1)