Re: [isabelle] Dedicated proof box
On 2011-07-01 15:38, Makarius wrote:
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 single Opteron?
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.
Thank you. This has also been duly noted.
If we can afford it, we might actually go for the two 6-cores then. I
have been looking at such boxes, and the prices don't seem to be too steep.
And yes, the efficiency of a single core is unlikely to improve
drastically, as the focus today is on creating chips with more cores. So
this setup should stay useful for quite a while.
This archive was generated by a fusion of
Pipermail (Mailman edition) and