[isabelle-dev] Deadlock while building HOL-Proof

[Makarius]

On 12/05/18 00:50, Makarius wrote:
> On 10/05/18 00:10, Makarius wrote:
>>
>> 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.
> 
> So far this change looks good on various test machines with only 2 cores.
> 
> In Isabelle/a8f40dd73c61 I have made the parallelism a little bit more
> ambitious, and keep watching resulting performance charts at
> https://isabelle.sketis.net/devel/build_status
> 
> All this are just workarounds to get back into a situation where all
> sessions work routinely most of the time.

The spurious problems with HOL-Proofs have remained open over some
months, despite a lot of tinkering. I have now taken another close look
at it: it appears that the situation with a few % CPU usage is due to
worker threads waiting for futures joined by other threads: some kind of
deadlock/livelock.

The following changes make this more robust, and right now it appears to
work properly:

https://isabelle.sketis.net/repos/isabelle-release/rev/6ee53660a911
https://isabelle.sketis.net/repos/isabelle-release/rev/be936cf061ab


	Makarius