Email Gateway (Aug 18 2022 at 17:54): Email Gateway (Aug 18 2022 at 17:54):From: Gerwin Klein <gerwin.klein@nicta.com.au>
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
Email Gateway (Aug 18 2022 at 17:55):From: Palle Raabjerg <palle.raabjerg@it.uu.se>
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.
Email Gateway (Aug 18 2022 at 17:58):From: Palle Raabjerg <palle.raabjerg@it.uu.se>
Thank you. I will take this into consideration.
It does indeed sound like a smaller number of powerful Xeon cores is the
best solution.
Email Gateway (Aug 18 2022 at 17:59):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 18 2022 at 18:00):From: Palle Raabjerg <palle.raabjerg@it.uu.se>
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.
Email Gateway (Aug 18 2022 at 18:06):From: Palle Raabjerg <palle.raabjerg@it.uu.se>
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
Email Gateway (Aug 18 2022 at 18:08):From: Simon Winwood <sjw@cse.unsw.edu.au>
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.
Simon
Last updated: Apr 30 2024 at 04:19 UTC