[isabelle-dev] Max threads & Sledgehammer

[Stefan Berghofer]

Hi Markus,

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.
>
> Can you say more about the hardware and operating system here?  How many CPUs do you have?

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".

> I've seen problems creating threads on the JVM (e.g. see f7ba30a816b9), but not for Poly/ML 5.5.0. Also note that the default (threads=0) is bounded by 8 at the moment.
>
> 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.

Greetings,
Stefan