[isabelle-dev] Multicores at TUM

[Fabian Immler]

Am 10.07.2013 um 13:54 schrieb Makarius <makarius at sketis.net>:

> 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?
It is about evaluating libraries for parallelism in Haskell, in Markus' case Repa [1].
Yutaka uses Isabelle to generate code for another library, DPH [2].
There have been disappointing measurements, but they were mostly due to the fact that both libraries are still under development.

Fabian

[1] http://repa.ouroborus.net/
[2] http://www.haskell.org/haskellwiki/GHC/Data_Parallel_Haskell

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