Re: [isabelle] Isabelle-friendly CPUs and benchmarks
On 11-15, Makarius wrote:
> 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).
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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and