Re: [isabelle] Isabelle-friendly CPUs and benchmarks

On Mon, 5 Nov 2012, Holger Blasum wrote:

Looking at 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 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.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.