[isabelle-dev] Deadlock while building HOL-Proof

[Makarius]

On 10/05/18 00:10, Makarius wrote:
> 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.

This thread is still open, but there are some new observations in the
background, related to changeset afa7c5a239e6 at its FIXME comment.

I will take at least one deep look at it again before the Isabelle2018
release, potentially also David Matthews.


	Makarius