[isabelle-dev] Max threads & Sledgehammer

David Matthews dm at prolingua.co.uk
Mon Jan 7 12:31:26 CET 2013


On 07/01/2013 10:11, Stefan Berghofer wrote:
> On 01/07/2013 10:45 AM, Makarius wrote:
>> On Fri, 4 Jan 2013, Stefan Berghofer wrote:
>>
>>> I am currently getting an exception Thread "Thread creation failed"
>>> after some time when compiling HOL with PolyML 5.5.0 on a machine
>>> with quite a few CPUs (I am using Isabelle repository version
>>> 30bcdd5c8e78). I have the impression that Isabelle just tries to
>>> create as many threads as there are CPUs, which exceeds the maximum
>>> number of threads allowed by the operating system for a single process.

> it's a server with 24 CPUs of the type "Intel(R) Xeon(R) CPU E7450 @
> 2.40GHz" and 132299948 kB RAM.
> The operating system is "Linux ts-2 3.2.0-0.bpo.4-amd64 #1 SMP Debian
> 3.2.35-2~bpo60+1 x86_64 GNU/Linux".

>> 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 :-(
>
>> You could try ML_OPTIONS="--gcthreads 8" in one of your settings.
>
> I tried it successfully with "--gcthreads 4", which looks like a
> reasonable value that is also used in
> some of the Admin/isatest/settings files.

Is there a limit on the number of threads per process in Linux?  I 
haven't been able to find anything about it.  You could certainly hit 
limits on memory for stacks with a large number of threads particularly 
if the default stack size is large.  What does "ulimit -s" say?  You 
could try setting that smaller.

By default without the --gcthreads option Poly/ML 5.5 creates one 
garbage collection thread for each processor.  That's probably more than 
are useful if you have 24 processors so -gcthreads 4 or 8 might well be 
a sensible setting.

David




More information about the isabelle-dev mailing list