Re: [isabelle] Stray processes on Windows

On Sat, 23 Nov 2013, Gottfried Barrow wrote:

I'm not having problems now, but then, I'm not demanding much of the PIDE because I've got done what I wanted. Surely, though, it was related to export_code because the file was so small, and commenting in and out "export_code" was about all I was doing.

A few more remarks, after looking once again over the external process management of Isabelle/Scala and Isabelle/ML.

Process management according to POSIX only allows flat (non-nested) process groups and asynchronous (unacknowledged) signals to kill another process. To give the appearance of managed hierarchies of processes, the Isabelle framework implements certain common-sense heuristics that usually work, but implicitly depend on a reasonable degree of reactivity.

Under heavy load, though, a process that is signalled to terminate, but remains unresponspive for too long, is killed the hard way. Thus it has no chance to terminate its sub-processes properly.

This explains why an abrupt termination of the outermost PIDE application can leave some external processes at the bottom of the hierarchy behind.


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