[isabelle-dev] Max threads & Sledgehammer

[Makarius]

On Mon, 7 Jan 2013, Stefan Berghofer wrote:

> it's a server with 24 CPUs of the type "Intel(R) Xeon(R) CPU E7450 @ 2.40GHz" 
> and 132299948 kB RAM.
>
>> What could happen here nonetheless is that Poly/ML tries to fork too many 
>> GC threads.
>
> This was indeed the problem.
>
>> So how many cores do you have?  I reckon it should work until 32 at the 
>> least.
>
> Well, obviously not :-(

Intel has hyperthreading, so it will report 48 CPUs here, or do you have 
12 cores that are reported as 24?  Anyway, we should tell David Matthews 
about it as well -- he could restrict his GC threads in a similar manner 
as Isabelle/ML does for the worker thread farm.

Generally, it is just another instance of "multicore numerology".  I've 
recently tried again to divinate more information from the JVM, so that 
Isabelle/Scala could impose better defaults on Isabelle components.  But 
the search ended at 
http://stackoverflow.com/questions/215236/threads-per-processor and 
http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5048379 (the "bug" 
database is just a collection of misunderstandings, and mostly changes of 
the documentation to fit better to the implementation).


 	Makarius