[isabelle-dev] polyml-test-15c840d48c9a with updated ARM64 code-generator

Makarius makarius at sketis.net
Mon Jan 24 22:33:58 CET 2022

In Isabelle/68ffcf5cc94b we now have Poly/ML with updated ARM64 
code-generator, see also the announcement by David Matthews on 16-Jan-2022 

The long-promised update to the ARM code-generator is now in Git master. This 
builds on the old version by adding the register allocation strategy borrowed 
from the X86 version as well as low-level peephole optimisation.  On my Apple 
M1 processor it now seems to be faster than X86 code with Rosetta.

There are still some improvements to be made, particularly with floating 
point, but no major changes are anticipated.  It includes one optimisation 
that isn't present on the X86 at the moment: small tuples are returned in 
registers rather than on the stack.

Please try it and let me know how it goes.

So far it looks pretty good, but we don't have systematic test and 
measurements so far.

(Side-remark: TUM appears to have problems with lxbroy10 and lxcisa0. I have 
simply switched over to isabelle.in.tum.de as SSH login machine.)


More information about the isabelle-dev mailing list