Re: [isabelle] Isabelle-friendly CPUs and benchmarks



Hi Makarius,

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).

Best,

-- 
Holger





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