[isabelle-dev] Max threads & Sledgehammer
makarius at sketis.net
Mon Jan 7 12:24:28 CET 2013
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
> 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://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).
More information about the isabelle-dev