# Re: [isabelle] Dedicated proof box

Thank you. I will take this into consideration.

It does indeed sound like a smaller number of powerful Xeon cores is the best solution.

- Palle

On 2011-07-01 14:58, Gerwin Klein wrote:

Hi Palle,

in our experience, it is better to go for more powerful processors instead of more cores. Also go for lots of memory (24G rather than 16G, 32 if you can get it cheap).

A fast disk for image writing and reading (additional SSD maybe, if that is an option) can make a few minutes difference for large sessions, depending on how much use of images you make.

It depends on the Isabelle version, but 3-4 concurrent threads seems to be the optimum point at the moment.

Hyperthreading as such is not a problem, you can easily tell Isabelle the maximum number of threads it should use and we haven't seen any significant overhead associated with that. Also, I vaguely recall that hyperthreading seems to have similar performance to separate cores, but I could be wrong there.

Cheers,
Gerwin

On 01/07/2011, at 2:37 PM, Palle Raabjerg wrote:


Hi all,

In our research group, we are currently considering getting a dedicated machine for working on proofs. Our Psi-calculus theories are large enough to incur significant waiting times whenever we have to restart the proof process. And there is more than one of us now, so simply getting powerful laptops is looking like the more expensive option.

So I am trying to find out what kind of setup is most effective for cutting proof times, since a dedicated box gives us a few interesting options for costumisation.
This paper presents some graphs that show performance benefits declining somewhat after the 4th core (as is also the case with many other parallel applications): http://www4.in.tum.de/~wenzelm/papers/parallel-isabelle.pdf
Since we are two Isabelle-guys now, and will probably be one or two more in the future, I am considering going for a box with 6-8 cores in total. And since I read from a previous post on this list that there is an additional memory-overhead for each core, that would likely put us at 16 or 24GB memory for those cores.
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?

Any thoughts on this would be appreciated. Particularly if someone has practical experience with running Isabelle on these architectures.

Best regards,
Palle Raabjerg








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