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


	Makarius





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