Re: [isabelle-dev] Isabelle build timing on high-end hardware
On 02/07/18 15:21, Makarius wrote: > > 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 Here are more timing results on that great machine of some Isabelle users: ML_PLATFORM="x86-linux" ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.7.1-8/x86-linux" ML_SYSTEM="polyml-5.7.1" ML_OPTIONS="--minheap 1500" Isabelle/8ef8905629ba AFP/234a91c26d02 isabelle build -o threads=6 -j10 -a -N -d '$AFP' -f -x HOL-ODE-Numerics -X slow 0:36:19 elapsed time, 19:13:18 cpu time, factor 31.75 Note that the sessions starting from HOL-ODE-Numerics are relatively slow, but insignificant for a meaningful test: ignoring them like the "slow" group leads to very good results, below the critical "Paris Commuter constant". It is even slightly better than the 45min from 2012, when "isabelle build" was new and that expression came up in Paris Sud. Shortly afterwards we've had a lot of activity on Isabelle + AFP, as a consequence of renovations of Isabelle/Pure/HOL + libraries -- when testing was fun. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle build timing on high-end hardware
On 02/07/18 15:53, Lawrence Paulson wrote: > 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. I was myself wondering about more cores: this is the best I have recently seen, but cores alone don't crunch it. Performance is ultimately a combination of many things: many cores, few NUMA nodes, fast SSD, fast memory. (That hardware has 4x 16 2Rx8 PC4-2666V RAM.) It also needs better scheduling on the Isabelle side: for this it always helps if people buy test hardware and grant access to me :-) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle build timing on high-end hardware
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 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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Isabelle build timing on high-end hardware
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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
