[isabelle-dev] Multicores at TUM
immler at in.tum.de
Wed Jul 10 14:50:10 CEST 2013
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 .
Yutaka uses Isabelle to generate code for another library, DPH .
There have been disappointing measurements, but they were mostly due to the fact that both libraries are still under development.
> 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.
More information about the isabelle-dev