AArch64 coRRExpNExp+DSB-TLBI-DSB+VMALL
{
0:X1=pte_x; 0:X3=x; 0:X6=(oa:phy_y);
1:X1=pte_x; 1:X2=(oa:phy_y);
y=1;
}
P0 | P1 ;
LDR X2,[X1] | STR X2,[X1];
DSB ISH | ;
TLBI VMALLE1IS | ;
DSB ISH | ;
LDR W4,[X3] | ;
CMP X2,X6 | ;
CSET W5,EQ | ;
exists (0:X4=0 /\ 0:X5=1)