[isabelle-dev] Isabelle build timing on high-end hardware

[Lawrence Paulson]

These speedups are certainly very impressive! I have wondered what sort of factor could be achieved with enough cores, but was never persistent enough in trying to borrow hardware from people who had it.

Larry

> On 2 Jul 2018, at 14:21, Makarius <makarius at sketis.net> wrote:
> 
> Just for the fun of it, here are some timings on truly high-end
> hardware: some colleagues have upgraded recently and granted me access
> to make some tests.
> 
> The results may help others in their hardware decisions.
> 
> Here is an Executive Summary:
> 
>  * Intel Xeon performs better than AMD
>  * fewer NUMA nodes are better
>  * SSD file-systems help to save and load heap images fast
> 
> 
> Here are some details:
> 
> 2 * Intel(R) Xeon(R) Gold 6148 CPU @ 2.40GHz;
> 2 NUMA nodes: distance factor 2.1 for memory access;
> each CPU with 20 cores and hyper-threading: total of 80 hardware threads
> 
> 256 GB SSD
> 
> Ubuntu Linux 16.04
> 
> 
> Isabelle/eb53f944c8cd + AFP/f7e9efc65d82
> ISABELLE_BUILD_OPTIONS="threads=6"
> 
> 
> * 64bit: ML_OPTIONS="--minheap 3g --maxheap 30g"
> 
> Finished HOL (0:02:21 elapsed time, 0:07:13 cpu time, factor 3.07)
> 
> isabelle build -j10 -a -N -f
> 0:13:37 elapsed time, 5:12:16 cpu time, factor 22.91
> 0:18:02 elapsed time, 5:57:58 cpu time, factor 19.85
> 
> isabelle build -j10 -a -N -f -x HOL-Proofs
> 0:15:24 elapsed time, 5:11:24 cpu time, factor 20.20
> 0:14:12 elapsed time, 4:45:27 cpu time, factor 20.10
> 
> isabelle build -j10 -g main -N -f
> 0:07:56 elapsed time, 0:43:58 cpu time, factor 5.53
> 0:08:07 elapsed time, 0:44:33 cpu time, factor 5.48
> 
> 
> * 32bit: ML_OPTIONS="--minheap 1500"
> 
> Finished HOL (0:02:10 elapsed time, 0:06:42 cpu time, factor 3.10)
> 
> isabelle build -j10 -a -N -f
> 0:11:13 elapsed time, 3:24:13 cpu time, factor 18.20
> 0:12:05 elapsed time, 4:07:12 cpu time, factor 20.45
> 
> isabelle build -j10 -a -N -f -x HOL-Proofs
> 0:09:13 elapsed time, 3:37:16 cpu time, factor 23.55
> 0:09:02 elapsed time, 3:27:56 cpu time, factor 22.99
> 
> isabelle build -j10 -g main -N -f
> 0:07:02 elapsed time, 0:39:45 cpu time, factor 5.64
> 0:07:02 elapsed time, 0:39:28 cpu time, factor 5.61
> 
> 
> isabelle build -j4 -o threads=10 -g main -N -f
> 0:06:17 elapsed time, 0:46:10 cpu time, factor 7.34
> 0:05:58 elapsed time, 0:45:26 cpu time, factor 7.60
> 
> isabelle build -j6 -o threads=8 -g main -N -f
> 0:06:40 elapsed time, 0:43:18 cpu time, factor 6.49
> 
> 
> When trying out changes of Pure or HOL, I usually test "-g main" first:
> it consists of HOL, HOL-Algebra, HOL-Analysis,
> HOL-Computational_Algebra, HOL-Library, HOL-Number_Theory,
> HOL-Probability, HOL-SPARK, HOL-Word, HOLCF. Afterwards there is a high
> chance that all of Isabelle works.
> 
> The numbers above are really good for that: 6min and 12min respectively.
> These are "quasi-interactive" builds as they should be today.
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev