[isabelle-dev] Multicores at TUM

[Makarius]

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

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.


 	Makarius