Re: [isabelle] Dedicated proof box
On Fri, 1 Jul 2011, Palle Raabjerg wrote:
We could also go for a single 8-12 core Opteron, but since it seems that
Xeon cores are fewer in number, though more powerful, the better idea
may be to go for two 4-core or one 6-core Xeon.
But one thing that worries me a bit in that case is Intel's
hyperthreading. So even if we get a 4-core Xeon, it would likely happily
run 8 threads at once, thus potentially doubling the memory requirement
and at the same time flattening the multicore-benefit curve quicker. And
in that case, maybe we should consider just having more real cores in a
I have worked both with AMD Opteron and Intel Xeon -- the papers alternate
in that respect without making it very explicit. See also the more recent
http://www4.in.tum.de/~wenzelm/papers/itp-smp.pdf which is for Xeon again.
I find it much easier to get actual performance out of Xeon our setting,
than with Opteron with nominally more cores. In practice that can mean a
well-equippped Mac Pro, but you can also get cheaper Linux boxes with
these CPUs, if you spend some time investigating the market.
It seems that the latest Intel Westmere is already replacing the
established Nehalem line -- which was very good in the past 2 years.
Hyperthreading is not getting in the way. Isabelle provides the soft
Multithreading.max_threads option, instead of relying on raw number of
CPUs reported by the operating system. Mac OS X, and presumably Linux,
are smart enough to map running threads on real cores, before using
hyperthreading. (Apple's Snow Leopard update on Leopard was a big
performance improvement in this respect.)
After Isabelle2011 it is easier to saturate 8 cores, and memory
requirements are descreasing a bit. So a midrange system with 2 sockets of
6 core Xeon, and maybe 32 GB memory, should make a very good workstation
for the next few years.
This archive was generated by a fusion of
Pipermail (Mailman edition) and