[isabelle-dev] Multicores at TUM
makarius at sketis.net
Wed Jul 10 13:54:17 CEST 2013
On Wed, 10 Jul 2013, Fabian Immler wrote:
> For his Bachelor's thesis he needs to carry out performance measurements
> on a machine with many cores (isabelle-server).
What is this project anyway?
Note that isabelle-server has many cores (24), but the hardware structure
is made for many independent processes (e.g. virtual machines), not
applications that use shared-memory multithreading. Thus the results of
measurement might be a bit disappointing, depending on the kind of
Intel Xeons (especially after Nehalem from 2009) are usually much better;
macbroy2 is the classic machine for that, although it is getting a bit old
now; I have the follow-up model in my office since 2010. It is possible
to get a real warp factor of 9.6 for parallel Isabelle in the best
situation (8 cores with hyperthreading).
I have seen a really hot 16-core Xeon at TUM recently, but it seems to
belong to a different "Lehrstuhl" that is subject to the same system
administration. It runs some boring batch process with 16 threads since a
couple of weeks/months.
More information about the isabelle-dev