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)