From fd2bb6607414bbd73e006328c0c16a24f8779f05 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 20:50:29 +0000 Subject: [PATCH 1/6] fix(destroy): freeze a group whose member ends between two reads before destroy gives up on it stopProgramGroup sent SIGSTOP only after a judgement of gone. A member of a fork chain that a scan shows can end before its autogroup read, so the judgement reads unknown, and stopProgramGroup returned with no freeze and no kill. A witness that ended before its read again made the loop judge again without a freeze. The wait after it then read the unseen chain ended, and destroy recorded destroyed while the chain ran. CI of #331 hit this in "gc keeps an exited session while a fork chain that the program left runs". Now every judgement that gets no kill and is not unproven sends SIGSTOP and judges the frozen group again: gone as before, unknown, and owned with a witness that ended. A stopped member cannot end, so the next judgement reads its autogroup and the witness, and the group gets the kill. The loop keeps its 5 attempts, and a frozen group that gets no kill still gets SIGCONT in the finally block. New unit tests: a member that ends before its autogroup read, and a witness that ends before its read again, both get SIGSTOP and then SIGKILL (both fail on main). A member whose autogroup /proc refuses now gets 5 SIGSTOP and a SIGCONT, and still no kill. facts.mjs reads the new loop. The model is unchanged: it already assumes that the freeze brings the witness into view. --- .../skills/verify-session-lifecycle/SKILL.md | 2 +- .../verify-session-lifecycle/coverage.json | 4 +- .../scripts/facts.mjs | 35 +++++++------ docs/USAGE.md | 4 +- src/host/README.md | 2 +- src/host/programGroup.ts | 44 +++++++++------- test/unit/host/programGroup.test.ts | 51 ++++++++++++++++++- 7 files changed, 101 insertions(+), 41 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 0804a2bd..3a35237b 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -546,7 +546,7 @@ kill -0 "$other" && echo alive # alive With a token, a kill needs a live member of the group in view, and a wait reads the group gone once no scan shows one. A program whose processes each fork their successor and end within about 2 ms, a fork chain, is almost never in view: by the time a scan reads a pid that its `/proc` listing showed, that process has ended, and the listing missed its successor. `stopProgramGroup` then killed nothing, the wait after it read the group gone, and `destroy` recorded `destroyed` while the chain ran (coder/agent-tty#244). -Now `stopProgramGroup` sends a group that `judgeLiveGroup` reads gone SIGSTOP and judges it again, until the loop's attempts run out. Each judgement that reads gone sends SIGSTOP again, so a member that a SIGCONT from elsewhere resumed stops again. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace, so `procShowsOwnPidSpace` reads false and no SIGSTOP goes out: the group id can name the CLI's own group there. The kernel delivers a group signal also to a child that a member forks during the delivery, so the whole chain stops, and a stopped process stays in view. The next judge finds a stopped member with the token, and the group gets the kill. A frozen group that gets no kill, because its members carry another autogroup, only zombies are left, or a scan throws, gets SIGCONT from a `finally` block. In the model, the constant `Unseen` hides every process of the program from the scans: without the guard the kill through the token kills nothing, and the wait reads the group gone. `current-unseen` checks every rule with `Unseen`, and `mutant-FreezesUnseenGroup-unseen` must violate R11. The integration test "destroy ends a fork chain that no scan of /proc shows" in `test/integration/lifecycle.test.ts` runs `test/fixtures/fork-chain.py` in a session. +Now `stopProgramGroup` sends a group that `judgeLiveGroup` reads gone SIGSTOP and judges it again, until the loop's attempts run out. A scan can also show a member that ends before its autogroup read, so the judgement reads `unknown`, or a witness that ends before it is read again. Those judgements get SIGSTOP and another judgement too: every judgement that gets no kill and is not `unproven` freezes the group. Without that, a loaded CI runner saw `destroy` record `destroyed` after such a judgement while the chain ran. That freezes only a group id that a judgement of gone would freeze too, never one that reads `unproven`. Each judgement that freezes sends SIGSTOP again, so a member that a SIGCONT from elsewhere resumed stops again. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace, so `procShowsOwnPidSpace` reads false and no SIGSTOP goes out: the group id can name the CLI's own group there. The kernel delivers a group signal also to a child that a member forks during the delivery, so the whole chain stops, and a stopped process stays in view. The next judge finds a stopped member with the token, and the group gets the kill. A frozen group that gets no kill, because its members carry another autogroup, only zombies are left, `/proc` refuses the boot id or the autogroup, or a scan throws, gets SIGCONT from a `finally` block. The model has no member that a scan shows and then cannot read, so it relies on this freeze. In the model, the constant `Unseen` hides every process of the program from the scans: without the guard the kill through the token kills nothing, and the wait reads the group gone. `current-unseen` checks every rule with `Unseen`, and `mutant-FreezesUnseenGroup-unseen` must violate R11. The integration test "destroy ends a fork chain that no scan of /proc shows" in `test/integration/lifecycle.test.ts` runs `test/fixtures/fork-chain.py` in a session. ```sh id=$(node --import tsx src/cli/main.ts create --json -- sh -c "python3 test/fixtures/fork-chain.py 30 0.002 $PWD/beat & wait" | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))') diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index e89f55bd..b0ea67af 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -124,7 +124,7 @@ "src/host/programGroup.ts#killProcessGroupBestEffort": "6d5d47cb5697681b", "src/host/programGroup.ts#signalProcessGroup": "c5a3a84361b67aa1", "src/host/programGroup.ts#isProgramGroupAlive": "f6fe01a280824f82", - "src/host/programGroup.ts#stopProgramGroup": "2a512f574e7bd5ae", + "src/host/programGroup.ts#stopProgramGroup": "e7f8b6ca3a5c6e55", "src/host/programGroup.ts#procShowsOwnPidSpace": "ac852506311bb328", "src/host/rpcClient.ts#toTransportCliError": "dd6531349c62bcbd", "src/host/sessionState.ts#SessionState.setDimensions": "08c4f06122d157e9", @@ -148,7 +148,7 @@ "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", "skill:model/SessionLifecycle.tla": "cd8639012467f13e", - "skill:scripts/facts.mjs": "3ef7fa152ec0af36", + "skill:scripts/facts.mjs": "f1ce7a3d3190c497", "skill:scripts/check.sh": "cad764a01b6eee50" }, "callSites": { diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 3f4d7271..29415d2f 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -1205,16 +1205,13 @@ function ownershipFacts() { return; } const st = node.statement.statements.map((s) => normalize(s.getText())); - const owned = st.findIndex((s) => - /^if \(judgement\.verdict !== 'owned'\) \{ (return|break); \}$/.test(s), - ); + // The only kill follows a judgement of owned and a read of its witness + // that owns the group too. checkedKill = st[0] === 'const judgement = judgeLiveGroup(group);' && - owned > 0 && - st[owned + 1] === 'const witness = readProcessRow(judgement.witness);' && - /^if \( witness !== null && judgeProgramGroup\(group, group\.bootId, \[witness\]\)\.verdict === 'owned' \) \{ killProcessGroupBestEffort\(group\.pid\); killed = true; return; \}$/.test( - st[owned + 2] ?? '', - ); + st[1] === "if (judgement.verdict === 'unproven') { return; }" && + st[2] === + "if (judgement.verdict === 'owned') { const witness = readProcessRow(judgement.witness); if ( witness !== null && judgeProgramGroup(group, group.bootId, [witness]).verdict === 'owned' ) { killProcessGroupBestEffort(group.pid); killed = true; return; } }"; }); const judge = normalize( requireDeclaration(module, 'judgeProgramGroup').getText(), @@ -1278,11 +1275,12 @@ function ownershipFacts() { }; } -// In stopProgramGroup's loop, each judgement of gone sends SIGSTOP to the -// group and judges again, so a member that a scan never shows stops and -// comes into view, while /proc names this process by its pid. The finally -// block sends a frozen group that got no kill SIGCONT, also when a scan -// throws. +// In stopProgramGroup's loop, each judgement that gets no kill and is not +// unproven sends SIGSTOP to the group and judges again: gone, unknown, and +// owned with a witness that ended before its read. So a member that a scan +// never shows, or that ends between two reads, stops and stays in view, +// while /proc names this process by its pid. The finally block sends a +// frozen group that got no kill SIGCONT, also when a scan throws. function freezeFacts(body) { const guarded = body.statements.find(ts.isTryStatement); const loop = guarded?.tryBlock.statements.find(ts.isForStatement); @@ -1301,8 +1299,15 @@ function freezeFacts(body) { before.at(-2) === 'let frozen = false;' && before.at(-1) === 'let killed = false;' && guarded.tryBlock.statements.length === 1 && - st[1] === - "if (judgement.verdict === 'gone' && procShowsOwnPidSpace()) { frozen = signalProcessGroup(group.pid, 'SIGSTOP') || frozen; if (frozen) { continue; } }" && + st.length === 6 && + st[1] === "if (judgement.verdict === 'unproven') { return; }" && + st[2].startsWith("if (judgement.verdict === 'owned') {") && + st.slice(3).join('\n') === + [ + 'if (!procShowsOwnPidSpace()) { return; }', + "frozen = signalProcessGroup(group.pid, 'SIGSTOP') || frozen;", + 'if (!frozen) { return; }', + ].join('\n') && normalize( requireDeclaration( 'src/host/programGroup.ts', diff --git a/docs/USAGE.md b/docs/USAGE.md index c7a7da90..463c096e 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -314,7 +314,7 @@ agent-tty record diff --at-seq-a 0 --json `destroy` ends the session's program and every process that the program left in its process group, then records the session as `destroyed`. On Linux it also ends those processes when the program has already exited or the session has failed. -A group whose processes each fork their successor and end too fast for any scan of `/proc` to show one, a fork chain, gets SIGSTOP first. Its stopped processes stay in view, so `destroy` can prove the group and kill it. A frozen group that agent-tty cannot prove is the session's gets SIGCONT. +A group whose processes each fork their successor and end too fast for any scan of `/proc` to show or read one, a fork chain, gets SIGSTOP first. Its stopped processes stay in view, so `destroy` can prove the group and kill it. A frozen group that agent-tty cannot prove is the session's gets SIGCONT. `destroy --force` kills the host and the program's group without asking the host first. When a read of the program's group fails with an error that every later read repeats, such as `program.json` that refuses the read (EACCES) or a `/proc` scan that fails (EIO), `gc` keeps the session and reports "failed to check the session's program group (destroy --force removes it)", or "failed to reconcile session (destroy --force removes it)" for a session whose host died. Those errors are EACCES, EPERM, EIO, EISDIR, ENOTDIR, ELOOP and ENAMETOOLONG. A plain `destroy` fails on the same read. When the read of `program.json` or the first check of the group fails that way twice, 100 ms apart, `destroy --force` stops the host alone, without the group, and records the session as `destroyed` once the host has ended, so the next `gc` removes it. A process that the program left can outlive such a `destroy --force`. When the second read passes, `destroy --force` stops the group as usual. A read that fails after that first check, a group that reads alive, or a host that does not end (`HOST_TIMEOUT`) still fails it. Other errors, such as EMFILE, ENOMEM or EAGAIN, can pass, so `gc` gives no such hint and `destroy --force` fails on them too. A `host.json` that cannot be read counts as missing, so the group reads as out of view: `destroy --force` fails with `HOST_TIMEOUT`, and `gc` removes the session, as in another pid namespace. `list`, `inspect`, `destroy` and `gc` reconcile a session whose host died: they kill the program's group and record the session as `failed` (or `exited` or `destroyed`). @@ -367,7 +367,7 @@ Limits: 1. `destroy` does not kill a process that has left the program's process group. A process leaves the group when it calls `setsid` (for example `setsid cmd` or a daemon), or when an interactive shell with job control runs it as a job (for example `cmd &` typed into `bash -i`). Stop such a process yourself, or keep it in the program's group. 2. Some sessions have no autogroup record: sessions on macOS and Windows, on Linux kernels without autogroups (`/proc/self/autogroup` is missing), on Linux when `/proc` refuses to show the autogroup, the boot id or the host's pid namespace at start-up, and sessions that an agent-tty version without `program.json` created. For these sessions, `destroy --force`, reconcile and the host's own kill at shutdown or at the idle time-out kill the process group (on Windows, the process) that `session.json` names, without the check, so such a kill can reach an unrelated process that took the group id after the program's group ended. `destroy` of a session whose program has already exited kills nothing. A `program.json` that agent-tty cannot read as a record, for example one that a newer version wrote, proves nothing: `destroy` and reconcile kill nothing for that session. -3. The check and the kill are separate system calls, a few microseconds apart. If every process of the group exits and an unrelated process takes the group id in that time, the kill reaches the unrelated process. No system call kills a process group through a handle, so this window remains. A group that no scan shows gets SIGSTOP before each check and SIGCONT when the checks fail. `gc` sends the same two signals to a group whose scans show only zombies while its id still names a process (see item 5). A CLI whose `/proc` belongs to another pid namespace sends no SIGSTOP. If the unrelated group is a job of an interactive shell, the shell reports the job as stopped, and after the SIGCONT the job runs in the background. If agent-tty itself dies between the two signals (SIGKILL, SIGINT, SIGTERM, SIGHUP, or the out-of-memory killer), an unrelated group that took the id stays stopped, and a later `destroy` does not resume it. Resume it with `kill -CONT -- -`, where `` is the Child PID that `inspect` shows. +3. The check and the kill are separate system calls, a few microseconds apart. If every process of the group exits and an unrelated process takes the group id in that time, the kill reaches the unrelated process. No system call kills a process group through a handle, so this window remains. A group that no scan shows, or whose process ends while agent-tty reads it, gets SIGSTOP before each check and SIGCONT when the checks fail. `gc` sends the same two signals to a group whose scans show only zombies while its id still names a process (see item 5). A CLI whose `/proc` belongs to another pid namespace sends no SIGSTOP. If the unrelated group is a job of an interactive shell, the shell reports the job as stopped, and after the SIGCONT the job runs in the background. If agent-tty itself dies between the two signals (SIGKILL, SIGINT, SIGTERM, SIGHUP, or the out-of-memory killer), an unrelated group that took the id stays stopped, and a later `destroy` does not resume it. Resume it with `kill -CONT -- -`, where `` is the Child PID that `inspect` shows. 4. The host writes `program.json` a few milliseconds after it starts the program. We timed 150 `create` calls on Linux, from the return of node-pty's spawn to the renamed `program.json`, at 1-minute load averages of 38 to 83: the median was 2.8 ms, the 90th percentile 4.3 ms, and the longest 66 ms. If the host dies in that window and the program ignores the hang-up signal, no file names the program, and `destroy` cannot end it. 5. `gc` kills nothing. It keeps the folder of a session that is not `destroyed` only while it proves that the program's group runs: the autogroup record in `program.json` proves that a live process of the group is the program's, or the group id still names a process that no scan of `/proc` shows, such as a fast fork chain. When the scans show only zombies of the group while its id still names a process, as for a fork chain under a PID 1 that never reaps, `gc` sends the group SIGSTOP, checks it again, and sends SIGCONT, up to twice in each of up to ten checks of the group, and it keeps the session only when such a check proves the group. A group that has ended gets all 20 frozen checks: with about 2,300 processes in `/proc`, they took about 3.5 s at a load of 90. Another `gc` or a `destroy` that runs at the same time can send SIGCONT before a frozen check. Only when that happens before all 20 of them can a live process of the chain escape every scan, and `gc` then removes the folder of a session whose group still runs. A kept session gets the reason "the session's program group still runs (destroy ends it)". When `gc` cannot check the group, it removes `program.json` with the folder, as it does without an autogroup record (see item 2). That happens in another pid namespace than the one that `host.json` names, for example after a container restart that keeps the agent-tty home, when `host.json` cannot be read, and when `/proc` refuses the boot id or the autogroup of a live process of the group, or hides the processes of other users. Otherwise such a session would stay forever, because no `destroy` can prove its group gone. A process that the program left can then no longer be stopped by agent-tty. Run `destroy` before `gc` when a program can leave processes behind. 6. Two cases where agent-tty cannot run the check end differently from a session that stays running: diff --git a/src/host/README.md b/src/host/README.md index 65f5f32f..77034538 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -57,7 +57,7 @@ - `runHost` handles PTY exit once. If the status is `destroying` it records `destroyed`, else `exited`. Shutdown runs once. [hostMain.ts:runHost] - `destroySession` throws `SESSION_NOT_FOUND` when there is no manifest, or when the session directory is gone at its `destroyed` write, and `SESSION_ALREADY_DESTROYED` for a destroyed session. When it records `destroyed` itself, `recordDestroyed` first writes the empty `/destroyed` marker with `writeDestroyMarker`. Before it records a terminal session as `destroyed`, it calls `stopProgramGroup` with the group from `readProvenProgramGroup`, so only a group with a token gets a signal, and it throws `HOST_TIMEOUT` while that group lives. A session already recorded `destroyed` with the unshared group gets no wait, because only a process that saw the group recorded it, after its wait. A running session gets the `destroy` RPC. With `force` it gets `SIGKILL` for the program's group and, only when `hostMatches` proves the host, for the host: on Linux `judgeHost` must return `alive`, elsewhere `/bin/ps` must show `_host `, and on Windows the host gets no signal. It polls every 100 ms for at most 50 attempts and throws `HOST_TIMEOUT` if the status is still not terminal. With `force`, when the read of `program.json` or the first `isProgramGroupAlive` of the group throws an error that `isUnreadableGroupError` accepts (a `STORAGE_READ_ERROR` whose cause, or a `/proc` read whose code, is in `UNREADABLE_ERRNOS`), `stopUnlessUnreadable` waits `DESTROY_POLL_INTERVAL_MS` (100 ms, abortable) and reads and judges the group again. Only when that read throws such an error too does it stop and wait for the host alone, and `destroySession` records `destroyed` once the host has ended. An error after that first judgement, as in the wait, still throws. `forceSkipsGroup` runs that read and first judgement and returns whether such an error came, so `gcSessions` names `destroy --force` for a failed reconcile only then. [lifecycle.ts:destroySession] [programGroup.ts:isUnreadableGroupError] [programGroup.ts:forceSkipsGroup] - `reconcileSession` writes `destroyed` (both PIDs `null`, the exit code kept, no failure fields) over a terminal manifest other than `destroyed` when the destroy marker exists (`writeMarkedDestroyed`). It then unlinks the socket, removes the Home's socket directory if it is empty, removes the old socket at `legacySocketPath` when `isOwnLegacySocket` accepts it, and returns. Otherwise it does nothing when the manifest is missing, the status is terminal or the host can be alive: `judgeHost` with the record from `host.json` does not return `dead`. A null `hostPid` counts as a dead host. `allocateSession` writes the host PID into the first manifest, so a new session already has a `hostPid`. After the liveness check, `reconcileSession` reads the manifest again and does nothing when it is now missing or terminal. Otherwise it maps the status it read again: `running` to `failed` (failure origin `host-death`), `exiting` to `exited`, `destroying` to `destroyed` and any other status to `failed` (origin `unknown`), and sets both PIDs to `null`. Right after that write, when its status was not `destroyed` and the destroy marker exists, it writes `destroyed` again from the same copy, with both PIDs `null` and no failure fields. When the session directory is gone at any of these writes, it returns. [lifecycle.ts:reconcileSession] [lifecycle.ts:writeMarkedDestroyed] -- Every kill of the program's process group goes through `stopProgramGroup`. For a record with a token, `judgeProgramGroup` returns `owned` only when a process that is not a zombie (a process whose main thread exited is not one while another of its threads runs) has the program's pid as its process group and session id, and the recorded autogroup on the recorded boot. A scan that finds no live member runs once more, because a member can fork and end after the scan listed `/proc`. `stopProgramGroup` reads that process again right before the kill. `unproven` (another boot id, or only members with another session id or autogroup) and `unknown` kill nothing. `gone` (no live member) sends the group SIGSTOP with `signalProcessGroup`, because a fork chain whose members each live about 2 ms is never in view, and a stopped member is. The judge then runs again, up to 5 times, and each judgement that reads `gone` sends SIGSTOP again, for a member that a SIGCONT from elsewhere resumed. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace and no SIGSTOP goes out. A frozen group that gets no kill gets SIGCONT, also when a scan throws. So a group id that an unrelated group took, whose members no scan shows either, gets a SIGSTOP and a SIGCONT. `unknown` means that `/proc` refused the boot id, or showed a member with the program's session id but no autogroup, so `isProgramGroupAlive` reads it alive. A record without a token gets the kill of its `pid`. A `{ childPid, sessionDirectory }` group gets the kill of `childPid`, and reads alive, only while `sessionDirectory` exists, checked in the same synchronous block. The unshared group `{ unshared: true }`, which a record with a token gives when `host.json` names another pid space, is missing or cannot be read (`readHostRecord` reads a failed read as missing), gets no signal and reads alive. [programGroup.ts:stopProgramGroup] [programGroup.ts:judgeProgramGroup] +- Every kill of the program's process group goes through `stopProgramGroup`. For a record with a token, `judgeProgramGroup` returns `owned` only when a process that is not a zombie (a process whose main thread exited is not one while another of its threads runs) has the program's pid as its process group and session id, and the recorded autogroup on the recorded boot. A scan that finds no live member runs once more, because a member can fork and end after the scan listed `/proc`. `stopProgramGroup` reads that process again right before the kill. `unproven` (another boot id, or only members with another session id or autogroup) and `unknown` kill nothing. `gone` (no live member) sends the group SIGSTOP with `signalProcessGroup`, because a fork chain whose members each live about 2 ms is never in view, and a stopped member is. `unknown` and an `owned` whose witness ended before it was read again do the same, because a member can end between two reads and a stopped member cannot. The judge then runs again, up to 5 times, and each such judgement sends SIGSTOP again, for a member that a SIGCONT from elsewhere resumed. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace and no SIGSTOP goes out. A frozen group that gets no kill gets SIGCONT, also when a scan throws. So a group id that an unrelated group took, whose members no scan shows either, gets a SIGSTOP and a SIGCONT. `unknown` means that `/proc` refused the boot id, or showed a member with the program's session id but no autogroup, so `isProgramGroupAlive` reads it alive. A record without a token gets the kill of its `pid`. A `{ childPid, sessionDirectory }` group gets the kill of `childPid`, and reads alive, only while `sessionDirectory` exists, checked in the same synchronous block. The unshared group `{ unshared: true }`, which a record with a token gives when `host.json` names another pid space, is missing or cannot be read (`readHostRecord` reads a failed read as missing), gets no signal and reads alive. [programGroup.ts:stopProgramGroup] [programGroup.ts:judgeProgramGroup] - `captureProgram` records a token only on Linux, for its own child that leads its own session and has an autogroup other than the host's, within 250 ms, and only when `/proc` shows the boot id. `runHost` calls it right after `createPty` and writes the record before its first manifest write, with no `await` in between. [programGroup.ts:captureProgram] [hostMain.ts:runHost] - `allocateSession` throws `INVALID_DIMENSIONS` for non-positive `cols` or `rows`, `STORAGE_READ_ERROR` when `cwd` is not a directory and `INVALID_INPUT` when the shell path is not a file. An empty `command` defaults to the shell path. It creates the session directory and calls `launch` only after these checks pass. [lifecycle.ts:allocateSession] - `buildReplayInput` validates the manifest with `SessionRecordSchema` and requires its `sessionId` to match. It validates the events with `validateEventRecords` unless `trustValidated` is set. `targetSeq` is -1 for no events, else from 0 to the last `seq`. [replay.ts:buildReplayInput] diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index 118a53d4..68340609 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -757,35 +757,41 @@ export function stopProgramGroup(group: ProgramGroup | null): void { } // A member that forks its successor and ends between scans is never in - // view. SIGSTOP freezes the group, also a child that a member forks while - // the kernel delivers it, and a stopped member stays in view, so a frozen - // group that reads gone is judged again. Each such judgement sends SIGSTOP - // again, for a member that a SIGCONT from elsewhere resumed. A frozen group - // that gets no kill gets SIGCONT, also when a scan throws. + // view. One that a scan shows can also end before its autogroup read + // (unknown) or before the witness is read again. SIGSTOP freezes the group, + // also a child that a member forks while the kernel delivers it, and a + // stopped member stays in view and cannot end, so a judgement that gets + // no kill and is not unproven sends SIGSTOP and judges the frozen group + // again. Each such judgement sends SIGSTOP again, for a member that a + // SIGCONT from elsewhere resumed. A frozen group that gets no kill gets + // SIGCONT, also when a scan throws. let frozen = false; let killed = false; try { for (let attempt = 0; attempt < STOP_ATTEMPTS; attempt += 1) { const judgement = judgeLiveGroup(group); - if (judgement.verdict === 'gone' && procShowsOwnPidSpace()) { - frozen = signalProcessGroup(group.pid, 'SIGSTOP') || frozen; - if (frozen) { - continue; - } - } - if (judgement.verdict !== 'owned') { + if (judgement.verdict === 'unproven') { return; } // No pidfd exists for a process group, so the kill races a reused // group id. Reading the witness again shrinks that race to the time // between this read and the kill. - const witness = readProcessRow(judgement.witness); - if ( - witness !== null && - judgeProgramGroup(group, group.bootId, [witness]).verdict === 'owned' - ) { - killProcessGroupBestEffort(group.pid); - killed = true; + if (judgement.verdict === 'owned') { + const witness = readProcessRow(judgement.witness); + if ( + witness !== null && + judgeProgramGroup(group, group.bootId, [witness]).verdict === 'owned' + ) { + killProcessGroupBestEffort(group.pid); + killed = true; + return; + } + } + if (!procShowsOwnPidSpace()) { + return; + } + frozen = signalProcessGroup(group.pid, 'SIGSTOP') || frozen; + if (!frozen) { return; } } diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index ec703008..00177afd 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -1413,6 +1413,50 @@ describe('a program group with a token, as a faked /proc shows it', () => { }); } + // A member that a scan shows can end before its autogroup read, so the + // judgement reads unknown. A stopped member cannot end. + it('freezes a group whose member ends before its autogroup read, and kills it once a stopped member carries the token', () => { + procShowsTokenGroup('S'); + const tokenRead = autogroupFile.read; + autogroupFile.read = (file) => + file === '/proc/100/autogroup' ? '' : (tokenRead?.(file) ?? null); + const kill = stopShowsMember(); + + stopProgramGroup(group); + + expect(kill.mock.calls).toEqual([ + [-CHILD_PID, 'SIGSTOP'], + [-CHILD_PID, 'SIGKILL'], + ]); + }); + + // The witness of a judgement can end before it is read again. + it('freezes a group whose witness ends before it is read again, and kills it once a stopped member carries the token', () => { + procShowsTokenGroup('S'); + const live = procHooks.stat as Map; + let reads = 0; + procHooks.stat = new (class extends Map { + override get(pid: string): string | Error | undefined { + if (pid !== '100') { + return live.get(pid); + } + // Each judgement reads the member once, and the read of the witness + // after it finds the member ended. + reads += 1; + return reads % 2 === 0 ? errno('ENOENT') : live.get(pid); + } + })(live); + const kill = stopShowsMember(); + + stopProgramGroup(group); + + expect(reads).toBe(2); + expect(kill.mock.calls).toEqual([ + [-CHILD_PID, 'SIGSTOP'], + [-CHILD_PID, 'SIGKILL'], + ]); + }); + it('freezes a group that no scan shows and kills it once a stopped member carries the token', () => { procShowsTokenGroup(); const kill = stopShowsMember(); @@ -1712,7 +1756,12 @@ describe.runIf(capturesToken)('a program group with a token', () => { stopProgramGroup(record); - expect(kill).not.toHaveBeenCalled(); + // Each judgement of unknown freezes the group, and the group gets + // SIGCONT at the end. + expect(kill.mock.calls).toEqual([ + ...Array.from({ length: 5 }, () => [-pid, 'SIGSTOP']), + [-pid, 'SIGCONT'], + ]); expect(isProgramGroupAlive(record)).toBe(true); expect(() => process.kill(-pid, 0)).not.toThrow(); }, From 756e3814185257ac8ad7d905966e60e0a8823032 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 21:45:43 +0000 Subject: [PATCH 2/6] fix(destroy): leave a stopped group alone when /proc refuses its autogroup Codex round 1 on #333: a group that job control stopped, whose autogroup or boot id /proc refuses, reads unknown at every judgement. The new freeze sent it SIGSTOP and then SIGCONT, which resumed a program that its user stopped. The unknown verdict now says whether a member without an autogroup still runs. A stopped member cannot end between two reads, so /proc refused its autogroup, and stopProgramGroup sends no signal then. A refused boot id is unknown without a running member too, because no later judgement can prove the group without it. A running member without an autogroup still gets the freeze, once: its stopped member reads the same way, and the group gets SIGCONT. New unit test: a stopped group whose member shows no autogroup gets no signal (fails on the previous head). --- .../skills/verify-session-lifecycle/SKILL.md | 2 +- .../verify-session-lifecycle/coverage.json | 6 ++-- .../scripts/facts.mjs | 6 ++-- src/host/README.md | 2 +- src/host/programGroup.ts | 36 +++++++++++++------ test/unit/host/programGroup.test.ts | 22 ++++++++++-- 6 files changed, 53 insertions(+), 21 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 3a35237b..9e426377 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -546,7 +546,7 @@ kill -0 "$other" && echo alive # alive With a token, a kill needs a live member of the group in view, and a wait reads the group gone once no scan shows one. A program whose processes each fork their successor and end within about 2 ms, a fork chain, is almost never in view: by the time a scan reads a pid that its `/proc` listing showed, that process has ended, and the listing missed its successor. `stopProgramGroup` then killed nothing, the wait after it read the group gone, and `destroy` recorded `destroyed` while the chain ran (coder/agent-tty#244). -Now `stopProgramGroup` sends a group that `judgeLiveGroup` reads gone SIGSTOP and judges it again, until the loop's attempts run out. A scan can also show a member that ends before its autogroup read, so the judgement reads `unknown`, or a witness that ends before it is read again. Those judgements get SIGSTOP and another judgement too: every judgement that gets no kill and is not `unproven` freezes the group. Without that, a loaded CI runner saw `destroy` record `destroyed` after such a judgement while the chain ran. That freezes only a group id that a judgement of gone would freeze too, never one that reads `unproven`. Each judgement that freezes sends SIGSTOP again, so a member that a SIGCONT from elsewhere resumed stops again. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace, so `procShowsOwnPidSpace` reads false and no SIGSTOP goes out: the group id can name the CLI's own group there. The kernel delivers a group signal also to a child that a member forks during the delivery, so the whole chain stops, and a stopped process stays in view. The next judge finds a stopped member with the token, and the group gets the kill. A frozen group that gets no kill, because its members carry another autogroup, only zombies are left, `/proc` refuses the boot id or the autogroup, or a scan throws, gets SIGCONT from a `finally` block. The model has no member that a scan shows and then cannot read, so it relies on this freeze. In the model, the constant `Unseen` hides every process of the program from the scans: without the guard the kill through the token kills nothing, and the wait reads the group gone. `current-unseen` checks every rule with `Unseen`, and `mutant-FreezesUnseenGroup-unseen` must violate R11. The integration test "destroy ends a fork chain that no scan of /proc shows" in `test/integration/lifecycle.test.ts` runs `test/fixtures/fork-chain.py` in a session. +Now `stopProgramGroup` sends a group that `judgeLiveGroup` reads gone SIGSTOP and judges it again, until the loop's attempts run out. A scan can also show a member that ends before its autogroup read, so the judgement reads `unknown`, or a witness that ends before it is read again. Those judgements get SIGSTOP and another judgement too: every judgement that gets no kill freezes the group, except `unproven` and an `unknown` whose members without an autogroup are all stopped (`running` false) or whose boot id `/proc` refuses. A stopped member cannot end, so `/proc` refused its autogroup, and a group that job control stopped gets no signal. Without that, a loaded CI runner saw `destroy` record `destroyed` after such a judgement while the chain ran. That freezes only a group id that a judgement of gone would freeze too, never one that reads `unproven`. Each judgement that freezes sends SIGSTOP again, so a member that a SIGCONT from elsewhere resumed stops again. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace, so `procShowsOwnPidSpace` reads false and no SIGSTOP goes out: the group id can name the CLI's own group there. The kernel delivers a group signal also to a child that a member forks during the delivery, so the whole chain stops, and a stopped process stays in view. The next judge finds a stopped member with the token, and the group gets the kill. A frozen group that gets no kill, because its members carry another autogroup, only zombies are left, `/proc` refuses the autogroup of its stopped member, or a scan throws, gets SIGCONT from a `finally` block. The model has no member that a scan shows and then cannot read, so it relies on this freeze. In the model, the constant `Unseen` hides every process of the program from the scans: without the guard the kill through the token kills nothing, and the wait reads the group gone. `current-unseen` checks every rule with `Unseen`, and `mutant-FreezesUnseenGroup-unseen` must violate R11. The integration test "destroy ends a fork chain that no scan of /proc shows" in `test/integration/lifecycle.test.ts` runs `test/fixtures/fork-chain.py` in a session. ```sh id=$(node --import tsx src/cli/main.ts create --json -- sh -c "python3 test/fixtures/fork-chain.py 30 0.002 $PWD/beat & wait" | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))') diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index b0ea67af..ecf8ab46 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -113,7 +113,7 @@ "src/host/programGroup.ts#readProgramRecord": "b02c48c2bff248a7", "src/host/programGroup.ts#readProvenProgramGroup": "79abfacfdeb33135", "src/host/programGroup.ts#readProgramGroup": "c783266ad349892e", - "src/host/programGroup.ts#judgeProgramGroup": "b8b3053a25f95bbf", + "src/host/programGroup.ts#judgeProgramGroup": "dddd91cb209eafa1", "src/host/programGroup.ts#readGroupMembers": "8f8103d1d5186e91", "src/host/programGroup.ts#judgeLiveGroup": "29c9c4bfd01c4338", "src/host/programGroup.ts#processGroupTarget": "88de1544b1553e54", @@ -124,7 +124,7 @@ "src/host/programGroup.ts#killProcessGroupBestEffort": "6d5d47cb5697681b", "src/host/programGroup.ts#signalProcessGroup": "c5a3a84361b67aa1", "src/host/programGroup.ts#isProgramGroupAlive": "f6fe01a280824f82", - "src/host/programGroup.ts#stopProgramGroup": "e7f8b6ca3a5c6e55", + "src/host/programGroup.ts#stopProgramGroup": "45733f4c2786197c", "src/host/programGroup.ts#procShowsOwnPidSpace": "ac852506311bb328", "src/host/rpcClient.ts#toTransportCliError": "dd6531349c62bcbd", "src/host/sessionState.ts#SessionState.setDimensions": "08c4f06122d157e9", @@ -148,7 +148,7 @@ "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", "skill:model/SessionLifecycle.tla": "cd8639012467f13e", - "skill:scripts/facts.mjs": "f1ce7a3d3190c497", + "skill:scripts/facts.mjs": "e4e67f62f1c1853b", "skill:scripts/check.sh": "cad764a01b6eee50" }, "callSites": { diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 29415d2f..e3d46b46 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -1209,7 +1209,8 @@ function ownershipFacts() { // that owns the group too. checkedKill = st[0] === 'const judgement = judgeLiveGroup(group);' && - st[1] === "if (judgement.verdict === 'unproven') { return; }" && + st[1] === + "if ( judgement.verdict === 'unproven' || (judgement.verdict === 'unknown' && !judgement.running) ) { return; }" && st[2] === "if (judgement.verdict === 'owned') { const witness = readProcessRow(judgement.witness); if ( witness !== null && judgeProgramGroup(group, group.bootId, [witness]).verdict === 'owned' ) { killProcessGroupBestEffort(group.pid); killed = true; return; } }"; }); @@ -1300,7 +1301,8 @@ function freezeFacts(body) { before.at(-1) === 'let killed = false;' && guarded.tryBlock.statements.length === 1 && st.length === 6 && - st[1] === "if (judgement.verdict === 'unproven') { return; }" && + st[1] === + "if ( judgement.verdict === 'unproven' || (judgement.verdict === 'unknown' && !judgement.running) ) { return; }" && st[2].startsWith("if (judgement.verdict === 'owned') {") && st.slice(3).join('\n') === [ diff --git a/src/host/README.md b/src/host/README.md index 77034538..4384014e 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -57,7 +57,7 @@ - `runHost` handles PTY exit once. If the status is `destroying` it records `destroyed`, else `exited`. Shutdown runs once. [hostMain.ts:runHost] - `destroySession` throws `SESSION_NOT_FOUND` when there is no manifest, or when the session directory is gone at its `destroyed` write, and `SESSION_ALREADY_DESTROYED` for a destroyed session. When it records `destroyed` itself, `recordDestroyed` first writes the empty `/destroyed` marker with `writeDestroyMarker`. Before it records a terminal session as `destroyed`, it calls `stopProgramGroup` with the group from `readProvenProgramGroup`, so only a group with a token gets a signal, and it throws `HOST_TIMEOUT` while that group lives. A session already recorded `destroyed` with the unshared group gets no wait, because only a process that saw the group recorded it, after its wait. A running session gets the `destroy` RPC. With `force` it gets `SIGKILL` for the program's group and, only when `hostMatches` proves the host, for the host: on Linux `judgeHost` must return `alive`, elsewhere `/bin/ps` must show `_host `, and on Windows the host gets no signal. It polls every 100 ms for at most 50 attempts and throws `HOST_TIMEOUT` if the status is still not terminal. With `force`, when the read of `program.json` or the first `isProgramGroupAlive` of the group throws an error that `isUnreadableGroupError` accepts (a `STORAGE_READ_ERROR` whose cause, or a `/proc` read whose code, is in `UNREADABLE_ERRNOS`), `stopUnlessUnreadable` waits `DESTROY_POLL_INTERVAL_MS` (100 ms, abortable) and reads and judges the group again. Only when that read throws such an error too does it stop and wait for the host alone, and `destroySession` records `destroyed` once the host has ended. An error after that first judgement, as in the wait, still throws. `forceSkipsGroup` runs that read and first judgement and returns whether such an error came, so `gcSessions` names `destroy --force` for a failed reconcile only then. [lifecycle.ts:destroySession] [programGroup.ts:isUnreadableGroupError] [programGroup.ts:forceSkipsGroup] - `reconcileSession` writes `destroyed` (both PIDs `null`, the exit code kept, no failure fields) over a terminal manifest other than `destroyed` when the destroy marker exists (`writeMarkedDestroyed`). It then unlinks the socket, removes the Home's socket directory if it is empty, removes the old socket at `legacySocketPath` when `isOwnLegacySocket` accepts it, and returns. Otherwise it does nothing when the manifest is missing, the status is terminal or the host can be alive: `judgeHost` with the record from `host.json` does not return `dead`. A null `hostPid` counts as a dead host. `allocateSession` writes the host PID into the first manifest, so a new session already has a `hostPid`. After the liveness check, `reconcileSession` reads the manifest again and does nothing when it is now missing or terminal. Otherwise it maps the status it read again: `running` to `failed` (failure origin `host-death`), `exiting` to `exited`, `destroying` to `destroyed` and any other status to `failed` (origin `unknown`), and sets both PIDs to `null`. Right after that write, when its status was not `destroyed` and the destroy marker exists, it writes `destroyed` again from the same copy, with both PIDs `null` and no failure fields. When the session directory is gone at any of these writes, it returns. [lifecycle.ts:reconcileSession] [lifecycle.ts:writeMarkedDestroyed] -- Every kill of the program's process group goes through `stopProgramGroup`. For a record with a token, `judgeProgramGroup` returns `owned` only when a process that is not a zombie (a process whose main thread exited is not one while another of its threads runs) has the program's pid as its process group and session id, and the recorded autogroup on the recorded boot. A scan that finds no live member runs once more, because a member can fork and end after the scan listed `/proc`. `stopProgramGroup` reads that process again right before the kill. `unproven` (another boot id, or only members with another session id or autogroup) and `unknown` kill nothing. `gone` (no live member) sends the group SIGSTOP with `signalProcessGroup`, because a fork chain whose members each live about 2 ms is never in view, and a stopped member is. `unknown` and an `owned` whose witness ended before it was read again do the same, because a member can end between two reads and a stopped member cannot. The judge then runs again, up to 5 times, and each such judgement sends SIGSTOP again, for a member that a SIGCONT from elsewhere resumed. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace and no SIGSTOP goes out. A frozen group that gets no kill gets SIGCONT, also when a scan throws. So a group id that an unrelated group took, whose members no scan shows either, gets a SIGSTOP and a SIGCONT. `unknown` means that `/proc` refused the boot id, or showed a member with the program's session id but no autogroup, so `isProgramGroupAlive` reads it alive. A record without a token gets the kill of its `pid`. A `{ childPid, sessionDirectory }` group gets the kill of `childPid`, and reads alive, only while `sessionDirectory` exists, checked in the same synchronous block. The unshared group `{ unshared: true }`, which a record with a token gives when `host.json` names another pid space, is missing or cannot be read (`readHostRecord` reads a failed read as missing), gets no signal and reads alive. [programGroup.ts:stopProgramGroup] [programGroup.ts:judgeProgramGroup] +- Every kill of the program's process group goes through `stopProgramGroup`. For a record with a token, `judgeProgramGroup` returns `owned` only when a process that is not a zombie (a process whose main thread exited is not one while another of its threads runs) has the program's pid as its process group and session id, and the recorded autogroup on the recorded boot. A scan that finds no live member runs once more, because a member can fork and end after the scan listed `/proc`. `stopProgramGroup` reads that process again right before the kill. `unproven` (another boot id, or only members with another session id or autogroup) and `unknown` kill nothing. `gone` (no live member) sends the group SIGSTOP with `signalProcessGroup`, because a fork chain whose members each live about 2 ms is never in view, and a stopped member is. An `unknown` whose member without an autogroup still runs (`running`), and an `owned` whose witness ended before it was read again, do the same, because a member can end between two reads and a stopped member cannot. An `unknown` whose such members are all stopped, or whose boot id `/proc` refuses, gets no signal, so a group that job control stopped stays stopped. The judge then runs again, up to 5 times, and each such judgement sends SIGSTOP again, for a member that a SIGCONT from elsewhere resumed. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace and no SIGSTOP goes out. A frozen group that gets no kill gets SIGCONT, also when a scan throws. So a group id that an unrelated group took, whose members no scan shows either, gets a SIGSTOP and a SIGCONT. `unknown` means that `/proc` refused the boot id, or showed a member with the program's session id but no autogroup, so `isProgramGroupAlive` reads it alive. A record without a token gets the kill of its `pid`. A `{ childPid, sessionDirectory }` group gets the kill of `childPid`, and reads alive, only while `sessionDirectory` exists, checked in the same synchronous block. The unshared group `{ unshared: true }`, which a record with a token gives when `host.json` names another pid space, is missing or cannot be read (`readHostRecord` reads a failed read as missing), gets no signal and reads alive. [programGroup.ts:stopProgramGroup] [programGroup.ts:judgeProgramGroup] - `captureProgram` records a token only on Linux, for its own child that leads its own session and has an autogroup other than the host's, within 250 ms, and only when `/proc` shows the boot id. `runHost` calls it right after `createPty` and writes the record before its first manifest write, with no `await` in between. [programGroup.ts:captureProgram] [hostMain.ts:runHost] - `allocateSession` throws `INVALID_DIMENSIONS` for non-positive `cols` or `rows`, `STORAGE_READ_ERROR` when `cwd` is not a directory and `INVALID_INPUT` when the shell path is not a file. An empty `command` defaults to the shell path. It creates the session directory and calls `launch` only after these checks pass. [lifecycle.ts:allocateSession] - `buildReplayInput` validates the manifest with `SessionRecordSchema` and requires its `sessionId` to match. It validates the events with `validateEventRecords` unless `trustValidated` is set. `targetSeq` is -1 for no events, else from 0 to the last `seq`. [replay.ts:buildReplayInput] diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index 68340609..9f47227f 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -377,10 +377,14 @@ export async function readProgramGroup( } // unknown: /proc refuses the boot id, or shows a member of the program's -// session without an autogroup, so the group can still be ours. +// session without an autogroup, so the group can still be ours. running: +// such a member is not stopped, so it can have ended between its stat and +// its autogroup read, as a member of a fork chain does. A stopped one cannot +// end, so /proc refused its autogroup. type GroupJudgement = | { readonly verdict: 'owned'; readonly witness: number } - | { readonly verdict: 'gone' | 'unproven' | 'unknown' }; + | { readonly verdict: 'unknown'; readonly running: boolean } + | { readonly verdict: 'gone' | 'unproven' }; export function judgeProgramGroup( record: ProvenRecord, @@ -394,7 +398,7 @@ export function judgeProgramGroup( return { verdict: 'gone' }; } if (bootId === null) { - return { verdict: 'unknown' }; + return { verdict: 'unknown', running: false }; } if (bootId !== record.bootId) { return { verdict: 'unproven' }; @@ -405,8 +409,14 @@ export function judgeProgramGroup( if (witness !== undefined) { return { verdict: 'owned', witness: witness.pid }; } - return members.some((row) => row.sid === record.pid && row.autogroup === null) - ? { verdict: 'unknown' } + const unread = members.filter( + (row) => row.sid === record.pid && row.autogroup === null, + ); + return unread.length > 0 + ? { + verdict: 'unknown', + running: unread.some((row) => row.state !== 'T' && row.state !== 't'), + } : { verdict: 'unproven' }; } @@ -758,11 +768,12 @@ export function stopProgramGroup(group: ProgramGroup | null): void { // A member that forks its successor and ends between scans is never in // view. One that a scan shows can also end before its autogroup read - // (unknown) or before the witness is read again. SIGSTOP freezes the group, - // also a child that a member forks while the kernel delivers it, and a - // stopped member stays in view and cannot end, so a judgement that gets - // no kill and is not unproven sends SIGSTOP and judges the frozen group - // again. Each such judgement sends SIGSTOP again, for a member that a + // (unknown, running) or before the witness is read again. SIGSTOP freezes + // the group, also a child that a member forks while the kernel delivers + // it, and a stopped member stays in view and cannot end, so a judgement + // that gets no kill and is neither unproven nor an unknown without a + // running member sends SIGSTOP and judges the frozen group again. A group + // that job control stopped, whose autogroup /proc refuses, gets no signal. Each such judgement sends SIGSTOP again, for a member that a // SIGCONT from elsewhere resumed. A frozen group that gets no kill gets // SIGCONT, also when a scan throws. let frozen = false; @@ -770,7 +781,10 @@ export function stopProgramGroup(group: ProgramGroup | null): void { try { for (let attempt = 0; attempt < STOP_ATTEMPTS; attempt += 1) { const judgement = judgeLiveGroup(group); - if (judgement.verdict === 'unproven') { + if ( + judgement.verdict === 'unproven' || + (judgement.verdict === 'unknown' && !judgement.running) + ) { return; } // No pidfd exists for a process group, so the kill races a reused diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index 00177afd..71434ebf 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -1430,6 +1430,20 @@ describe('a program group with a token, as a faked /proc shows it', () => { ]); }); + // A stopped member cannot end, so /proc refused its autogroup. A SIGCONT + // would resume a group that job control stopped. + it('sends no signal to a stopped group whose member shows no autogroup', () => { + procShowsTokenGroup('T'); + const tokenRead = autogroupFile.read; + autogroupFile.read = (file) => + file === '/proc/100/autogroup' ? '' : (tokenRead?.(file) ?? null); + const kill = vi.spyOn(process, 'kill').mockReturnValue(true); + + stopProgramGroup(group); + + expect(kill).not.toHaveBeenCalled(); + }); + // The witness of a judgement can end before it is read again. it('freezes a group whose witness ends before it is read again, and kills it once a stopped member carries the token', () => { procShowsTokenGroup('S'); @@ -1756,10 +1770,12 @@ describe.runIf(capturesToken)('a program group with a token', () => { stopProgramGroup(record); - // Each judgement of unknown freezes the group, and the group gets - // SIGCONT at the end. + // A running member without an autogroup can be a member of a fork + // chain that ended between two reads, so the group gets SIGSTOP. Its + // stopped member still shows no autogroup, so /proc refuses it, and + // the group gets SIGCONT. expect(kill.mock.calls).toEqual([ - ...Array.from({ length: 5 }, () => [-pid, 'SIGSTOP']), + [-pid, 'SIGSTOP'], [-pid, 'SIGCONT'], ]); expect(isProgramGroupAlive(record)).toBe(true); From 98cc404b2ba5eea9b419ebbb2b66d0b973be7fe0 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 22:54:27 +0000 Subject: [PATCH 3/6] fix(destroy): read a group that no scan shows alive while a second probe finds its id When the probe kill(-pgid, 0) found the group but no scan showed a member, live or zombie, isProcessGroupAlive read the group ended: it took the processes for ones reaped before the scans. A fork chain that no scan shows reads the same way, so a freeze that missed the chain let the wait after it read the running chain ended, and destroy recorded destroyed. Now a second probe after the scans decides: reaped processes are gone, and a chain still holds the id, so the wait times out with HOST_TIMEOUT instead. Scans that show only zombies still read the group ended, because under a PID 1 that never reaps the zombies of a killed group stay. Model: the guard WaitProbesUnseenGroup and the environment constant FreezeMisses (every freeze of an Unseen group misses, as when a SIGCONT from another process comes before each judgement). ProbeSees now reads the program's processes under Unseen only through that probe, as the code does. GroupJudged keeps gc on its own probe. New runs: current-unseen-misses (pass, 68,556,464 distinct states) and mutant-WaitProbesUnseenGroup-unseen-misses (violates R11). mutant-FreezesUnseenGroup-unseen becomes mutant-UnseenBothGuards-unseen: either guard alone keeps R11. That makes 92 runs and forty guards. Also from the advisor on #333: - stopProgramGroup sends no SIGSTOP before its first freeze to a group that shows a member that job control or a tracer stopped, so the SIGCONT after the judgements cannot resume that member beside a running one. - src/host/README.md names the freeze of a member that ends between two reads, and the comment of stopProgramGroup is rewrapped. --- .../skills/verify-session-lifecycle/SKILL.md | 19 +++++-- .../verify-session-lifecycle/coverage.json | 11 ++-- .../model/SessionLifecycle.tla | 39 ++++++++++--- .../verify-session-lifecycle/scripts/check.sh | 16 +++++- .../scripts/facts.mjs | 24 +++++++- docs/USAGE.md | 4 +- src/host/README.md | 2 +- src/host/programGroup.ts | 36 ++++++++---- test/unit/host/programGroup.test.ts | 56 +++++++++++++++++-- 9 files changed, 168 insertions(+), 39 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 9e426377..f096ee11 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -65,13 +65,13 @@ From the repo root: .agents/skills/verify-session-lifecycle/scripts/check.sh ``` -It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. `CHECK_JOBS` runs run at a time (a new one starts as soon as one ends; the bash 3.2 of macOS waits for each batch). The runs that expect pass share the CPUs as TLC workers, at least 1 each, and the others keep 1 worker, so their traces stay the shortest. Eleven runs explore more than 20 million distinct states each, so `CHECK_JOBS=90` starts every run at once and takes about as long as the longest run. `JAVA=/path/to/java` picks another Java. `TLA2TOOLS_JAR=/path/to/tla2tools.jar` uses a jar you already have, which must be the same 1.7.4 build. `CHECK_OUT=` keeps the results in that folder (default: a new temp folder, printed at the end). +It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. `CHECK_JOBS` runs run at a time (a new one starts as soon as one ends; the bash 3.2 of macOS waits for each batch). The runs that expect pass share the CPUs as TLC workers, at least 1 each, and the others keep 1 worker, so their traces stay the shortest. Fourteen runs explore more than 20 million distinct states each, so `CHECK_JOBS=92` starts every run at once and takes about as long as the longest run. `JAVA=/path/to/java` picks another Java. `TLA2TOOLS_JAR=/path/to/tla2tools.jar` uses a jar you already have, which must be the same 1.7.4 build. `CHECK_OUT=` keeps the results in that folder (default: a new temp folder, printed at the end). What it does: -1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the thirty-nine guards that the rules depend on and the status sets of the policy table, and it hashes each covered function with comments and layout removed. +1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the forty guards that the rules depend on and the status sets of the policy table, and it hashes each covered function with comments and layout removed. 2. It writes one TLC config per run, with those facts as constants. A guard that is not in the code, in the expected place and order, reads FALSE, and the model then runs without it. -3. It runs TLC 90 times and prints one line per run. +3. It runs TLC 92 times and prints one line per run. 4. It compares the guard values, the status sets, the hashes and the call sites with `coverage.json`. Exit codes: 0 means every run gave the expected result and the covered code matches the sync record. 1 means at least one run gave an unexpected result; the line says `UNEXPECTED`. 3 means every result was as expected, but covered code changed since the sync commit; that is not a pass, so follow "When you change covered code on purpose". 2 means a tool could not run. When both 1 and 3 apply, the exit code is 1. @@ -89,8 +89,11 @@ At the sync commit, the expected results are: | `witness-*-no-token` | violated | Eight of those states without a token: a `create` that gave up recorded the session destroyed, a crash is reconciled, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` and `destroy --force`, and a reconcile writes destroyed again over the failed that it wrote. They show that `current-no-token` reaches the fallback kill and the EPERM probe. | | `mutant-CreateRecordsHostPid`, `mutant-HostWaitsForManifest`, `mutant-ReconcileRereads`, `mutant-HostSerializesWrites`, `mutant-ReconcileSkipsLiveHost`, `mutant-HostStopsAfterTerminalWrite`, `mutant-DestroyRecordsDestroyed`, `mutant-DestroyKeepsExitCode`, `mutant-ManifestWriteNeedsFolder`, `mutant-KillsProgramGroup`, `mutant-HostWaitsForGroup`, `mutant-ReconcileWaitsForGroup`, `mutant-ReRunsInNewSession`, `mutant-InsideCheckReadsEnv`, `mutant-RecordsProgramSync`, `mutant-ProvesGroupOwnership`, `mutant-DestroyStopsLeftovers`, `mutant-FallbackNeedsFolder`, `mutant-ReconcileRepairsDestroyed`, `mutant-CreateStopsOnGiveUp`, `mutant-TokenNamesProgram`, `mutant-ProvesHostPid`, `mutant-GcBothChecks`, `mutant-GcKeepsLiveGroup`, `mutant-ShutdownBothChecks` | violated | Each run removes a guard from the model and checks only the rule that the guard protects. That rule must break, which shows the check can fail. | | `mutant-ProbeCountsDeniedGroup-no-token`, `mutant-KillsProgramGroup-no-token`, `mutant-HostWaitsForGroup-no-token`, `mutant-ReconcileWaitsForGroup-no-token` | violated | The same without a token. The fallback depends on these guards as the code before `program.json` did. With a token, the token check reads a process of another user in view, so only this path checks `ProbeCountsDeniedGroup`. | -| `mutant-FreezesUnseenGroup-unseen`, `mutant-GcProbesUnseenGroup-unseen` | violated | Without the freeze, the kill through the token finds no member in view, the wait reads the group gone, and `destroy` records destroyed while the fork chain runs (R11). | +| `mutant-UnseenBothGuards-unseen` | violated | With neither the freeze nor the wait's probe, the kill through the token finds no member in view, the wait reads the group gone, and `destroy` records destroyed while the fork chain runs (R11). Either guard alone keeps R11. | +| `mutant-GcProbesUnseenGroup-unseen` | violated | Without the probe, gc reads the fork chain ended and removes `program.json` while it runs (R20). | | `mutant-GcFreezesUnseenGroup-unseen-zombies` | violated | `ZombiesInView`: under a PID 1 that never reaps, the fork chain also leaves zombies in view. Without the freeze, gc reads the group ended and removes `program.json` while the chain runs (R20). With every guard, `ZombiesInView` changes nothing, so `current-unseen` covers the pass run. | +| `current-unseen-misses`, the code as it is with a fork chain that every freeze misses, every rule | pass | `FreezeMisses`: no freeze brings a member of the chain into view, as when a SIGCONT from another process comes before each judgement. The wait's probe reads the chain alive, so `destroy` fails with `HOST_TIMEOUT` instead of recording destroyed. | +| `mutant-WaitProbesUnseenGroup-unseen-misses` | violated | R11: without the probe, the wait after a missed freeze reads the chain ended, and `destroy` records destroyed while it runs. | | `mutant-ReusedIdReadsGone` | pass | Without the guard, a group that took the program's id reads alive, so no wait of `destroy` passes while it runs, and `WitnessWaitPassesReusedId` is never reached. The model has no rule for a wait that never ends, so this run checks that witness instead of a rule. | | `mutant-ReconcileRepairsMarked` | violated | R18: without the guard, a `list` that died between its write and its repair leaves `failed`, and the next reconcile skips it as it skips any terminal manifest. | | `mutant-ReconcileSkipsTerminal` | pass | The re-read in `reconcileSession` also returns on a terminal manifest, so the first terminal return alone is redundant. | @@ -546,7 +549,7 @@ kill -0 "$other" && echo alive # alive With a token, a kill needs a live member of the group in view, and a wait reads the group gone once no scan shows one. A program whose processes each fork their successor and end within about 2 ms, a fork chain, is almost never in view: by the time a scan reads a pid that its `/proc` listing showed, that process has ended, and the listing missed its successor. `stopProgramGroup` then killed nothing, the wait after it read the group gone, and `destroy` recorded `destroyed` while the chain ran (coder/agent-tty#244). -Now `stopProgramGroup` sends a group that `judgeLiveGroup` reads gone SIGSTOP and judges it again, until the loop's attempts run out. A scan can also show a member that ends before its autogroup read, so the judgement reads `unknown`, or a witness that ends before it is read again. Those judgements get SIGSTOP and another judgement too: every judgement that gets no kill freezes the group, except `unproven` and an `unknown` whose members without an autogroup are all stopped (`running` false) or whose boot id `/proc` refuses. A stopped member cannot end, so `/proc` refused its autogroup, and a group that job control stopped gets no signal. Without that, a loaded CI runner saw `destroy` record `destroyed` after such a judgement while the chain ran. That freezes only a group id that a judgement of gone would freeze too, never one that reads `unproven`. Each judgement that freezes sends SIGSTOP again, so a member that a SIGCONT from elsewhere resumed stops again. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace, so `procShowsOwnPidSpace` reads false and no SIGSTOP goes out: the group id can name the CLI's own group there. The kernel delivers a group signal also to a child that a member forks during the delivery, so the whole chain stops, and a stopped process stays in view. The next judge finds a stopped member with the token, and the group gets the kill. A frozen group that gets no kill, because its members carry another autogroup, only zombies are left, `/proc` refuses the autogroup of its stopped member, or a scan throws, gets SIGCONT from a `finally` block. The model has no member that a scan shows and then cannot read, so it relies on this freeze. In the model, the constant `Unseen` hides every process of the program from the scans: without the guard the kill through the token kills nothing, and the wait reads the group gone. `current-unseen` checks every rule with `Unseen`, and `mutant-FreezesUnseenGroup-unseen` must violate R11. The integration test "destroy ends a fork chain that no scan of /proc shows" in `test/integration/lifecycle.test.ts` runs `test/fixtures/fork-chain.py` in a session. +Now `stopProgramGroup` sends a group that `judgeLiveGroup` reads gone SIGSTOP and judges it again, until the loop's attempts run out. A scan can also show a member that ends before its autogroup read, so the judgement reads `unknown`, or a witness that ends before it is read again. Those judgements get SIGSTOP and another judgement too: every judgement that gets no kill freezes the group, except `unproven` and an `unknown` whose members without an autogroup are all stopped (`running` false) or whose boot id `/proc` refuses. A stopped member cannot end, so `/proc` refused its autogroup, and a group that job control stopped gets no signal. Before its first freeze, a group that shows any member that job control or a tracer stopped gets no SIGSTOP either (`showsStoppedMember`), so the SIGCONT after the judgements cannot resume that member beside a running one. Without that, a loaded CI runner saw `destroy` record `destroyed` after such a judgement while the chain ran. That freezes only a group id that a judgement of gone would freeze too, never one that reads `unproven`. Each judgement that freezes sends SIGSTOP again, so a member that a SIGCONT from elsewhere resumed stops again. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace, so `procShowsOwnPidSpace` reads false and no SIGSTOP goes out: the group id can name the CLI's own group there. The kernel delivers a group signal also to a child that a member forks during the delivery, so the whole chain stops, and a stopped process stays in view. The next judge finds a stopped member with the token, and the group gets the kill. A frozen group that gets no kill, because its members carry another autogroup, only zombies are left, `/proc` refuses the autogroup of its stopped member, or a scan throws, gets SIGCONT from a `finally` block. The model has no member that a scan shows and then cannot read, so it relies on this freeze. In the model, the constant `Unseen` hides every process of the program from the scans: without the guard the kill through the token kills nothing, and, without `WaitProbesUnseenGroup` (below), the wait reads the group gone. `current-unseen` checks every rule with `Unseen`, and `mutant-UnseenBothGuards-unseen`, without the freeze and the wait's probe, must violate R11. The integration test "destroy ends a fork chain that no scan of /proc shows" in `test/integration/lifecycle.test.ts` runs `test/fixtures/fork-chain.py` in a session. ```sh id=$(node --import tsx src/cli/main.ts create --json -- sh -c "python3 test/fixtures/fork-chain.py 30 0.002 $PWD/beat & wait" | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))') @@ -554,6 +557,12 @@ sleep 1; node --import tsx src/cli/main.ts destroy "$id" --json # ok: true, de a=$(cat beat); sleep 1; [ "$a" = "$(cat beat)" ] && echo ended # ended ``` +### `WaitProbesUnseenGroup`: a missed freeze lets destroy record destroyed (R11) + +When the probe `kill(-pgid, 0)` found the group but no scan showed a member, live or zombie, `isProcessGroupAlive` read the group ended: the processes that the probe found had been reaped before the scans. A fork chain that no scan shows reads the same way. So when the freeze of `stopProgramGroup` missed the chain, the wait after it read the running chain ended, and `destroy` recorded `destroyed`. A loaded CI runner hit that through the judgements that the freeze did not cover before (an `unknown` from a member that ended before its autogroup read). + +Now `isProcessGroupAlive` probes again after such scans. Processes that were reaped are gone then (ESRCH), and the group reads ended. A fork chain still holds the id, so the group reads alive, and the wait times out with `HOST_TIMEOUT` instead. Scans that show only zombies still read the group ended, because under a PID 1 that never reaps the zombies of a killed group stay. So under such a PID 1, a freeze that misses a chain still lets `destroy` record destroyed. The model leaves that case out: `current-unseen-misses` runs without `ZombiesInView`. In the model, the environment constant `FreezeMisses` makes every freeze of an `Unseen` group miss, as when a SIGCONT from another process comes before each judgement, and `ProbeFindsUnseen` is the second probe. The probe of a group without a token (`ProbeSees`) now reads the program's processes alive under `Unseen` only through that probe, as the code does. `current-unseen-misses` checks every rule with `FreezeMisses`, and `mutant-WaitProbesUnseenGroup-unseen-misses` must violate R11. The unit tests "is alive while no scan shows a member and the probe finds the id" and "on linux, reads a group ended when no scan shows a member and the second probe finds none" in `test/unit/host/programGroup.test.ts` cover both reads. + ## When you change covered code on purpose 1. Read the diff of every item that `STALE` lists, and the commits that the check prints. For a change that is not committed yet, read `git diff`. diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index d3cdea61..a9cc4e08 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -33,6 +33,7 @@ "RecordsProgramSync": true, "ProvesGroupOwnership": true, "FreezesUnseenGroup": true, + "WaitProbesUnseenGroup": true, "FallbackNeedsFolder": true, "UnsharedGroupReadsUnknown": true, "TokenNamesProgram": true, @@ -120,11 +121,11 @@ "src/host/programGroup.ts#procHidesOtherUsers": "214f60a56d6573fa", "src/host/programGroup.ts#groupHasLiveProcess": "1d8026f335463a72", "src/host/programGroup.ts#scanGroup": "babc9d5767424243", - "src/host/programGroup.ts#isProcessGroupAlive": "ce1b8fca10085d51", + "src/host/programGroup.ts#isProcessGroupAlive": "cb20b5d3ec5d2979", "src/host/programGroup.ts#killProcessGroupBestEffort": "6d5d47cb5697681b", "src/host/programGroup.ts#signalProcessGroup": "c5a3a84361b67aa1", "src/host/programGroup.ts#isProgramGroupAlive": "f6fe01a280824f82", - "src/host/programGroup.ts#stopProgramGroup": "45733f4c2786197c", + "src/host/programGroup.ts#stopProgramGroup": "bbdb4374697df170", "src/host/programGroup.ts#procShowsOwnPidSpace": "ac852506311bb328", "src/host/rpcClient.ts#toTransportCliError": "dd6531349c62bcbd", "src/host/sessionState.ts#SessionState.setDimensions": "08c4f06122d157e9", @@ -147,9 +148,9 @@ "src/host/hostMain.ts#runHost(final try)": "e0615a9709fefb67", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "cd8639012467f13e", - "skill:scripts/facts.mjs": "e4e67f62f1c1853b", - "skill:scripts/check.sh": "17f2ce5bd1b1b090" + "skill:model/SessionLifecycle.tla": "9d2f5e19d5de78d2", + "skill:scripts/facts.mjs": "85928ae0e99639e2", + "skill:scripts/check.sh": "81d1f6f959f1dfca" }, "callSites": { "writeManifest": [ diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index 7906292c..3c66b8fc 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -137,6 +137,9 @@ CONSTANTS ProvesHostPid, \* lifecycle.ts, hostRecord.ts: destroy --force \* kills the host only while its pid shows the \* boot id and start time that host.json holds + WaitProbesUnseenGroup, \* programGroup.ts: isProcessGroupAlive probes + \* the group again when no scan shows a member, + \* and reads it alive while the probe finds it FreezesUnseenGroup, \* programGroup.ts: stopProgramGroup sends \* SIGSTOP to a group that no scan shows and \* judges it again @@ -150,6 +153,10 @@ CONSTANTS Unseen, \* the environment: no scan of /proc shows a \* live process of the program, as for a fork \* chain whose processes each live about 2 ms + FreezeMisses, \* the environment: with Unseen, no freeze of + \* stopProgramGroup brings a member into view, + \* as when a SIGCONT from another process comes + \* before each judgement ZombiesInView, \* the environment: with Unseen, the scans show \* zombies of the program's group, as under a \* PID 1 that never reaps @@ -173,6 +180,7 @@ CONSTANTS ASSUME MaxListReconciles \in 1..3 ASSUME Token \in BOOLEAN ASSUME Unseen \in BOOLEAN +ASSUME FreezeMisses \in BOOLEAN ASSUME ZombiesInView \in BOOLEAN ASSUME OtherPidSpace \in BOOLEAN ASSUME Win32 \in BOOLEAN @@ -197,7 +205,8 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, GcKeepsLiveGroup, ReconcileRepairsDestroyed, ReconcileRepairsMarked, TokenNamesProgram, ReusedIdReadsGone, ProvesHostPid, CreateRecordsHost, - FreezesUnseenGroup, UnsharedGroupReadsUnknown} : b \in BOOLEAN + FreezesUnseenGroup, WaitProbesUnseenGroup, + UnsharedGroupReadsUnknown} : b \in BOOLEAN Readers == {"gc", "list"} \* the two processes that run reconcileSession \* The group that a kill went through, and that the wait after it probes: @@ -394,7 +403,8 @@ NoKill == UNCHANGED <> ProvenKill == IF ~TokenNamesProgram THEN NoKill ELSE IF ProvesGroupOwnership /\ reused THEN NoKill - ELSE IF Unseen /\ ~FreezesUnseenGroup /\ ~reused /\ ~foreign THEN NoKill + ELSE IF Unseen /\ (~FreezesUnseenGroup \/ FreezeMisses) /\ ~reused + /\ ~foreign THEN NoKill ELSE KillsGroupId \* Without a token, readProgramGroup falls back to the childPid of the @@ -426,8 +436,14 @@ GroupAlive == prog \/ foreign \* isProcessGroupAlive probes kill(-pgid, 0): every process with that group \* id reads alive, also one of an unrelated group that took it. EPERM, when \* every process left belongs to another user, reads alive only with -\* ProbeCountsDeniedGroup. -ProbeSees == prog \/ left \/ reused \/ (ProbeCountsDeniedGroup /\ foreign) +\* ProbeCountsDeniedGroup. When the probe finds the group, the scans after it +\* decide: with Unseen they show no process of the program, and with +\* WaitProbesUnseenGroup a second probe that still finds the group reads it +\* alive. Scans that show only zombies read the group ended either way. +ProbeFindsUnseen == WaitProbesUnseenGroup /\ ~ZombiesInView +ProbeSees == + \/ (prog \/ left) /\ (~Unseen \/ ProbeFindsUnseen) + \/ reused \/ (ProbeCountsDeniedGroup /\ foreign) \* isProgramGroupAlive in waitForProcessesToExit, for the group that the \* kill before it went through. With a token it reads the group alive while @@ -441,9 +457,11 @@ ProbeSees == prog \/ left \/ reused \/ (ProbeCountsDeniedGroup /\ foreign) \* TokenNamesProgram no member carries the recorded autogroup, so the group \* reads gone. Without ReusedIdReadsGone a group that took the id reads \* alive, because its members carry another autogroup. With Unseen the scans -\* show no process of the program, and the probe after them reads the -\* group gone, since the wait does not freeze it. -GroupSeen(kind) == +\* show no process of the program, so the group reads gone, and the probe +\* after them decides (ProbeFindsUnseen). GroupJudged leaves out that probe +\* of a group with a token: gc judges such a group with its own probe +\* (GcSeesGroup). +GroupJudged(kind) == /\ KillsProgramGroup /\ \/ kind = "proven" /\ TokenNamesProgram /\ (((prog \/ left) /\ ~Unseen) \/ foreign) @@ -451,6 +469,11 @@ GroupSeen(kind) == \/ kind = "bare" /\ ProbeSees \/ kind = "numeric" /\ FallbackReaches /\ ProbeSees +GroupSeen(kind) == + \/ GroupJudged(kind) + \/ /\ KillsProgramGroup /\ kind = "proven" + /\ Unseen /\ ProbeFindsUnseen /\ (prog \/ left) + \* The group as destroy and reconcile see it. With OtherPidSpace no scan and \* no probe of theirs shows the program's processes: a group with a token \* reads gone, and gets no kill, because no member is in view. @@ -1240,7 +1263,7 @@ GcReadsReconciled == \* often. GcSeesGroup == /\ ~OtherPidSpace /\ ~Refused - /\ \/ GroupSeen("proven") + /\ \/ GroupJudged("proven") \/ /\ GcProbesUnseenGroup /\ Unseen /\ (prog \/ left) /\ (~ZombiesInView \/ GcFreezesUnseenGroup) diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index c09d2607..48988076 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/check.sh +++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh @@ -166,7 +166,7 @@ TERMINAL=$(node -e ' const c = JSON.parse(require("node:fs").readFileSync(process.argv[1], "utf8")).constants; console.log("{" + c.Terminal.map((s) => JSON.stringify(s)).join(", ") + "}"); ' "$OUT/facts.json") -GUARDS="GcSkipsNonCollectable GcFinalCheck GcKeepsLiveGroup GcProbesUnseenGroup GcFreezesUnseenGroup ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed ReconcileRepairsMarked CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid CreateRecordsHost FreezesUnseenGroup UnsharedGroupReadsUnknown HostChecksCreateFailed HostPollsCreateFailed CreateRetriesMarker ForceSkipsUnreadableGroup" +GUARDS="GcSkipsNonCollectable GcFinalCheck GcKeepsLiveGroup GcProbesUnseenGroup GcFreezesUnseenGroup ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed ReconcileRepairsMarked CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid CreateRecordsHost FreezesUnseenGroup UnsharedGroupReadsUnknown HostChecksCreateFailed HostPollsCreateFailed CreateRetriesMarker ForceSkipsUnreadableGroup WaitProbesUnseenGroup" # One "Guard=TRUE|FALSE" word per guard, read from the code by facts.mjs. FACTS_LINE=$(node -e ' const c = JSON.parse(require("node:fs").readFileSync(process.argv[1], "utf8")).constants; @@ -195,6 +195,10 @@ UNSEEN=FALSE # ZOMBIES: whether, with UNSEEN, the scans show zombies of the program's # group, as under a PID 1 that never reaps. ZOMBIES=FALSE +# MISSES: whether, with UNSEEN, no freeze of stopProgramGroup brings a +# member into view, as when a SIGCONT from another process comes before +# each judgement. +MISSES=FALSE # OTHER: whether destroy, list and gc run in another pid space than the host. OTHER=FALSE # WIN32: whether SIGTERM ends the host at once, as on Windows. @@ -224,6 +228,7 @@ write_run() { done echo " Token = $TOKEN" echo " Unseen = $UNSEEN" + echo " FreezeMisses = $MISSES" echo " ZombiesInView = $ZOMBIES" echo " OtherPidSpace = $OTHER" echo " Win32 = $WIN32" @@ -283,13 +288,20 @@ write_run mutant-ShutdownBothChecks violated TerminalIsFinal "ShutdownChecksComm # group is frozen. UNSEEN=TRUE write_run current-unseen pass "$RULES" "" "the code with a program that no scan shows: every rule holds" -write_run mutant-FreezesUnseenGroup-unseen violated DestroyedProgramStopped "FreezesUnseenGroup=FALSE" "without the freeze, the kill finds no member in view, and destroy records destroyed while a fork chain runs" DestroyedProgramStopped +# The wait probes the group that no scan shows, so the freeze and the probe +# each keep destroy from recording destroyed while the chain runs. +write_run mutant-UnseenBothGuards-unseen violated DestroyedProgramStopped "FreezesUnseenGroup=FALSE WaitProbesUnseenGroup=FALSE" "with neither the freeze nor the wait's probe, the kill finds no member in view, and destroy records destroyed while a fork chain runs" DestroyedProgramStopped write_run mutant-GcProbesUnseenGroup-unseen violated RemovedSessionStopped "GcProbesUnseenGroup=FALSE" "without the probe, gc removes program.json while a fork chain that the program left runs" RemovedSessionStopped # Under a PID 1 that never reaps, the chain also leaves zombies in view. # With every guard, that changes nothing, so current-unseen covers it. ZOMBIES=TRUE write_run mutant-GcFreezesUnseenGroup-unseen-zombies violated RemovedSessionStopped "GcFreezesUnseenGroup=FALSE" "without the freeze, gc reads a fork chain behind its zombies ended and removes program.json while it runs" RemovedSessionStopped ZOMBIES=FALSE +# Every freeze misses the chain. The wait then times out. +MISSES=TRUE +write_run current-unseen-misses pass "$RULES" "" "the code with a fork chain that every freeze misses: every rule holds" +write_run mutant-WaitProbesUnseenGroup-unseen-misses violated DestroyedProgramStopped "WaitProbesUnseenGroup=FALSE" "without the probe, the wait after a missed freeze reads the chain ended, and destroy records destroyed while it runs" DestroyedProgramStopped +MISSES=FALSE UNSEEN=FALSE # destroy, list and gc run without /proc, or in another pid namespace or on diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index e3d46b46..d5924f92 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -1273,14 +1273,33 @@ function ownershipFacts() { signalParam === "signal: 'SIGSTOP' | 'SIGCONT'" && !stray, FreezesUnseenGroup: freezeFacts(stop.body), + WaitProbesUnseenGroup: waitProbeFacts(), }; } +// isProcessGroupAlive, which every wait reads through isProgramGroupAlive, +// probes the group again when its probe found the group but no scan showed +// a member, live or zombie, and reads the group alive while that probe finds +// it. Without the second probe it reads such a group ended. +function waitProbeFacts() { + const module = 'src/host/programGroup.ts'; + const alive = requireDeclaration(module, 'isProcessGroupAlive').body + .statements; + return ( + normalize(alive.at(-1)?.getText() ?? '') === + 'return groupHasLiveProcess(pgid) ?? probeFindsGroup(pgid);' && + normalize(requireDeclaration(module, 'probeFindsGroup').body.getText()) === + "{ try { process.kill(processGroupTarget(pgid), 0); return true; } catch (error) { if (hasErrorCode(error, 'ESRCH')) { return false; } if (hasErrorCode(error, 'EPERM')) { return true; } throw error; } }" + ); +} + // In stopProgramGroup's loop, each judgement that gets no kill and is not // unproven sends SIGSTOP to the group and judges again: gone, unknown, and // owned with a witness that ended before its read. So a member that a scan // never shows, or that ends between two reads, stops and stays in view, -// while /proc names this process by its pid. The finally block sends a +// while /proc names this process by its pid. Before the first freeze, a +// group that shows a stopped member gets none, so the SIGCONT cannot resume +// a member that job control stopped. The finally block sends a // frozen group that got no kill SIGCONT, also when a scan throws. function freezeFacts(body) { const guarded = body.statements.find(ts.isTryStatement); @@ -1300,13 +1319,14 @@ function freezeFacts(body) { before.at(-2) === 'let frozen = false;' && before.at(-1) === 'let killed = false;' && guarded.tryBlock.statements.length === 1 && - st.length === 6 && + st.length === 7 && st[1] === "if ( judgement.verdict === 'unproven' || (judgement.verdict === 'unknown' && !judgement.running) ) { return; }" && st[2].startsWith("if (judgement.verdict === 'owned') {") && st.slice(3).join('\n') === [ 'if (!procShowsOwnPidSpace()) { return; }', + 'if (!frozen && showsStoppedMember(group.pid)) { return; }', "frozen = signalProcessGroup(group.pid, 'SIGSTOP') || frozen;", 'if (!frozen) { return; }', ].join('\n') && diff --git a/docs/USAGE.md b/docs/USAGE.md index 463c096e..da0d0456 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -314,7 +314,7 @@ agent-tty record diff --at-seq-a 0 --json `destroy` ends the session's program and every process that the program left in its process group, then records the session as `destroyed`. On Linux it also ends those processes when the program has already exited or the session has failed. -A group whose processes each fork their successor and end too fast for any scan of `/proc` to show or read one, a fork chain, gets SIGSTOP first. Its stopped processes stay in view, so `destroy` can prove the group and kill it. A frozen group that agent-tty cannot prove is the session's gets SIGCONT. +A group whose processes each fork their successor and end too fast for any scan of `/proc` to show or read one, a fork chain, gets SIGSTOP first. Its stopped processes stay in view, so `destroy` can prove the group and kill it. A frozen group that agent-tty cannot prove is the session's gets SIGCONT. When the freeze misses a fork chain, as when another process resumes it before each check, the wait still finds the group id, and `destroy` fails with `HOST_TIMEOUT` instead of recording the session as `destroyed`. Under a PID 1 that never reaps, a group whose scans show only zombies reads ended, so there such a missed chain can outlive a `destroy` that reports success. `destroy --force` kills the host and the program's group without asking the host first. When a read of the program's group fails with an error that every later read repeats, such as `program.json` that refuses the read (EACCES) or a `/proc` scan that fails (EIO), `gc` keeps the session and reports "failed to check the session's program group (destroy --force removes it)", or "failed to reconcile session (destroy --force removes it)" for a session whose host died. Those errors are EACCES, EPERM, EIO, EISDIR, ENOTDIR, ELOOP and ENAMETOOLONG. A plain `destroy` fails on the same read. When the read of `program.json` or the first check of the group fails that way twice, 100 ms apart, `destroy --force` stops the host alone, without the group, and records the session as `destroyed` once the host has ended, so the next `gc` removes it. A process that the program left can outlive such a `destroy --force`. When the second read passes, `destroy --force` stops the group as usual. A read that fails after that first check, a group that reads alive, or a host that does not end (`HOST_TIMEOUT`) still fails it. Other errors, such as EMFILE, ENOMEM or EAGAIN, can pass, so `gc` gives no such hint and `destroy --force` fails on them too. A `host.json` that cannot be read counts as missing, so the group reads as out of view: `destroy --force` fails with `HOST_TIMEOUT`, and `gc` removes the session, as in another pid namespace. `list`, `inspect`, `destroy` and `gc` reconcile a session whose host died: they kill the program's group and record the session as `failed` (or `exited` or `destroyed`). @@ -367,7 +367,7 @@ Limits: 1. `destroy` does not kill a process that has left the program's process group. A process leaves the group when it calls `setsid` (for example `setsid cmd` or a daemon), or when an interactive shell with job control runs it as a job (for example `cmd &` typed into `bash -i`). Stop such a process yourself, or keep it in the program's group. 2. Some sessions have no autogroup record: sessions on macOS and Windows, on Linux kernels without autogroups (`/proc/self/autogroup` is missing), on Linux when `/proc` refuses to show the autogroup, the boot id or the host's pid namespace at start-up, and sessions that an agent-tty version without `program.json` created. For these sessions, `destroy --force`, reconcile and the host's own kill at shutdown or at the idle time-out kill the process group (on Windows, the process) that `session.json` names, without the check, so such a kill can reach an unrelated process that took the group id after the program's group ended. `destroy` of a session whose program has already exited kills nothing. A `program.json` that agent-tty cannot read as a record, for example one that a newer version wrote, proves nothing: `destroy` and reconcile kill nothing for that session. -3. The check and the kill are separate system calls, a few microseconds apart. If every process of the group exits and an unrelated process takes the group id in that time, the kill reaches the unrelated process. No system call kills a process group through a handle, so this window remains. A group that no scan shows, or whose process ends while agent-tty reads it, gets SIGSTOP before each check and SIGCONT when the checks fail. `gc` sends the same two signals to a group whose scans show only zombies while its id still names a process (see item 5). A CLI whose `/proc` belongs to another pid namespace sends no SIGSTOP. If the unrelated group is a job of an interactive shell, the shell reports the job as stopped, and after the SIGCONT the job runs in the background. If agent-tty itself dies between the two signals (SIGKILL, SIGINT, SIGTERM, SIGHUP, or the out-of-memory killer), an unrelated group that took the id stays stopped, and a later `destroy` does not resume it. Resume it with `kill -CONT -- -`, where `` is the Child PID that `inspect` shows. +3. The check and the kill are separate system calls, a few microseconds apart. If every process of the group exits and an unrelated process takes the group id in that time, the kill reaches the unrelated process. No system call kills a process group through a handle, so this window remains. A group that no scan shows, or whose process ends while agent-tty reads it, gets SIGSTOP before each check and SIGCONT when the checks fail. A group that shows a process that job control stopped (`kill -STOP`, or Ctrl-Z in a shell) gets no SIGSTOP, so that SIGCONT cannot resume the process. `gc` sends the same two signals to a group whose scans show only zombies while its id still names a process (see item 5). A CLI whose `/proc` belongs to another pid namespace sends no SIGSTOP. If the unrelated group is a job of an interactive shell, the shell reports the job as stopped, and after the SIGCONT the job runs in the background. If agent-tty itself dies between the two signals (SIGKILL, SIGINT, SIGTERM, SIGHUP, or the out-of-memory killer), an unrelated group that took the id stays stopped, and a later `destroy` does not resume it. Resume it with `kill -CONT -- -`, where `` is the Child PID that `inspect` shows. 4. The host writes `program.json` a few milliseconds after it starts the program. We timed 150 `create` calls on Linux, from the return of node-pty's spawn to the renamed `program.json`, at 1-minute load averages of 38 to 83: the median was 2.8 ms, the 90th percentile 4.3 ms, and the longest 66 ms. If the host dies in that window and the program ignores the hang-up signal, no file names the program, and `destroy` cannot end it. 5. `gc` kills nothing. It keeps the folder of a session that is not `destroyed` only while it proves that the program's group runs: the autogroup record in `program.json` proves that a live process of the group is the program's, or the group id still names a process that no scan of `/proc` shows, such as a fast fork chain. When the scans show only zombies of the group while its id still names a process, as for a fork chain under a PID 1 that never reaps, `gc` sends the group SIGSTOP, checks it again, and sends SIGCONT, up to twice in each of up to ten checks of the group, and it keeps the session only when such a check proves the group. A group that has ended gets all 20 frozen checks: with about 2,300 processes in `/proc`, they took about 3.5 s at a load of 90. Another `gc` or a `destroy` that runs at the same time can send SIGCONT before a frozen check. Only when that happens before all 20 of them can a live process of the chain escape every scan, and `gc` then removes the folder of a session whose group still runs. A kept session gets the reason "the session's program group still runs (destroy ends it)". When `gc` cannot check the group, it removes `program.json` with the folder, as it does without an autogroup record (see item 2). That happens in another pid namespace than the one that `host.json` names, for example after a container restart that keeps the agent-tty home, when `host.json` cannot be read, and when `/proc` refuses the boot id or the autogroup of a live process of the group, or hides the processes of other users. Otherwise such a session would stay forever, because no `destroy` can prove its group gone. A process that the program left can then no longer be stopped by agent-tty. Run `destroy` before `gc` when a program can leave processes behind. 6. Two cases where agent-tty cannot run the check end differently from a session that stays running: diff --git a/src/host/README.md b/src/host/README.md index 4384014e..8ff6b841 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -26,7 +26,7 @@ - `reconcileSession(sessionDirectory)` moves a non-terminal session to a terminal status when its host process is gone. [lifecycle.ts:reconcileSession] - `captureProgram(pid)` returns a `ProgramRecord` (`version`, `pid`, `bootId`, `autogroup`) for the program that the host just spawned, and `writeProgramRecord(sessionDirectory, record)` writes it to `program.json`. `bootId` is a string and `autogroup` a number, or both are `null`. [programGroup.ts:captureProgram] [programGroup.ts:writeProgramRecord] - `readProvenProgramGroup(sessionDirectory)` returns the `program.json` record when it has a token and `sharesHostPids` reads true, the unshared group (below) when it has a token and `sharesHostPids` reads false, else `null`. `readProgramGroup(sessionDirectory, childPid)` returns the same for a record with a token, else `{ childPid, sessionDirectory }`, or `null` when `childPid` is `null` or, on Linux, when `host.json` names another pid namespace or machine id than the CLI's (`sharesHostPids`). For a record with a token where `sharesHostPids` reads false, which includes a missing `host.json`, a CLI that cannot read `/proc/self/ns/pid` and a CLI whose `/proc/self` does not name its own pid, both return the unshared group `{ unshared: true }`: no scan or probe of this process shows the program's processes, so `isProgramGroupAlive` reads it alive and `stopProgramGroup` sends it nothing. A `program.json` that does not validate reads as `null` in both, so it gets no kill and no throw. [programGroup.ts:readProgramRecord] [programGroup.ts:readProvenProgramGroup] [programGroup.ts:readProgramGroup] [hostRecord.ts:sharesHostPids] -- `stopProgramGroup(group)` SIGKILLs the group when the record proves it. A group that no scan shows gets SIGSTOP and another judgement, at each of up to 5 judgements while `/proc/self` names this process's pid, and SIGCONT when it gets no kill. `isProgramGroupAlive(group)` reports whether the group still holds a process that the kill would target. `judgeProgramGroup(record, bootId, rows)` is the pure decision: `owned`, `gone`, `unproven` or `unknown`. `parseProcStat` and `parseAutogroup` parse `/proc//stat` and `/proc//autogroup`. `parseAutogroup` returns `null` for text that names no autogroup, and a member whose autogroup file cannot be read or parsed carries no token. [programGroup.ts:stopProgramGroup] [programGroup.ts:isProgramGroupAlive] [programGroup.ts:judgeProgramGroup] [programGroup.ts:parseProcStat] +- `stopProgramGroup(group)` SIGKILLs the group when the record proves it. A group that no scan shows, or whose member ends between two reads (its stat and its autogroup, or the witness and its re-read), gets SIGSTOP and another judgement, at each of up to 5 judgements while `/proc/self` names this process's pid, and SIGCONT when it gets no kill. A group that shows a member that job control or a tracer stopped gets no SIGSTOP before its first freeze, so the SIGCONT cannot resume that member. `isProgramGroupAlive(group)` reports whether the group still holds a process that the kill would target. When its probe `kill(-pgid, 0)` finds the group but no scan shows a member, live or zombie, `isProcessGroupAlive` probes again: a group whose processes were reaped meanwhile reads ended, and one that still holds the id, such as a fork chain that a freeze missed, reads alive. Scans that show only zombies read the group ended. `judgeProgramGroup(record, bootId, rows)` is the pure decision: `owned`, `gone`, `unproven` or `unknown`. `parseProcStat` and `parseAutogroup` parse `/proc//stat` and `/proc//autogroup`. `parseAutogroup` returns `null` for text that names no autogroup, and a member whose autogroup file cannot be read or parsed carries no token. [programGroup.ts:stopProgramGroup] [programGroup.ts:isProgramGroupAlive] [programGroup.ts:judgeProgramGroup] [programGroup.ts:parseProcStat] - `captureHost(pid)` returns a `HostRecord` (`version`, `pid`, `bootId`, `startTicks`, `pidNamespace`, `timeNamespace`, `machineId`) on Linux when `/proc` shows the process and the boot id, else `null`. `machineId` is the first of `/etc/machine-id` and `/var/lib/dbus/machine-id` that holds 32 hex characters, else `null`. A record without `timeNamespace` and `machineId`, which a build between #260 and #267 wrote, still reads, and only the checks of those two fields are skipped. `writeHostRecord(sessionDirectory, record)` writes it as `host.json`, and `readHostRecord(sessionDirectory)` returns it, or `null` when it is missing or unreadable. `judgeHost(pid, record)` returns `dead` only when no process has the pid, a zombie has it, or the record names another boot id or start time, `alive` when both match, and `unknown` otherwise: also off Linux for a pid that exists, for a CLI in another pid namespace or on another machine than the record names, and, instead of a start time mismatch, for a CLI in another time namespace. [hostRecord.ts:captureHost] [hostRecord.ts:writeHostRecord] [hostRecord.ts:readHostRecord] [hostRecord.ts:judgeHost] - `SessionState` holds the host's in-memory `SessionRecord` (type from `src/protocol/schemas.ts`). Methods: `snapshot`, `setChildPid`, `setDimensions`, `setFailureOrigin`, `requestDestroy`, `recordDestroyed` and `recordExit`. [sessionState.ts:SessionState] - `createSerialManifestWriter(path, snapshot, write?)` returns a function that writes `snapshot()` to `path`. The default `write` is `writeManifest` (`src/storage/manifests.ts`). `runHost` sends every manifest write through one such function. [manifestWriter.ts:createSerialManifestWriter] [hostMain.ts:runHost] diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index 9f47227f..e08e7995 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -435,6 +435,14 @@ function readProcessRow(pid: number): ProcessRow | null { return stat === null ? null : toProcessRow(stat); } +// Whether a scan shows a member of the group that job control or a tracer +// stopped. +function showsStoppedMember(pgid: number): boolean { + return readGroupMembers(pgid).some( + (row) => row.state === 'T' || row.state === 't', + ); +} + function readGroupMembers(pgid: number): ProcessRow[] { let entries: string[]; try { @@ -579,8 +587,11 @@ function isProcessGroupAlive(pgid: number): boolean { throw error; } - // None in view: the kill found processes that were reaped before the scan. - return groupHasLiveProcess(pgid) ?? false; + // None in view: the kill found processes that were reaped before the scan, + // or members of a fork chain that end before a scan reads them. A second + // probe tells them apart: reaped processes are gone, a fork chain still + // holds the id. Scans that show only zombies read the group ended. + return groupHasLiveProcess(pgid) ?? probeFindsGroup(pgid); } function killProcessGroupBestEffort(pgid: number): void { @@ -767,15 +778,17 @@ export function stopProgramGroup(group: ProgramGroup | null): void { } // A member that forks its successor and ends between scans is never in - // view. One that a scan shows can also end before its autogroup read - // (unknown, running) or before the witness is read again. SIGSTOP freezes - // the group, also a child that a member forks while the kernel delivers - // it, and a stopped member stays in view and cannot end, so a judgement - // that gets no kill and is neither unproven nor an unknown without a - // running member sends SIGSTOP and judges the frozen group again. A group - // that job control stopped, whose autogroup /proc refuses, gets no signal. Each such judgement sends SIGSTOP again, for a member that a + // view. One that a scan shows can also end between two reads: before its + // autogroup read (unknown, running) or before the witness is read again. + // SIGSTOP freezes the group, also a child that a member forks while the + // kernel delivers it, and a stopped member stays in view and cannot end, + // so a judgement that gets no kill and is neither unproven nor an unknown + // without a running member sends SIGSTOP and judges the frozen group + // again. Each such judgement sends SIGSTOP again, for a member that a // SIGCONT from elsewhere resumed. A frozen group that gets no kill gets - // SIGCONT, also when a scan throws. + // SIGCONT, also when a scan throws. So a group that shows a member that + // job control stopped before the first freeze gets no SIGSTOP: the + // SIGCONT would resume that member. let frozen = false; let killed = false; try { @@ -804,6 +817,9 @@ export function stopProgramGroup(group: ProgramGroup | null): void { if (!procShowsOwnPidSpace()) { return; } + if (!frozen && showsStoppedMember(group.pid)) { + return; + } frozen = signalProcessGroup(group.pid, 'SIGSTOP') || frozen; if (!frozen) { return; diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index 71434ebf..26322460 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -704,10 +704,12 @@ describe('a program group without a token', () => { expect(isProgramGroupAlive(group)).toBe(true); }); + // ['ok', []]: no scan shows a member while the probes find the id, as for + // a fork chain whose members end before a scan reads them. it.each([ ['ok', ['Z', 'X'], false], ['ok', ['Z', 'S'], true], - ['ok', [], false], + ['ok', [], true], ['EPERM', ['Z'], false], ['EPERM', ['R'], true], ['EPERM', [], true], @@ -722,6 +724,24 @@ describe('a program group without a token', () => { }, ); + // The probe can find processes that are reaped before the scans. The + // probe after the scans then finds none. + it('on linux, reads a group ended when no scan shows a member and the second probe finds none', () => { + Object.defineProperty(process, 'platform', { value: 'linux' }); + procShowsGroup(); + let probes = 0; + vi.spyOn(process, 'kill').mockImplementation(() => { + probes += 1; + if (probes > 1) { + throw errno('ESRCH'); + } + return true; + }); + + expect(isProgramGroupAlive(group)).toBe(false); + expect(probes).toBe(2); + }); + // A process whose main thread called pthread_exit shows Z while another // of its threads runs. it.each([ @@ -1444,6 +1464,23 @@ describe('a program group with a token, as a faked /proc shows it', () => { expect(kill).not.toHaveBeenCalled(); }); + // A member that job control stopped would resume at the SIGCONT after a + // freeze, so a group that shows one gets no SIGSTOP before its first + // freeze, also beside a running member without an autogroup. + it('sends no signal to a group with a stopped member and a running member that shows no autogroup', () => { + procShowsTokenGroup('T', 'S'); + const tokenRead = autogroupFile.read; + autogroupFile.read = (file) => + file === '/proc/100/autogroup' || file === '/proc/101/autogroup' + ? '' + : (tokenRead?.(file) ?? null); + const kill = vi.spyOn(process, 'kill').mockReturnValue(true); + + stopProgramGroup(group); + + expect(kill).not.toHaveBeenCalled(); + }); + // The witness of a judgement can end before it is read again. it('freezes a group whose witness ends before it is read again, and kills it once a stopped member carries the token', () => { procShowsTokenGroup('S'); @@ -1454,8 +1491,9 @@ describe('a program group with a token, as a faked /proc shows it', () => { if (pid !== '100') { return live.get(pid); } - // Each judgement reads the member once, and the read of the witness - // after it finds the member ended. + // The judgement reads the member, the read of the witness after it + // finds the member ended, and the scan for a stopped member before + // the freeze reads it running. reads += 1; return reads % 2 === 0 ? errno('ENOENT') : live.get(pid); } @@ -1464,7 +1502,7 @@ describe('a program group with a token, as a faked /proc shows it', () => { stopProgramGroup(group); - expect(reads).toBe(2); + expect(reads).toBe(3); expect(kill.mock.calls).toEqual([ [-CHILD_PID, 'SIGSTOP'], [-CHILD_PID, 'SIGKILL'], @@ -1702,6 +1740,16 @@ describe('a program group with a token, as a faked /proc shows it', () => { expect(isProgramGroupAlive(group)).toBe(false); }); + // A fork chain whose members end before a scan reads them: a freeze that + // misses it, as after a SIGCONT from elsewhere, leaves the wait to the + // probe, which still finds the id. + it('is alive while no scan shows a member and the probe finds the id', () => { + procShowsTokenGroup(); + probeEnds('ok'); + + expect(isProgramGroupAlive(group)).toBe(true); + }); + it('is not alive when /proc hides other users and the probe finds no process', () => { procShowsTokenGroup(); procHooks.mountinfo = procMount('rw,hidepid=2'); From 738daeeef2984b8d330f6209ae3ab3bd2f320ae0 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Thu, 5 Nov 2026 00:38:07 +0000 Subject: [PATCH 4/6] fix(destroy): let a SIGSTOP take effect before the next judgement of the group The merge-group CI of #333 failed "gets no kill and reads alive when the autogroup of its member names no autogroup": the real group got two SIGSTOPs before its SIGCONT. A SIGSTOP takes effect only when the kernel next runs the member. A read of /proc//stat right after kill() showed the member not yet stopped in 1,984 of 2,000 tries here, and the stop took about 30 us (max 405 us) on an idle machine. A full /proc scan usually gives it that time, but on a loaded runner the next judgement read the member running and froze the group again. The code is safe either way: a member that still runs gets another SIGSTOP, within the 5 judgements, and the group still gets its SIGCONT. stopProgramGroup now waits STOP_SETTLE_MS (1 ms) after each SIGSTOP, so the next judgement mostly reads the frozen members stopped and fewer of the 5 judgements go to a stop that has not taken effect. On one CPU shared with four busy loops, the test saw a second SIGSTOP in 6 of 24 runs without the wait and in 1 of 24 with it. The test now accepts 1 to 5 SIGSTOPs before the SIGCONT. facts.mjs reads the wait as part of the freeze. --- .agents/skills/verify-session-lifecycle/coverage.json | 4 ++-- .../skills/verify-session-lifecycle/scripts/facts.mjs | 3 ++- src/host/programGroup.ts | 8 ++++++++ test/unit/host/programGroup.test.ts | 11 +++++++++-- 4 files changed, 21 insertions(+), 5 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 95ef451c..05ae0f31 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -125,7 +125,7 @@ "src/host/programGroup.ts#killProcessGroupBestEffort": "6d5d47cb5697681b", "src/host/programGroup.ts#signalProcessGroup": "c5a3a84361b67aa1", "src/host/programGroup.ts#isProgramGroupAlive": "f6fe01a280824f82", - "src/host/programGroup.ts#stopProgramGroup": "45733f4c2786197c", + "src/host/programGroup.ts#stopProgramGroup": "215a685d9337aeb3", "src/host/programGroup.ts#procShowsOwnPidSpace": "ac852506311bb328", "src/host/rpcClient.ts#toTransportCliError": "dd6531349c62bcbd", "src/host/sessionState.ts#SessionState.setDimensions": "08c4f06122d157e9", @@ -149,7 +149,7 @@ "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", "skill:model/SessionLifecycle.tla": "cd8639012467f13e", - "skill:scripts/facts.mjs": "f007734bffb0f4a1", + "skill:scripts/facts.mjs": "ff97d3d2dfab5811", "skill:scripts/check.sh": "17f2ce5bd1b1b090" }, "callSites": { diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index f54140a1..ea63f4b3 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -1300,7 +1300,7 @@ function freezeFacts(body) { before.at(-2) === 'let frozen = false;' && before.at(-1) === 'let killed = false;' && guarded.tryBlock.statements.length === 1 && - st.length === 6 && + st.length === 7 && st[1] === "if ( judgement.verdict === 'unproven' || (judgement.verdict === 'unknown' && !judgement.running) ) { return; }" && st[2].startsWith("if (judgement.verdict === 'owned') {") && @@ -1309,6 +1309,7 @@ function freezeFacts(body) { 'if (!procShowsOwnPidSpace()) { return; }', "frozen = signalProcessGroup(group.pid, 'SIGSTOP') || frozen;", 'if (!frozen) { return; }', + 'Atomics.wait(settleCell, 0, 0, STOP_SETTLE_MS);', ].join('\n') && normalize( requireDeclaration( diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index 9f47227f..d2692173 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -61,6 +61,13 @@ export type ProgramGroup = ProgramRecord | ChildPidGroup | UnsharedGroup; const CAPTURE_BUDGET_MS = 250; const STOP_ATTEMPTS = 5; +// A SIGSTOP takes effect only when the kernel next runs the member: about +// 30 us on an idle machine, longer under load. stopProgramGroup waits this +// long after each SIGSTOP, so the next judgement mostly reads the frozen +// members stopped. A member that still runs then gets another SIGSTOP. +const STOP_SETTLE_MS = 1; +const settleCell = new Int32Array(new SharedArrayBuffer(4)); + interface ProcStat { readonly pid: number; readonly state: string; @@ -808,6 +815,7 @@ export function stopProgramGroup(group: ProgramGroup | null): void { if (!frozen) { return; } + Atomics.wait(settleCell, 0, 0, STOP_SETTLE_MS); } } finally { if (frozen && !killed) { diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index 71434ebf..8373042a 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -1773,9 +1773,16 @@ describe.runIf(capturesToken)('a program group with a token', () => { // A running member without an autogroup can be a member of a fork // chain that ended between two reads, so the group gets SIGSTOP. Its // stopped member still shows no autogroup, so /proc refuses it, and - // the group gets SIGCONT. + // the group gets SIGCONT. A SIGSTOP takes effect only when the kernel + // runs the member, so under load a judgement can still read it + // running, and it gets another SIGSTOP. + const stops = kill.mock.calls.filter( + ([, signal]) => signal === 'SIGSTOP', + ).length; + expect(stops).toBeGreaterThanOrEqual(1); + expect(stops).toBeLessThanOrEqual(5); expect(kill.mock.calls).toEqual([ - [-pid, 'SIGSTOP'], + ...Array.from({ length: stops }, () => [-pid, 'SIGSTOP']), [-pid, 'SIGCONT'], ]); expect(isProgramGroupAlive(record)).toBe(true); From f650f76e18e788ae0c9912b4940f9622d5e7c6c0 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Thu, 5 Nov 2026 00:40:15 +0000 Subject: [PATCH 5/6] fix(gc): let the SIGSTOP of a frozen judgement take effect before the scan The same asynchronous stop as in stopProgramGroup: judgeFrozenGroup judged the group right after its SIGSTOP, so on a loaded machine the scan could read the chain still forking, and the frozen judgement read gone. It now waits STOP_SETTLE_MS (1 ms) inside the try, before the judgement, so the SIGCONT in the finally block still follows every SIGSTOP. An ended group costs 20 such waits, 20 ms, on top of its ten passes. --- .agents/skills/verify-session-lifecycle/coverage.json | 4 ++-- .agents/skills/verify-session-lifecycle/scripts/facts.mjs | 5 ++++- src/host/programGroup.ts | 2 ++ 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 8eba101f..ad480ee5 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -54,7 +54,7 @@ "src/cli/commands/gc.ts#defaultDependencies": "ae2347cdb778b488", "src/host/programGroup.ts#provenProgramGroupRuns": "7b50817618b4b769", "src/host/programGroup.ts#judgeGroupForGc": "fb133ba2739116d1", - "src/host/programGroup.ts#judgeFrozenGroup": "e3a6c281e3f579fc", + "src/host/programGroup.ts#judgeFrozenGroup": "8bfe9ea5c92a1c8f", "src/host/programGroup.ts#FROZEN_JUDGEMENTS": "d4eb06aa7addbaa9", "src/host/programGroup.ts#isUnreadableGroupError": "e2d852aa5b45cb53", "src/host/programGroup.ts#UNREADABLE_ERRNOS": "24de7f719ccf14be", @@ -150,7 +150,7 @@ "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", "skill:model/SessionLifecycle.tla": "9d2f5e19d5de78d2", - "skill:scripts/facts.mjs": "3baf20931a40c589", + "skill:scripts/facts.mjs": "36ed7de152b0c580", "skill:scripts/check.sh": "81d1f6f959f1dfca" }, "callSites": { diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 29bc664b..2b3a5e1a 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -1578,7 +1578,10 @@ function frozenJudgesTwice() { judged.catchClause === undefined && judged.finallyBlock !== undefined && statementsOf(judged.tryBlock).join('\n') === - 'verdict = judgeLiveGroup(group).verdict;' && + [ + 'Atomics.wait(settleCell, 0, 0, STOP_SETTLE_MS);', + 'verdict = judgeLiveGroup(group).verdict;', + ].join('\n') && statementsOf(judged.finallyBlock).join('\n') === "signalProcessGroup(group.pid, 'SIGCONT');" && normalize(decides?.getText() ?? '') === diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index f80c0572..4e55c9ad 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -740,6 +740,8 @@ function judgeFrozenGroup(group: ProvenRecord): boolean | null { } let verdict: GroupJudgement['verdict']; try { + // The SIGSTOP takes effect only when the kernel next runs a member. + Atomics.wait(settleCell, 0, 0, STOP_SETTLE_MS); verdict = judgeLiveGroup(group).verdict; } finally { signalProcessGroup(group.pid, 'SIGCONT'); From b6081873341f015f6ed67933860c463f20af5861 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Thu, 5 Nov 2026 00:40:29 +0000 Subject: [PATCH 6/6] docs(destroy): name the wait after each SIGSTOP in the README and SKILL --- .agents/skills/verify-session-lifecycle/SKILL.md | 2 +- src/host/README.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 4ba43cec..a4e900b1 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -549,7 +549,7 @@ kill -0 "$other" && echo alive # alive With a token, a kill needs a live member of the group in view, and a wait reads the group gone once no scan shows one. A program whose processes each fork their successor and end within about 2 ms, a fork chain, is almost never in view: by the time a scan reads a pid that its `/proc` listing showed, that process has ended, and the listing missed its successor. `stopProgramGroup` then killed nothing, the wait after it read the group gone, and `destroy` recorded `destroyed` while the chain ran (coder/agent-tty#244). -Now `stopProgramGroup` sends a group that `judgeLiveGroup` reads gone SIGSTOP and judges it again, until the loop's attempts run out. A scan can also show a member that ends before its autogroup read, so the judgement reads `unknown`, or a witness that ends before it is read again. Those judgements get SIGSTOP and another judgement too: every judgement that gets no kill freezes the group, except `unproven` and an `unknown` whose members without an autogroup are all stopped (`running` false) or whose boot id `/proc` refuses. A stopped member cannot end, so `/proc` refused its autogroup, and a group that job control stopped gets no signal. Before its first freeze, a group that shows any member that job control or a tracer stopped gets no SIGSTOP either (`showsStoppedMember`), so the SIGCONT after the judgements cannot resume that member beside a running one. Without that, a loaded CI runner saw `destroy` record `destroyed` after such a judgement while the chain ran. That freezes only a group id that a judgement of gone would freeze too, never one that reads `unproven`. Each judgement that freezes sends SIGSTOP again, so a member that a SIGCONT from elsewhere resumed stops again. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace, so `procShowsOwnPidSpace` reads false and no SIGSTOP goes out: the group id can name the CLI's own group there. The kernel delivers a group signal also to a child that a member forks during the delivery, so the whole chain stops, and a stopped process stays in view. The next judge finds a stopped member with the token, and the group gets the kill. A frozen group that gets no kill, because its members carry another autogroup, only zombies are left, `/proc` refuses the autogroup of its stopped member, or a scan throws, gets SIGCONT from a `finally` block. The model has no member that a scan shows and then cannot read, so it relies on this freeze. In the model, the constant `Unseen` hides every process of the program from the scans: without the guard the kill through the token kills nothing, and, without `WaitProbesUnseenGroup` (below), the wait reads the group gone. `current-unseen` checks every rule with `Unseen`, and `mutant-UnseenBothGuards-unseen`, without the freeze and the wait's probe, must violate R11. The integration test "destroy ends a fork chain that no scan of /proc shows" in `test/integration/lifecycle.test.ts` runs `test/fixtures/fork-chain.py` in a session. +Now `stopProgramGroup` sends a group that `judgeLiveGroup` reads gone SIGSTOP and judges it again, until the loop's attempts run out. A scan can also show a member that ends before its autogroup read, so the judgement reads `unknown`, or a witness that ends before it is read again. Those judgements get SIGSTOP and another judgement too: every judgement that gets no kill freezes the group, except `unproven` and an `unknown` whose members without an autogroup are all stopped (`running` false) or whose boot id `/proc` refuses. A stopped member cannot end, so `/proc` refused its autogroup, and a group that job control stopped gets no signal. Before its first freeze, a group that shows any member that job control or a tracer stopped gets no SIGSTOP either (`showsStoppedMember`), so the SIGCONT after the judgements cannot resume that member beside a running one. A SIGSTOP takes effect only when the kernel next runs a member (about 30 us idle, longer under load), so `stopProgramGroup` and gc's `judgeFrozenGroup` wait `STOP_SETTLE_MS` (1 ms) after each SIGSTOP before they judge, and a member that still runs gets another SIGSTOP within the 5 judgements. Without that, a loaded CI runner saw `destroy` record `destroyed` after such a judgement while the chain ran. That freezes only a group id that a judgement of gone would freeze too, never one that reads `unproven`. Each judgement that freezes sends SIGSTOP again, so a member that a SIGCONT from elsewhere resumed stops again. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace, so `procShowsOwnPidSpace` reads false and no SIGSTOP goes out: the group id can name the CLI's own group there. The kernel delivers a group signal also to a child that a member forks during the delivery, so the whole chain stops, and a stopped process stays in view. The next judge finds a stopped member with the token, and the group gets the kill. A frozen group that gets no kill, because its members carry another autogroup, only zombies are left, `/proc` refuses the autogroup of its stopped member, or a scan throws, gets SIGCONT from a `finally` block. The model has no member that a scan shows and then cannot read, so it relies on this freeze. In the model, the constant `Unseen` hides every process of the program from the scans: without the guard the kill through the token kills nothing, and, without `WaitProbesUnseenGroup` (below), the wait reads the group gone. `current-unseen` checks every rule with `Unseen`, and `mutant-UnseenBothGuards-unseen`, without the freeze and the wait's probe, must violate R11. The integration test "destroy ends a fork chain that no scan of /proc shows" in `test/integration/lifecycle.test.ts` runs `test/fixtures/fork-chain.py` in a session. ```sh id=$(node --import tsx src/cli/main.ts create --json -- sh -c "python3 test/fixtures/fork-chain.py 30 0.002 $PWD/beat & wait" | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))') diff --git a/src/host/README.md b/src/host/README.md index 3428b485..b8181e4a 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -26,7 +26,7 @@ - `reconcileSession(sessionDirectory)` moves a non-terminal session to a terminal status when its host process is gone. [lifecycle.ts:reconcileSession] - `captureProgram(pid)` returns a `ProgramRecord` (`version`, `pid`, `bootId`, `autogroup`) for the program that the host just spawned, and `writeProgramRecord(sessionDirectory, record)` writes it to `program.json`. `bootId` is a string and `autogroup` a number, or both are `null`. [programGroup.ts:captureProgram] [programGroup.ts:writeProgramRecord] - `readProvenProgramGroup(sessionDirectory)` returns the `program.json` record when it has a token and `sharesHostPids` reads true, the unshared group (below) when it has a token and `sharesHostPids` reads false, else `null`. `readProgramGroup(sessionDirectory, childPid)` returns the same for a record with a token, else `{ childPid, sessionDirectory }`, or `null` when `childPid` is `null` or, on Linux, when `host.json` names another pid namespace or machine id than the CLI's (`sharesHostPids`). For a record with a token where `sharesHostPids` reads false, which includes a missing `host.json`, a CLI that cannot read `/proc/self/ns/pid` and a CLI whose `/proc/self` does not name its own pid, both return the unshared group `{ unshared: true }`: no scan or probe of this process shows the program's processes, so `isProgramGroupAlive` reads it alive and `stopProgramGroup` sends it nothing. A `program.json` that does not validate reads as `null` in both, so it gets no kill and no throw. [programGroup.ts:readProgramRecord] [programGroup.ts:readProvenProgramGroup] [programGroup.ts:readProgramGroup] [hostRecord.ts:sharesHostPids] -- `stopProgramGroup(group)` SIGKILLs the group when the record proves it. A group that no scan shows, or whose member ends between two reads (its stat and its autogroup, or the witness and its re-read), gets SIGSTOP and another judgement, at each of up to 5 judgements while `/proc/self` names this process's pid, and SIGCONT when it gets no kill. A group that shows a member that job control or a tracer stopped gets no SIGSTOP before its first freeze, so the SIGCONT cannot resume that member. `isProgramGroupAlive(group)` reports whether the group still holds a process that the kill would target. When its probe `kill(-pgid, 0)` finds the group but no scan shows a member, live or zombie, `isProcessGroupAlive` probes again: a group whose processes were reaped meanwhile reads ended, and one that still holds the id, such as a fork chain that a freeze missed, reads alive. Scans that show only zombies read the group ended. `judgeProgramGroup(record, bootId, rows)` is the pure decision: `owned`, `gone`, `unproven` or `unknown`. `parseProcStat` and `parseAutogroup` parse `/proc//stat` and `/proc//autogroup`. `parseAutogroup` returns `null` for text that names no autogroup, and a member whose autogroup file cannot be read or parsed carries no token. [programGroup.ts:stopProgramGroup] [programGroup.ts:isProgramGroupAlive] [programGroup.ts:judgeProgramGroup] [programGroup.ts:parseProcStat] +- `stopProgramGroup(group)` SIGKILLs the group when the record proves it. A group that no scan shows, or whose member ends between two reads (its stat and its autogroup, or the witness and its re-read), gets SIGSTOP and another judgement, at each of up to 5 judgements while `/proc/self` names this process's pid, and SIGCONT when it gets no kill. A group that shows a member that job control or a tracer stopped gets no SIGSTOP before its first freeze, so the SIGCONT cannot resume that member. Each SIGSTOP is followed by a synchronous wait of `STOP_SETTLE_MS` (1 ms), because the stop takes effect only when the kernel next runs a member. `isProgramGroupAlive(group)` reports whether the group still holds a process that the kill would target. When its probe `kill(-pgid, 0)` finds the group but no scan shows a member, live or zombie, `isProcessGroupAlive` probes again: a group whose processes were reaped meanwhile reads ended, and one that still holds the id, such as a fork chain that a freeze missed, reads alive. Scans that show only zombies read the group ended. `judgeProgramGroup(record, bootId, rows)` is the pure decision: `owned`, `gone`, `unproven` or `unknown`. `parseProcStat` and `parseAutogroup` parse `/proc//stat` and `/proc//autogroup`. `parseAutogroup` returns `null` for text that names no autogroup, and a member whose autogroup file cannot be read or parsed carries no token. [programGroup.ts:stopProgramGroup] [programGroup.ts:isProgramGroupAlive] [programGroup.ts:judgeProgramGroup] [programGroup.ts:parseProcStat] - `captureHost(pid)` returns a `HostRecord` (`version`, `pid`, `bootId`, `startTicks`, `pidNamespace`, `timeNamespace`, `machineId`) on Linux when `/proc` shows the process and the boot id, else `null`. `machineId` is the first of `/etc/machine-id` and `/var/lib/dbus/machine-id` that holds 32 hex characters, else `null`. A record without `timeNamespace` and `machineId`, which a build between #260 and #267 wrote, still reads, and only the checks of those two fields are skipped. `writeHostRecord(sessionDirectory, record)` writes it as `host.json`, and `readHostRecord(sessionDirectory)` returns it, or `null` when it is missing or unreadable. `hostRecordError(sessionDirectory)` returns the error when the file exists but its read or its check fails, else `null`, so that the `HOST_TIMEOUT` of `destroySession` for an unshared group names `host.json` and that error instead of another pid namespace, and says to make the file readable only for EACCES or EPERM. `judgeHost(pid, record)` returns `dead` only when no process has the pid, a zombie has it, or the record names another boot id or start time, `alive` when both match, and `unknown` otherwise: also off Linux for a pid that exists, for a CLI in another pid namespace or on another machine than the record names, and, instead of a start time mismatch, for a CLI in another time namespace. [hostRecord.ts:captureHost] [hostRecord.ts:writeHostRecord] [hostRecord.ts:readHostRecord] [hostRecord.ts:hostRecordError] [hostRecord.ts:judgeHost] - `SessionState` holds the host's in-memory `SessionRecord` (type from `src/protocol/schemas.ts`). Methods: `snapshot`, `setChildPid`, `setDimensions`, `setFailureOrigin`, `requestDestroy`, `recordDestroyed` and `recordExit`. [sessionState.ts:SessionState] - `createSerialManifestWriter(path, snapshot, write?)` returns a function that writes `snapshot()` to `path`. The default `write` is `writeManifest` (`src/storage/manifests.ts`). `runHost` sends every manifest write through one such function. [manifestWriter.ts:createSerialManifestWriter] [hostMain.ts:runHost]