Re: [isabelle] Isabelle-friendly CPUs and benchmarks
On Mon, 5 Nov 2012, Holger Blasum wrote:
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?
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and