crux-llvm: amend or document the "group murder" SIGTERM handler

[Ptival]

I've been encountering a recurring issue when building a VSCode extension for crux-llvm where killing the crux-llvm process would bring down my entire IDE.

After being very suspicious of VSCode's behavior and trying many things to debug it, it became more and more clear that only the crux-llvm process was causing such issues. So I looked into the code and found out about:

https://github.com/GaloisInc/crucible/blob/a42ef5b65faea52d3530d53ed7ac800a3a14f1e3/crux-llvm/exe/unix/RealMain.hs#L10-L18

I'm assuming the intent of this is for all the potentially running solver backends as well as the crux-llvm process to die whenever a SIGTERM signal is triggered, by being part of the same process group.

An unintended consequence of this, however, is that the processes that spawned crux-llvm also die, unless they take some precaution so as to not be part of the same process group.

Should we consider:

1. making it so that the crux-llvm process creates its own group, separate from the caller? (something involving setpgrp, setsid, setpgid?)
2. or documenting this behavior if it is wanted, explaining why it is wanted, and some standard ways of putting a harness around it for calling code?

[robdockins]

Indeed, the intent is to ensure that any solver processes are cleaned up as expected. Frankly, this solution feels like a real hack to me, but I'm not sure how to do it better. For your use case, maybe it makes sense to make this behavior configurable somehow, or use a separate top level executable that doesn't install this handler. As to making a new process group, I think you'd have to do that in the spawning process, or do some double-fork trickery, I'm not really sure.

[robdockins]

Looks like we can probably just call createSession (http://hackage.haskell.org/package/unix-2.7.2.2/docs/System-Posix-Process.html#v:createSession), which looks like it boils down into a setsid(). I don't know offhand what effect this would have if invoked as usual from a shell.

EDIT: actually it looks like http://hackage.haskell.org/package/unix-2.7.2.2/docs/System-Posix-Process.html#v:createProcessGroupFor would be better, as it doesn't create a new session.

[Ptival]

As a note, for my use case, Node's child_process allows for a detach option that effectively spawns the process in its own process group, so it is not of utmost importance, but other users of the tool may need to relearn this lesson the hard way! :-)

If the only intended use of the feature is indeed "kill crux-llvm and all its subprocesses", and never "and also all its parent attached processes", I'd be happy proposing a pull request changing the behavior to using createProcessGroupFor.

[robdockins]

Yeah, the intent is only to kill spawned subprocesses, so using createProcessGroupFor is probably the right thing to do regardless.

[kquick]

It's also worth noting that What4 has recently been updated (https://github.com/GaloisInc/what4/pull/128) to have enforced goal timeout handling, and it's much better about managing solver processes and also propagates Ctrl-C to the solvers, so while it might be prudent to have this additional protection, it may be less critical at this point.