Terminal lease hardening - #286
Merged
Merged
Conversation
Parallel redo builds failed with "Error reclaiming terminal control: ... no such process": each mshell's recorded previous foreground group could be a sibling's transient child group, dead by release time, and the failed restore escalated into failing a command whose child exited 0. - Gate the foreground transaction on tcgetpgrp(tty) == getpgrp(), the standard bash/fish "am I in charge of this terminal" check. A shell that is not the owner skips the handoff entirely. - Fall back to restoring mshell's own process group when the recorded previous group is gone (ESRCH); reclaim problems are now warnings on stderr and never override the child's exit status. - Extend POSIXTerminalControl.tla with the environment the original model omitted: a foreign owner group, a steal window, dead-group hand-back, the gate, and the fallback; add a shared-terminal TLC config. All six bounded checks pass; removing the gate from the model violates the new NonOwnerShellNeverForegrounds invariant. - Add a PTY regression test with six shells sharing one terminal that reproduced the production failure before the fix. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
ERRNO_AUDIT.md traces every errno of every controller syscall to an explicit policy. Fixes from the audit: - Wrap terminal-mode restore (tcsetattr) in SIGTTOU protection; it could stop the shell mid-Release when another group owned the terminal. - Treat ESRCH during acquisition as "job already finished": a fast pipeline reaped concurrently could vanish before tcsetpgrp/SIGCONT, and the failure killed and failed a job whose children exited 0. Also records: Linux TIOCSPGRP's undocumented ESRCH, the non-reentrancy constraint of IgnoreSignalsForJobControl, and open recommendations R1 (closeTerminal failure fails a successful pipeline) and R2 (non-ESRCH acquisition failure kills a healthy child where bash would degrade). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- R1: a failure closing the retained pipeline terminal handle is now a stderr warning, never a failure of a pipeline whose commands succeeded (same bookkeeping-vs-result policy as reclaim). - R3: POSIXTerminalControl.tla gains a reaped state distinct from zombie exited, early process exits, and concurrent reaping. A zombie keeps its pgid (tcsetpgrp succeeds); a fully reaped group is ESRCH, carried as a ~GroupDead kernel-contract guard on GiveTerminal, with GiveTerminalTargetGone modeling the skip-on-ESRCH fix. New invariant UnsupervisedJobNeverOwnsTerminal covers both skip paths and is mutation-verified non-vacuous. All six TLC checks pass (main config 284 -> 720 distinct states). - R2 stays open; trade-off analysis recorded in ERRNO_AUDIT.md. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
No behavior change. mshell has no stopped-job recovery yet, so degrading like bash risks an unrecoverable SIGTTIN hang; the kill also approximates SIGHUP for children in their own process groups. Revisit when the jobs/fg/WUNTRACED milestone lands. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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
1 participant
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.
No description provided.