Email Gateway (Aug 19 2022 at 09:16): Email Gateway (Aug 19 2022 at 09:16):From: Holger Blasum <hbl@sysgo.com>
Dear all,
Looking at
http://www.notebookcheck.net/Mobile-Processors-Benchmarklist.2436.0.html
as well as
I would guess that integer-heavy benchmarks like dhrystone
and coremark are most relevant to Isabelle performance on HW.
A well-known caveat of dhrystone is that it fits into most modern
caches. Any opinions or references on this?
(For the general Isabelle performance on multicore I am aware
of Wenzel, "Parallel Proof Checking in Isabelle/Isar", e.g.
at http://www.lri.fr/~wenzel/papers/parallel-isabelle.pdf )
TIA,
Email Gateway (Aug 19 2022 at 09:21):From: Makarius <makarius@sketis.net>
I've lost track of these classic benchmarks many years ago -- it is
unclear to me what they actually measure on the increasingly complex
hardware and software situation of today.
As a general rule of thumb, Isabelle as symbolic application does almost
no float computation, little int computation, and a lot of shuffling of
memory content. So as the general trend of multi/many-core hardware goes,
memory bandwidth becomes the main issue. Luckily, Poly/ML 5.5.x is pretty
good and making this fast for the large immutable heaps we have in
Isabelle.
My impression from practical work with Poly/ML and Isabelle is that
high-end Intel chips work best, something like current i5/i6 with 4-16
cores and good memory sub-system. Hyperthreading also helps a bit to make
up for memory wait-cycles: on 8 core * hyperthreaded Xeon, I've seen a
peak speedup of 10 in isolated situations (overall wall-clock speedup is a
slightly different thing).
As complete systems, the Mac Pro is particularly nice, because everything
fits together without having to spend extra on system-software
configuration -- you do spend extra money, though.
Makarius
Email Gateway (Aug 19 2022 at 09:23):From: Holger Blasum <hbl@sysgo.com>
Hi Makarius,
Given that mobility and energy usage concerns suggested a laptop, making
a q&d crossmatrix of the benchmarklist mentioned in initial post with a set
of three-digit offers by a popular laptop site here in Germany mostly gave models
containing the i7-3610QM, 3612QM, 3630QM, 3632QM, 3520QM processors
(QM means "quadcore mobile") for good dhrystone, aes and superpi benchmarks.
3dmark6 while probably useless for Isabelle also was mostly
consistent with above results. Looking for a small (<= 14 inch, no useless num
block to carry around) laptop looking out for 3612QM and 3632QM was helpful
in my case (they come on slightly smaller dies than their 3610QM/3630QM
cousins). For the record, in the benchmarklist mentioned in the initial
post (up to quadcore), the best (affordable) mobile 3612QM rated at 86945 dhrystones
vs the best desktop at 136990 (3820QM), consistent with the specified
processor speeds (the 3632QM is out since this Oct, slightly faster than
3612QM, and was not yet on the list).
Best,
Last updated: Apr 19 2024 at 16:20 UTC