Re: [isabelle] Stray processes on Windows



On Tue, 26 Nov 2013, Lars Noschinski wrote:

On 26.11.2013 11:50, Makarius wrote:
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.

I recently learned that recent linux kernels (>=3.4) allow setting the
PR_SET_CHILD_SUBREAPER flag on a process. Basically this means that all
(indirect) children of this process will be reparented to it instead of
PID 1, when their parent dies.

Linux has many interesting things that are not generally known nor used.

Linus Torvalds has recently given an interview with two notable points: (1) most people ignore the really good things of the Linux kernel -- for portability reasons, and (2) Linux desktop projects are all really bad, and the continuous forking of projects works against the whole movement towards total world domination.


Anyway, when I say "POSIX", it means the intersection of Mac OS X, Windows + Cygwin, and Linux. In this equation, Linux is more and more getting on the fringe, due to the bad state of major Linux distributions in the past 1-2 years.

Our multiplatform hints and guidelines http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-1/Admin/PLATFORMS refer to Ubuntu 10.04 LTS as the reference platform to build Isabelle components for Linux. This means, before every Isabelle release I need to boot up certain virtual machines to check things or recompile some add-on tools.

Doing it this time, I was just surprised how nice and stable Ubuntu 10.04 was compared to current versions (not just Ubuntu, also other Linux distributions). I still need to get my own machine back into shape, and will probably try Centos next. (At the danger of missing messed-up Debian/Ubuntu packages of basic Unix tools the next time.)


	Makarius




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