Email Gateway (Aug 22 2022 at 19:35): Email Gateway (Aug 22 2022 at 19:35):From: Makarius <makarius@sketis.net>
Dear Isabelle users,
I mentioned my great new Engineering Workstation for Isabelle, and was
asked to say more about it:
* CPU: Intel i7-9700K 3.6GHz (4.9 GHz turbo), 8 Cores, no
hyperthreading, 12 MB cache
* RAM: 2 * 16 GB at 3.6GHz
* persistant storage: 1000 GB Samsung EVO Plus (NVMe PCIe)
* graphics: Nvidia GT 1030 with passive cooling (UHD: DisplayPort at
60Hz + HDMI at 30Hz)
* OS: Linux preinstalled (Ubuntu Budgie)
Total price: 1410 EUR before VAT, 1670 EUR with VAT -- by a local Linux
Hardware provider. (I've even met them today at the Linux and Opensource
conference in Augsburg.)
The CPU is very fast and very hot, only the Intel i9-9900K model is even
hotter (Intel tries to compete with AMD again.) It means that running 8
cores in full turbo mode consumes a lot of power and makes quite some
fan noise: so I have switched off the turbo in the BIOS and only use it
in regular 3.6GHz mode; this fits nicely to the extra-fast memory at the
same speed. Thus the fan is almost off under normal circumstances, and
becomes barely audible when "isabelle build -a" starts to crunch.
The persistant storage helps to speed up loading of these ultra-fat JVM
artifacts that we are running with Isabelle/jEdit. It also helps a lot
for stored heap images of Poly/ML. (I would never go back to an actual
"disk".)
The extra graphics card (80 EUR) could have been omitted: that Intel CPU
has quite capable UHD graphics on-chip, but the mainboard exposed it
only as HDMI (30Hz), not as DisplayPort (60Hz) for my fancy Samsung UHD
display (300 EUR in 2018, 250 EUR in 2019).
Here are some adhoc numbers from "isabelle build -g main" (approximately
at Isabelle2019-RC0):
ISABELLE_BUILD_OPTIONS="threads=6"
ML_PLATFORM="x86_64_32-linux"
ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.8/x86_64_32-linux"
ML_SYSTEM="polyml-5.8"
ML_OPTIONS="--minheap 1500"
Finished HOL (0:02:12 elapsed time, 0:06:43 cpu time, factor 3.05)
Finished HOL-Analysis (0:04:09 elapsed time, 0:18:37 cpu time, factor 4.48)
Finished HOL-Library (0:01:05 elapsed time, 0:05:01 cpu time, factor 4.60)
Finished HOL-Computational_Algebra (0:00:36 elapsed time, 0:01:44 cpu
time, factor 2.89)
Finished HOL-Algebra (0:00:40 elapsed time, 0:03:33 cpu time, factor 5.24)
Finished HOL-Probability (0:00:39 elapsed time, 0:03:14 cpu time, factor
4.94)
Finished HOL-Number_Theory (0:00:30 elapsed time, 0:02:11 cpu time,
factor 4.33)
I will try this again tomorrow, with all 8 cores, and also with this
hot/noisy turbo mode.
(The above looks already like an invitation to Larry to port even more
HOL-Analysis stuff by John Harrison :-)
Makarius
Email Gateway (Aug 22 2022 at 19:36):From: Makarius <makarius@sketis.net>
That is now, so here are more measurements in turbo mode (CPU up to
4.9GHz, fan noise approx. 46dB at 1m distance, 43dB at 2m distance).
First with ISABELLE_BUILD_OPTIONS="threads=6":
$ isabelle build -g main -f
Finished Pure (0:00:10 elapsed time, 0:00:10 cpu time, factor 0.99)
Finished HOL (0:01:43 elapsed time, 0:05:18 cpu time, factor 3.08)
Finished HOL-Analysis (0:03:19 elapsed time, 0:14:55 cpu time, factor 4.50)
Finished HOL-Library (0:00:53 elapsed time, 0:04:06 cpu time, factor 4.62)
Finished HOL-Computational_Algebra (0:00:28 elapsed time, 0:01:22 cpu
time, factor 2.93)
Finished HOL-Algebra (0:00:32 elapsed time, 0:02:52 cpu time, factor 5.33)
Finished HOL-Probability (0:00:30 elapsed time, 0:02:37 cpu time, factor
5.11)
Finished HOL-Number_Theory (0:00:23 elapsed time, 0:01:45 cpu time,
factor 4.40)
Finished HOLCF (0:00:06 elapsed time, 0:00:15 cpu time, factor 2.43)
Finished ZF (0:00:05 elapsed time, 0:00:17 cpu time, factor 3.21)
Finished HOL-Word (0:00:04 elapsed time, 0:00:19 cpu time, factor 4.15)
0:08:27 elapsed time, 0:34:02 cpu time, factor 4.02
Now with ISABELLE_BUILD_OPTIONS="threads=8", attempting to saturate this
8-core CPU:
$ isabelle build -g main -f
Finished Pure (0:00:10 elapsed time, 0:00:10 cpu time, factor 0.99)
Finished HOL (0:01:44 elapsed time, 0:05:33 cpu time, factor 3.20)
Finished HOL-Analysis (0:02:54 elapsed time, 0:16:08 cpu time, factor 5.56)
Finished HOL-Library (0:00:49 elapsed time, 0:04:29 cpu time, factor 5.41)
Finished HOL-Computational_Algebra (0:00:28 elapsed time, 0:01:26 cpu
time, factor 3.01)
Finished HOL-Algebra (0:00:32 elapsed time, 0:03:02 cpu time, factor 5.62)
Finished HOL-Probability (0:00:27 elapsed time, 0:02:48 cpu time, factor
6.21)
Finished HOL-Number_Theory (0:00:23 elapsed time, 0:01:51 cpu time,
factor 4.72)
Finished HOLCF (0:00:06 elapsed time, 0:00:15 cpu time, factor 2.50)
Finished ZF (0:00:05 elapsed time, 0:00:18 cpu time, factor 3.22)
Finished HOL-Word (0:00:04 elapsed time, 0:00:20 cpu time, factor 4.22)
0:07:56 elapsed time, 0:36:25 cpu time, factor 4.59
Such test times << 10min of the main library sessions are very important
when exploring changes on Pure or basic HOL.
More serious library maintenance (against AFP) requires a server-class
multicore monster: e.g. 2 * 20 cores (Intel) or 8 * 8 cores (AMD). This
results in approx. 45..90..120 min total build time for everything. The
server scenario also explains the ANNOUNCE entry of Isabelle2019-RC0:
Since we are still moving forward on both legs, AFP applications can
still grow, and we continue to live and prosper.
Makarius
Email Gateway (Aug 22 2022 at 19:36):From: Wenda Li <wl302@cam.ac.uk>
Hi Makarius,
Thanks for sharing your fantastic setup!
If noise is a concern, it might be worth devoting a little to the cooler & the case. My personal PC is with a 9700k CPU and a 2080ti GPU (which I believe is much hotter than GT 1030, but it is quite handy when playing around with neural networks). The CPU cooler I use is Dark Rock Pro 4 and the case is Fractal Design Define S2 Mid Tower, both of which are meant for quietness. Though I haven’t properly measured the noise level, I can say it is totally tolerable even when both CPU and GPU are 100% loaded — the CPU cooler is advertised to only have 24.3dB noise even at 100% PWM fan speed.
In addition, I believe better thermal paste (e.g. Thermal Grizzly) can help with the noise. I only used the paste that came with my cooler: since the noise level is already pretty good, I didn’t upgrade the paste to reduce it further.
Wenda
Email Gateway (Aug 22 2022 at 19:36):From: Makarius <makarius@sketis.net>
For completeness, here is the same test with 3.6GHz (no turbo, no noise):
ISABELLE_BUILD_OPTIONS="threads=8"
ML_PLATFORM="x86_64_32-linux"
ML_HOME="/home/makarius/.isabelle/contrib/polyml-5.8/x86_64_32-linux"
ML_SYSTEM="polyml-5.8"
ML_OPTIONS="--minheap 1500"
Finished Pure (0:00:13 elapsed time, 0:00:13 cpu time, factor 0.99)
Finished HOL (0:02:10 elapsed time, 0:06:47 cpu time, factor 3.13)
Finished HOL-Analysis (0:03:22 elapsed time, 0:18:44 cpu time, factor 5.55)
Finished HOL-Library (0:00:56 elapsed time, 0:05:08 cpu time, factor 5.43)
Finished HOL-Computational_Algebra (0:00:35 elapsed time, 0:01:45 cpu
time, factor 2.95)
Finished HOL-Algebra (0:00:39 elapsed time, 0:03:36 cpu time, factor 5.51)
Finished HOL-Probability (0:00:32 elapsed time, 0:03:16 cpu time, factor
6.04)
Finished HOL-Number_Theory (0:00:28 elapsed time, 0:02:13 cpu time,
factor 4.63)
Finished HOLCF (0:00:07 elapsed time, 0:00:19 cpu time, factor 2.47)
Finished ZF (0:00:06 elapsed time, 0:00:22 cpu time, factor 3.27)
Finished HOL-Word (0:00:05 elapsed time, 0:00:25 cpu time, factor 4.23)
0:09:31 elapsed time, 0:42:53 cpu time, factor 4.50
Makarius
Last updated: May 02 2024 at 16:19 UTC