Email Gateway (Jan 24 2022 at 21:34): Email Gateway (Jan 24 2022 at 21:34):From: Makarius <makarius@sketis.net>
In Isabelle/68ffcf5cc94b we now have Poly/ML with updated ARM64
code-generator, see also the announcement by David Matthews on 16-Jan-2022
(http://lists.inf.ed.ac.uk/pipermail/polyml/2022-January/002489.html):
"""
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.)
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Jan 28 2022 at 17:55):From: Makarius <makarius@sketis.net>
Here are some measurements on macOS Big Sur for Isabelle/7483347efb4c, with
the following build parameters:
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
ISABELLE_BUILD_OPTIONS="threads=4"
ML_OPTIONS="--minheap 1500 --maxheap=10g"
Finished HOL (0:03:08 elapsed time, 0:09:11 cpu time, factor 2.93)
Finished HOL-Library (0:02:49 elapsed time, 0:09:04 cpu time, factor 3.21)
Finished HOL-Analysis (0:05:25 elapsed time, 0:19:00 cpu time, factor 3.50)
Finished HOL-Proofs (0:05:41 elapsed time, 0:10:09 cpu time, factor 1.79)
Finished HOL-Decision_Procs (0:03:21 elapsed time, 0:11:21 cpu time, factor 3.39)
Finished HOL-Data_Structures (0:04:02 elapsed time, 0:14:37 cpu time, factor 3.62)
Finished HOL-Nominal-Examples (0:03:14 elapsed time, 0:11:54 cpu time, factor
3.68)
Finished HOL-ex (0:03:11 elapsed time, 0:11:08 cpu time, factor 3.49)
Finished HOL (0:02:47 elapsed time, 0:07:59 cpu time, factor 2.87)
Finished HOL-Library (0:02:24 elapsed time, 0:07:39 cpu time, factor 3.18)
Finished HOL-Analysis (0:05:16 elapsed time, 0:17:12 cpu time, factor 3.27)
Finished HOL-Proofs (0:05:37 elapsed time, 0:09:47 cpu time, factor 1.74)
Finished HOL-Decision_Procs (0:03:50 elapsed time, 0:11:17 cpu time, factor 2.95)
Finished HOL-Data_Structures (0:03:22 elapsed time, 0:12:16 cpu time, factor 3.63)
Finished HOL-Nominal-Examples (0:02:59 elapsed time, 0:10:18 cpu time, factor
3.45)
Finished HOL-ex (0:02:43 elapsed time, 0:09:29 cpu time, factor 3.49)
Finished HOL (0:02:18 elapsed time, 0:06:40 cpu time, factor 2.88)
Finished HOL-Library (0:02:04 elapsed time, 0:06:40 cpu time, factor 3.21)
Finished HOL-Analysis (0:04:43 elapsed time, 0:15:24 cpu time, factor 3.26)
Finished HOL-Proofs (0:04:09 elapsed time, 0:07:25 cpu time, factor 1.79)
Finished HOL-Decision_Procs (0:03:01 elapsed time, 0:09:08 cpu time, factor 3.03)
Finished HOL-Data_Structures (0:02:52 elapsed time, 0:10:30 cpu time, factor 3.66)
Finished HOL-Nominal-Examples (0:02:30 elapsed time, 0:08:58 cpu time, factor
3.58)
Finished HOL-ex (0:02:28 elapsed time, 0:08:32 cpu time, factor 3.45)
Remark on the hardware: MacMini8,1 has 6 cores, MacMini9,1 has 8 cores (4
small, 4 big). The build option threads=4 unifies this to some extent, for
better comparison.
Conclusion: the new Apple hardware, Rosetta 2, and the new Poly/ML ARM64
code-generator are all excellent.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Jul 15 2022 at 23:21 UTC