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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
