Re: [isabelle] Isabelle2016-RC0 - does not exit on Linux



On Mon, 4 Jan 2016, Lars Hupel wrote:

This sounds like the JVM/AWT shutdown problem, that I've now addressed
in http://isabelle.in.tum.de/repos/isabelle/rev/8bcbf1c93119

For the records, I've also experienced shutdown problems in libisabelle.
The main reason is that the threads created by the thread pool are not
flagged to be daemon, although I don't know whether this is intentional
or not.

The situation is even more entangled.

Quite long ago I started making various threads daemons, in order to increase chances that the JVM terminates, while these threads are still hanging around.

But this later caused the problem introduced in Isabelle/3ad2b2055ffc (05-Oct-2015): the daemon thread was sending something to the AWT thread and waiting for the result; the AWT thread was already terminated, because it only waits for non-daemon threads before shutting itself down; so the wait of the daemon ended up as deadlock.

Today I first tried to make the daemon thread a non-daemon, but got entangled elesewhere, for unknown reasons.

Then I just gave up the ambition to be ultra-smart in the inter-thread ping-pong. So in 8bcbf1c93119 we are back to a situation where a daemon thread sends asynchronously a task on the queue of the AWT thread, without waiting for a result. It means that the whole task stays on the AWT thread, when it actually happens -- causing several milliseconds of potential GUI lock-up.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.