[isabelle-dev] Max threads & Sledgehammer

[David Matthews]

On 07/01/2013 11:24, Makarius wrote:
> 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.

What does Thread.Thread.numProcessors() report?  That's the number that 
will be used for the GC threads.

I'm not inclined to put an arbitrary limit on the number of threads. 
There are certain parts of the GC process such as the sharing detection 
that can use as much parallelism as there is available.  Other parts 
seem to max out at only a few processors.  I'll bear this in mind.  The 
parallel GC is very new and we need some experience of how it works out 
in practice and whether it needs some tuning.

David