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

[Makarius]

On 24/01/2022 22:33, Makarius wrote:
> 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):

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

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"


* MacMini8,1 Intel x86_64_32-darwin:

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)


* MacMini9,1 Apple M1 x86_64_32-darwin (Rosetta 2):

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)


* MacMini9,1 Apple M1 arm64_32-darwin:

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