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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
