[isabelle-dev] Deadlock while building HOL-Proof

[Makarius]

On 10/03/18 11:06, Makarius wrote:
> On 08/03/18 13:08, Makarius wrote:
>>
>>> Since David Matthews has make a lot of changes concerning fine-points of
>>> heap management in the past few months, I would like to test it with
>>> some Poly/ML repository version. But this does not build on macOS at the
>>> moment.
>>
>> I will continue with the investigations here.
> 
> I have now tested it with various experimental versions of Poly/ML: the
> problem persists.
> 
> Looking more closely at the ML statistics of the process (after killing
> it) reveals that the ML world is fine and active, only my future thread
> farm is somehow blocked.
> 
> This indicates that the problem is in my area of responsibility.

In the past couple of weeks I have sporadically tried to work around
this resource problem, but failed so far.

The latest attempt is Isabelle/f6a22490cca8. As usual, it "works for me
on my usual test machines", but there is a remaining chance of problems
coming back on other configurations.


Overall, my guess is that the Poly/ML parallel GC vs. Isabelle/ML future
thread management somehow get into trouble, due to massive resource
requirements in parallel HOL-Proofs with a sudden spike of approx. 50000
futures that require a lot of memory. Even x86_64 does not really help.

In a sense, it is just the normal situation "invisible concrete wall
ahead" -- we've that had occasionally in the past 10-20 years. It is a
reminder that scaling is not for free, but explicit efforts are required
for it.


	Makarius