[isabelle-dev] Max threads & Sledgehammer
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.
More information about the isabelle-dev