Kill orphaned prover processes on Linux when tlapm dies - #284
Open
tangruize wants to merge 1 commit into
Open
Conversation
When tlapm is SIGKILLed or OOM-killed it cannot run its usual cleanup, so the prover it spawned (e.g. z3) is reparented to init and keeps consuming CPU and memory, unmanaged by tlapm, until it happens to terminate on its own. Run each prover via `exec setpriv --pdeathsig KILL` on Linux so the kernel SIGKILLs it when tlapm dies. Injected at the single choke point get_exec, so it covers all single-command backends. Timeout semantics are unchanged; on non-Linux, or when setpriv is missing or too old to support --pdeathsig, the prefix is empty and behaviour is identical. Signed-off-by: Ruize Tang <1466040111@qq.com>
Member
|
This PR is Linux-specific, which is completely reasonable. That said, I’m seeing a similar issue on macOS (when using AI to drive TLAPS). It would be great to address the same problem on macOS and Windows in a future follow-up. |
wkirschenmann
pushed a commit
to wkirschenmann/tlapm
that referenced
this pull request
Aug 21, 2026
… and survey them Two fixes to the upstream section. **tlaplus#286 is ours**, not an external reference, and the plan now says so plainly: same team, opened 2026-07-27, still unanswered, and its four patch families ARE our items 3, 6, 14, 15 and 20 -- already-public proposals re-implemented, not contributions of this branch. What the branch adds on them is what tlaplus#286 could not offer: single-topic reviewable commits with stated invariants and mechanical gates, and attribution per commit instead of per patch set. **Other people's PRs get their own section**, after checking upstream: `master` is at 4600b24, exactly this branch's base, so nothing has landed since the fork and only the open PRs matter. * tlaplus#284 (open, LGTM) kills orphaned provers via `exec setpriv --pdeathsig KILL` when *tlapm dies*. Same family as our item 2, complementary failure mode: ours covers tlapm alive but its kill ignored (SIGHUP set to SIG_IGN by nohup, inherited through exec). Neither subsumes the other, and tlaplus#284 supplies the SIGKILL escalation our fix lacks -- reference it, do not duplicate it. * tlaplus#285 (open) modifies `let_normalize`/`except_normalize`, the two functions item 15 calls per hypothesis. Textual conflict certain; the per-hypothesis equivalence argument must be re-established with the oracle afterwards. Kept in the survey for that reason only. * tlaplus#275 (open) makes SANY an opt-in parser, so item 7 keeps its value -- but the editor floor is now 95 % parse, and SANY does semantic analysis inside "parsing", which item 19 does not assume. * tlaplus#268 (open, extends the merged tlaplus#241) is the feature items 18-19 currently break: the decomposition code actions locate steps by range, and scoped re-elaboration leaves inner positions stale. This is why those modes stay flag-gated. * tlaplus#283 (merged) gives a deterministic Z3 budget -- worth adopting in measurement protocol P2 to remove prover-side variance. * tlaplus#266 (open) changes an SMT axiom, so item 3's subset gate must be re-run against it; tlaplus#248 (open) upgrades Z3 and invalidates absolutes. * tlaplus#264 closed without adopting an LLM policy -- escalated to the TLA+ Foundation board. The stated maintainer position (human first contact, per-commit disclosure of models used) is the one to assume, and the 441-lines-for-most-of-the-gain framing is what answers the review-workload concern behind it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CUUoeEmuL3jsYhUb3UrhJH
wkirschenmann
pushed a commit
to wkirschenmann/tlapm
that referenced
this pull request
Aug 21, 2026
Bugfixes were sitting in the ranked list because two of them have a positive performance effect. That mixes two decisions of different natures: an optimization is a trade -- review effort and risk against a measured gain, declinable on either side -- while a bugfix repairs behaviour the program already advertises, and declining it means keeping the defect. Ranking them together invites the wrong conversation. The three are now item #0, out of the table: the broken `--timing` accounting (B1), the spurious prover timeouts (B2, already in tlaplus#286), and the prover left alive when the hangup signal is ignored (B3). Grouped effect stated once -- 5 commits, 8 files, +138/-35 -- with a verification recipe each, and B3's large measured effect explicitly framed as an argument for urgency rather than the reason to take the change. The optimizations renumber 1-18 accordingly, and every cross-reference follows: the three per-item tables, the dependency orderings (tlaplus#2's two commits, tlaplus#10 requires tlaplus#13, tlaplus#13's three commits, tlaplus#17 requires tlaplus#4, and tlaplus#2 must not ship without tlaplus#13), the batching, the guard list, the tlaplus#286 family mapping, the local-proof table and its "weak signal" list, and the tlaplus#284 comparison. The headline recomputes to 429 added lines (-130) across seven files for items 1-8, since the SIGTERM fix is no longer counted among them. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CUUoeEmuL3jsYhUb3UrhJH
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Problem
tlapm launches every backend prover (z3, cvc4, zenon, …) as a child process and terminates it as part of its own cleanup. If tlapm dies without getting to run that cleanup — an uncatchable
SIGKILL, or an OOM-kill under memory pressure — the prover it spawned is reparented toinitand keeps running. Most solvers impose no limit on themselves, so the orphan goes on consuming CPU and memory until it happens to finish on its own.Fix
On Linux, run each prover through util-linux
setpriv --pdeathsig KILL, which arms the kernel parent-death signal (PR_SET_PDEATHSIG): the kernel sendsSIGKILLto the prover the moment its parent (tlapm) dies, including theSIGKILLand OOM cases where tlapm can no longer act itself.The leading
execmakes the prover replace the shell that launches it, so the prover becomes tlapm's direct child — the process the parent-death signal actually watches — instead of a grandchild under an intermediate/bin/sh. Without it that shell would stay alive and keep the prover running.The prefix is added at the single point where every backend command string is assembled, so all provers are covered at once. On non-Linux, or on Linux where
setprivis missing or too old to support--pdeathsig, the prefix is empty and behaviour is unchanged.