diff --git a/.gitignore b/.gitignore index 1d3ad906..620df4b6 100644 --- a/.gitignore +++ b/.gitignore @@ -41,6 +41,9 @@ cover.html cover.out cover_funcs.txt +# TLA+ model checker artifacts +**/states/ + # REDOGI doc/all doc/build/**/*.html diff --git a/CHANGELOG.md b/CHANGELOG.md index 7287a831..a9c1de12 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -266,6 +266,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Fixed +- Attempted to formally improve the semantics of job control and terminal control on both Linux and Windows. + Should fix potential bugs when running TUI programs from within mshell scripts. - On Windows, a command name containing a forward slash (e.g. `./script.msh`) is now treated as a file reference instead of being searched for on `PATH`, matching the behavior on Linux/macOS. Previously only backslashes were diff --git a/ai/terminal-control/ASSUMPTIONS.md b/ai/terminal-control/ASSUMPTIONS.md new file mode 100644 index 00000000..914c3fee --- /dev/null +++ b/ai/terminal-control/ASSUMPTIONS.md @@ -0,0 +1,82 @@ +# Trusted platform contracts + +Checked against primary documentation on 2026-08-09. These are assumptions at +the formal model boundary and must be revisited when supported Go or operating +system versions change. + +## POSIX Issue 8 + +- A controlling terminal records one foreground process-group ID. Terminal + access by background process groups is governed by the terminal driver and can + stop readers with `SIGTTIN` (and writers with `SIGTTOU` when `TOSTOP` applies). +- `tcsetpgrp()` requires a terminal associated with the caller's session and a + process group in that session. It can fail, including when the caller is a + background group and does not appropriately block or ignore `SIGTTOU`. +- Each job is placed in its own process group. The POSIX rationale recommends + calling `setpgid()` in both child and parent to close the fork/exec race. +- A shell foregrounds a job with `tcsetpgrp()`, observes stopped children with + `waitpid(..., WUNTRACED)`, reclaims the terminal, and foregrounds a stopped job + before sending `SIGCONT`. + +Sources: + +- https://pubs.opengroup.org/onlinepubs/9799919799/utilities/V3_chap02.html#tag_19_11 +- https://pubs.opengroup.org/onlinepubs/9699919799/functions/tcsetpgrp.html +- https://pubs.opengroup.org/onlinepubs/009604599/xrat/xbd_chap03.html +- https://pubs.opengroup.org/onlinepubs/9799919799/basedefs/V1_chap03.html + +## Windows console + +- Any number of processes can share one console and its queued input buffer. + Windows has no POSIX-equivalent kernel foreground process group that gates + reads. Therefore mshell must make its own reader quiescent before allowing a + foreground child to read the shared queue. +- `CREATE_NEW_PROCESS_GROUP` creates a control-event group, not an input-owner + group. It disables Ctrl+C in the new group. `CTRL_BREAK_EVENT` can target the + group; `CTRL_C_EVENT` cannot be limited to a nonzero group. +- the SetConsoleCtrlHandler Ctrl+C-ignore attribute is inherited. Handler tables + are reset by `AttachConsole`, `AllocConsole`, and `FreeConsole`. +- Console modes belong to console buffers, so processes sharing a buffer observe + changes to that shared state. Mode changes need owner-scoped save/restore. +- A ConPTY uses synchronous input and output channels. Microsoft recommends a + separate servicing thread for each direction to avoid deadlock. The host must + close its copies of handles given to the pseudoconsole after child creation so + broken-channel/EOF detection works. Teardown output must continue to be + drained while closing the pseudoconsole. +- Windows handle inheritance requires both an inheritable handle and inheritance + at `CreateProcess`; `PROC_THREAD_ATTRIBUTE_HANDLE_LIST` restricts the exact + inherited set. Inherited handles refer to the same underlying objects. + +Sources: + +- https://learn.microsoft.com/en-us/windows/console/consoles +- https://learn.microsoft.com/en-us/windows/console/console-input-buffer +- https://learn.microsoft.com/en-us/windows/win32/procthread/process-creation-flags +- https://learn.microsoft.com/en-us/windows/console/generateconsolectrlevent +- https://learn.microsoft.com/en-us/windows/console/setconsolectrlhandler +- https://learn.microsoft.com/en-us/windows/console/creating-a-pseudoconsole-session +- https://learn.microsoft.com/en-us/windows/win32/procthread/inheritance + +## Go process creation + +The current development toolchain reports Go 1.26.5. Its local source is the +authoritative implementation reference for this checkout. + +- `exec.Cmd` copies non-`*os.File` stdin/stdout/stderr through goroutines; `Wait` + also waits for those copy goroutines under the documented rules. +- On Unix, `syscall.SysProcAttr` exposes `Setpgid`, `Pgid`, and `Foreground`. + `Foreground` performs foreground placement in the child-side creation path and + requires a parent controlling-terminal descriptor in `Ctty`. +- On Windows, `syscall.SysProcAttr` exposes `CreationFlags`, + `AdditionalInheritedHandles`, and `NoInheritHandles`; Go uses an extended + startup-info handle list for the selected inherited handles. +- `os.Process.Signal(os.Interrupt)` is not implemented on Windows. Windows + control events require platform-specific code and the limitations above. + +Sources: + +- https://pkg.go.dev/os/exec +- https://pkg.go.dev/syscall#SysProcAttr +- `/usr/lib/go/src/os/exec/exec.go` +- `/usr/lib/go/src/syscall/exec_linux.go` +- `/usr/lib/go/src/syscall/exec_windows.go` diff --git a/ai/terminal-control/IMPLEMENTATION.md b/ai/terminal-control/IMPLEMENTATION.md new file mode 100644 index 00000000..69f69d0b --- /dev/null +++ b/ai/terminal-control/IMPLEMENTATION.md @@ -0,0 +1,159 @@ +# Implementation blueprint + +## Current failure + +The current execution path resolves a child `cmd.Stdin`, but foreground control +later tests and operates on `os.Stdin`. This fails when mshell is reading a pipe +and a child receives an explicitly opened terminal, as in `brename`: + +1. the editor receives a terminal handle as its effective stdin; +2. mshell sees that its own inherited stdin is not a terminal and skips the + foreground transfer; +3. the editor emits a terminal query (the observed OSC color sequence is an + example) and exits or fails to consume the response correctly; +4. the response remains in the terminal input queue; and +5. mshell resumes its interactive parser and treats response bytes such as `;r` + as user input, invoking the file-manager binding. + +The escape parser is not the correct primary fix. While an editor owns the +terminal, mshell must not read or interpret its input. Parser hardening remains +defense in depth for input received while mshell genuinely owns the terminal. + +The current code also discards errors from foreground transfer and restoration. +That makes recovery unverifiable: the in-memory control flow can claim a handoff +that the kernel rejected. + +## Proposed architecture + +Introduce one serialized `JobController`; do not spread process creation, +terminal modes, input reading, waiting, and recovery across `RunProcess`, +`RunPipeline`, the prompt, and platform helpers. + +```text +resolved command and endpoints + | + v + JobController + / | \ + reader gate process launcher terminal backend + | | / \ + prompt lexer process/job table POSIX Windows +``` + +Core types should make the proof state visible: + +- `ResolvedEndpoint`: stream direction, concrete reader/writer, optional terminal + identity, ownership/lifetime, and child inheritance information. +- `ResolvedStdio`: three endpoints plus aliases used by stream merging. +- `Job`: stable ID, process records, pipeline topology, state, placement, + platform group/isolation identity, saved terminal mode, and completion state. +- `ControlTransaction`: the one job currently acquiring or releasing terminal + control. TLC found that this serialization cannot safely be implicit. +- `InputGate`: starts, quiesces, and resumes the shell input reader and confirms + quiescence before a job is activated. +- `TerminalBackend`: transactional acquire/reclaim/save/restore operations with + typed errors. A failed acquire must run an explicit rollback. + +Every transition should return an error that identifies both the failed action +and the recovery result. No terminal-control error should be discarded. + +## Endpoint resolution + +Resolve all three child streams before process creation. Terminal control is +based on the resolved controlling-terminal identity, not on file-descriptor +number 0 and not just on `os.Stdin`. + +For the original case, an `*os.File` opened from `/dev/tty` is both the child's +stdin endpoint and a candidate controlling-terminal descriptor for +`tcgetpgrp`/`tcsetpgrp`. If the child has terminal output but redirected input, +the job can still require foreground control for signals and output policy, so +the decision is a job property rather than a single `stdinIsTerminal` test. + +Abstract `io.Reader`/`io.Writer` values without a descriptor are never guessed to +be terminals. Wrappers that intentionally preserve terminal identity should +implement a private endpoint interface instead of relying on incidental Go type +assertions throughout the evaluator. + +## POSIX backend + +1. Establish whether mshell has a controlling terminal independently from its + standard streams. Interactive job control also requires mshell to be in its + own process group and in the terminal foreground before reading a prompt. +2. Quiesce the shell reader and restore the shell's cooked baseline. +3. Create one process group per job. Use child-side `Setpgid` before exec and a + parent-side `setpgid`/verification where useful to close the documented race. +4. Launch all pipeline members into that group. Track start failure per member; + do not destroy the group when its leader exits early. +5. Save shell modes, call `tcsetpgrp` with a descriptor for the controlling + terminal, check the result, restore the job's saved modes when continuing, and + send `SIGCONT` only after foregrounding a stopped job. +6. Wait with stopped/continued status enabled and aggregate process state into + job state. +7. On stop, exit, or error: save the job's modes if applicable, reclaim the + foreground group, restore shell modes, then resume the shell reader. + +Signal disposition must follow shell rules: the shell protects itself while it +manipulates the terminal, children receive default job-control dispositions, and +the protection is scoped and restored. + +## Windows backends + +Windows needs two explicit profiles because documented APIs cannot make a shared +console enforce exclusive input access for background jobs. + +### Direct attached-console compatibility profile + +- Quiesce the shell reader before process creation/activation and do not resume + it until the child has stopped or exited. +- Save and restore console input/output modes because they are shared buffer + state. +- Treat `CREATE_NEW_PROCESS_GROUP` only as a control-event routing mechanism. + It is not terminal ownership, and it disables Ctrl+C for the created group. +- Document Ctrl+C versus Ctrl+Break behavior exactly; targeted Ctrl+C via + `GenerateConsoleCtrlEvent` is not available. +- Do not claim enforceable background-input isolation. A background process + retaining the shared console input handle can consume the queue. + +This profile can correctly fix the foreground editor handoff, but it is not the +foundation for full Windows job control. + +### Isolated ConPTY job-control profile + +- Give every terminal-using job its own ConPTY. The child reads only its ConPTY + input; mshell is the sole reader of the real console and forwards input only to + the foreground job. +- Service ConPTY input and output on independent workers with bounded queues and + cancellation. Continue draining output through teardown as Microsoft + requires. +- Restrict inherited handles with the extended startup handle list. Close host + copies of child-only channel ends immediately after creation on success and on + every rollback path. +- Combine the ConPTY with a Windows Job Object for process-tree accounting and + cleanup. A Job Object is not the same concept as a shell job, so wrap it behind + the platform backend. +- Define stop/continue semantics explicitly. Windows exposes no documented + equivalent of POSIX `SIGTSTP`/`SIGCONT` for arbitrary console trees; the first + implementation may need to report stop/continue as unsupported rather than use + undocumented process-suspension APIs and falsely promise correctness. + +ConPTY changes presentation: mshell becomes a terminal relay and must forward +virtual-terminal bytes transparently. It should recognize only the terminal +queries that mshell itself must answer as host; it must not reinterpret child +output as shell input. + +## Testing strategy + +- Unit-test every controller transition and injected backend failure. +- Generate transition traces from the TLA+ state graph and replay them against a + fake backend. +- On POSIX, use a fresh session and pseudo-terminal for integration tests. Cover + piped shell stdin plus `/dev/tty`, early pipeline-leader exit, stop/continue, + nested shells, terminal loss, and failed `tcsetpgrp`/mode restoration. +- On Windows, test both classic Console Host and Windows Terminal, redirected + handles, Ctrl+C/Ctrl+Break, ConPTY resize, EOF, child-created descendants, and + teardown with a full output buffer. +- Every interactive test must have a deadline and retain process/job handles so a + hung tree can be terminated and diagnosed. Never rely only on killing the + immediate child. +- Add a byte-stream corpus for parser defense in depth, but keep it separate from + ownership tests. Escape-sequence coverage cannot prove terminal handoff. diff --git a/ai/terminal-control/IMPLEMENTATION_STATUS.md b/ai/terminal-control/IMPLEMENTATION_STATUS.md new file mode 100644 index 00000000..36a703fe --- /dev/null +++ b/ai/terminal-control/IMPLEMENTATION_STATUS.md @@ -0,0 +1,70 @@ +# Implementation status + +Last updated: 2026-08-09. + +## Implemented + +- Resolved stdin/stdout/stderr metadata remains attached to the `exec.Cmd` + streams after redirects and merges are applied. +- Terminal selection distinguishes an arbitrary TTY from the session's + controlling terminal and prefers resolved stdin, then stdout and stderr. +- One serialized foreground transaction spans acquisition, `SIGCONT`, wait, and + reclamation, corresponding to the model's `controlJob` reservation. +- Terminal/console modes are captured before transfer and restored only after + ownership is reclaimed. Shell input remains blocked if either restoration + step fails. +- The shell input gate rejects a foreground acquisition while an input read is + outstanding and rejects shell reads while a foreground job owns input. +- POSIX single commands and pipelines use the resolved controlling-terminal + descriptor rather than `os.Stdin`. +- A process group that may have stopped on `SIGTTIN` between `Start` and + `tcsetpgrp` receives `SIGCONT` only after it is foreground. +- Pipeline stages retain a duplicated terminal handle through reclamation. The + full test suite exposed the original borrowed-handle version closing too early; + the retained-handle implementation fixes that counterexample. +- Acquisition failure kills and reaps the immediate child or pipeline processes + instead of waiting forever on a stopped terminal reader. +- Windows direct-console control-handler installation errors are reported, and + the same serialized input gate prevents mshell from competing with a + foreground child for the shared console queue. +- Windows and POSIX restore the exact previous foreground marker/process group + recorded during acquisition. +- Foreground Windows commands inherit their resolved console and standard + handles directly. The surrounding console host remains responsible for + keyboard input, output, escape sequences, Unicode, and resize events while + mshell stops reading and waits. +- A nested foreground ConPTY was implemented and then removed because it made + mshell an unnecessary terminal proxy. ConPTY remains a possible future + isolation mechanism for interactive background jobs, not the foreground + handoff mechanism. + +## Verification currently passing + +- Controller unit tests inject mode capture, acquisition, continue, rollback, + ownership restoration, and mode restoration failures and check operation order + and input-gate state. +- A deadline-protected PTY test runs msh logic with piped shell stdin while the + child reads `/dev/tty`. It kills the entire test session on timeout. +- A second PTY test covers an interactive pipeline stage and terminal-handle + lifetime through pipeline completion. +- Linux package tests pass. +- Windows amd64 and macOS amd64 test binaries cross-compile. +- All five bounded TLC configurations pass after the implementation changes. + `StreamLifecycle` was strengthened with the retained-terminal-handle invariant + discovered during implementation. + +## Not yet implemented + +- Durable job objects and user-facing `jobs`, `fg`, and `bg` operations. +- Stopped/continued process aggregation and terminal-mode snapshots per stopped + job. +- Asynchronous reaping for background jobs. +- Per-job Windows ConPTY isolation, relay workers, resizing, and Job Object + cleanup. These are future background-job facilities; foreground jobs should + continue to use direct console inheritance. +- Mechanical trace replay or refinement checking between Go and TLA+. +- Conditional liveness checks and unbounded TLAPS proofs. + +These remaining items are the future full-job-control program. The current +milestone fixes synchronous foreground handoff without pretending that the full +program is complete. diff --git a/ai/terminal-control/MODEL_RESULTS.md b/ai/terminal-control/MODEL_RESULTS.md new file mode 100644 index 00000000..45adf15a --- /dev/null +++ b/ai/terminal-control/MODEL_RESULTS.md @@ -0,0 +1,59 @@ +# TLC results + +Tool: TLA+ tools 1.7.4, TLC 2.19 (`5a47802`), Java 17. + +Last complete run: 2026-08-09. + +| Model | Configured size | Distinct states | Result | +| --- | ---: | ---: | --- | +| `TerminalControl` | 2 jobs | 204 | all configured invariants hold | +| `POSIXTerminalControl` | 2 processes; shell stdin non-TTY, child stdin TTY | 58 | all configured invariants hold | +| `POSIXTerminalControl` | 2 processes; child stdin non-TTY | 2 | all configured invariants hold | +| `WindowsTerminalControl` | one foreground job | 11 | all configured invariants hold | +| `StreamLifecycle` | 2 processes, 5 stream handles, retained terminal | 36 | all configured invariants hold | + +`check.sh` uses `-deadlock` because terminal `done` and explicitly failed states +are expected to have no enabled action. Invariant checking still explores their +complete reachable state graph. + +## Counterexample found during modeling + +The first `TerminalControl` version did not serialize acquisition transactions. +TLC found this trace: + +1. job 1 begins a foreground launch; +2. job 2 begins in the background and requests `fg`; +3. job 2 pauses the shell; +4. job 1 fails and enters recovery; +5. job 2 acquires the terminal, stops, reclaims it, and resumes the shell; and +6. job 1 remains forever in a recovery state that can no longer satisfy its + preconditions. + +The model now has a single `controlJob` reservation spanning resolution through +recovery. This is a design requirement for the future Go controller, not merely +a modeling convenience. + +## Boundaries and unfinished proof work + +- These are exhaustive finite-state safety checks, not unbounded TLAPS proofs. +- The current platform modules are contract models, not yet mechanically checked + refinement mappings to `TerminalControl`. +- Progress requirements are documented but not checked yet. Fairness must be + stated carefully because children are allowed to run forever or retain handles. +- The Windows model covers reader quiescence in a shared console. A separate, + larger ConPTY relay model is required before claiming full Windows isolation. +- Terminal resize, nested shells, signal masks, per-process stopped/continued + aggregation, mode-snapshot failure, and shutdown policy need additional state. +- The Go controller and failure-injection tests mirror the principal ownership + transitions, but no refinement checker has mechanically proved that every Go + execution implements the TLA+ specification. Generated trace replay remains + a next conformance step. + +The stream model now also requires a duplicated controlling-terminal handle to +remain live from endpoint resolution through job completion and to be closed in +terminal states. This invariant was added after the Go integration tests found +that retaining only a borrowed pipeline descriptor allowed a stage to close it +before terminal reclamation. + +Accordingly, the present result should be described as a checked formal design +foundation, not as “mshell terminal handling is formally verified.” diff --git a/ai/terminal-control/POSIXNonTerminal.cfg b/ai/terminal-control/POSIXNonTerminal.cfg new file mode 100644 index 00000000..0cab321f --- /dev/null +++ b/ai/terminal-control/POSIXNonTerminal.cfg @@ -0,0 +1,17 @@ +CONSTANTS + Procs = {p1, p2} + ShellPgrp = shellPgrp + JobPgrp = jobPgrp + ShellStdinIsTTY = TRUE + ChildStdinIsTTY = FALSE + +INIT Init +NEXT Next + +INVARIANTS + TypeOK + ShellReaderHasForeground + JobForegroundPausesShell + RunningProcessesAreGroupedBeforeForeground + PromptModeIsRestored + ResolvedChildEndpointControlsHandoff diff --git a/ai/terminal-control/POSIXTerminalControl.cfg b/ai/terminal-control/POSIXTerminalControl.cfg new file mode 100644 index 00000000..7bdbd0c1 --- /dev/null +++ b/ai/terminal-control/POSIXTerminalControl.cfg @@ -0,0 +1,17 @@ +CONSTANTS + Procs = {p1, p2} + ShellPgrp = shellPgrp + JobPgrp = jobPgrp + ShellStdinIsTTY = FALSE + ChildStdinIsTTY = TRUE + +INIT Init +NEXT Next + +INVARIANTS + TypeOK + ShellReaderHasForeground + JobForegroundPausesShell + RunningProcessesAreGroupedBeforeForeground + PromptModeIsRestored + ResolvedChildEndpointControlsHandoff diff --git a/ai/terminal-control/POSIXTerminalControl.tla b/ai/terminal-control/POSIXTerminalControl.tla new file mode 100644 index 00000000..bd761ab5 --- /dev/null +++ b/ai/terminal-control/POSIXTerminalControl.tla @@ -0,0 +1,170 @@ +----------------------- MODULE POSIXTerminalControl ----------------------- +EXTENDS FiniteSets, TLC + +CONSTANTS Procs, ShellPgrp, JobPgrp, ShellStdinIsTTY, ChildStdinIsTTY + +ASSUME /\ Procs # {} + /\ ShellPgrp # JobPgrp + /\ ShellStdinIsTTY \in BOOLEAN + /\ ChildStdinIsTTY \in BOOLEAN + +VARIABLES phase, shellReader, ttyForeground, procState, grouped, + terminalMode, failure + +vars == <> + +ProcStates == {"idle", "running", "stopped", "exited", "startFailed"} + +Init == + /\ phase = "idle" + /\ shellReader = "active" + /\ ttyForeground = ShellPgrp + /\ procState = [p \in Procs |-> "idle"] + /\ grouped = [p \in Procs |-> FALSE] + /\ terminalMode = "shellRaw" + /\ failure = "none" + +ResolveTerminalEndpoint == + /\ phase = "idle" + /\ ChildStdinIsTTY + /\ phase' = "resolved" + /\ UNCHANGED <> + +ResolveNonTerminalEndpoint == + /\ phase = "idle" + /\ ~ChildStdinIsTTY + /\ phase' = "done" + /\ UNCHANGED <> + +PauseShell == + /\ phase = "resolved" + /\ shellReader = "active" + /\ shellReader' = "paused" + /\ terminalMode' = "shellCooked" + /\ phase' = "launching" + /\ UNCHANGED <> + +StartProc(p) == + /\ phase = "launching" + /\ procState[p] = "idle" + \* Go's child-side Setpgid contract makes membership effective before exec. + /\ procState' = [procState EXCEPT ![p] = "running"] + /\ grouped' = [grouped EXCEPT ![p] = TRUE] + /\ UNCHANGED <> + +StartProcFails(p) == + /\ phase = "launching" + /\ procState[p] = "idle" + /\ procState' = [procState EXCEPT ![p] = "startFailed"] + /\ grouped' = [grouped EXCEPT ![p] = FALSE] + /\ UNCHANGED <> + +LaunchComplete == + /\ phase = "launching" + /\ \A p \in Procs: procState[p] # "idle" + /\ \E p \in Procs: procState[p] = "running" + /\ phase' = "groupReady" + /\ UNCHANGED <> + +AllStartFailed == + /\ phase = "launching" + /\ \A p \in Procs: procState[p] = "startFailed" + /\ phase' = "reclaiming" + /\ failure' = "start" + /\ UNCHANGED <> + +GiveTerminal == + /\ phase = "groupReady" + /\ shellReader = "paused" + /\ ttyForeground = ShellPgrp + /\ \A p \in Procs: procState[p] = "running" => grouped[p] + /\ ttyForeground' = JobPgrp + /\ terminalMode' = "jobMode" + /\ phase' = "foreground" + /\ UNCHANGED <> + +TcsetpgrpFails == + /\ phase = "groupReady" + /\ phase' = "reclaiming" + /\ failure' = "tcsetpgrp" + /\ UNCHANGED <> + +ProcExits(p) == + /\ phase = "foreground" + /\ procState[p] = "running" + /\ procState' = [procState EXCEPT ![p] = "exited"] + /\ UNCHANGED <> + +JobStops == + /\ phase = "foreground" + /\ \E p \in Procs: procState[p] = "running" + /\ procState' = [p \in Procs |-> + IF procState[p] = "running" THEN "stopped" ELSE procState[p]] + /\ phase' = "reclaiming" + /\ UNCHANGED <> + +JobExited == + /\ phase = "foreground" + /\ \A p \in Procs: procState[p] \in {"exited", "startFailed"} + /\ phase' = "reclaiming" + /\ UNCHANGED <> + +ReclaimTerminal == + /\ phase = "reclaiming" + /\ shellReader = "paused" + /\ ttyForeground \in {ShellPgrp, JobPgrp} + /\ ttyForeground' = ShellPgrp + /\ terminalMode' = "shellCooked" + /\ phase' = "resuming" + /\ UNCHANGED <> + +ResumeShell == + /\ phase = "resuming" + /\ ttyForeground = ShellPgrp + /\ shellReader' = "active" + /\ terminalMode' = "shellRaw" + /\ phase' = "done" + /\ UNCHANGED <> + +Next == + ResolveTerminalEndpoint \/ ResolveNonTerminalEndpoint \/ PauseShell \/ + (\E p \in Procs: StartProc(p) \/ StartProcFails(p) \/ ProcExits(p)) \/ + LaunchComplete \/ AllStartFailed \/ GiveTerminal \/ TcsetpgrpFails \/ + JobStops \/ JobExited \/ ReclaimTerminal \/ ResumeShell + +Spec == Init /\ [][Next]_vars + +TypeOK == + /\ phase \in {"idle", "resolved", "launching", "groupReady", + "foreground", "reclaiming", "resuming", "done"} + /\ shellReader \in {"active", "paused"} + /\ ttyForeground \in {ShellPgrp, JobPgrp} + /\ procState \in [Procs -> ProcStates] + /\ grouped \in [Procs -> BOOLEAN] + /\ terminalMode \in {"shellRaw", "shellCooked", "jobMode"} + /\ failure \in {"none", "start", "tcsetpgrp"} + +ShellReaderHasForeground == + shellReader = "active" => ttyForeground = ShellPgrp + +JobForegroundPausesShell == + ttyForeground = JobPgrp => shellReader = "paused" + +RunningProcessesAreGroupedBeforeForeground == + ttyForeground = JobPgrp => + \A p \in Procs: procState[p] = "running" => grouped[p] + +PromptModeIsRestored == + shellReader = "active" => terminalMode = "shellRaw" + +ResolvedChildEndpointControlsHandoff == + ~ChildStdinIsTTY => phase \notin {"resolved", "launching", "groupReady", + "foreground", "reclaiming", "resuming"} + +============================================================================= diff --git a/ai/terminal-control/README.md b/ai/terminal-control/README.md new file mode 100644 index 00000000..c4fdc1d7 --- /dev/null +++ b/ai/terminal-control/README.md @@ -0,0 +1,63 @@ +# Terminal control formalization + +This directory is the persistent design and formal-model workspace for mshell's +standard-I/O, terminal-control, and job-control implementation. + +## Long-term scope + +The target is **full job control**, even though mshell does not expose all of it +today. Every design choice and implementation step must preserve a path to: + +- foreground and background jobs; +- multi-process pipelines treated as one job; +- stop, continue, `fg`, and `bg` transitions; +- terminal-mode save and restore for both the shell and stopped jobs; +- correct signal or console-control-event routing; +- asynchronous reaping and durable job status; and +- interactive programs whose terminal endpoint differs from mshell's inherited + standard input, including an explicit `/dev/tty`-style input while mshell is + reading a pipe. + +This requirement is intentional and must not be narrowed to the current +`brename`/editor failure when this work is resumed. + +## What is proved + +The TLA+ models describe the control protocol, not the implementations of the +operating-system calls. TLC exhaustively checks the configured finite models. +A successful TLC run means that the stated invariants hold for every modeled +interleaving and failure in that finite state space, subject to the contracts in +[ASSUMPTIONS.md](ASSUMPTIONS.md). It is not a proof that an arbitrary Go +implementation conforms to the model, nor a proof of the operating systems. + +The model suite is deliberately split: + +- `TerminalControl.tla` models platform-neutral job and terminal ownership. +- `POSIXTerminalControl.tla` models process groups and the controlling terminal. +- `WindowsTerminalControl.tla` models the shared console input queue and Ctrl + event limitations. +- `StreamLifecycle.tla` models standard-handle resolution, inheritance, closure, + and EOF. This is kept separate to control state-space growth. + +Run every bounded check with `./check.sh`. Set `TLA2TOOLS_JAR` to use a jar in a +different location. + +Production conformance progress is tracked in +[IMPLEMENTATION_STATUS.md](IMPLEMENTATION_STATUS.md). +The chosen Windows foreground architecture and the rejected nested-ConPTY +alternative are recorded in +[WINDOWS_DIRECT_HANDOFF.md](WINDOWS_DIRECT_HANDOFF.md). + +## Proof roadmap + +1. Keep the TLC models executable alongside implementation work and add every + discovered race as a modeled transition. +2. Introduce a single Go terminal/job controller whose states and operations map + directly to the abstract actions. +3. Add model-based and pseudo-terminal integration tests, including injected + failures and deadlines that kill hung process trees. +4. Write refinement mappings from the POSIX and Windows models to the abstract + model. +5. Use TLAPS for unbounded invariant proofs after the state machines stabilize. +6. Consider Gobra contracts for the critical Go controller. System calls remain + trusted contracts, so this supplements rather than replaces the TLA+ work. diff --git a/ai/terminal-control/REQUIREMENTS.md b/ai/terminal-control/REQUIREMENTS.md new file mode 100644 index 00000000..f3bdaab5 --- /dev/null +++ b/ai/terminal-control/REQUIREMENTS.md @@ -0,0 +1,69 @@ +# Requirements and invariants + +## Vocabulary + +A **job** is one command or one pipeline and is the unit of foreground, +background, stop, continue, signal, wait, and terminal ownership state. + +An **endpoint** is the fully resolved source or destination of a standard stream: +terminal, pipe, file, capture buffer, inherited abstract reader/writer, or null. +Terminal-control decisions use resolved endpoints and the controlling-terminal +handle; they must never be inferred solely from `os.Stdin`. + +Terminal **ownership** is permission to consume terminal input. It is distinct +from having an inherited handle, being a Windows console process group, and being +the target of a control event. + +## Safety requirements + +1. At most one job, or the shell, may be authorized to consume terminal input. +2. The shell input reader is quiescent before a foreground job can consume input. +3. The shell cannot display an interactive prompt unless it owns the terminal, + has no foreground job, and has restored its input mode. +4. A background job never owns terminal input. +5. All processes in a POSIX pipeline belong to the job's process group before the + group is relied on for terminal access or signaling. +6. Every foreground transition is transactional: failure either leaves the shell + in its prior usable state or enters an explicit recovery state. Errors from + ownership, mode, process-group, wait, or restoration operations are not lost. +7. The shell reclaims the terminal after a foreground job exits, stops, or fails + to launch, before resuming its reader. +8. Terminal modes are saved and restored by owner. A stopped foreground job's + modes are retained for a later `fg`; the shell's modes are restored for the + prompt. +9. Standard handles are resolved before process creation. Only intended handles + are inherited, and every parent copy of a child-only pipe end is closed on all + success and failure paths so EOF remains observable. +10. Output bytes and terminal responses produced while a child owns the terminal + are not interpreted as shell keystrokes. The terminal emulator, not mshell's + input lexer, interprets child output escape sequences. +11. Stop, continue, exit, and signal state is tracked at job and process level; + partial pipeline completion does not destroy the job prematurely. +12. Shutdown and cancellation terminate or detach jobs according to an explicit + policy and do not leak goroutines, handles, processes, or terminal modes. + +## Progress requirements + +Under explicit fairness assumptions that the operating system eventually +returns from non-hung calls and that a child eventually stops or exits after the +required external event: + +- every foreground job eventually stops, exits, or is reported as unrecoverable; +- every completed process is eventually reaped; +- every terminal-recovery state eventually returns ownership to the shell or + reports a terminal-loss condition; and +- pipe readers eventually observe data or EOF after all writers close. + +Progress properties are conditional. An arbitrary child can intentionally run +forever, ignore events, or retain a pipe handle; the shell cannot prove otherwise. + +## Required support profiles + +- POSIX interactive shell with a controlling terminal. +- POSIX non-interactive execution with no controlling terminal. +- POSIX piped mshell stdin plus a child endpoint opened from the controlling + terminal (the original editor case). +- Windows classic attached console, whose input buffer is shared by processes. +- Windows redirected standard handles while a console remains attached. +- Windows ConPTY hosting, with independently serviced synchronous channels. +- Nested shells and shells started outside the foreground process group. diff --git a/ai/terminal-control/StreamLifecycle.cfg b/ai/terminal-control/StreamLifecycle.cfg new file mode 100644 index 00000000..cd77fb56 --- /dev/null +++ b/ai/terminal-control/StreamLifecycle.cfg @@ -0,0 +1,16 @@ +CONSTANTS + Procs = {p1, p2} + Handles = {stdinHandle, stdoutHandle, stderrHandle, pipeRead, pipeWrite} + TerminalUsed = TRUE + +INIT Init +NEXT Next + +INVARIANTS + TypeOK + ExactInheritance + NoSpawnBeforeResolution + EOFIsSound + TerminalStatesLeakNoHandles + TerminalHandleLifetime + TerminalHandleReleasedAtEnd diff --git a/ai/terminal-control/StreamLifecycle.tla b/ai/terminal-control/StreamLifecycle.tla new file mode 100644 index 00000000..112288e8 --- /dev/null +++ b/ai/terminal-control/StreamLifecycle.tla @@ -0,0 +1,144 @@ +------------------------- MODULE StreamLifecycle ------------------------- +EXTENDS FiniteSets, TLC + +CONSTANTS Procs, Handles, TerminalUsed + +ASSUME /\ Procs # {} + /\ Handles # {} + /\ TerminalUsed \in BOOLEAN + +VARIABLES phase, resolved, desired, inherited, parentOpen, childOpen, + terminalRetained, procState, eofObserved, failure + +vars == <> + +Init == + /\ phase = "idle" + /\ resolved = FALSE + /\ desired = [p \in Procs |-> {}] + /\ inherited = [p \in Procs |-> {}] + /\ parentOpen = Handles + /\ childOpen = [p \in Procs |-> {}] + /\ terminalRetained = FALSE + /\ procState = [p \in Procs |-> "idle"] + /\ eofObserved = FALSE + /\ failure = "none" + +Resolve == + /\ phase = "idle" + \* The bounded model gives every process exactly its intended standard/pipe handles. + /\ desired' = [p \in Procs |-> Handles] + /\ resolved' = TRUE + /\ terminalRetained' = TerminalUsed + /\ phase' = "resolved" + /\ UNCHANGED <> + +Start(p) == + /\ phase \in {"resolved", "starting"} + /\ resolved + /\ procState[p] = "idle" + /\ inherited' = [inherited EXCEPT ![p] = desired[p]] + /\ childOpen' = [childOpen EXCEPT ![p] = desired[p]] + /\ procState' = [procState EXCEPT ![p] = "running"] + /\ phase' = "starting" + /\ UNCHANGED <> + +StartFails(p) == + /\ phase \in {"resolved", "starting"} + /\ procState[p] = "idle" + /\ procState' = [procState EXCEPT ![p] = "failed"] + /\ phase' = "starting" + /\ UNCHANGED <> + +AllStartsReported == + /\ phase = "starting" + /\ \A p \in Procs: procState[p] # "idle" + /\ phase' = "closeParentCopies" + /\ UNCHANGED <> + +CloseParentCopies == + /\ phase = "closeParentCopies" + /\ parentOpen' = {} + /\ phase' = "running" + /\ UNCHANGED <> + +AbortBeforeRunning == + /\ phase \in {"resolved", "starting", "closeParentCopies"} + /\ parentOpen' = {} + /\ childOpen' = [p \in Procs |-> {}] + /\ terminalRetained' = FALSE + /\ procState' = [p \in Procs |-> + IF procState[p] = "running" THEN "failed" ELSE procState[p]] + /\ phase' = "failed" + /\ failure' = "launch" + /\ UNCHANGED <> + +Exit(p) == + /\ phase = "running" + /\ procState[p] = "running" + /\ childOpen' = [childOpen EXCEPT ![p] = {}] + /\ procState' = [procState EXCEPT ![p] = "exited"] + /\ UNCHANGED <> + +ObserveEOF == + /\ phase = "running" + /\ parentOpen = {} + /\ \A p \in Procs: childOpen[p] = {} + /\ eofObserved' = TRUE + /\ terminalRetained' = FALSE + /\ phase' = "done" + /\ UNCHANGED <> + +Next == Resolve \/ (\E p \in Procs: Start(p) \/ StartFails(p) \/ Exit(p)) \/ + AllStartsReported \/ CloseParentCopies \/ AbortBeforeRunning \/ ObserveEOF + +Spec == Init /\ [][Next]_vars + +TypeOK == + /\ phase \in {"idle", "resolved", "starting", "closeParentCopies", + "running", "failed", "done"} + /\ resolved \in BOOLEAN + /\ desired \in [Procs -> SUBSET Handles] + /\ inherited \in [Procs -> SUBSET Handles] + /\ parentOpen \subseteq Handles + /\ childOpen \in [Procs -> SUBSET Handles] + /\ terminalRetained \in BOOLEAN + /\ procState \in [Procs -> {"idle", "running", "exited", "failed"}] + /\ eofObserved \in BOOLEAN + /\ failure \in {"none", "launch"} + +ExactInheritance == + \A p \in Procs: procState[p] = "running" => inherited[p] = desired[p] + +NoSpawnBeforeResolution == + (\E p \in Procs: procState[p] = "running") => resolved + +EOFIsSound == + eofObserved => + /\ parentOpen = {} + /\ \A p \in Procs: childOpen[p] = {} + +TerminalStatesLeakNoHandles == + phase \in {"failed", "done"} => + /\ parentOpen = {} + /\ \A p \in Procs: childOpen[p] = {} + +TerminalHandleLifetime == + TerminalUsed /\ phase \in {"resolved", "starting", "closeParentCopies", "running"} + => terminalRetained + +TerminalHandleReleasedAtEnd == + phase \in {"failed", "done"} => ~terminalRetained + +============================================================================= diff --git a/ai/terminal-control/TerminalControl.cfg b/ai/terminal-control/TerminalControl.cfg new file mode 100644 index 00000000..a4302fa1 --- /dev/null +++ b/ai/terminal-control/TerminalControl.cfg @@ -0,0 +1,15 @@ +CONSTANTS + Jobs = {j1, j2} + NoJob = NoJob + +INIT Init +NEXT Next + +INVARIANTS + TypeOK + ShellReadRequiresOwnership + PromptIsSafe + OwnerMatchesForeground + NoBackgroundTerminalOwner + SingleForegroundJob + ControlTransactionIsExclusive diff --git a/ai/terminal-control/TerminalControl.tla b/ai/terminal-control/TerminalControl.tla new file mode 100644 index 00000000..e198857e --- /dev/null +++ b/ai/terminal-control/TerminalControl.tla @@ -0,0 +1,233 @@ +-------------------------- MODULE TerminalControl -------------------------- +EXTENDS Naturals, FiniteSets, TLC + +CONSTANTS Jobs, NoJob + +ASSUME /\ Jobs # {} + /\ NoJob \notin Jobs + +JobStates == {"idle", "preparing", "running", "stopped", "exited", "failed"} +Places == {"none", "foreground", "background"} +Phases == {"idle", "resolving", "ready", "spawning", "activating", + "active", "reclaiming", "resuming", "done"} +Owners == Jobs \cup {"shell"} +Modes == {"shellRaw", "shellCooked", "jobMode"} + +VARIABLES jobState, place, phase, terminalOwner, foregroundJob, + controlJob, shellReader, terminalMode + +vars == <> + +Init == + /\ jobState = [j \in Jobs |-> "idle"] + /\ place = [j \in Jobs |-> "none"] + /\ phase = [j \in Jobs |-> "idle"] + /\ terminalOwner = "shell" + /\ foregroundJob = NoJob + /\ controlJob = NoJob + /\ shellReader = "active" + /\ terminalMode = "shellRaw" + +BeginForeground(j) == + /\ jobState[j] = "idle" + /\ terminalOwner = "shell" + /\ shellReader = "active" + /\ foregroundJob = NoJob + /\ controlJob = NoJob + /\ jobState' = [jobState EXCEPT ![j] = "preparing"] + /\ place' = [place EXCEPT ![j] = "foreground"] + /\ phase' = [phase EXCEPT ![j] = "resolving"] + /\ controlJob' = j + /\ UNCHANGED <> + +ResolveForeground(j) == + /\ jobState[j] = "preparing" + /\ place[j] = "foreground" + /\ phase[j] = "resolving" + /\ phase' = [phase EXCEPT ![j] = "ready"] + /\ UNCHANGED <> + +PauseAndPrepare(j) == + /\ phase[j] = "ready" + /\ place[j] = "foreground" + /\ controlJob = j + /\ terminalOwner = "shell" + /\ foregroundJob = NoJob + /\ shellReader = "active" + /\ shellReader' = "paused" + /\ terminalMode' = "shellCooked" + /\ phase' = [phase EXCEPT ![j] = + IF jobState[j] = "preparing" THEN "spawning" ELSE "activating"] + /\ UNCHANGED <> + +Spawn(j) == + /\ jobState[j] = "preparing" + /\ phase[j] = "spawning" + /\ shellReader = "paused" + /\ jobState' = [jobState EXCEPT ![j] = "running"] + /\ phase' = [phase EXCEPT ![j] = "activating"] + /\ UNCHANGED <> + +Activate(j) == + /\ jobState[j] \in {"running", "stopped"} + /\ place[j] = "foreground" + /\ phase[j] = "activating" + /\ controlJob = j + /\ terminalOwner = "shell" + /\ foregroundJob = NoJob + /\ shellReader = "paused" + /\ jobState' = [jobState EXCEPT ![j] = "running"] + /\ phase' = [phase EXCEPT ![j] = "active"] + /\ terminalOwner' = j + /\ foregroundJob' = j + /\ terminalMode' = "jobMode" + /\ UNCHANGED <> + +ForegroundStops(j) == + /\ terminalOwner = j + /\ foregroundJob = j + /\ jobState[j] = "running" + /\ phase[j] = "active" + /\ jobState' = [jobState EXCEPT ![j] = "stopped"] + /\ phase' = [phase EXCEPT ![j] = "reclaiming"] + /\ UNCHANGED <> + +ForegroundExits(j) == + /\ terminalOwner = j + /\ foregroundJob = j + /\ jobState[j] = "running" + /\ phase[j] = "active" + /\ jobState' = [jobState EXCEPT ![j] = "exited"] + /\ phase' = [phase EXCEPT ![j] = "reclaiming"] + /\ UNCHANGED <> + +FailLaunch(j) == + /\ jobState[j] = "preparing" + /\ controlJob = j + /\ phase[j] \in {"resolving", "ready", "spawning", "activating"} + /\ jobState' = [jobState EXCEPT ![j] = "failed"] + /\ phase' = [phase EXCEPT ![j] = + IF shellReader = "paused" THEN "reclaiming" ELSE "done"] + /\ controlJob' = IF shellReader = "paused" THEN j ELSE NoJob + /\ UNCHANGED <> + +Reclaim(j) == + /\ phase[j] = "reclaiming" + /\ place[j] = "foreground" + /\ controlJob = j + /\ shellReader = "paused" + /\ terminalOwner \in {"shell", j} + /\ foregroundJob \in {NoJob, j} + /\ terminalOwner' = "shell" + /\ foregroundJob' = NoJob + /\ terminalMode' = "shellCooked" + /\ phase' = [phase EXCEPT ![j] = "resuming"] + /\ UNCHANGED <> + +ResumeShell(j) == + /\ phase[j] = "resuming" + /\ controlJob = j + /\ terminalOwner = "shell" + /\ foregroundJob = NoJob + /\ shellReader = "paused" + /\ shellReader' = "active" + /\ terminalMode' = "shellRaw" + /\ phase' = [phase EXCEPT ![j] = "done"] + /\ controlJob' = NoJob + /\ UNCHANGED <> + +BeginBackground(j) == + /\ jobState[j] = "idle" + /\ terminalOwner = "shell" + /\ shellReader = "active" + /\ jobState' = [jobState EXCEPT ![j] = "running"] + /\ place' = [place EXCEPT ![j] = "background"] + /\ phase' = [phase EXCEPT ![j] = "active"] + /\ UNCHANGED <> + +BackgroundStops(j) == + /\ jobState[j] = "running" + /\ place[j] = "background" + /\ jobState' = [jobState EXCEPT ![j] = "stopped"] + /\ UNCHANGED <> + +ContinueBackground(j) == + /\ jobState[j] = "stopped" + /\ place[j] = "background" + /\ jobState' = [jobState EXCEPT ![j] = "running"] + /\ UNCHANGED <> + +RequestForeground(j) == + /\ jobState[j] \in {"running", "stopped"} + /\ place[j] = "background" + /\ terminalOwner = "shell" + /\ shellReader = "active" + /\ foregroundJob = NoJob + /\ controlJob = NoJob + /\ place' = [place EXCEPT ![j] = "foreground"] + /\ phase' = [phase EXCEPT ![j] = "ready"] + /\ controlJob' = j + /\ UNCHANGED <> + +Finish(j) == + /\ phase[j] = "done" + /\ jobState[j] \in {"exited", "failed"} + /\ jobState' = [jobState EXCEPT ![j] = "idle"] + /\ place' = [place EXCEPT ![j] = "none"] + /\ phase' = [phase EXCEPT ![j] = "idle"] + /\ UNCHANGED <> + +Next == \E j \in Jobs: + BeginForeground(j) \/ ResolveForeground(j) \/ PauseAndPrepare(j) \/ + Spawn(j) \/ Activate(j) \/ ForegroundStops(j) \/ ForegroundExits(j) \/ + FailLaunch(j) \/ Reclaim(j) \/ ResumeShell(j) \/ BeginBackground(j) \/ + BackgroundStops(j) \/ ContinueBackground(j) \/ RequestForeground(j) \/ + Finish(j) + +Spec == Init /\ [][Next]_vars + +TypeOK == + /\ jobState \in [Jobs -> JobStates] + /\ place \in [Jobs -> Places] + /\ phase \in [Jobs -> Phases] + /\ terminalOwner \in Owners + /\ foregroundJob \in Jobs \cup {NoJob} + /\ controlJob \in Jobs \cup {NoJob} + /\ shellReader \in {"active", "paused"} + /\ terminalMode \in Modes + +ShellReadRequiresOwnership == + shellReader = "active" => terminalOwner = "shell" + +PromptIsSafe == + shellReader = "active" => + /\ foregroundJob = NoJob + /\ terminalMode = "shellRaw" + +OwnerMatchesForeground == + terminalOwner \in Jobs => + /\ foregroundJob = terminalOwner + /\ place[terminalOwner] = "foreground" + /\ shellReader = "paused" + +NoBackgroundTerminalOwner == + \A j \in Jobs: place[j] = "background" => terminalOwner # j + +SingleForegroundJob == + Cardinality({j \in Jobs: place[j] = "foreground" /\ phase[j] = "active"}) <= 1 + +ControlTransactionIsExclusive == + controlJob # NoJob => + /\ place[controlJob] = "foreground" + /\ phase[controlJob] \in {"resolving", "ready", "spawning", + "activating", "active", "reclaiming", "resuming"} + +============================================================================= diff --git a/ai/terminal-control/WINDOWS_DIRECT_HANDOFF.md b/ai/terminal-control/WINDOWS_DIRECT_HANDOFF.md new file mode 100644 index 00000000..dab620ed --- /dev/null +++ b/ai/terminal-control/WINDOWS_DIRECT_HANDOFF.md @@ -0,0 +1,42 @@ +# Windows foreground handoff + +Last reviewed: 2026-08-09. + +## Chosen architecture + +Synchronous foreground commands use direct console inheritance. +After standard streams and redirections have been resolved, mshell starts the +child with those exact handles, stops all of its own terminal reads, waits for +the child, restores the captured console modes, and only then resumes shell +input. + +The surrounding console host remains directly connected to the child. +It—not mshell—handles keyboard input, output, escape sequences, Unicode, cursor +state, and terminal resize events. +There are no mshell input/output relays and no resize-forwarding worker. + +## Why foreground ConPTY proxying was rejected + +A nested ConPTY was prototyped for foreground commands. +That design placed mshell between the existing terminal host and every child: + +```text +terminal host -> mshell console -> mshell relays -> nested ConPTY -> child +``` + +It required mshell to proxy input, output, encoding, resize events, cancellation, +and teardown. +Those responsibilities added failure modes without solving a foreground problem: +the synchronous shell can simply stop reading while the child uses the inherited +console directly. + +## Future job control + +Full job control remains the long-term requirement. +Windows has no POSIX foreground process-group gate, so an interactive background +job sharing the console could compete with mshell for input. +A per-job ConPTY and Job Object may be appropriate for that future isolation +case, but it must be introduced with durable job records and explicit `jobs`, +`fg`, and `bg` semantics. +It must not complicate the direct foreground path merely in anticipation of +those features. diff --git a/ai/terminal-control/WindowsTerminalControl.cfg b/ai/terminal-control/WindowsTerminalControl.cfg new file mode 100644 index 00000000..55ad411d --- /dev/null +++ b/ai/terminal-control/WindowsTerminalControl.cfg @@ -0,0 +1,10 @@ +INIT Init +NEXT Next + +INVARIANTS + TypeOK + NoCompetingReads + ShellReadRequiresOwnership + ChildReadRequiresOwnership + ChildActivationRequiresQuiescence + CtrlGroupIsNotInputOwnership diff --git a/ai/terminal-control/WindowsTerminalControl.tla b/ai/terminal-control/WindowsTerminalControl.tla new file mode 100644 index 00000000..ae91563b --- /dev/null +++ b/ai/terminal-control/WindowsTerminalControl.tla @@ -0,0 +1,127 @@ +---------------------- MODULE WindowsTerminalControl ---------------------- +EXTENDS TLC + +VARIABLES phase, shellRead, childRead, inputOwner, consoleMode, + ctrlGroup, failure + +vars == <> + +Init == + /\ phase = "idle" + /\ shellRead = "outstanding" + /\ childRead = "none" + /\ inputOwner = "shell" + /\ consoleMode = "shellRaw" + /\ ctrlGroup = "none" + /\ failure = "none" + +BeginHandoff == + /\ phase = "idle" + /\ shellRead = "outstanding" + /\ shellRead' = "cancelPending" + /\ phase' = "quiescing" + /\ UNCHANGED <> + +ShellReadQuiesces == + /\ phase = "quiescing" + /\ shellRead = "cancelPending" + /\ shellRead' = "none" + /\ consoleMode' = "shellCooked" + /\ phase' = "ready" + /\ UNCHANGED <> + +QuiesceFails == + /\ phase = "quiescing" + /\ shellRead = "cancelPending" + /\ shellRead' = "outstanding" + /\ phase' = "failed" + /\ failure' = "quiesce" + /\ UNCHANGED <> + +CreateChildGroup == + /\ phase = "ready" + /\ shellRead = "none" + /\ ctrlGroup' = "job" + /\ phase' = "created" + /\ UNCHANGED <> + +CreateFails == + /\ phase = "ready" + /\ phase' = "reclaiming" + /\ failure' = "create" + /\ UNCHANGED <> + +ActivateChild == + /\ phase = "created" + /\ shellRead = "none" + /\ inputOwner = "shell" + /\ inputOwner' = "job" + /\ childRead' = "outstanding" + /\ consoleMode' = "jobMode" + /\ phase' = "foreground" + /\ UNCHANGED <> + +ChildReadCompletes == + /\ phase = "foreground" + /\ childRead = "outstanding" + /\ childRead' = "none" + /\ UNCHANGED <> + +ChildStartsAnotherRead == + /\ phase = "foreground" + /\ childRead = "none" + /\ childRead' = "outstanding" + /\ UNCHANGED <> + +ChildStopsOrExits == + /\ phase = "foreground" + /\ childRead \in {"none", "outstanding"} + /\ childRead' = "none" + /\ phase' = "reclaiming" + /\ UNCHANGED <> + +Reclaim == + /\ phase = "reclaiming" + /\ shellRead = "none" + /\ childRead = "none" + /\ inputOwner' = "shell" + /\ consoleMode' = "shellRaw" + /\ ctrlGroup' = "none" + /\ shellRead' = "outstanding" + /\ phase' = "done" + /\ UNCHANGED <> + +Next == BeginHandoff \/ ShellReadQuiesces \/ QuiesceFails \/ + CreateChildGroup \/ CreateFails \/ ActivateChild \/ + ChildReadCompletes \/ ChildStartsAnotherRead \/ + ChildStopsOrExits \/ Reclaim + +Spec == Init /\ [][Next]_vars + +TypeOK == + /\ phase \in {"idle", "quiescing", "ready", "created", "foreground", + "reclaiming", "failed", "done"} + /\ shellRead \in {"none", "outstanding", "cancelPending"} + /\ childRead \in {"none", "outstanding"} + /\ inputOwner \in {"shell", "job"} + /\ consoleMode \in {"shellRaw", "shellCooked", "jobMode"} + /\ ctrlGroup \in {"none", "job"} + /\ failure \in {"none", "quiesce", "create"} + +NoCompetingReads == + ~(shellRead = "outstanding" /\ childRead = "outstanding") + +ShellReadRequiresOwnership == + shellRead = "outstanding" => inputOwner = "shell" + +ChildReadRequiresOwnership == + childRead = "outstanding" => inputOwner = "job" + +ChildActivationRequiresQuiescence == + inputOwner = "job" => shellRead = "none" + +CtrlGroupIsNotInputOwnership == + ctrlGroup = "job" /\ phase = "created" => inputOwner = "shell" + +============================================================================= diff --git a/ai/terminal-control/check.sh b/ai/terminal-control/check.sh new file mode 100755 index 00000000..9747d1ea --- /dev/null +++ b/ai/terminal-control/check.sh @@ -0,0 +1,17 @@ +#!/usr/bin/env bash +set -euo pipefail + +jar="${TLA2TOOLS_JAR:-$HOME/.local/share/tlaplus/tla2tools.jar}" + +if [[ ! -f "$jar" ]]; then + echo "TLA+ tools jar not found: $jar" >&2 + exit 2 +fi + +for model in TerminalControl POSIXTerminalControl WindowsTerminalControl StreamLifecycle; do + java -XX:+UseParallelGC -cp "$jar" tlc2.TLC -workers 1 -deadlock \ + -config "$model.cfg" "$model.tla" +done + +java -XX:+UseParallelGC -cp "$jar" tlc2.TLC -workers 1 -deadlock \ + -config POSIXNonTerminal.cfg POSIXTerminalControl.tla diff --git a/mshell/Evaluator.go b/mshell/Evaluator.go index 3bfc1ee9..1adcb79f 100644 --- a/mshell/Evaluator.go +++ b/mshell/Evaluator.go @@ -4053,6 +4053,13 @@ func RunProcess(list MShellList, context ExecuteContext, state *EvalState) (Eval cmd.Stderr = cmd.Stdout } + resolvedStdio := resolveProcessStdio(cmd.Stdin, cmd.Stdout, cmd.Stderr) + if context.InPipeline && context.PipelineGroup != nil { + if err := context.PipelineGroup.registerTerminal(resolvedStdio.ControlTerminal()); err != nil { + return state.FailWithMessage(fmt.Sprintf("Error retaining pipeline terminal: %s\n", err)), 1, commandSubWriter.Bytes(), stderrBuffer.Bytes() + } + } + var startErr error var exitCode int @@ -4100,6 +4107,9 @@ func RunProcess(list MShellList, context ExecuteContext, state *EvalState) (Eval // Print out current stdout and stderr startErr = cmd.Start() publishLeader() + if startErr == nil && context.InPipeline && context.PipelineGroup != nil { + context.PipelineGroup.registerProcess(cmd.Process) + } markLaunched() if startErr != nil { @@ -4113,6 +4123,9 @@ func RunProcess(list MShellList, context ExecuteContext, state *EvalState) (Eval // Use Start + Wait instead of Run so we can set the foreground process group startErr = cmd.Start() publishLeader() + if startErr == nil && context.InPipeline && context.PipelineGroup != nil { + context.PipelineGroup.registerProcess(cmd.Process) + } markLaunched() if startErr != nil { fmt.Fprintf(os.Stderr, "Error starting command: %s\n", startErr.Error()) @@ -4122,16 +4135,20 @@ func RunProcess(list MShellList, context ExecuteContext, state *EvalState) (Eval } exitCode = classifyStartError(startErr) } else { - // If stdin is a terminal and we're not in a pipeline, set the subprocess as - // the foreground process group so that CTRL-C goes to it instead of the shell. - // For pipelines, RunPipeline handles foreground process group management. - stdinFd := int(os.Stdin.Fd()) - shouldSetForeground := !context.InPipeline && IsTerminal(stdinFd) && cmd.Process != nil - if shouldSetForeground { - // Ignore SIGTTOU/SIGTTIN to prevent shell from stopping when manipulating foreground - restoreSignals := IgnoreSignalsForJobControl() - SetForegroundProcessGroup(stdinFd, cmd.Process.Pid) - restoreSignals() + // The child endpoint was resolved after redirection. It may be a terminal + // even when mshell's inherited os.Stdin is a pipe. + var foregroundLease *ForegroundLease + if !context.InPipeline && cmd.Process != nil { + foregroundLease, err = acquireForeground(resolvedStdio.ControlTerminal(), cmd.Process.Pid) + if err != nil { + // A terminal-reading child can otherwise remain stopped in SIGTTIN + // forever. Terminate the group and reap the immediate child before + // returning the failed control transaction. + KillProcessGroup(cmd.Process.Pid) + cmd.Process.Kill() + cmd.Wait() + return state.FailWithMessage(fmt.Sprintf("Error acquiring terminal control: %s\n", err)), 1, commandSubWriter.Bytes(), stderrBuffer.Bytes() + } } // As the pipeline group leader, wait until every other stage has @@ -4146,11 +4163,10 @@ func RunProcess(list MShellList, context ExecuteContext, state *EvalState) (Eval waitErr := cmd.Wait() - // Restore the shell as the foreground process group - if shouldSetForeground { - restoreSignals := IgnoreSignalsForJobControl() - RestoreForegroundProcessGroup(stdinFd) - restoreSignals() + // Reclaim the exact terminal and previous process group recorded by the + // acquisition transaction before evaluation can resume shell input. + if err := foregroundLease.Release(); err != nil { + return state.FailWithMessage(fmt.Sprintf("Error reclaiming terminal control: %s\n", err)), 1, commandSubWriter.Bytes(), stderrBuffer.Bytes() } if waitErr != nil { @@ -4193,6 +4209,8 @@ type PipelineGroup struct { claimed bool // whether a leader has been chosen pgid int // leader pid == process group id; 0 until known/usable ready chan struct{} // closed once the leader has started (or failed to) + terminal *TerminalEndpoint // resolved controlling terminal for the job, if any + processes []*os.Process // immediate processes retained for failed-launch cleanup // Launch barrier: the leader must not reap itself (cmd.Wait) until every // stage has finished launching, otherwise reaping destroys the shared @@ -4203,6 +4221,64 @@ type PipelineGroup struct { launchDone chan struct{} } +func (pg *PipelineGroup) registerProcess(process *os.Process) { + if process == nil { + return + } + pg.mu.Lock() + pg.processes = append(pg.processes, process) + pg.mu.Unlock() +} + +func (pg *PipelineGroup) killProcesses() { + pg.mu.Lock() + processes := append([]*os.Process(nil), pg.processes...) + pg.mu.Unlock() + for _, process := range processes { + process.Kill() + } +} + +// registerTerminal records a controlling terminal from a stage's resolved stdio. +// A pipeline is one job, so RunPipeline performs one foreground transaction. +func (pg *PipelineGroup) registerTerminal(endpoint *TerminalEndpoint) error { + if endpoint == nil { + return nil + } + terminal, err := duplicateTerminalEndpoint(endpoint) + if err != nil { + return err + } + pg.mu.Lock() + if pg.terminal == nil { + pg.terminal = terminal + terminal = nil + } + pg.mu.Unlock() + if terminal != nil { + return terminal.Close() + } + return nil +} + +func (pg *PipelineGroup) foregroundTerminal() *TerminalEndpoint { + pg.mu.Lock() + defer pg.mu.Unlock() + if pg.terminal == nil { + return nil + } + terminal := *pg.terminal + return &terminal +} + +func (pg *PipelineGroup) closeTerminal() error { + pg.mu.Lock() + terminal := pg.terminal + pg.terminal = nil + pg.mu.Unlock() + return terminal.Close() +} + func NewPipelineGroup(totalStages int) *PipelineGroup { return &PipelineGroup{ ready: make(chan struct{}), @@ -4405,33 +4481,27 @@ func (state *EvalState) RunPipeline(MShellPipe MShellPipe, context ExecuteContex }(i, item.(Executable)) } - // Make the pipeline's shared process group the terminal foreground so CTRL-C - // goes to the pipeline instead of the shell, and so an interactive stage can - // read the controlling terminal. Wait briefly for the leader to start; if no - // external process starts (e.g. an all-builtin pipeline), skip foreground. - stdinFd := int(os.Stdin.Fd()) - setForeground := IsTerminal(stdinFd) - if setForeground { - pgid := pipelineGroup.foregroundPgid(100 * time.Millisecond) + // Wait until every stage has either started or failed before choosing the + // resolved terminal endpoint. This is also the pipeline launch barrier in + // the formal stream-lifecycle model. + pipelineGroup.waitAllStagesLaunched() + pgid := pipelineGroup.foregroundPgid(100 * time.Millisecond) + foregroundLease, foregroundErr := acquireForeground(pipelineGroup.foregroundTerminal(), pgid) + if foregroundErr != nil { if pgid > 0 { - // Ignore SIGTTOU/SIGTTIN to prevent shell from stopping when manipulating foreground - restoreSignals := IgnoreSignalsForJobControl() - SetForegroundProcessGroup(stdinFd, pgid) - restoreSignals() - } else { - setForeground = false + KillProcessGroup(pgid) } + pipelineGroup.killProcesses() } // Wait for all processes to complete wg.Wait() - // Restore the shell as the foreground process group - if setForeground { - restoreSignals := IgnoreSignalsForJobControl() - RestoreForegroundProcessGroup(stdinFd) - restoreSignals() + var reclaimErr error + if foregroundLease != nil { + reclaimErr = foregroundLease.Release() } + closeTerminalErr := pipelineGroup.closeTerminal() var stdoutBytes []byte var stderrBytes []byte @@ -4448,6 +4518,16 @@ func (state *EvalState) RunPipeline(MShellPipe MShellPipe, context ExecuteContex stderrBytes = nil } + if foregroundErr != nil { + return state.FailWithMessage(fmt.Sprintf("Error acquiring pipeline terminal control: %s\n", foregroundErr)), 1, stdoutBytes, stderrBytes + } + if reclaimErr != nil { + return state.FailWithMessage(fmt.Sprintf("Error reclaiming pipeline terminal control: %s\n", reclaimErr)), 1, stdoutBytes, stderrBytes + } + if closeTerminalErr != nil { + return state.FailWithMessage(fmt.Sprintf("Error closing retained pipeline terminal: %s\n", closeTerminalErr)), 1, stdoutBytes, stderrBytes + } + // Check for errors for i, result := range results { if !result.Success { diff --git a/mshell/Main.go b/mshell/Main.go index eba1046e..9a0bb1dc 100644 --- a/mshell/Main.go +++ b/mshell/Main.go @@ -2189,7 +2189,11 @@ func (state *StdinReaderState) ReadByte() (byte, error) { // Do fresh read // fmt.Fprintf(f, "Reading from stdin...\n") // fmt.Fprintf(f, "%s", debug.Stack()) + if err := processShellInputGate.beginRead(); err != nil { + return 0, err + } n, err := os.Stdin.Read(state.array) + processShellInputGate.endRead() // fmt.Fprintf(f, "Read %d from stdin...\n", n) if err != nil { @@ -2230,7 +2234,12 @@ func (state *TermState) StdinReader(stdInChan chan byte, pauseChan chan bool) { } default: // Read char + if err := processShellInputGate.beginRead(); err != nil { + fmt.Fprintf(os.Stderr, "Error acquiring shell input: %s\n", err) + return + } n, err := os.Stdin.Read(readBuffer) + processShellInputGate.endRead() if err != nil { if err == io.EOF { os.Exit(0) diff --git a/mshell/Pathbin_darwin.go b/mshell/Pathbin_darwin.go index 41a9e58a..e7cacf8f 100644 --- a/mshell/Pathbin_darwin.go +++ b/mshell/Pathbin_darwin.go @@ -263,10 +263,21 @@ func SetForegroundProcessGroup(ttyFd int, pgid int) (int, error) { return oldPgid, nil } -// RestoreForegroundProcessGroup restores the shell's process group as foreground +// RestoreForegroundProcessGroup restores the previous process group as foreground // IMPORTANT: Call IgnoreSignalsForJobControl() before this to avoid SIGTTOU stopping the shell. -func RestoreForegroundProcessGroup(ttyFd int) error { - return unix.IoctlSetPointerInt(ttyFd, unix.TIOCSPGRP, syscall.Getpgrp()) +func RestoreForegroundProcessGroup(ttyFd int, pgid int) error { + return unix.IoctlSetPointerInt(ttyFd, unix.TIOCSPGRP, pgid) +} + +// ContinueProcessGroup resumes a process group that may have stopped on an +// early terminal read before it became foreground. +func ContinueProcessGroup(pgid int) error { + return syscall.Kill(-pgid, syscall.SIGCONT) +} + +// KillProcessGroup terminates every process in a failed foreground launch. +func KillProcessGroup(pgid int) error { + return syscall.Kill(-pgid, syscall.SIGKILL) } // IsTerminal returns true if the file descriptor is connected to a terminal @@ -274,6 +285,38 @@ func IsTerminal(fd int) bool { return term.IsTerminal(fd) } +// CanControlTerminal reports whether fd names this session's controlling +// terminal, rather than merely some terminal device. +func CanControlTerminal(fd int) bool { + _, err := unix.IoctlGetInt(fd, unix.TIOCGPGRP) + return err == nil +} + +func DuplicateTerminalHandle(fd int) (int, error) { + return unix.Dup(fd) +} + +func CloseTerminalHandle(fd int) error { + return syscall.Close(fd) +} + +type posixTerminalModeSnapshot struct { + fd int + state *term.State +} + +func CaptureTerminalMode(fd int) (TerminalModeSnapshot, error) { + state, err := term.GetState(fd) + if err != nil { + return nil, err + } + return &posixTerminalModeSnapshot{fd: fd, state: state}, nil +} + +func (snapshot *posixTerminalModeSnapshot) Restore() error { + return term.Restore(snapshot.fd, snapshot.state) +} + func IsPathSeparator(c uint8) bool { return c == '/' } diff --git a/mshell/Pathbin_linux.go b/mshell/Pathbin_linux.go index 7799f98f..88bc7638 100644 --- a/mshell/Pathbin_linux.go +++ b/mshell/Pathbin_linux.go @@ -254,10 +254,21 @@ func SetForegroundProcessGroup(ttyFd int, pgid int) (int, error) { return oldPgid, nil } -// RestoreForegroundProcessGroup restores the shell's process group as foreground +// RestoreForegroundProcessGroup restores the previous process group as foreground // IMPORTANT: Call IgnoreSignalsForJobControl() before this to avoid SIGTTOU stopping the shell. -func RestoreForegroundProcessGroup(ttyFd int) error { - return unix.IoctlSetPointerInt(ttyFd, unix.TIOCSPGRP, syscall.Getpgrp()) +func RestoreForegroundProcessGroup(ttyFd int, pgid int) error { + return unix.IoctlSetPointerInt(ttyFd, unix.TIOCSPGRP, pgid) +} + +// ContinueProcessGroup resumes a process group that may have stopped on an +// early terminal read before it became foreground. +func ContinueProcessGroup(pgid int) error { + return syscall.Kill(-pgid, syscall.SIGCONT) +} + +// KillProcessGroup terminates every process in a failed foreground launch. +func KillProcessGroup(pgid int) error { + return syscall.Kill(-pgid, syscall.SIGKILL) } // IsTerminal returns true if the file descriptor is connected to a terminal @@ -265,6 +276,38 @@ func IsTerminal(fd int) bool { return term.IsTerminal(fd) } +// CanControlTerminal reports whether fd names this session's controlling +// terminal, rather than merely some terminal device. +func CanControlTerminal(fd int) bool { + _, err := unix.IoctlGetInt(fd, unix.TIOCGPGRP) + return err == nil +} + +func DuplicateTerminalHandle(fd int) (int, error) { + return unix.Dup(fd) +} + +func CloseTerminalHandle(fd int) error { + return syscall.Close(fd) +} + +type posixTerminalModeSnapshot struct { + fd int + state *term.State +} + +func CaptureTerminalMode(fd int) (TerminalModeSnapshot, error) { + state, err := term.GetState(fd) + if err != nil { + return nil, err + } + return &posixTerminalModeSnapshot{fd: fd, state: state}, nil +} + +func (snapshot *posixTerminalModeSnapshot) Restore() error { + return term.Restore(snapshot.fd, snapshot.state) +} + func IsPathSeparator(c uint8) bool { return c == '/' } diff --git a/mshell/Pathbin_windows.go b/mshell/Pathbin_windows.go index ba40f193..a09c12de 100644 --- a/mshell/Pathbin_windows.go +++ b/mshell/Pathbin_windows.go @@ -364,6 +364,7 @@ const ( var ( kernel32 = syscall.NewLazyDLL("kernel32.dll") procSetConsoleCtrlHandler = kernel32.NewProc("SetConsoleCtrlHandler") + consoleCtrlCallback = syscall.NewCallback(consoleCtrlHandler) ) // consoleCtrlHandler handles console control events (CTRL-C, CTRL-BREAK, etc.) @@ -386,16 +387,24 @@ func consoleCtrlHandler(ctrlType uint32) uintptr { return 0 } -// installCtrlHandler installs the console control handler if not already installed -func installCtrlHandler() { +// installCtrlHandler installs the console control handler if not already installed. +// Installation failure is part of the foreground transaction and must not be hidden. +func installCtrlHandler() error { foregroundPgidMu.Lock() defer foregroundPgidMu.Unlock() if !ctrlHandlerInstalled { // SetConsoleCtrlHandler with add=true (1) adds the handler to the list - procSetConsoleCtrlHandler.Call(syscall.NewCallback(consoleCtrlHandler), 1) + result, _, callErr := procSetConsoleCtrlHandler.Call(consoleCtrlCallback, 1) + if result == 0 { + if callErr != nil && callErr != syscall.Errno(0) { + return callErr + } + return fmt.Errorf("SetConsoleCtrlHandler returned failure") + } ctrlHandlerInstalled = true } + return nil } // IgnoreSignalsForJobControl is a no-op on Windows. @@ -408,7 +417,9 @@ func IgnoreSignalsForJobControl() func() { // On Windows, this causes the console control handler to ignore CTRL-C for the shell, // allowing only the child to be terminated. func SetForegroundProcessGroup(ttyFd int, pgid int) (int, error) { - installCtrlHandler() + if err := installCtrlHandler(); err != nil { + return 0, err + } foregroundPgidMu.Lock() oldPgid := foregroundPgid @@ -418,15 +429,25 @@ func SetForegroundProcessGroup(ttyFd int, pgid int) (int, error) { return int(oldPgid), nil } -// RestoreForegroundProcessGroup marks that no child process is running. -// CTRL-C will now terminate the shell again. -func RestoreForegroundProcessGroup(ttyFd int) error { +// RestoreForegroundProcessGroup restores the prior in-memory foreground marker. +func RestoreForegroundProcessGroup(ttyFd int, pgid int) error { foregroundPgidMu.Lock() - foregroundPgid = 0 + foregroundPgid = uint32(pgid) foregroundPgidMu.Unlock() return nil } +// ContinueProcessGroup is a no-op for the direct-console compatibility backend. +func ContinueProcessGroup(pgid int) error { + return nil +} + +// KillProcessGroup cannot terminate a Windows process tree without a Job Object. +// Callers still kill the immediate os.Process while the isolated backend is built. +func KillProcessGroup(pgid int) error { + return nil +} + // IsTerminal returns true if the file descriptor is connected to a terminal func IsTerminal(fd int) bool { // Check if it's a console handle @@ -435,3 +456,72 @@ func IsTerminal(fd int) bool { err := windows.GetConsoleMode(handle, &mode) return err == nil } + +// CanControlTerminal is equivalent to console membership for the direct-console +// backend. Windows has no kernel foreground process-group gate. +func CanControlTerminal(fd int) bool { + return IsTerminal(fd) +} + +func DuplicateTerminalHandle(fd int) (int, error) { + process := windows.CurrentProcess() + var duplicate windows.Handle + err := windows.DuplicateHandle( + process, + windows.Handle(fd), + process, + &duplicate, + 0, + false, + windows.DUPLICATE_SAME_ACCESS, + ) + return int(duplicate), err +} + +func CloseTerminalHandle(fd int) error { + return windows.CloseHandle(windows.Handle(fd)) +} + +type windowsConsoleMode struct { + handle windows.Handle + mode uint32 +} + +type windowsTerminalModeSnapshot struct { + modes []windowsConsoleMode +} + +func CaptureTerminalMode(fd int) (TerminalModeSnapshot, error) { + handles := []windows.Handle{ + windows.Handle(fd), + windows.Handle(os.Stdin.Fd()), + windows.Handle(os.Stdout.Fd()), + windows.Handle(os.Stderr.Fd()), + } + seen := make(map[windows.Handle]struct{}) + snapshot := &windowsTerminalModeSnapshot{} + for _, handle := range handles { + if _, exists := seen[handle]; exists { + continue + } + seen[handle] = struct{}{} + var mode uint32 + if err := windows.GetConsoleMode(handle, &mode); err == nil { + snapshot.modes = append(snapshot.modes, windowsConsoleMode{handle: handle, mode: mode}) + } + } + if len(snapshot.modes) == 0 { + return nil, fmt.Errorf("no console mode available for handle %d", fd) + } + return snapshot, nil +} + +func (snapshot *windowsTerminalModeSnapshot) Restore() error { + var firstErr error + for _, consoleMode := range snapshot.modes { + if err := windows.SetConsoleMode(consoleMode.handle, consoleMode.mode); err != nil && firstErr == nil { + firstErr = err + } + } + return firstErr +} diff --git a/mshell/ProcessTerminalControl.go b/mshell/ProcessTerminalControl.go new file mode 100644 index 00000000..3b2c5683 --- /dev/null +++ b/mshell/ProcessTerminalControl.go @@ -0,0 +1,308 @@ +package main + +import ( + "fmt" + "io" + "os" + "sync" +) + +// TerminalEndpoint is a resolved terminal used by a child process. The file +// descriptor/handle belongs to the already-resolved standard stream; it is not +// inferred from os.Stdin after redirection has been applied. +type TerminalEndpoint struct { + fd int + controlsForeground bool + owned bool +} + +func duplicateTerminalEndpoint(endpoint *TerminalEndpoint) (*TerminalEndpoint, error) { + if endpoint == nil { + return nil, nil + } + fd, err := DuplicateTerminalHandle(endpoint.fd) + if err != nil { + return nil, err + } + return &TerminalEndpoint{ + fd: fd, + controlsForeground: endpoint.controlsForeground, + owned: true, + }, nil +} + +func (endpoint *TerminalEndpoint) Close() error { + if endpoint == nil || !endpoint.owned { + return nil + } + endpoint.owned = false + return CloseTerminalHandle(endpoint.fd) +} + +// ResolvedProcessStdio records the final streams passed to exec.Cmd together +// with any terminal identity they preserve. Keeping this metadata beside the +// streams prevents process control from re-resolving a different default. +type ResolvedProcessStdio struct { + Stdin io.Reader + Stdout io.Writer + Stderr io.Writer + StdinTerminal *TerminalEndpoint + StdoutTerminal *TerminalEndpoint + StderrTerminal *TerminalEndpoint +} + +// resolveControlTerminalEndpoint checks whether a resolved stream can control +// this process's foreground job. The platform probe also establishes terminal +// identity, so a separate IsTerminal call would duplicate the same OS work. +func resolveControlTerminalEndpoint(stream any, fallback *os.File) *TerminalEndpoint { + if stream == nil { + stream = fallback + } + if stream == nil { + return nil + } + + fdProvider, ok := stream.(fileDescriptorProvider) + if !ok { + return nil + } + + fd := int(fdProvider.Fd()) + if !CanControlTerminal(fd) { + return nil + } + + return &TerminalEndpoint{ + fd: fd, + controlsForeground: true, + } +} + +func resolveProcessStdio(stdin io.Reader, stdout, stderr io.Writer) ResolvedProcessStdio { + stdio := ResolvedProcessStdio{ + Stdin: stdin, + Stdout: stdout, + Stderr: stderr, + } + + // Terminal selection is ordered, so stop probing as soon as the governing + // endpoint is known. This avoids repeated ioctls/GetConsoleMode calls for + // the usual case where all three streams share one terminal. + stdio.StdinTerminal = resolveControlTerminalEndpoint(stdin, os.Stdin) + if stdio.StdinTerminal != nil { + return stdio + } + stdio.StdoutTerminal = resolveControlTerminalEndpoint(stdout, os.Stdout) + if stdio.StdoutTerminal != nil { + return stdio + } + stdio.StderrTerminal = resolveControlTerminalEndpoint(stderr, os.Stderr) + return stdio +} + +// ControlTerminal returns the terminal governing the job. Stdin is preferred +// because it is the endpoint whose read access is gated by foreground control. +// A synchronous job with redirected stdin can still need foreground signal and +// output semantics, so terminal stdout/stderr are valid fallbacks. +func (stdio ResolvedProcessStdio) ControlTerminal() *TerminalEndpoint { + if stdio.StdinTerminal != nil && stdio.StdinTerminal.controlsForeground { + return stdio.StdinTerminal + } + if stdio.StdoutTerminal != nil && stdio.StdoutTerminal.controlsForeground { + return stdio.StdoutTerminal + } + if stdio.StderrTerminal != nil && stdio.StderrTerminal.controlsForeground { + return stdio.StderrTerminal + } + return nil +} + +// TerminalModeSnapshot is platform-specific saved state for every console/TTY +// mode affected by a foreground job. +type TerminalModeSnapshot interface { + Restore() error +} + +type terminalControlBackend interface { + captureMode(terminalFd int) (TerminalModeSnapshot, error) + setForeground(terminalFd, pgid int) (int, error) + restoreForeground(terminalFd, pgid int) error + continueProcessGroup(pgid int) error +} + +type platformTerminalControlBackend struct{} + +func (platformTerminalControlBackend) captureMode(terminalFd int) (TerminalModeSnapshot, error) { + return CaptureTerminalMode(terminalFd) +} + +func (platformTerminalControlBackend) setForeground(terminalFd, pgid int) (int, error) { + restoreSignals := IgnoreSignalsForJobControl() + previousPgid, err := SetForegroundProcessGroup(terminalFd, pgid) + restoreSignals() + return previousPgid, err +} + +func (platformTerminalControlBackend) restoreForeground(terminalFd, pgid int) error { + restoreSignals := IgnoreSignalsForJobControl() + err := RestoreForegroundProcessGroup(terminalFd, pgid) + restoreSignals() + return err +} + +func (platformTerminalControlBackend) continueProcessGroup(pgid int) error { + return ContinueProcessGroup(pgid) +} + +// shellInputGate makes the no-competing-reads invariant executable. Today the +// interactive reader is synchronous, but keeping this gate at the actual Read +// boundary preserves the invariant if input later moves to a worker goroutine. +type shellInputGate struct { + mu sync.Mutex + readInProgress bool + foregroundActive bool +} + +func (gate *shellInputGate) beginRead() error { + gate.mu.Lock() + defer gate.mu.Unlock() + if gate.foregroundActive { + return fmt.Errorf("shell input read attempted while a foreground job owns the terminal") + } + if gate.readInProgress { + return fmt.Errorf("concurrent shell input reads are not allowed") + } + gate.readInProgress = true + return nil +} + +func (gate *shellInputGate) endRead() { + gate.mu.Lock() + gate.readInProgress = false + gate.mu.Unlock() +} + +func (gate *shellInputGate) beginForeground() error { + gate.mu.Lock() + defer gate.mu.Unlock() + if gate.readInProgress { + return fmt.Errorf("cannot foreground a job while a shell input read is outstanding") + } + if gate.foregroundActive { + return fmt.Errorf("another foreground job already owns shell input") + } + gate.foregroundActive = true + return nil +} + +func (gate *shellInputGate) endForeground() { + gate.mu.Lock() + gate.foregroundActive = false + gate.mu.Unlock() +} + +var processShellInputGate = &shellInputGate{} + +// foregroundController implements the single controlJob reservation in the +// formal model. Its mutex remains held from acquisition through reclamation. +type foregroundController struct { + mu sync.Mutex + backend terminalControlBackend + inputGate *shellInputGate +} + +var processForegroundController = foregroundController{ + backend: platformTerminalControlBackend{}, + inputGate: processShellInputGate, +} + +type ForegroundLease struct { + controller *foregroundController + terminal TerminalEndpoint + previousPgid int + modeSnapshot TerminalModeSnapshot + released bool + releaseErr error +} + +func acquireForeground(endpoint *TerminalEndpoint, pgid int) (*ForegroundLease, error) { + return processForegroundController.acquire(endpoint, pgid) +} + +func (controller *foregroundController) acquire(endpoint *TerminalEndpoint, pgid int) (*ForegroundLease, error) { + if endpoint == nil || pgid <= 0 { + return nil, nil + } + + controller.mu.Lock() + if err := controller.inputGate.beginForeground(); err != nil { + controller.mu.Unlock() + return nil, err + } + modeSnapshot, err := controller.backend.captureMode(endpoint.fd) + if err != nil { + controller.inputGate.endForeground() + controller.mu.Unlock() + return nil, fmt.Errorf("capture terminal fd %d mode: %w", endpoint.fd, err) + } + previousPgid, err := controller.backend.setForeground(endpoint.fd, pgid) + if err != nil { + controller.inputGate.endForeground() + controller.mu.Unlock() + return nil, fmt.Errorf("give terminal fd %d to process group %d: %w", endpoint.fd, pgid, err) + } + + // A process that attempted a terminal read between Start and tcsetpgrp may + // already have been stopped by SIGTTIN. Foreground it before continuing it. + if err := controller.backend.continueProcessGroup(pgid); err != nil { + restoreErr := controller.backend.restoreForeground(endpoint.fd, previousPgid) + var modeRestoreErr error + if restoreErr == nil { + modeRestoreErr = modeSnapshot.Restore() + } + if restoreErr == nil && modeRestoreErr == nil { + controller.inputGate.endForeground() + } + controller.mu.Unlock() + if restoreErr != nil { + return nil, fmt.Errorf("continue process group %d: %w; terminal rollback also failed: %v", pgid, err, restoreErr) + } + if modeRestoreErr != nil { + return nil, fmt.Errorf("continue process group %d: %w; terminal-mode rollback also failed: %v", pgid, err, modeRestoreErr) + } + return nil, fmt.Errorf("continue process group %d: %w", pgid, err) + } + + return &ForegroundLease{ + controller: controller, + terminal: *endpoint, + previousPgid: previousPgid, + modeSnapshot: modeSnapshot, + }, nil +} + +func (lease *ForegroundLease) Release() error { + if lease == nil { + return nil + } + if lease.released { + return lease.releaseErr + } + lease.released = true + + err := lease.controller.backend.restoreForeground(lease.terminal.fd, lease.previousPgid) + var modeRestoreErr error + if err == nil { + modeRestoreErr = lease.modeSnapshot.Restore() + } + if err == nil && modeRestoreErr == nil { + lease.controller.inputGate.endForeground() + } + lease.controller.mu.Unlock() + if err != nil { + lease.releaseErr = fmt.Errorf("restore terminal fd %d to process group %d: %w", lease.terminal.fd, lease.previousPgid, err) + } else if modeRestoreErr != nil { + lease.releaseErr = fmt.Errorf("restore terminal fd %d mode: %w", lease.terminal.fd, modeRestoreErr) + } + return lease.releaseErr +} diff --git a/mshell/ProcessTerminalControl_test.go b/mshell/ProcessTerminalControl_test.go new file mode 100644 index 00000000..717ccc7f --- /dev/null +++ b/mshell/ProcessTerminalControl_test.go @@ -0,0 +1,278 @@ +package main + +import ( + "errors" + "reflect" + "strings" + "sync" + "testing" + "time" +) + +type fakeTerminalControlBackend struct { + mu sync.Mutex + operations []string + previousPgid int + captureErr error + setErr error + continueErr error + restoreErr error + modeRestoreErr error +} + +type fakeTerminalModeSnapshot struct { + backend *fakeTerminalControlBackend + err error +} + +func (snapshot *fakeTerminalModeSnapshot) Restore() error { + snapshot.backend.record("restoreMode") + return snapshot.err +} + +func (backend *fakeTerminalControlBackend) captureMode(terminalFd int) (TerminalModeSnapshot, error) { + backend.record("capture") + if backend.captureErr != nil { + return nil, backend.captureErr + } + return &fakeTerminalModeSnapshot{backend: backend, err: backend.modeRestoreErr}, nil +} + +func (backend *fakeTerminalControlBackend) record(operation string) { + backend.mu.Lock() + backend.operations = append(backend.operations, operation) + backend.mu.Unlock() +} + +func (backend *fakeTerminalControlBackend) setForeground(terminalFd, pgid int) (int, error) { + backend.record("set") + return backend.previousPgid, backend.setErr +} + +func (backend *fakeTerminalControlBackend) restoreForeground(terminalFd, pgid int) error { + backend.record("restore") + return backend.restoreErr +} + +func (backend *fakeTerminalControlBackend) continueProcessGroup(pgid int) error { + backend.record("continue") + return backend.continueErr +} + +func (backend *fakeTerminalControlBackend) recordedOperations() []string { + backend.mu.Lock() + defer backend.mu.Unlock() + return append([]string(nil), backend.operations...) +} + +func TestForegroundControllerAcquireAndReleaseOrder(t *testing.T) { + backend := &fakeTerminalControlBackend{previousPgid: 41} + controller := foregroundController{backend: backend, inputGate: &shellInputGate{}} + + lease, err := controller.acquire(&TerminalEndpoint{fd: 9}, 52) + if err != nil { + t.Fatalf("acquire returned error: %v", err) + } + if lease == nil { + t.Fatal("acquire returned a nil lease") + } + if err := lease.Release(); err != nil { + t.Fatalf("release returned error: %v", err) + } + + want := []string{"capture", "set", "continue", "restore", "restoreMode"} + if got := backend.recordedOperations(); !reflect.DeepEqual(got, want) { + t.Fatalf("operations = %v, want %v", got, want) + } +} + +func TestResolvedProcessStdioPrefersInputTerminal(t *testing.T) { + stdin := &TerminalEndpoint{fd: 1, controlsForeground: true} + stdout := &TerminalEndpoint{fd: 2, controlsForeground: true} + stderr := &TerminalEndpoint{fd: 3, controlsForeground: true} + stdio := ResolvedProcessStdio{ + StdinTerminal: stdin, + StdoutTerminal: stdout, + StderrTerminal: stderr, + } + + if got := stdio.ControlTerminal(); got != stdin { + t.Fatalf("ControlTerminal() = %v, want stdin terminal", got) + } + stdio.StdinTerminal = nil + if got := stdio.ControlTerminal(); got != stdout { + t.Fatalf("ControlTerminal() = %v, want stdout terminal fallback", got) + } + stdio.StdoutTerminal = nil + if got := stdio.ControlTerminal(); got != stderr { + t.Fatalf("ControlTerminal() = %v, want stderr terminal fallback", got) + } + stderr.controlsForeground = false + if got := stdio.ControlTerminal(); got != nil { + t.Fatalf("ControlTerminal() = %v, want nil for a non-controlling TTY", got) + } +} + +func TestForegroundControllerRollsBackContinueFailure(t *testing.T) { + backend := &fakeTerminalControlBackend{ + previousPgid: 7, + continueErr: errors.New("continue failed"), + } + controller := foregroundController{backend: backend, inputGate: &shellInputGate{}} + + lease, err := controller.acquire(&TerminalEndpoint{fd: 3}, 8) + if lease != nil { + t.Fatal("failed acquire returned a lease") + } + if err == nil || !strings.Contains(err.Error(), "continue failed") { + t.Fatalf("acquire error = %v, want continue failure", err) + } + + want := []string{"capture", "set", "continue", "restore", "restoreMode"} + if got := backend.recordedOperations(); !reflect.DeepEqual(got, want) { + t.Fatalf("operations = %v, want rollback sequence %v", got, want) + } + + // A rollback must release the serialized control transaction. + backend.continueErr = nil + secondLease, err := controller.acquire(&TerminalEndpoint{fd: 3}, 9) + if err != nil { + t.Fatalf("second acquire returned error: %v", err) + } + if err := secondLease.Release(); err != nil { + t.Fatalf("second release returned error: %v", err) + } +} + +func TestForegroundControllerReleasesGateAfterModeCaptureFailure(t *testing.T) { + backend := &fakeTerminalControlBackend{captureErr: errors.New("capture failed")} + gate := &shellInputGate{} + controller := foregroundController{backend: backend, inputGate: gate} + + lease, err := controller.acquire(&TerminalEndpoint{fd: 3}, 8) + if lease != nil { + t.Fatal("failed mode capture returned a lease") + } + if err == nil || !strings.Contains(err.Error(), "capture failed") { + t.Fatalf("acquire error = %v, want mode-capture failure", err) + } + if got := backend.recordedOperations(); !reflect.DeepEqual(got, []string{"capture"}) { + t.Fatalf("operations = %v, want capture only", got) + } + if err := gate.beginRead(); err != nil { + t.Fatalf("shell input remained blocked after capture failure: %v", err) + } + gate.endRead() +} + +func TestForegroundControllerSerializesTransactions(t *testing.T) { + backend := &fakeTerminalControlBackend{previousPgid: 1} + controller := foregroundController{backend: backend, inputGate: &shellInputGate{}} + first, err := controller.acquire(&TerminalEndpoint{fd: 3}, 10) + if err != nil { + t.Fatalf("first acquire returned error: %v", err) + } + + type acquireResult struct { + lease *ForegroundLease + err error + } + result := make(chan acquireResult, 1) + go func() { + lease, acquireErr := controller.acquire(&TerminalEndpoint{fd: 3}, 11) + result <- acquireResult{lease: lease, err: acquireErr} + }() + + select { + case second := <-result: + if second.lease != nil { + second.lease.Release() + } + t.Fatal("second foreground transaction acquired before the first released") + case <-time.After(50 * time.Millisecond): + } + + if err := first.Release(); err != nil { + t.Fatalf("first release returned error: %v", err) + } + + select { + case second := <-result: + if second.err != nil { + t.Fatalf("second acquire returned error: %v", second.err) + } + if err := second.lease.Release(); err != nil { + t.Fatalf("second release returned error: %v", err) + } + case <-time.After(time.Second): + t.Fatal("second foreground transaction did not acquire after release") + } +} + +func TestForegroundControllerRejectsOutstandingShellRead(t *testing.T) { + backend := &fakeTerminalControlBackend{} + gate := &shellInputGate{} + controller := foregroundController{backend: backend, inputGate: gate} + if err := gate.beginRead(); err != nil { + t.Fatalf("begin shell read: %v", err) + } + + lease, err := controller.acquire(&TerminalEndpoint{fd: 3}, 12) + if lease != nil { + t.Fatal("acquire with an outstanding read returned a lease") + } + if err == nil || !strings.Contains(err.Error(), "outstanding") { + t.Fatalf("acquire error = %v, want outstanding-read error", err) + } + if got := backend.recordedOperations(); len(got) != 0 { + t.Fatalf("backend operations = %v, want none before input quiescence", got) + } + + gate.endRead() + lease, err = controller.acquire(&TerminalEndpoint{fd: 3}, 12) + if err != nil { + t.Fatalf("acquire after read quiesced: %v", err) + } + if err := lease.Release(); err != nil { + t.Fatalf("release: %v", err) + } +} + +func TestReclaimFailureKeepsShellInputBlocked(t *testing.T) { + backend := &fakeTerminalControlBackend{restoreErr: errors.New("restore failed")} + gate := &shellInputGate{} + controller := foregroundController{backend: backend, inputGate: gate} + + lease, err := controller.acquire(&TerminalEndpoint{fd: 3}, 13) + if err != nil { + t.Fatalf("acquire: %v", err) + } + if err := lease.Release(); err == nil { + t.Fatal("release succeeded despite injected restore failure") + } + if err := lease.Release(); err == nil { + t.Fatal("repeated release hid the prior restoration failure") + } + if err := gate.beginRead(); err == nil { + gate.endRead() + t.Fatal("shell input was unblocked after terminal restoration failed") + } +} + +func TestModeRestoreFailureKeepsShellInputBlocked(t *testing.T) { + backend := &fakeTerminalControlBackend{modeRestoreErr: errors.New("mode restore failed")} + gate := &shellInputGate{} + controller := foregroundController{backend: backend, inputGate: gate} + + lease, err := controller.acquire(&TerminalEndpoint{fd: 3}, 14) + if err != nil { + t.Fatalf("acquire: %v", err) + } + if err := lease.Release(); err == nil || !strings.Contains(err.Error(), "mode restore failed") { + t.Fatalf("release error = %v, want terminal-mode restoration failure", err) + } + if err := gate.beginRead(); err == nil { + gate.endRead() + t.Fatal("shell input was unblocked after terminal-mode restoration failed") + } +} diff --git a/mshell/ProcessTerminalControl_unix_test.go b/mshell/ProcessTerminalControl_unix_test.go new file mode 100644 index 00000000..af3a2421 --- /dev/null +++ b/mshell/ProcessTerminalControl_unix_test.go @@ -0,0 +1,162 @@ +//go:build linux || darwin + +package main + +import ( + "bytes" + "fmt" + "io" + "os" + "os/exec" + "strings" + "syscall" + "testing" + "time" + + "github.com/creack/pty" +) + +const terminalHandoffHelperEnv = "MSHELL_TERMINAL_HANDOFF_HELPER" + +// TestTerminalHandoffHelper runs only in the subprocess placed inside a fresh +// session and controlling PTY by TestPipedShellStdinCanForegroundTTYChild. +func TestTerminalHandoffHelper(t *testing.T) { + if os.Getenv(terminalHandoffHelperEnv) != "1" { + t.Skip("terminal handoff helper") + } + + list := NewList(3) + list.Items[0] = MShellString{Content: "sh"} + list.Items[1] = MShellString{Content: "-c"} + list.Items[2] = MShellString{Content: "printf 'READY\\n'; IFS= read -r value; printf 'GOT:%s\\n' \"$value\""} + list.StdinBehavior = STDIN_FILE + list.StandardInputFile = "/dev/tty" + + pbm := NewPathBinManager() + state := &EvalState{} + context := ExecuteContext{ + StandardOutput: os.Stdout, + StandardError: os.Stderr, + Pbm: pbm, + } + + result, exitCode, _, _ := RunProcess(*list, context, state) + if !result.Success || exitCode != 0 { + t.Fatalf("RunProcess result.Success = %v, exitCode = %d", result.Success, exitCode) + } + fmt.Fprintln(os.Stdout, "HELPER_DONE") +} + +func TestPipelineTerminalHandoffHelper(t *testing.T) { + if os.Getenv(terminalHandoffHelperEnv) != "1" { + t.Skip("pipeline terminal handoff helper") + } + + producer := NewList(3) + producer.Items[0] = MShellString{Content: "sh"} + producer.Items[1] = MShellString{Content: "-c"} + producer.Items[2] = MShellString{Content: "printf 'unused pipe data\\n'"} + + consumer := NewList(3) + consumer.Items[0] = MShellString{Content: "sh"} + consumer.Items[1] = MShellString{Content: "-c"} + consumer.Items[2] = MShellString{Content: "printf 'PIPE_READY\\n'; IFS= read -r value; printf 'PIPE_GOT:%s\\n' \"$value\""} + consumer.StdinBehavior = STDIN_FILE + consumer.StandardInputFile = "/dev/tty" + + pipeline := MShellPipe{ + List: MShellList{Items: []MShellObject{producer, consumer}}, + } + pbm := NewPathBinManager() + state := &EvalState{} + stack := MShellStack{} + context := ExecuteContext{ + StandardOutput: os.Stdout, + StandardError: os.Stderr, + Variables: make(map[string]MShellObject), + Pbm: pbm, + } + + result, exitCode, _, _ := state.RunPipeline(pipeline, context, &stack) + if !result.Success || exitCode != 0 { + t.Fatalf("RunPipeline result.Success = %v, exitCode = %d", result.Success, exitCode) + } + fmt.Fprintln(os.Stdout, "PIPE_HELPER_DONE") +} + +func TestPipedShellStdinCanForegroundTTYChild(t *testing.T) { + if testing.Short() { + t.Skip("PTY integration test") + } + runPipedStdinPTYHelper(t, "TestTerminalHandoffHelper", "hello from tty\n", "GOT:hello from tty", "HELPER_DONE") +} + +func TestPipelineCanForegroundTTYStage(t *testing.T) { + if testing.Short() { + t.Skip("PTY integration test") + } + runPipedStdinPTYHelper(t, "TestPipelineTerminalHandoffHelper", "hello pipeline\n", "PIPE_GOT:hello pipeline", "PIPE_HELPER_DONE") +} + +func runPipedStdinPTYHelper(t *testing.T, helperName, terminalInput string, expectedOutput ...string) { + t.Helper() + + // The wrapper owns a fresh controlling PTY but gives the Go helper a pipe as + // stdin. RunProcess then gives its child /dev/tty explicitly. Testing + // os.Stdin would skip tcsetpgrp and the child would stop forever on SIGTTIN. + command := exec.Command("sh", "-c", "printf 'piped shell input\\n' | \"$1\" -test.run \"^$2$\"", "sh", os.Args[0], helperName) + command.Env = append(os.Environ(), terminalHandoffHelperEnv+"=1") + ptmx, err := pty.Start(command) + if err != nil { + t.Fatalf("start helper in PTY: %v", err) + } + + readDone := make(chan []byte, 1) + go func() { + output, _ := io.ReadAll(ptmx) + readDone <- output + }() + + if _, err := ptmx.Write([]byte(terminalInput)); err != nil { + terminatePTYProcess(t, command, ptmx) + t.Fatalf("write terminal input: %v", err) + } + + waitDone := make(chan error, 1) + go func() { + waitDone <- command.Wait() + }() + + select { + case err := <-waitDone: + ptmx.Close() + output := <-readDone + if err != nil { + t.Fatalf("PTY helper failed: %v\noutput:\n%s", err, output) + } + for _, expected := range expectedOutput { + if !bytes.Contains(output, []byte(expected)) { + t.Fatalf("PTY output does not contain %q; output:\n%s", expected, output) + } + } + case <-time.After(5 * time.Second): + terminatePTYProcess(t, command, ptmx) + output := <-readDone + t.Fatalf("terminal handoff hung; killed helper process group\noutput:\n%s", output) + } +} + +func terminatePTYProcess(t *testing.T, command *exec.Cmd, ptmx *os.File) { + t.Helper() + if command.Process != nil { + // pty.Start creates a new session led by command.Process, so a negative + // pid terminates the wrapper and every descendant instead of leaving a + // stopped child behind after a failed test. + killErr := syscall.Kill(-command.Process.Pid, syscall.SIGKILL) + if killErr != nil && !strings.Contains(killErr.Error(), "no such process") { + t.Logf("kill PTY process group: %v", killErr) + } + command.Process.Kill() + } + ptmx.Close() +} diff --git a/mshell/go.mod b/mshell/go.mod index 25f5b909..043c51d2 100644 --- a/mshell/go.mod +++ b/mshell/go.mod @@ -4,6 +4,7 @@ go 1.25 require ( github.com/cespare/xxhash v1.1.0 + github.com/creack/pty v1.1.24 go.lsp.dev/protocol v0.12.0 golang.org/x/net v0.42.0 golang.org/x/sys v0.34.0 diff --git a/mshell/go.sum b/mshell/go.sum index ae206cc6..66d45874 100644 --- a/mshell/go.sum +++ b/mshell/go.sum @@ -4,6 +4,8 @@ github.com/benbjohnson/clock v1.1.0 h1:Q92kusRqC1XV2MjkWETPvjJVqKetz1OzxZB7mHJLj github.com/benbjohnson/clock v1.1.0/go.mod h1:J11/hYXuz8f4ySSvYwY0FKfm+ezbsZBKZxNJlLklBHA= github.com/cespare/xxhash v1.1.0 h1:a6HrQnmkObjyL+Gs60czilIUGqrzKutQD6XZog3p+ko= github.com/cespare/xxhash v1.1.0/go.mod h1:XrSqR1VqqWfGrhpAt58auRo0WTKS1nRRg3ghfAqPWnc= +github.com/creack/pty v1.1.24 h1:bJrF4RRfyJnbTJqzRLHzcGaZK1NeM5kTC9jGgovnR1s= +github.com/creack/pty v1.1.24/go.mod h1:08sCNb52WyoAwi2QDyzUCTgcvVFhUzewun7wtTfvcwE= github.com/davecgh/go-spew v1.1.0/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38= github.com/davecgh/go-spew v1.1.1 h1:vj9j/u1bqnvCEfJOwUhtlOARqs3+rkHYY13jYWTU97c= github.com/davecgh/go-spew v1.1.1/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38=