Re: [isabelle] Dedicated proof box

I have considered this. And thank you for me reminding me. I need to look up how to do it. Unfortunately, we do frequently change stuff in the core theories, so I am not sure how well this would work out.

- Palle

On 2011-07-01 14:54, Simon Winwood wrote:
	As a side note, we get around this problem (somewhat, although it
is still annoying) by building images for the theories that don't change much ---
if you aren't changing your core definitions and proofs, this can save time.

	Of course, if you are changing stuff all over your theories, this won't help.


On 01/07/2011, at 10: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):
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.