From 5ebe5da12d8ce4aa6864cddde253bbdef54340cb Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 08:08:23 +0000 Subject: [PATCH 01/17] fix(gc): freeze a group whose scans show only zombies before gc reads it ended Codex on #302: under a PID 1 that never reaps, a fork chain leaves its zombies in view while its live member escapes both scans, so gc read the group ended and removed program.json while the chain ran. judgeFrozenGroup now sends SIGSTOP, as stopProgramGroup does, judges the stopped group, and sends SIGCONT in a finally. The integration test runs the chain under the subreaper that never reaps. --- src/host/programGroup.ts | 19 ++++++++- test/integration/non-reaping-init.test.ts | 47 ++++++++++++++++++++++ test/unit/host/programGroup.test.ts | 49 +++++++++++++++++++++++ 3 files changed, 114 insertions(+), 1 deletion(-) diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index 798127ae..c4784cf3 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -639,7 +639,24 @@ function judgeGroupForGc(group: ProvenRecord): boolean | null { return false; } const live = groupHasLiveProcess(group.pid); - return live === null ? true : live ? null : false; + return live === null ? true : live ? null : judgeFrozenGroup(group); +} + +// The scans show only zombies of the group while the probe finds its id. +// Under a PID 1 that never reaps, the zombies of a fork chain stay, and its +// live member can escape both scans. SIGSTOP freezes the group, as in +// stopProgramGroup, and a stopped member stays in view, so a judgement of +// the frozen group decides. The group gets SIGCONT, also when a scan throws. +function judgeFrozenGroup(group: ProvenRecord): boolean | null { + if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { + return false; + } + try { + const { verdict } = judgeLiveGroup(group); + return verdict === 'owned' ? true : verdict === 'unknown' ? null : false; + } finally { + signalProcessGroup(group.pid, 'SIGCONT'); + } } function probeFindsGroup(pgid: number): boolean { diff --git a/test/integration/non-reaping-init.test.ts b/test/integration/non-reaping-init.test.ts index fd49f236..20c7d0f7 100644 --- a/test/integration/non-reaping-init.test.ts +++ b/test/integration/non-reaping-init.test.ts @@ -165,6 +165,53 @@ describe.runIf(process.platform === 'linux')( expect(destroy.status).toBe(0); }); + // Each process of the fork chain forks its successor and ends, and the + // subreaper never reaps it, so the chain leaves zombies in view while its + // live process escapes the scans. gc freezes such a group before it reads + // it ended. + it('gc keeps an exited session while a fork chain runs behind its zombies', async ({ + skip, + }) => { + const beat = join(testHome, 'beat'); + const recorded = join(testHome, 'sessions', '$AGENT_TTY_SESSION_ID'); + const sessionId = await createUnderSubreaper( + `trap "" HUP; python3 '${resolve('test/fixtures/fork-chain.py')}' 20 0.002 '${beat}' & ` + + `until [ -f "${recorded}/program.json" ]; do sleep 0.01; done; touch "$0"; exit 0`, + ); + const record = JSON.parse( + await readFile( + join(testHome, 'sessions', sessionId, 'program.json'), + 'utf8', + ), + ) as { bootId: unknown }; + if (record.bootId === null) { + skip('the host captured no session token'); + } + const deadline = Date.now() + 10_000; + while ( + inspectSession(testHome, sessionId).status !== 'exited' || + groupStates(pgid).filter((state) => state === 'Z').length < 200 + ) { + expect(Date.now()).toBeLessThan(deadline); + await sleep(100); + } + + const kept = runCli(['gc', '--json'], { AGENT_TTY_HOME: testHome }); + expect(kept.status).toBe(0); + expect(JSON.parse(kept.stdout)).toMatchObject({ + ok: true, + result: { removedSessionCount: 0 }, + }); + + const destroy = runCli(['destroy', sessionId, '--json'], { + AGENT_TTY_HOME: testHome, + }); + expect( + (JSON.parse(destroy.stdout) as { error?: unknown }).error, + ).toBeUndefined(); + expect(groupStates(pgid).every((state) => state === 'Z')).toBe(true); + }); + it('destroy ends a program whose killed background process stays a zombie', async () => { const sessionId = await createUnderSubreaper( 'trap "" HUP; sleep 300 & touch "$0"; wait', diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index 6d6f4460..b9aa086b 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -983,6 +983,55 @@ describe('a program group with a token, as a faked /proc shows it', () => { } }); + // Under a PID 1 that never reaps, the zombies of a fork chain stay in + // view while its live member escapes both scans. A stopped member stays + // in view, so gc freezes the group and judges it again. + it.each([ + { frozen: ['Z', 'T'], runs: true }, + { frozen: ['Z'], runs: false }, + ])( + 'freezes a group whose scans show only zombies, and reads it running: $runs when the frozen group shows $frozen', + async ({ frozen, runs }) => { + const directory = await recordedSession(); + try { + procShowsTokenGroup('Z'); + const signals: unknown[] = []; + vi.spyOn(process, 'kill').mockImplementation((_pid, signal) => { + signals.push(signal); + if (signal === 'SIGSTOP') { + procShowsTokenGroup(...frozen); + } + return true; + }); + + expect(await provenProgramGroupRuns(directory)).toBe(runs); + expect(signals).toEqual([0, 'SIGSTOP', 'SIGCONT']); + } finally { + await rm(directory, { recursive: true, force: true }); + } + }, + ); + + it('gives a frozen group SIGCONT when its judgement throws', async () => { + const directory = await recordedSession(); + try { + procShowsTokenGroup('Z'); + const signals: unknown[] = []; + vi.spyOn(process, 'kill').mockImplementation((_pid, signal) => { + signals.push(signal); + if (signal === 'SIGSTOP') { + procHooks.listError = errno('EIO'); + } + return true; + }); + + await expect(provenProgramGroupRuns(directory)).rejects.toThrow('EIO'); + expect(signals).toEqual([0, 'SIGSTOP', 'SIGCONT']); + } finally { + await rm(directory, { recursive: true, force: true }); + } + }); + // A member of a fork chain can end between its stat and its autogroup // read, so gc judges again. it('judges again after a member that ended before its autogroup read', async () => { From 5736dbae0e9cdca2e7b20b54c132c3a5ff92c533 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 08:11:16 +0000 Subject: [PATCH 02/17] feat(model): check gc's freeze of a fork chain behind its zombies The model gets the guard GcFreezesUnseenGroup and the environment constant ZombiesInView. With zombies in view the probe alone proves nothing, and gc sees the chain only through the freeze. mutant-GcFreezesUnseenGroup-unseen-zombies must violate R20. With every guard, ZombiesInView changes nothing, so current-unseen covers the pass run. ProvesGroupOwnership lets judgeFrozenGroup send SIGSTOP and SIGCONT, and the raw kill stays in stopProgramGroup. USAGE limits 3 and 5 name the two signals. --- .../skills/verify-session-lifecycle/SKILL.md | 11 ++--- .../model/SessionLifecycle.tla | 36 ++++++++++------ .../verify-session-lifecycle/scripts/check.sh | 11 ++++- .../scripts/facts.mjs | 42 ++++++++++++++----- docs/USAGE.md | 4 +- 5 files changed, 74 insertions(+), 30 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 8ea09871..6a65632f 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -42,7 +42,7 @@ The tool is TLC, the TLA+ model checker, pinned to release 1.7.4 by sha256. The Yes, when the diff changes any of these: - `src/host/lifecycle.ts`: `allocateSession` (and the order of its `launch` call and first manifest write), `launchHost`, `isProcessAlive`, the host proof (`readSessionHost`, `psShowsSessionHost`, `isHostAlive`, `hostMatches`, `killHostBestEffort`), `cliRunsInsideProgramSession` with `ownLinuxSessionId`, `ownProcessGroupId`, `controllingTerminal` and `sharesControllingTerminal`, `reconcileSession`, and `destroySession` with its local `stopLeftoversThenRecordDestroyed` and its helpers `recordDestroyed`, `stopSessionProcesses`, `readSessionManifestOrThrow`, `waitForTerminalManifest`, `waitForProcessesToExit` and `killProcessBestEffort`, and `removeDeadHostSocket`, which `gc` and `destroySession` call. -- `src/host/programGroup.ts`: the token capture (`captureProgram`, `captureToken`, `readAutogroup`, `parseAutogroup`, `parseProcStat`), the `/proc` reads (`readProcFileIfExists`, `readLiveThreadState`, `readProcStat`, `readShownProcStat`, `isRefusedRead`, `readBootId`), the record (`writeProgramRecord`, `readProgramRecord`, `readProvenProgramGroup`, `readProgramGroup`, `provenProgramGroupRuns` with its `GC_JUDGEMENTS` limit, `judgeGroupForGc`, `probeFindsGroup`), `procShowsOwnPidSpace`, the verdict (`judgeProgramGroup`, `readGroupMembers`), and the kill and the probe (`stopProgramGroup`, `isProgramGroupAlive`, `processGroupTarget`, `isProcessGroupAlive` with `groupHasLiveProcess` and `procHidesOtherUsers`, `killProcessGroupBestEffort`, `signalProcessGroup`). +- `src/host/programGroup.ts`: the token capture (`captureProgram`, `captureToken`, `readAutogroup`, `parseAutogroup`, `parseProcStat`), the `/proc` reads (`readProcFileIfExists`, `readLiveThreadState`, `readProcStat`, `readShownProcStat`, `isRefusedRead`, `readBootId`), the record (`writeProgramRecord`, `readProgramRecord`, `readProvenProgramGroup`, `readProgramGroup`, `provenProgramGroupRuns` with its `GC_JUDGEMENTS` limit, `judgeGroupForGc`, `judgeFrozenGroup`, `probeFindsGroup`), `procShowsOwnPidSpace`, the verdict (`judgeProgramGroup`, `readGroupMembers`), and the kill and the probe (`stopProgramGroup`, `isProgramGroupAlive`, `processGroupTarget`, `isProcessGroupAlive` with `groupHasLiveProcess` and `procHidesOtherUsers`, `killProcessGroupBestEffort`, `signalProcessGroup`). - `src/host/hostMain.ts`: `waitForManifestFromCreate`, `isSessionCommandable`, and in `runHost` the start-up statements (the manifest wait, the `hostPid === process.pid` check, the `host.json` write with `captureHost` and `writeHostRecord`, `createSerialManifestWriter`, `EventLog.open`, the create-failed marker check, `createPty`, `setChildPid`, `captureProgram`), `hangUpProgram` with its kill timer and the `SHUTDOWN_KILL_GRACE_MS` constant, `startIdlePolling` (the idle time-out), `initiateShutdown`, `startShutdown`, `handlePtyExit` with its wait for the program's group, `pty.onExit`, the `SIGTERM` handler, the `resize` and `destroy` handlers, and the last `try` block (the `program.json` write, the start-up manifest write and `rpcServer.listen`). - `src/host/manifestWriter.ts` `createSerialManifestWriter`. - `src/cli/commands/gc.ts` `gcSessions` and `defaultDependencies`, `src/cli/commands/create.ts` `runCreateCommand` with `waitForReadyHost`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`. @@ -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. On a CI runner with 4 vCPUs and the default `CHECK_JOBS` of 4 it takes about an hour, so CI runs it in four shares. Ten runs explore more than 20 million distinct states each, so `CHECK_JOBS=78` 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. On a CI runner with 4 vCPUs and the default `CHECK_JOBS` of 4 it takes about an hour, so CI runs it in four shares. Ten runs explore more than 20 million distinct states each, so `CHECK_JOBS=79` 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-five 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 thirty-six 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 78 times and prints one line per run. +3. It runs TLC 79 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. @@ -90,6 +90,7 @@ At the sync commit, the expected results are: | `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-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. | | `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` | pass | Without the guard, a reconcile skips a marked `failed` as it skips any terminal manifest. The reconcile that wrote that `failed` always repairs it in the model, because the model has no crash of a reconciling process, so no rule breaks. The unit tests in `test/unit/host/lifecycle.test.ts` cover the crash. | | `mutant-ReconcileSkipsTerminal` | pass | The re-read in `reconcileSession` also returns on a terminal manifest, so the first terminal return alone is redundant. | @@ -473,7 +474,7 @@ node -e 'console.log(require(process.argv[1]).status)' "$d/session.json" Without the guard, `gcSessions` removed the folder of every collectable session. A program that exits on its own can leave a process in its group, such as `sleep 300 &` after `trap "" HUP`, and the host does not kill at a normal exit. The rm deleted `program.json` with the folder, and that record is the only proof that the process is the program's, so no later command could stop it. -Now `gcSessions` calls `provenProgramGroupRuns` after its other checks and before the rm. It judges the group that `readProvenProgramGroup` gives, as the waits of `destroy` do, and gc skips the session with the reason "the session's program group still runs (destroy ends it)" while it proves the group, also under `--dry-run`: a live member carries the token. A read that throws skips the session too, with the error as the reason. A member of a fork chain can end between its stat and its autogroup read (`unknown`), or show up only after the judge's scans, so `judgeGroupForGc` reads such a judgement as inconclusive, and gc judges again, at most ten times. gc does not check a destroyed session, because `destroy` records destroyed only after a wait that read the group gone. A record without a token proves nothing, so gc removes such a session as before. gc never keeps a session that no command can remove: a group that gc cannot check proves nothing, and gc removes its session as before. That covers another pid space, where the group reads `unshared` (as after a container restart that keeps the home, when `host.json` names a pid namespace that no longer exists), and a `/proc` that refuses the boot id or the autogroup of a live member (`unknown`). So R20 holds only for a gc in the host's pid space, and `witness-WitnessUnsharedGcRemovesLeftover-otherspace` shows that a gc in another one removes an exited session while a process that the program left runs. gc sends no SIGSTOP, so a fork chain that no scan shows reads gone to the judge. So `provenProgramGroupRuns` also counts the group as running while the probe `kill(-pgid, 0)` finds its id and no scan shows a member, live or zombie (`GcProbesUnseenGroup`). An unrelated group that took the id is in view and reads `unproven`, so it does not keep the session. `mutant-GcProbesUnseenGroup-unseen` must violate R20. The integration tests "gc keeps an exited session while a process that the program left runs" and "... while a fork chain that the program left runs" in `test/integration/lifecycle.test.ts` cover both, and "gc removes an exited session whose host.json names another pid namespace" covers the restart. +Now `gcSessions` calls `provenProgramGroupRuns` after its other checks and before the rm. It judges the group that `readProvenProgramGroup` gives, as the waits of `destroy` do, and gc skips the session with the reason "the session's program group still runs (destroy ends it)" while it proves the group, also under `--dry-run`: a live member carries the token. A read that throws skips the session too, with the error as the reason. A member of a fork chain can end between its stat and its autogroup read (`unknown`), or show up only after the judge's scans, so `judgeGroupForGc` reads such a judgement as inconclusive, and gc judges again, at most ten times. gc does not check a destroyed session, because `destroy` records destroyed only after a wait that read the group gone. A record without a token proves nothing, so gc removes such a session as before. gc never keeps a session that no command can remove: a group that gc cannot check proves nothing, and gc removes its session as before. That covers another pid space, where the group reads `unshared` (as after a container restart that keeps the home, when `host.json` names a pid namespace that no longer exists), and a `/proc` that refuses the boot id or the autogroup of a live member (`unknown`). So R20 holds only for a gc in the host's pid space, and `witness-WitnessUnsharedGcRemovesLeftover-otherspace` shows that a gc in another one removes an exited session while a process that the program left runs. gc judges without a SIGSTOP first, so a fork chain that no scan shows reads gone to the judge. So `provenProgramGroupRuns` also counts the group as running while the probe `kill(-pgid, 0)` finds its id and no scan shows a member, live or zombie (`GcProbesUnseenGroup`). Under a PID 1 that never reaps, the chain also leaves zombies in view, so the scans show only zombies while its live member escapes them. Then `judgeFrozenGroup` sends SIGSTOP, as `stopProgramGroup` does, judges the stopped group, whose stopped member stays in view, and sends SIGCONT in a `finally` (`GcFreezesUnseenGroup`). It sends SIGSTOP only where `/proc` shows its own pid space. `mutant-GcFreezesUnseenGroup-unseen-zombies` must violate R20, and "gc keeps an exited session while a fork chain runs behind its zombies" in `test/integration/non-reaping-init.test.ts` covers it. An unrelated group that took the id is in view and reads `unproven`, so it does not keep the session. `mutant-GcProbesUnseenGroup-unseen` must violate R20. The integration tests "gc keeps an exited session while a process that the program left runs" and "... while a fork chain that the program left runs" in `test/integration/lifecycle.test.ts` cover both, and "gc removes an exited session whose host.json names another pid namespace" covers the restart. ```sh id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'trap "" HUP; sleep 300 & exit 0' | 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/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index 7a96a5ff..ae65e610 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -50,6 +50,9 @@ CONSTANTS GcProbesUnseenGroup, \* programGroup.ts: provenProgramGroupRuns also \* counts a group id that the probe finds \* while no scan shows a member + GcFreezesUnseenGroup, \* programGroup.ts: gc sends SIGSTOP to a group + \* whose scans show only zombies while the + \* probe finds its id, and judges it again ReconcileSkipsTerminal, \* lifecycle.ts: return when the manifest is terminal ReconcileSkipsLiveHost, \* lifecycle.ts: return when hostPid is set and alive CreateRecordsHostPid, \* lifecycle.ts: launch the host, then write the @@ -134,6 +137,9 @@ 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 + ZombiesInView, \* the environment: with Unseen, the scans show + \* zombies of the program's group, as under a + \* PID 1 that never reaps OtherPidSpace, \* the environment: destroy, list and gc run \* where no scan and no probe shows the host's \* processes (no /proc, an empty /proc, @@ -147,10 +153,11 @@ CONSTANTS ASSUME MaxListReconciles \in 1..3 ASSUME Token \in BOOLEAN ASSUME Unseen \in BOOLEAN +ASSUME ZombiesInView \in BOOLEAN ASSUME OtherPidSpace \in BOOLEAN ASSUME Win32 \in BOOLEAN ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, GcKeepsLiveGroup, - GcProbesUnseenGroup, + GcProbesUnseenGroup, GcFreezesUnseenGroup, ReconcileSkipsTerminal, ReconcileSkipsLiveHost, CreateRecordsHostPid, HostWaitsForManifest, ReconcileRereads, @@ -1088,20 +1095,25 @@ GcReadsReconciled == \* provenProgramGroupRuns reads program.json and judges the group, as the \* waits of destroy do, but it counts only a group that it proves: a live -\* member carries the token. gc sends no SIGSTOP, so with Unseen no scan -\* shows the program's processes, and with GcProbesUnseenGroup the probe -\* kill(-pgid, 0) then finds them. An unrelated group that took the id is -\* in view and reads unproven. With OtherPidSpace gc cannot check the group -\* and reads it not proven, so that a session whose pid space is gone, as -\* after a container restart, does not stay forever. With GcKeepsLiveGroup -\* gc skips a session that is not destroyed while it proves the group -\* ("the session's program group still runs"). The code tests the status -\* of manifestAfter, which cannot turn from destroyed back, so this current -\* status skips no more often. +\* member carries the token. With Unseen no scan shows the program's +\* processes, and with GcProbesUnseenGroup the probe kill(-pgid, 0) then +\* finds them while no scan shows a member, not even a zombie. With +\* ZombiesInView the scans show zombies of the group, which the probe also +\* finds, so gc needs GcFreezesUnseenGroup: it sends SIGSTOP, a stopped +\* member stays in view, and the judgement after it finds the program's +\* processes. An unrelated group that took the id is in view and reads +\* unproven. With OtherPidSpace gc cannot check the group and reads it not +\* proven, so that a session whose pid space is gone, as after a container +\* restart, does not stay forever. With GcKeepsLiveGroup gc skips a session +\* that is not destroyed while it proves the group ("the session's program +\* group still runs"). The code tests the status of manifestAfter, which +\* cannot turn from destroyed back, so this current status skips no more +\* often. GcSeesGroup == /\ ~OtherPidSpace /\ \/ GroupSeen("proven") - \/ GcProbesUnseenGroup /\ Unseen /\ (prog \/ left) + \/ /\ GcProbesUnseenGroup /\ Unseen /\ (prog \/ left) + /\ (~ZombiesInView \/ GcFreezesUnseenGroup) GcChecksGroup == /\ pc["gc"] = "group" diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index fcb6ab42..0d500c93 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 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" +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" # 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; @@ -192,6 +192,9 @@ RUNS="" TOKEN=TRUE # UNSEEN: whether no scan of /proc shows a live process of the program. 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 # 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. @@ -216,6 +219,7 @@ write_run() { done echo " Token = $TOKEN" echo " Unseen = $UNSEEN" + echo " ZombiesInView = $ZOMBIES" echo " OtherPidSpace = $OTHER" echo " Win32 = $WIN32" echo " MaxListReconciles = 2" @@ -273,6 +277,11 @@ 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 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 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 6ff06fa3..7b961476 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -1009,8 +1009,9 @@ function programRecordFacts() { // with a token it kills only right after it read a live member of the group // again and found the program's session id, autogroup and boot id on it. // No other code calls the raw group kill or builds a group target, except -// the two probes, which send signal 0, and only stopProgramGroup sends the -// SIGSTOP and SIGCONT of signalProcessGroup. +// the two probes, which send signal 0. Only stopProgramGroup and gc's +// judgeFrozenGroup send the SIGSTOP and SIGCONT of signalProcessGroup, which +// kill nothing. function ownershipFacts() { const module = 'src/host/programGroup.ts'; const stop = requireDeclaration(module, 'stopProgramGroup'); @@ -1052,13 +1053,16 @@ function ownershipFacts() { let stray = false; for (const file of listSources('src')) { walk(source(file), (node) => { - if ( - isCall(node, 'killProcessGroupBestEffort') || - isCall(node, 'signalProcessGroup') - ) { + if (isCall(node, 'killProcessGroupBestEffort')) { rawKills += 1; stray ||= file !== module || ownerPath(node) !== 'stopProgramGroup'; } + if (isCall(node, 'signalProcessGroup')) { + rawKills += 1; + stray ||= + file !== module || + !['stopProgramGroup', 'judgeFrozenGroup'].includes(ownerPath(node)); + } if (isCall(node, 'processGroupTarget')) { targets += 1; const owner = ownerPath(node); @@ -1426,16 +1430,21 @@ function gcFacts() { "if (verdict !== 'gone') { return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; }"; // Then a group that reads gone, whose id the probe finds while no scan // shows a member, live or zombie, counts as running too. Without the - // probe, gone reads false. - const probeTail = [ + // probe, gone reads false. When the scans show only zombies, the group is + // judged again frozen, or, without the freeze, reads ended. + const probeHead = [ 'if (!probeFindsGroup(group.pid)) { return false; }', 'const live = groupHasLiveProcess(group.pid);', - 'return live === null ? true : live ? null : false;', ]; const tail = judge.slice(2); + const last = tail.at(-1); const probes = judges && - tail.join('\n') === probeTail.join('\n') && + tail.length === 3 && + tail.slice(0, 2).join('\n') === probeHead.join('\n') && + (last === 'return live === null ? true : live ? null : false;' || + last === + 'return live === null ? true : live ? null : judgeFrozenGroup(group);') && normalize( requireDeclaration( 'src/host/programGroup.ts', @@ -1445,6 +1454,17 @@ function gcFacts() { "{ try { process.kill(processGroupTarget(pgid), 0); return true; } catch (error) { if (hasErrorCode(error, 'ESRCH')) { return false; } if (hasErrorCode(error, 'EPERM')) { return true; } throw error; } }"; const judgesGone = probes || (tail.length === 1 && tail[0] === 'return false;'); + // judgeFrozenGroup sends SIGSTOP only where /proc shows this process's pid + // space, judges the stopped group, and sends SIGCONT in a finally. + const freezes = + probes && + last === + 'return live === null ? true : live ? null : judgeFrozenGroup(group);' && + body('judgeFrozenGroup').join('\n') === + [ + "if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { return false; }", + "try { const { verdict } = judgeLiveGroup(group); return verdict === 'owned' ? true : verdict === 'unknown' ? null : false; } finally { signalProcessGroup(group.pid, 'SIGCONT'); }", + ].join('\n'); return { GcSkipsNonCollectable: reconcile >= 0 && collectable > reconcile, GcFinalCheck: finalCheck, @@ -1456,6 +1476,7 @@ function gcFacts() { judges && judgesGone, GcProbesUnseenGroup: probes, + GcFreezesUnseenGroup: freezes, }; } @@ -1499,6 +1520,7 @@ const COVERED = [ ['src/cli/commands/gc.ts', 'defaultDependencies'], ['src/host/programGroup.ts', 'provenProgramGroupRuns'], ['src/host/programGroup.ts', 'judgeGroupForGc'], + ['src/host/programGroup.ts', 'judgeFrozenGroup'], ['src/host/programGroup.ts', 'GC_JUDGEMENTS'], ['src/host/programGroup.ts', 'probeFindsGroup'], ['src/host/lifecycle.ts', 'allocateSession'], diff --git a/docs/USAGE.md b/docs/USAGE.md index fba99531..a0b70efa 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -366,9 +366,9 @@ 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. 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 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. It then reports "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, 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. +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. It then reports "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, 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: - At the idle time-out, a host that cannot run the check kills nothing, but it still records the session as `exited` once the program has exited, while a process that the program left can still run. A later `destroy` then fails with `HOST_TIMEOUT`, and `gc` can remove the session folder. - When `/proc` hides the processes of other users (mounted with `hidepid=2`, `hidepid=4`, `hidepid=invisible` or `hidepid=ptraceable`), a group whose processes agent-tty cannot see counts as running. A `destroy` that cannot prove such a group gone fails with `HOST_TIMEOUT` and does not record the session as `destroyed`. From 0ea48c887e16b3f1751f5f66032f1696dd76497d Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 08:57:49 +0000 Subject: [PATCH 03/17] chore: sync the lifecycle coverage record after the gc freeze check.sh --update-coverage at 1c1bd1c6 gave 79/79 runs as expected in 1,121 s. current has 29,309,460 distinct states and current-no-token 29,186,546. --- .agents/skills/verify-session-lifecycle/coverage.json | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index cfb65dd6..1b903163 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -7,6 +7,7 @@ "GcFinalCheck": true, "GcKeepsLiveGroup": true, "GcProbesUnseenGroup": true, + "GcFreezesUnseenGroup": true, "CreateRecordsHostPid": true, "CreateRecordsHost": true, "CreateStopsOnGiveUp": true, @@ -46,7 +47,8 @@ "src/cli/commands/gc.ts#gcSessions": "a2ac8bd10f100332", "src/cli/commands/gc.ts#defaultDependencies": "81a9894438cb5be7", "src/host/programGroup.ts#provenProgramGroupRuns": "7b50817618b4b769", - "src/host/programGroup.ts#judgeGroupForGc": "e0cd1b46a60eb1fe", + "src/host/programGroup.ts#judgeGroupForGc": "fb133ba2739116d1", + "src/host/programGroup.ts#judgeFrozenGroup": "54e81ca84cfeabac", "src/host/programGroup.ts#GC_JUDGEMENTS": "180a0af01a4b81c7", "src/host/programGroup.ts#probeFindsGroup": "31ea7b5e835c0509", "src/host/lifecycle.ts#allocateSession": "43819af8c6c271ec", @@ -137,9 +139,9 @@ "src/host/hostMain.ts#runHost(final try)": "251f1e68a4ec17cc", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "19775a9a74c5ca9a", - "skill:scripts/facts.mjs": "4aff1bce5c8ba086", - "skill:scripts/check.sh": "0e69ddb1068b5df4" + "skill:model/SessionLifecycle.tla": "77ec28d60359f635", + "skill:scripts/facts.mjs": "d44209b878acbb50", + "skill:scripts/check.sh": "e33db0960de216fe" }, "callSites": { "writeManifest": [ From 5556816300787ee991e192897f0f11234a2c71de Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 09:15:23 +0000 Subject: [PATCH 04/17] fix(destroy): destroy --force ends a session whose program group it cannot read A read of program.json, host.json or /proc that fails with a system error, such as EACCES or EIO, failed every later check, so gc kept the session forever and destroy failed on the same read. destroy --force of a session whose host is gone now stops what it can without the group and records destroyed. A group that reads alive and a host that does not end (HOST_TIMEOUT) still fail it. gc's skip reasons name destroy --force for such a read. --- src/cli/commands/gc.ts | 15 +++- src/host/lifecycle.ts | 67 +++++++++------ src/host/programGroup.ts | 18 ++++ test/integration/lifecycle.test.ts | 123 ++++++++++++++++++++++++++++ test/unit/commands/gc.test.ts | 34 ++++++++ test/unit/host/programGroup.test.ts | 25 ++++++ 6 files changed, 256 insertions(+), 26 deletions(-) diff --git a/src/cli/commands/gc.ts b/src/cli/commands/gc.ts index d1bb1134..49ecc14d 100644 --- a/src/cli/commands/gc.ts +++ b/src/cli/commands/gc.ts @@ -8,7 +8,10 @@ import { reconcileSession, removeDeadHostSocket, } from '../../host/lifecycle.js'; -import { provenProgramGroupRuns } from '../../host/programGroup.js'; +import { + isUnreadableGroupError, + provenProgramGroupRuns, +} from '../../host/programGroup.js'; import { ERROR_CODES, makeCliError } from '../../protocol/errors.js'; import { isCollectableSessionStatus, @@ -289,6 +292,12 @@ export function parseDurationToMs(value: string): number { return durationMs; } +// A read of the program's group that fails with a system error fails every +// later check too. destroy --force ends such a session without the read. +function forceRemovesIt(error: unknown): string { + return isUnreadableGroupError(error) ? ' (destroy --force removes it)' : ''; +} + export async function gcSessions( home: string, options: GcExecutionOptions, @@ -370,7 +379,7 @@ export async function gcSessions( } catch (error) { result.skippedSessions.push({ sessionId: manifestBefore.sessionId, - reason: `failed to reconcile session: ${getErrorMessage(error)}`, + reason: `failed to reconcile session${forceRemovesIt(error)}: ${getErrorMessage(error)}`, }); continue; } @@ -434,7 +443,7 @@ export async function gcSessions( } catch (error) { result.skippedSessions.push({ sessionId, - reason: `failed to check the session's program group: ${getErrorMessage(error)}`, + reason: `failed to check the session's program group${forceRemovesIt(error)}: ${getErrorMessage(error)}`, }); continue; } diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index 1ffc620a..a11fde16 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -35,6 +35,7 @@ import { invariant } from '../util/assert.js'; import { hasErrorCode } from '../util/hasErrorCode.js'; import { isProgramGroupAlive, + isUnreadableGroupError, parseProcStat, readProgramGroup, readProvenProgramGroup, @@ -909,22 +910,49 @@ export async function destroySession( }); } + // destroy --force of a session whose host is gone also ends a session + // whose program group it cannot read: a read of program.json or /proc + // that fails with a system error. It then stops what it can without the + // group and records destroyed, so a process that the program left can + // outlive it. A group that reads alive, or a host that does not end + // (HOST_TIMEOUT), still fails the destroy. + const stopUnlessUnreadable = async ( + host: SessionHost | null, + readGroup: () => Promise, + ): Promise => { + try { + const group = await readGroup(); + await stopSessionProcesses( + sessionId, + host, + group, + sessionDirectory, + signal, + ); + return group; + } catch (error) { + if (force !== true || !isUnreadableGroupError(error)) { + throw error; + } + } + await stopSessionProcesses(sessionId, host, null, sessionDirectory, signal); + return null; + }; + const stopLeftoversThenRecordDestroyed = async ( terminal: SessionRecord, ): Promise => { - const group = await readProvenProgramGroup(sessionDirectory); - // Only a process that sees the program's group records destroyed, after - // a wait that read the group gone. So a destroyed record needs no wait - // for a group out of view. - await stopSessionProcesses( - sessionId, - null, - terminal.status === 'destroyed' && group !== null && 'unshared' in group + await stopUnlessUnreadable(null, async () => { + const group = await readProvenProgramGroup(sessionDirectory); + // Only a process that sees the program's group records destroyed, + // after a wait that read the group gone. So a destroyed record needs no + // wait for a group out of view. + return terminal.status === 'destroyed' && + group !== null && + 'unshared' in group ? null - : group, - sessionDirectory, - signal, - ); + : group; + }); await recordDestroyed(manifestFile, socketFile, terminal, null); }; @@ -934,23 +962,16 @@ export async function destroySession( } if (force === true) { - await stopSessionProcesses( - sessionId, + await stopUnlessUnreadable( await readSessionHost(sessionDirectory, manifest), - await readProgramGroup(sessionDirectory, manifest.childPid), - sessionDirectory, - signal, + () => readProgramGroup(sessionDirectory, manifest.childPid), ); // The host is dead now, so this read is final. It can name a child that // the first read did not. const current = await readSessionManifestOrThrow(sessionId, manifestFile); - const group = await readProgramGroup(sessionDirectory, current.childPid); - await stopSessionProcesses( - sessionId, + const group = await stopUnlessUnreadable( await readSessionHost(sessionDirectory, current), - group, - sessionDirectory, - signal, + () => readProgramGroup(sessionDirectory, current.childPid), ); await recordDestroyed(manifestFile, socketFile, current, group); return; diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index c4784cf3..f7330632 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -3,6 +3,7 @@ import process from 'node:process'; import { z } from 'zod'; +import { CliError } from '../cli/errors.js'; import { ERROR_CODES, makeCliError } from '../protocol/errors.js'; import { readValidatedJsonFile, @@ -296,6 +297,23 @@ async function readProgramRecord( } } +// Whether a read of the program's group failed with a system error: a read +// of program.json or host.json (STORAGE_READ_ERROR), or a read of /proc +// (an errno code such as EIO or EACCES). A verdict, HOST_TIMEOUT, an abort +// or a bug is none of these. +export function isUnreadableGroupError(error: unknown): boolean { + if (hasErrorCode(error, ERROR_CODES.STORAGE_READ_ERROR)) { + return true; + } + const code: unknown = + error instanceof Error ? (error as { code?: unknown }).code : undefined; + return ( + !(error instanceof CliError) && + typeof code === 'string' && + /^E[A-Z0-9]+$/.test(code) + ); +} + export async function readProvenProgramGroup( sessionDirectory: string, ): Promise { diff --git a/test/integration/lifecycle.test.ts b/test/integration/lifecycle.test.ts index 06046646..8b741c62 100644 --- a/test/integration/lifecycle.test.ts +++ b/test/integration/lifecycle.test.ts @@ -1115,6 +1115,129 @@ describe('lifecycle integration', { timeout: 60_000 }, () => { }, ); + // A read of program.json that fails with EACCES fails every later + // check too. destroy --force ends such a session without the read, so + // gc does not keep it forever. Root reads any file, so these tests skip + // under root. + async function statusOf(sessionId: string): Promise { + const manifest = JSON.parse( + await readFile( + join(testHome, 'sessions', sessionId, 'session.json'), + 'utf8', + ), + ) as { status: string }; + return manifest.status; + } + + it.runIf(process.getuid?.() !== 0)( + 'destroy --force ends an exited session whose program.json it cannot read', + async () => { + const sessionId = await createProgram( + `trap "" HUP; sleep 300 & ${untilRecorded()}; touch "$0"; exit 0`, + ); + const deadline = Date.now() + 10_000; + while ((await statusOf(sessionId)) !== 'exited') { + expect(Date.now()).toBeLessThan(deadline); + await sleep(100); + } + await chmod(join(testHome, 'sessions', sessionId, 'program.json'), 0); + + const kept = runCli(['gc', '--json'], { AGENT_TTY_HOME: testHome }); + expect(JSON.parse(kept.stdout)).toMatchObject({ + ok: true, + result: { + removedSessionCount: 0, + homes: [ + { + skippedSessions: [ + { + sessionId, + reason: expect.stringContaining( + 'destroy --force removes it', + ) as string, + }, + ], + }, + ], + }, + }); + const plain = runCli(['destroy', sessionId, '--json'], { + AGENT_TTY_HOME: testHome, + }); + expect(JSON.parse(plain.stdout)).toMatchObject({ ok: false }); + expect(await statusOf(sessionId)).toBe('exited'); + + const forced = runCli(['destroy', sessionId, '--force', '--json'], { + AGENT_TTY_HOME: testHome, + }); + expect( + (JSON.parse(forced.stdout) as { error?: unknown }).error, + ).toBeUndefined(); + expect(await statusOf(sessionId)).toBe('destroyed'); + // The documented trade-off: the process that the program left runs on. + expect(isGroupAlive(pgid)).toBe(true); + const removed = runCli(['gc', '--json'], { AGENT_TTY_HOME: testHome }); + expect(JSON.parse(removed.stdout)).toMatchObject({ + ok: true, + result: { removedSessionCount: 1 }, + }); + }, + ); + + it.runIf(process.getuid?.() !== 0)( + 'destroy --force ends a session whose host died and whose program.json it cannot read', + async () => { + const sessionId = await createProgram( + `trap "" HUP; ${untilRecorded()}; touch "$0"; exec sleep 300`, + ); + const sessionFile = join( + testHome, + 'sessions', + sessionId, + 'session.json', + ); + const { hostPid } = JSON.parse(await readFile(sessionFile, 'utf8')) as { + hostPid: number; + }; + process.kill(hostPid, 'SIGKILL'); + const deadline = Date.now() + 10_000; + while (isProcessAlive(hostPid)) { + expect(Date.now()).toBeLessThan(deadline); + await sleep(50); + } + await chmod(join(testHome, 'sessions', sessionId, 'program.json'), 0); + + const kept = runCli(['gc', '--json'], { AGENT_TTY_HOME: testHome }); + expect(JSON.parse(kept.stdout)).toMatchObject({ + ok: true, + result: { + removedSessionCount: 0, + homes: [ + { + skippedSessions: [ + { + sessionId, + reason: expect.stringContaining( + 'destroy --force removes it', + ) as string, + }, + ], + }, + ], + }, + }); + expect(await statusOf(sessionId)).toBe('running'); + + const forced = runCli(['destroy', sessionId, '--force', '--json'], { + AGENT_TTY_HOME: testHome, + }); + expect( + (JSON.parse(forced.stdout) as { error?: unknown }).error, + ).toBeUndefined(); + expect(await statusOf(sessionId)).toBe('destroyed'); + }, + ); + // A token proves the group only beside host.json, which names its pid // space, so a host that cannot record itself records no token. it.runIf(capturesToken)( diff --git a/test/unit/commands/gc.test.ts b/test/unit/commands/gc.test.ts index 754941d1..d083afcd 100644 --- a/test/unit/commands/gc.test.ts +++ b/test/unit/commands/gc.test.ts @@ -451,6 +451,40 @@ describe('gc command helpers', () => { expect(socketCleanups).toEqual([`${home}/sessions/exited-01 exited`]); }); + it('names destroy --force when a read of the group fails with a system error', async () => { + const home = '/tmp/agent-tty'; + const { dependencies, removedPaths } = createMockDependencies(home, { + 'unreadable-01': { + manifest: createSessionRecord({ + sessionId: 'unreadable-01', + status: 'exited', + createdAt: '2026-03-20T08:00:00.000Z', + }), + }, + }); + dependencies.provenProgramGroupRuns = () => + Promise.reject( + Object.assign(new Error('EIO: i/o error, scandir /proc'), { + code: 'EIO', + }), + ); + + const result = await gcSessions( + home, + { dryRun: false, staleOnly: false, olderThanMs: null }, + dependencies, + ); + + expect(result.skippedSessions).toEqual([ + { + sessionId: 'unreadable-01', + reason: + "failed to check the session's program group (destroy --force removes it): EIO: i/o error, scandir /proc", + }, + ]); + expect(removedPaths).toEqual([]); + }); + it('reports removals in dry-run mode without deleting anything', async () => { const home = '/tmp/agent-tty'; const { dependencies, removedPaths, bytesBySession } = diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index b9aa086b..bffca74a 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -19,6 +19,7 @@ import { afterEach, beforeEach, describe, expect, it, vi } from 'vitest'; import { captureProgram, isProgramGroupAlive, + isUnreadableGroupError, judgeProgramGroup, parseAutogroup, parseProcStat, @@ -30,6 +31,7 @@ import { type ProcessRow, type ProgramRecord, } from '../../../src/host/programGroup.js'; +import { ERROR_CODES, makeCliError } from '../../../src/protocol/errors.js'; import { programRecordPath, sessionDir, @@ -1641,3 +1643,26 @@ describe.runIf(platform === 'linux')('a program record with a token', () => { expect(kill).not.toHaveBeenCalled(); }); }); + +// destroy --force ends a session without its group only after such a read. +describe('isUnreadableGroupError', () => { + it.each([ + [ + 'a program.json that the read refuses', + makeCliError(ERROR_CODES.STORAGE_READ_ERROR), + true, + ], + ['a /proc scan that fails with EIO', errno('EIO'), true], + ['a /proc read that fails with EACCES', errno('EACCES'), true], + ['HOST_TIMEOUT', makeCliError(ERROR_CODES.HOST_TIMEOUT), false], + [ + 'an assertion', + Object.assign(new Error('x'), { code: 'ERR_ASSERTION' }), + false, + ], + ['an error without a code', new Error('EIO'), false], + ['a value that is no error', { code: 'EIO' }, false], + ])('reads %s as unreadable: %s', (_name, error, unreadable) => { + expect(isUnreadableGroupError(error)).toBe(unreadable); + }); +}); From 3cd8ff4fafe9912c75fb68d81b598ad823212b46 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 09:21:26 +0000 Subject: [PATCH 05/17] feat(model): check destroy --force without a readable group, and gc under refused reads CheckFails: while program.json names the program, every read of it by destroy, list and gc fails. gc and its reconcile skip the session, plain destroy fails, and with ForceSkipsUnreadableGroup destroy --force records destroyed after it stopped the host alone. The ghost dblind marks such a record, which R11, R16 and R20 leave out, and WitnessUncheckedForceDestroys shows it. Refused: /proc of the CLI refuses the program's autogroup, so the group reads alive while it runs, gets no kill, and gc reads it not proven. R20 leaves Refused out, and WitnessRefusedGcRemovesLeftover shows that removal. facts.mjs reads the new guard and the stopUnlessUnreadable steps of destroySession. --- .../model/SessionLifecycle.tla | 139 +++++++++++++----- .../verify-session-lifecycle/scripts/check.sh | 25 +++- .../scripts/facts.mjs | 128 ++++++++++++---- 3 files changed, 221 insertions(+), 71 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index ae65e610..ca0695e4 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -111,6 +111,10 @@ CONSTANTS \* it reads the manifest, and the host checks \* for it before the spawn and right after its \* start-up write, and then ends the session + ForceSkipsUnreadableGroup, \* lifecycle.ts: destroy --force of a session + \* whose host is gone records destroyed also + \* when the read of the group fails with a + \* system error, after it stops the host alone TokenNamesProgram, \* programGroup.ts: captureToken records an \* autogroup only once the program leads its \* own session in an autogroup other than the @@ -148,6 +152,13 @@ CONSTANTS Win32, \* the environment: Windows, where SIGTERM ends \* the host at once, so create sends it only \* when the manifest names the program + CheckFails, \* the environment: while program.json names + \* the program, every read of it by destroy, + \* list and gc fails with a system error (EACCES, + \* or EIO on /proc), as does every judgement + Refused, \* the environment: /proc of destroy, list and gc + \* refuses the autogroup of the program's + \* processes, so no judgement proves the group MaxListReconciles \* how many times the "list" process reconciles ASSUME MaxListReconciles \in 1..3 @@ -156,6 +167,8 @@ ASSUME Unseen \in BOOLEAN ASSUME ZombiesInView \in BOOLEAN ASSUME OtherPidSpace \in BOOLEAN ASSUME Win32 \in BOOLEAN +ASSUME CheckFails \in BOOLEAN +ASSUME Refused \in BOOLEAN ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, GcKeepsLiveGroup, GcProbesUnseenGroup, GcFreezesUnseenGroup, ReconcileSkipsTerminal, @@ -170,7 +183,7 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, GcKeepsLiveGroup, InsideCheckReadsEnv, RecordsProgramSync, ProvesGroupOwnership, DestroyStopsLeftovers, FallbackNeedsFolder, CreateStopsOnGiveUp, - HostChecksCreateFailed, + HostChecksCreateFailed, ForceSkipsUnreadableGroup, ReconcileRepairsDestroyed, ReconcileRepairsMarked, TokenNamesProgram, ReusedIdReadsGone, ProvesHostPid, CreateRecordsHost, @@ -179,8 +192,10 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, GcKeepsLiveGroup, Readers == {"gc", "list"} \* the two processes that run reconcileSession \* The group that a kill went through, and that the wait after it probes: \* "proven" (program.json with a token), "numeric" (a childPid without a -\* token), "bare" (the host's own record without a token) or "none". -GroupKinds == {"none", "proven", "numeric", "bare"} +\* token), "bare" (the host's own record without a token), "blind" (destroy +\* --force could not read the group, see ForceSkipsUnreadableGroup) or +\* "none". +GroupKinds == {"none", "proven", "numeric", "bare", "blind"} NoRead == [pid |-> FALSE, origin |-> "none", code |-> FALSE, child |-> FALSE, grp |-> "none"] @@ -261,7 +276,9 @@ VARIABLES dres, \* what destroy reported: "pending", "ok", "error", or \* "killed" (it died before it reported) dsaw, \* ghost: destroy wrote "destroyed" or read it last - dkill \* ghost: destroy --force killed a live host + dkill, \* ghost: destroy --force killed a live host + dblind \* ghost: destroy --force recorded destroyed without a read + \* of the program's group (CheckFails) diskVars == <> @@ -271,7 +288,7 @@ groupVars == <> shutVars == <> readerVars == <> -destroyVars == <> +destroyVars == <> vars == <> @@ -298,7 +315,7 @@ Init == /\ lruns = 0 /\ dpc = "check" /\ dforce \in BOOLEAN /\ dinside = FALSE /\ drd = NoRead /\ dres = "pending" - /\ dsaw = FALSE /\ dkill = FALSE + /\ dsaw = FALSE /\ dkill = FALSE /\ dblind = FALSE \* writeManifest in src/storage/manifests.ts: write a temp file in the session \* directory and rename it over session.json. The rename is the visible step. @@ -420,12 +437,23 @@ GroupSeen(kind) == \* readProgramGroup and readProvenProgramGroup give a group with a token \* that reads alive instead, so their waits time out. The host always runs \* in its own pid space, so it keeps GroupSeen and HostKill. CliHostAlive -\* gives the CLI's view of the host. +\* gives the CLI's view of the host. With Refused a live member of the +\* program's session shows no autogroup, so a group with a token reads +\* unknown, which reads alive, while a process of it runs, and it gets no +\* kill, because nothing proves it. CliGroupSeen(kind) == IF OtherPidSpace THEN kind = "proven" /\ UnsharedGroupReadsUnknown + ELSE IF Refused /\ kind = "proven" + THEN KillsProgramGroup /\ (prog \/ left \/ foreign) ELSE GroupSeen(kind) -CliKillThrough(named) == IF OtherPidSpace THEN NoKill ELSE KillThrough(named) +CliKillThrough(named) == + IF OtherPidSpace \/ (Refused /\ rec) THEN NoKill ELSE KillThrough(named) + +\* With CheckFails every read of program.json by destroy, list and gc fails +\* while the record exists, and so does every judgement of the group that +\* it names. +Unreadable == CheckFails /\ rec \* The host fails to start because its files are missing or were rewritten. HostFailsToStart == @@ -968,13 +996,22 @@ ReconcileRereadsManifest(p) == \* `const group = await readProgramGroup(sessionDirectory, \* current.childPid)` reads program.json, then stopProgramGroup(group). +\* With Unreadable the read throws, and so does reconcileSession: gc skips +\* the session ("failed to reconcile session (destroy --force removes it)"), +\* and list goes on. ReconcileReadsRecord(p) == /\ pc[p] = "r_record" - /\ CliKillThrough(rd[p].child) - /\ rd' = [rd EXCEPT ![p].grp = KindThrough(rd[p].child)] - /\ pc' = [pc EXCEPT ![p] = AfterGroupKill] + /\ IF Unreadable + THEN /\ NoKill /\ UNCHANGED rd + /\ pc' = [pc EXCEPT ![p] = IF p = "gc" THEN "done" + ELSE AfterReconcile(p)] + /\ gres' = IF p = "gc" THEN "skipped" ELSE gres + ELSE /\ CliKillThrough(rd[p].child) + /\ rd' = [rd EXCEPT ![p].grp = KindThrough(rd[p].child)] + /\ pc' = [pc EXCEPT ![p] = AfterGroupKill] + /\ UNCHANGED gres /\ UNCHANGED <> @@ -1110,14 +1147,15 @@ GcReadsReconciled == \* cannot turn from destroyed back, so this current status skips no more \* often. GcSeesGroup == - /\ ~OtherPidSpace + /\ ~OtherPidSpace /\ ~Refused /\ \/ GroupSeen("proven") \/ /\ GcProbesUnseenGroup /\ Unseen /\ (prog \/ left) /\ (~ZombiesInView \/ GcFreezesUnseenGroup) GcChecksGroup == /\ pc["gc"] = "group" - /\ IF GcKeepsLiveGroup /\ mst # "destroyed" /\ rec /\ GcSeesGroup + /\ IF GcKeepsLiveGroup /\ mst # "destroyed" + /\ (Unreadable \/ (rec /\ GcSeesGroup)) THEN GcSkips ELSE GcGoesTo("final") /\ UNCHANGED <> + readerVars, dforce, dinside, dsaw, dkill, dblind, + groupVars>> \* runDestroyCommand: cliRunsInsideProgramSession first compares \* AGENT_TTY_SESSION_ID, which the program and its processes inherit at @@ -1204,7 +1243,8 @@ DestroyChecksSession == /\ (InsideCheckReadsEnv \/ mchild))) /\ dpc' = "read" /\ UNCHANGED <> + readerVars, dforce, drd, dres, dsaw, dkill, dblind, + groupVars>> ReadCopy == [pid |-> mpid, origin |-> morigin, code |-> mcode, child |-> mchild, grp |-> "none"] @@ -1255,7 +1295,7 @@ DestroyReads == ELSE /\ dpc' = "rpc" /\ UNCHANGED <> /\ sock' = (sock /\ (mst # "destroyed" \/ (mpid /\ CliHostAlive))) /\ UNCHANGED <> + readerVars, dforce, dinside, dkill, dblind, groupVars>> \* stopLeftoversThenRecordDestroyed: stopSessionProcesses(sessionId, null, \* await readProvenProgramGroup(sessionDirectory), ...). The program.json @@ -1264,12 +1304,18 @@ DestroyReads == \* Then waitForProcessesToExit (DestroyPollsGroup, at "twait"). DestroyKillsLeftovers == /\ DestroyAt({"tkill"}) - /\ IF rec /\ ~OtherPidSpace THEN ProvenKill ELSE NoKill - /\ drd' = [drd EXCEPT !.grp = IF rec THEN "proven" ELSE "none"] - /\ dpc' = "twait" + /\ IF Unreadable /\ ~(dforce /\ ForceSkipsUnreadableGroup) + THEN /\ NoKill /\ DestroyEnds("error") + ELSE /\ IF rec /\ ~OtherPidSpace /\ ~Refused /\ ~Unreadable + THEN ProvenKill ELSE NoKill + /\ drd' = [drd EXCEPT !.grp = IF Unreadable THEN "blind" + ELSE IF rec THEN "proven" + ELSE "none"] + /\ dpc' = "twait" + /\ UNCHANGED dres /\ UNCHANGED <> \* recordDestroyed: writeDestroyMarker, an empty file written with no mkdir. @@ -1294,9 +1340,10 @@ DestroyWritesDestroyed == THEN /\ Write("destroyed", drd.pid, drd.origin, DestroyKeepsExitCode /\ drd.code, drd.child) /\ dpc' = "tunlink" /\ drd' = NoRead /\ dsaw' = TRUE + /\ dblind' = (dblind \/ drd.grp = "blind") /\ UNCHANGED dres ELSE /\ DestroyEnds("error") - /\ UNCHANGED diskVars + /\ UNCHANGED <> /\ UNCHANGED <> @@ -1306,7 +1353,7 @@ DestroyUnlinksSocket == /\ sock' = FALSE /\ dpc' = "done" /\ dres' = "ok" /\ UNCHANGED <> + dforce, dinside, drd, dsaw, dkill, dblind, groupVars>> \* killHostBestEffort(host) of the copy that destroy read. With \* ProvesHostPid it kills only a host that hostMatches proves: the live host @@ -1332,13 +1379,19 @@ KillsHost == \* wait ("rkill"). DestroyKills == /\ DestroyAt({"kill", "rkill"}) - /\ CliKillThrough(drd.child) - /\ KillsHost - /\ drd' = [drd EXCEPT !.grp = KindThrough(drd.child)] - /\ dpc' = IF dpc = "kill" THEN "kwait" ELSE "rwait" + /\ IF Unreadable /\ ~ForceSkipsUnreadableGroup + THEN /\ NoKill /\ DestroyEnds("error") + /\ UNCHANGED <> + ELSE /\ IF Unreadable THEN NoKill ELSE CliKillThrough(drd.child) + /\ KillsHost + /\ drd' = [drd EXCEPT !.grp = IF Unreadable THEN "blind" + ELSE KindThrough(drd.child)] + /\ dpc' = IF dpc = "kill" THEN "kwait" ELSE "rwait" + /\ UNCHANGED dres /\ UNCHANGED <> + readerVars, dforce, dinside, dsaw, dblind, rec, reused, + hrec, hreused, passedReused>> \* waitForProcessesToExit in stopSessionProcesses polls until the host is \* dead and isProgramGroupAlive(group) reads false. A host that the kill @@ -1362,7 +1415,7 @@ DestroyPollsGroup == THEN /\ dpc' = "tunlink" /\ drd' = NoRead /\ UNCHANGED <> ELSE /\ dpc' = Records /\ UNCHANGED <> /\ UNCHANGED <> @@ -1377,7 +1430,7 @@ DestroyRereads == /\ dsaw' = (mst = "destroyed") /\ UNCHANGED dres /\ UNCHANGED <> + readerVars, dforce, dinside, dkill, dblind, groupVars>> \* sendRpc(socketFile, 'destroy') reaches the host, whose destroy handler \* calls startShutdown and answers. The host does the work, so this is one @@ -1387,7 +1440,7 @@ DestroySendsRpc == /\ StartShutdown(WriteQueued) /\ dpc' = "poll" /\ UNCHANGED <> \* No socket file, or nobody listens on it: HOST_UNREACHABLE. destroy then @@ -1396,7 +1449,7 @@ DestroyRpcFails == /\ DestroyAt({"rpc"}) /\ ~(sock /\ hostAlive) /\ dpc' = "final" /\ UNCHANGED <> \* waitForTerminalManifest: readManifest until it is terminal. A missing @@ -1410,7 +1463,7 @@ DestroyPolls == THEN DestroyFinishes ELSE /\ dpc' = "final" /\ UNCHANGED <> /\ UNCHANGED <> + readerVars, dforce, dinside, dkill, dblind, groupVars>> \* readSessionManifestOrThrow after destroy's own reconcile: terminal means \* success, anything else throws. @@ -1418,7 +1471,7 @@ DestroyFinalRead == /\ DestroyAt({"final"}) /\ IF mst \in Terminal THEN DestroyFinishes ELSE DestroyEnds("error") /\ UNCHANGED <> + readerVars, dforce, dinside, dkill, dblind, groupVars>> \* Every process is finished. This step keeps TLC from reporting the end \* states as deadlocks. Any other state without a step is a model error. @@ -1467,7 +1520,8 @@ TypeOK == /\ {dir, mpid, mchild, wasTerminal, wasExited, wasNamed, dmark, cmark, startFailed, readRepaired, sock, - hostAlive, prog, foreign, sig, dforce, dinside, dsaw, dkill, rec, left, + hostAlive, prog, foreign, sig, dforce, dinside, dsaw, dkill, dblind, + rec, left, reused, hitUnrelated, diedUnrecorded, passedReused, hrec, hreused, hitUnrelatedHost} \subseteq BOOLEAN @@ -1552,7 +1606,8 @@ RemovedFolderStaysRemoved == gres = "removed" => ~dir \* process that a program left when it exited on its own (`left`, which R16 \* covers), nor a program that no manifest named: its host died before the \* start-up write (see the Scope section of SKILL.md). -DestroyedProgramStopped == (mst = "destroyed" /\ wasNamed) => ~GroupAlive +DestroyedProgramStopped == + (mst = "destroyed" /\ wasNamed /\ ~dblind) => ~GroupAlive \* R13: while a process of the program's group runs, a manifest that named \* the program still names it, so a later destroy or reconcile can still @@ -1572,7 +1627,7 @@ NoUnrelatedGroupKilled == ~hitUnrelated \* the host died after it started the program and before program.json named \* it (see the Scope section of SKILL.md). DestroyedSessionStopped == - (mst = "destroyed" /\ ~diedUnrecorded) => ~(GroupAlive \/ left) + (mst = "destroyed" /\ ~diedUnrecorded /\ ~dblind) => ~(GroupAlive \/ left) \* R17: once create gave up, its host keeps the session "running" only \* while create's SIGTERM is still on its way to it, or while the host has @@ -1601,7 +1656,8 @@ NoUnrelatedHostKilled == ~hitUnrelatedHost \* space cannot check the group, and it removes the folder as it does \* without a token (WitnessUnsharedGcRemovesLeftover). RemovedSessionStopped == - (gres = "removed" /\ ~diedUnrecorded /\ ~OtherPidSpace) + (gres = "removed" /\ ~diedUnrecorded /\ ~OtherPidSpace /\ ~Refused + /\ ~dblind) => ~(GroupAlive \/ left) \* Witnesses. check.sh expects TLC to report each one VIOLATED, which shows @@ -1652,6 +1708,9 @@ WitnessUnsharedDestroyCompletes == \* With OtherPidSpace gc removes an exited session while a process that \* the program left runs, because it cannot check the group there: the \* state that R20 leaves out. +WitnessUncheckedForceDestroys == ~(dblind /\ dres = "ok" /\ left) +WitnessRefusedGcRemovesLeftover == + ~(Refused /\ gres = "removed" /\ ~diedUnrecorded /\ left) WitnessUnsharedGcRemovesLeftover == ~(OtherPidSpace /\ gres = "removed" /\ ~diedUnrecorded /\ left) ============================================================================= diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index 0d500c93..3fe8ab0f 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" +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 ForceSkipsUnreadableGroup" # 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; @@ -199,6 +199,11 @@ ZOMBIES=FALSE OTHER=FALSE # WIN32: whether SIGTERM ends the host at once, as on Windows. WIN32=FALSE +# CHECKFAILS: whether destroy, list and gc fail every read of program.json. +CHECKFAILS=FALSE +# REFUSED: whether /proc of destroy, list and gc refuses the program's +# autogroup. +REFUSED=FALSE write_run() { local name=$1 expect=$2 invariants=$3 overrides=$4 note=$5 must=${6:-} local dir="$OUT/$name" fact guard value @@ -222,6 +227,8 @@ write_run() { echo " ZombiesInView = $ZOMBIES" echo " OtherPidSpace = $OTHER" echo " Win32 = $WIN32" + echo " CheckFails = $CHECKFAILS" + echo " Refused = $REFUSED" echo " MaxListReconciles = 2" echo "SPECIFICATION Spec" echo "CHECK_DEADLOCK TRUE" @@ -294,6 +301,22 @@ write_run mutant-UnsharedGroupReadsUnknown-otherspace violated DestroyedSessionS write_run mutant-CreateRecordsHost-otherspace violated HostDeathOnlyWhenDead "CreateRecordsHost=FALSE" "without the record from create, a reconcile in another pid space reads the starting host dead and records it failed" HostDeathOnlyWhenDead OTHER=FALSE +# destroy, list and gc cannot read program.json (EACCES), or /proc fails with +# a system error. gc keeps the session, and destroy --force ends it without +# the read. +CHECKFAILS=TRUE +write_run current-checkfails pass "$RULES" "" "the code with program.json unreadable for destroy, list and gc: every rule holds" +write_run witness-WitnessUncheckedForceDestroys-checkfails violated WitnessUncheckedForceDestroys "" "destroy --force ends a session whose group it cannot read while a process that the program left runs" +write_run mutant-ForceSkipsUnreadableGroup-checkfails pass WitnessUncheckedForceDestroys "ForceSkipsUnreadableGroup=FALSE" "without the fallback, destroy --force fails on the read, so no command removes the session" +CHECKFAILS=FALSE + +# /proc of destroy, list and gc refuses the autogroup of the program's +# processes. gc cannot check the group, and destroy cannot prove it. +REFUSED=TRUE +write_run current-refused pass "$RULES" "" "the code with a /proc that refuses the program's autogroup: every rule holds" +write_run witness-WitnessRefusedGcRemovesLeftover-refused violated WitnessRefusedGcRemovesLeftover "" "gc cannot check the group, so it removes an exited session while a process that the program left runs" +REFUSED=FALSE + # Without a token every kill falls back to the id that a manifest or the # host's own record names, as before program.json existed. TOKEN=FALSE diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 7b961476..be1f0af1 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -630,7 +630,7 @@ function destroyFacts() { const block = force.thenStatement; const first = indexOfStatement( block, - /^await stopSessionProcesses\(\s*sessionId,\s*await readSessionHost\(sessionDirectory, manifest\),\s*await readProgramGroup\(/, + /^await stopUnlessUnreadable\(\s*await readSessionHost\(sessionDirectory, manifest\),\s*\(\) => readProgramGroup\(sessionDirectory, manifest\.childPid\),?\s*\);$/, ); const reread = indexOfStatement( block, @@ -638,11 +638,7 @@ function destroyFacts() { ); const group = indexOfStatement( block, - /^const group = await readProgramGroup\(/, - ); - const second = indexOfStatement( - block, - /^await stopSessionProcesses\(\s*sessionId,\s*await readSessionHost\(sessionDirectory, current\),\s*group,/, + /^const group = await stopUnlessUnreadable\(\s*await readSessionHost\(sessionDirectory, current\),\s*\(\) => readProgramGroup\(sessionDirectory, current\.childPid\),?\s*\);$/, ); const records = indexOfStatement( block, @@ -652,8 +648,8 @@ function destroyFacts() { first >= 0 && reread > first && group > reread && - second > group && - records > second && + records > group && + stopsThenRecords.stops && calls(block, 'reconcileSession').length === 0; } const stop = requireDeclaration( @@ -683,6 +679,7 @@ function destroyFacts() { stopWaits && waitsForProcessesOnly, DestroyKeepsExitCode: keepsExitCode, + ForceSkipsUnreadableGroup: forceRecords && stopsThenRecords.skipsUnreadable, DestroyStopsLeftovers: stopsThenRecords.records && stopsThenRecords.stops && @@ -697,52 +694,123 @@ function destroyFacts() { }; } -// The statements of destroySession's local stopLeftoversThenRecordDestroyed: -// with DestroyStopsLeftovers it stops the group that program.json proves, -// waits for it, and only then records destroyed. readProvenProgramGroup -// returns the record whenever it has a token, or the unshared group when -// this process cannot prove that it shares the host's pid space. A session -// that a process which saw the group recorded destroyed gets no wait for an -// unshared group (trustsDestroyed). +// destroySession's local stopLeftoversThenRecordDestroyed hands +// stopUnlessUnreadable the read of program.json, and only then records +// destroyed. readProvenProgramGroup returns the record whenever it has a +// token, or the unshared group when this process cannot prove that it +// shares the host's pid space. A session that a process which saw the +// group recorded destroyed gets no wait for an unshared group +// (trustsDestroyed). stopUnlessUnreadable reads the group, stops it and +// waits. With skipsUnreadable, destroy --force that cannot read the group +// (a system error) stops the host alone instead. const UNSHARED_RETURN = 'return (await sharesHostPids(sessionDirectory, false)) ? record : UNSHARED_GROUP;'; -const STOP_UNLESS_TRUSTED = - "await stopSessionProcesses( sessionId, null, terminal.status === 'destroyed' && group !== null && 'unshared' in group ? null : group, sessionDirectory, signal, );"; -const STOP_ALWAYS = - 'await stopSessionProcesses( sessionId, null, group, sessionDirectory, signal, );'; +const RETURN_UNLESS_TRUSTED = + "return terminal.status === 'destroyed' && group !== null && 'unshared' in group ? null : group;"; -function stopLeftoversThenRecordDestroyed(destroy) { - let found = []; +function localArrows(destroy) { + const out = new Map(); walk(destroy.body, (node) => { if ( ts.isVariableDeclaration(node) && - node.name.getText() === 'stopLeftoversThenRecordDestroyed' && node.initializer !== undefined && ts.isArrowFunction(node.initializer) && ts.isBlock(node.initializer.body) ) { - found = node.initializer.body.statements.map((st) => - normalize(st.getText()), - ); + out.set(node.name.getText(), node.initializer.body.statements); } }); + return out; +} + +function statementsOf(block) { + return block.statements.map((st) => normalize(st.getText())); +} + +function stopUnlessUnreadableFacts(arrows) { + const st = arrows.get('stopUnlessUnreadable') ?? []; + const attempt = st[0]; + if ( + attempt === undefined || + !ts.isTryStatement(attempt) || + attempt.catchClause === undefined || + attempt.finallyBlock !== undefined + ) { + return { stops: false, skipsUnreadable: false }; + } + const tried = statementsOf(attempt.tryBlock).join('\n'); + const caught = statementsOf(attempt.catchClause.block).join('\n'); + const after = st.slice(1).map((s) => normalize(s.getText())); + const stops = + tried === + [ + 'const group = await readGroup();', + 'await stopSessionProcesses( sessionId, host, group, sessionDirectory, signal, );', + 'return group;', + ].join('\n'); + const skipsUnreadable = + caught === + 'if (force !== true || !isUnreadableGroupError(error)) { throw error; }' && + after.join('\n') === + [ + 'await stopSessionProcesses(sessionId, host, null, sessionDirectory, signal);', + 'return null;', + ].join('\n') && + bodyIs( + 'isUnreadableGroupError', + "if (hasErrorCode(error, ERROR_CODES.STORAGE_READ_ERROR)) { return true; } const code: unknown = error instanceof Error ? (error as { code?: unknown }).code : undefined; return ( !(error instanceof CliError) && typeof code === 'string' && /^E[A-Z0-9]+$/.test(code) );", + ); + return { + stops: stops && (caught === 'throw error;' || skipsUnreadable), + skipsUnreadable: stops && skipsUnreadable, + }; +} + +function stopLeftoversThenRecordDestroyed(destroy) { + const arrows = localArrows(destroy); + const found = arrows.get('stopLeftoversThenRecordDestroyed') ?? []; + const first = found[0]; + let read = []; + if ( + first !== undefined && + ts.isExpressionStatement(first) && + ts.isAwaitExpression(first.expression) && + ts.isCallExpression(first.expression.expression) + ) { + const call = first.expression.expression; + const reader = call.arguments[1]; + if ( + call.expression.getText() === 'stopUnlessUnreadable' && + call.arguments.length === 2 && + call.arguments[0].getText() === 'null' && + reader !== undefined && + ts.isArrowFunction(reader) && + ts.isBlock(reader.body) + ) { + read = statementsOf(reader.body); + } + } + const unless = stopUnlessUnreadableFacts(arrows); return { records: found.length > 0 && /^await recordDestroyed\(manifestFile, socketFile, terminal, null\);$/.test( - found.at(-1), + normalize(found.at(-1).getText()), ), stops: - found.length === 3 && - found[0] === + found.length === 2 && + read.length === 2 && + read[0] === 'const group = await readProvenProgramGroup(sessionDirectory);' && - [STOP_UNLESS_TRUSTED, STOP_ALWAYS].includes(found[1]) && + [RETURN_UNLESS_TRUSTED, 'return group;'].includes(read[1]) && + unless.stops && bodyIs( 'readProvenProgramGroup', `const record = await readProgramRecord(sessionDirectory); if (typeof record !== 'object' || !hasToken(record)) { return null; } ${UNSHARED_RETURN}`, ) && bodyIs('hasToken', 'return record.bootId !== null;'), - trustsDestroyed: found[1] === STOP_UNLESS_TRUSTED, + trustsDestroyed: read[1] === RETURN_UNLESS_TRUSTED, + skipsUnreadable: unless.skipsUnreadable, }; } From 4e9707e09855a9cf37ed54d47765c1c4849c9f07 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 09:25:28 +0000 Subject: [PATCH 06/17] fix(model): keep dblind unchanged when destroy writes the destroy marker --- .../skills/verify-session-lifecycle/model/SessionLifecycle.tla | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index ca0695e4..f23f0769 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -1328,7 +1328,7 @@ DestroyMarksFolder == ELSE /\ DestroyEnds("error") /\ UNCHANGED dmark /\ UNCHANGED <> \* recordDestroyed: writeManifest({ ...manifest, status: 'destroyed' }) from From 1c3c2772268d893426943d0eb9a7e6c5fb315447 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 09:27:32 +0000 Subject: [PATCH 07/17] docs: describe destroy --force without a readable group, and the refused-read runs USAGE says when gc names destroy --force and that a process the program left can outlive it. SKILL.md gets the ForceSkipsUnreadableGroup section, the five new runs, R11, R16 and R20 with their exclusions, and the Refused scope. facts.mjs hashes isUnreadableGroupError. --- .../skills/verify-session-lifecycle/SKILL.md | 65 +++++++++++-------- .../scripts/facts.mjs | 1 + docs/USAGE.md | 1 + 3 files changed, 40 insertions(+), 27 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 6a65632f..6ae64976 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -13,27 +13,27 @@ The tool is TLC, the TLA+ model checker, pinned to release 1.7.4 by sha256. The ## The rules -| Rule | What must hold | Harm when it breaks | -| ------------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | -| R1 `NoLiveSessionDeleted` | gc never removes the folder of a session whose host can still write to it. | A running or starting session loses its manifest and event log. | -| R2 `HostDeathOnlyWhenDead` | The manifest says "failed, host died" only when the host process is dead. | `list` and `inspect` show a live session as failed. Commands refuse it. | -| R3 `TerminalIsFinal` | Once the manifest shows exited, failed or destroyed, it never shows running again. | A finished session looks running, and the next reconcile marks it failed. | -| R4 `RecordedExitKept` | Once the manifest records that the program exited, only `destroy` changes it, to destroyed, and keeps the exit code. | A program that exited 0 is reported as failed, with its exit code lost. | -| R5 `RunningSessionReachable` | While the host serves a running program, the socket file exists. | The session runs, but no command can reach it. | -| R6 `HostStartsWhenCreated` | A host never fails to start because another process removed or rewrote its files. | `create` fails with `HOST_UNREACHABLE` for a session nobody touched. | -| R7 `TerminalIsLastWrite` | Once the manifest shows exited, failed or destroyed, the host has no write left to make. | gc removes the folder while the host still writes to it, and the host's write then fails. | -| R8 `DestroyedOnlyWhenEnded` | While the host lives, the manifest says destroyed only after the host saw the program end. | `list` hides a program that still runs, and gc removes its folder. | -| R9 `DestroyEndsDestroyed` | `destroy` reports success only after it wrote destroyed or read it. | `destroy` says `destroyed: true`, but the session reads failed, "host process died unexpectedly", until a second `destroy`. | -| R10 `RemovedFolderStaysRemoved` | Once gc removed the session folder, no write brings it back. | A late write creates the folder again with only `session.json`. `list --all` shows that stub session until the next gc removes it. | -| R11 `DestroyedProgramStopped` | When the manifest says destroyed, no process of the program's process group runs, unless the program exited on its own first or no manifest named its pid. | A process of the session keeps running, `list` hides it, and nothing stops it later. | -| R13 `LiveGroupStaysNamed` | While a process of the program's process group runs, a manifest that named the program still names it. | The session reads failed or destroyed without `childPid`, so no later `destroy` or reconcile can stop the process that still runs. | -| R14 `DestroyOutlivesProgram` | `destroy` is never killed before it reports, also when it runs inside the program's session. | `destroy` prints nothing. With `--force` it kills its own group, and the session reads exited, not destroyed. | -| R15 `NoUnrelatedGroupKilled` | No kill reaches a process group that took the program's group id after the program's group ended. | `destroy`, `destroy --force`, a reconcile or the host's shutdown sends SIGKILL to an unrelated group, such as the program of another session. | -| R16 `DestroyedSessionStopped` | When the manifest says destroyed, no process of the program's group runs, also none that the program left when it exited on its own, unless the host died before `program.json` named the program. | `destroy` reports `destroyed: true` while a process of the session runs, `list` hides it, and nothing stops it later. | -| R17 `FailedCreateStopped` | Once `create` gave up on its host, the host keeps the session `running` only while `create`'s SIGTERM is on its way to it, or while the host has yet to check for the create-failed marker. | `create` fails with `HOST_UNREACHABLE`, but the session runs, and `list --all` shows it running. | -| R18 `DestroyedStaysDestroyed` | Once `destroy` reported success, the manifest says destroyed while the session folder exists, except while a reconcile that wrote over it has yet to write destroyed again. | `destroy` reports `destroyed: true`, and the session then reads `failed`. | -| R19 `NoUnrelatedHostKilled` | No kill of `destroy --force` reaches a process that took the host's pid after the host ended. | `destroy --force` sends SIGKILL to an unrelated process that got the crashed host's pid. | -| R20 `RemovedSessionStopped` | gc in the host's pid space removes a session folder, and with it `program.json`, only once no process of the program's group runs, also none that the program left when it exited on its own. | A process of the session keeps running, and nothing can prove or stop it later. | +| Rule | What must hold | Harm when it breaks | +| ------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | +| R1 `NoLiveSessionDeleted` | gc never removes the folder of a session whose host can still write to it. | A running or starting session loses its manifest and event log. | +| R2 `HostDeathOnlyWhenDead` | The manifest says "failed, host died" only when the host process is dead. | `list` and `inspect` show a live session as failed. Commands refuse it. | +| R3 `TerminalIsFinal` | Once the manifest shows exited, failed or destroyed, it never shows running again. | A finished session looks running, and the next reconcile marks it failed. | +| R4 `RecordedExitKept` | Once the manifest records that the program exited, only `destroy` changes it, to destroyed, and keeps the exit code. | A program that exited 0 is reported as failed, with its exit code lost. | +| R5 `RunningSessionReachable` | While the host serves a running program, the socket file exists. | The session runs, but no command can reach it. | +| R6 `HostStartsWhenCreated` | A host never fails to start because another process removed or rewrote its files. | `create` fails with `HOST_UNREACHABLE` for a session nobody touched. | +| R7 `TerminalIsLastWrite` | Once the manifest shows exited, failed or destroyed, the host has no write left to make. | gc removes the folder while the host still writes to it, and the host's write then fails. | +| R8 `DestroyedOnlyWhenEnded` | While the host lives, the manifest says destroyed only after the host saw the program end. | `list` hides a program that still runs, and gc removes its folder. | +| R9 `DestroyEndsDestroyed` | `destroy` reports success only after it wrote destroyed or read it. | `destroy` says `destroyed: true`, but the session reads failed, "host process died unexpectedly", until a second `destroy`. | +| R10 `RemovedFolderStaysRemoved` | Once gc removed the session folder, no write brings it back. | A late write creates the folder again with only `session.json`. `list --all` shows that stub session until the next gc removes it. | +| R11 `DestroyedProgramStopped` | When the manifest says destroyed, no process of the program's process group runs, unless the program exited on its own first, no manifest named its pid, or `destroy --force` could not read the group. | A process of the session keeps running, `list` hides it, and nothing stops it later. | +| R13 `LiveGroupStaysNamed` | While a process of the program's process group runs, a manifest that named the program still names it. | The session reads failed or destroyed without `childPid`, so no later `destroy` or reconcile can stop the process that still runs. | +| R14 `DestroyOutlivesProgram` | `destroy` is never killed before it reports, also when it runs inside the program's session. | `destroy` prints nothing. With `--force` it kills its own group, and the session reads exited, not destroyed. | +| R15 `NoUnrelatedGroupKilled` | No kill reaches a process group that took the program's group id after the program's group ended. | `destroy`, `destroy --force`, a reconcile or the host's shutdown sends SIGKILL to an unrelated group, such as the program of another session. | +| R16 `DestroyedSessionStopped` | When the manifest says destroyed, no process of the program's group runs, also none that the program left when it exited on its own, unless the host died before `program.json` named the program or `destroy --force` could not read the group. | `destroy` reports `destroyed: true` while a process of the session runs, `list` hides it, and nothing stops it later. | +| R17 `FailedCreateStopped` | Once `create` gave up on its host, the host keeps the session `running` only while `create`'s SIGTERM is on its way to it, or while the host has yet to check for the create-failed marker. | `create` fails with `HOST_UNREACHABLE`, but the session runs, and `list --all` shows it running. | +| R18 `DestroyedStaysDestroyed` | Once `destroy` reported success, the manifest says destroyed while the session folder exists, except while a reconcile that wrote over it has yet to write destroyed again. | `destroy` reports `destroyed: true`, and the session then reads `failed`. | +| R19 `NoUnrelatedHostKilled` | No kill of `destroy --force` reaches a process that took the host's pid after the host ended. | `destroy --force` sends SIGKILL to an unrelated process that got the crashed host's pid. | +| R20 `RemovedSessionStopped` | gc in the host's pid space, with a `/proc` that shows the autogroups, removes a session folder, and with it `program.json`, only once no process of the program's group runs, also none that the program left when it exited on its own, unless `destroy --force` could not read the group. | A process of the session keeps running, and nothing can prove or stop it later. | `TypeOK` also runs in every run. When it breaks, the model is wrong, not the code. @@ -41,8 +41,8 @@ The tool is TLC, the TLA+ model checker, pinned to release 1.7.4 by sha256. The Yes, when the diff changes any of these: -- `src/host/lifecycle.ts`: `allocateSession` (and the order of its `launch` call and first manifest write), `launchHost`, `isProcessAlive`, the host proof (`readSessionHost`, `psShowsSessionHost`, `isHostAlive`, `hostMatches`, `killHostBestEffort`), `cliRunsInsideProgramSession` with `ownLinuxSessionId`, `ownProcessGroupId`, `controllingTerminal` and `sharesControllingTerminal`, `reconcileSession`, and `destroySession` with its local `stopLeftoversThenRecordDestroyed` and its helpers `recordDestroyed`, `stopSessionProcesses`, `readSessionManifestOrThrow`, `waitForTerminalManifest`, `waitForProcessesToExit` and `killProcessBestEffort`, and `removeDeadHostSocket`, which `gc` and `destroySession` call. -- `src/host/programGroup.ts`: the token capture (`captureProgram`, `captureToken`, `readAutogroup`, `parseAutogroup`, `parseProcStat`), the `/proc` reads (`readProcFileIfExists`, `readLiveThreadState`, `readProcStat`, `readShownProcStat`, `isRefusedRead`, `readBootId`), the record (`writeProgramRecord`, `readProgramRecord`, `readProvenProgramGroup`, `readProgramGroup`, `provenProgramGroupRuns` with its `GC_JUDGEMENTS` limit, `judgeGroupForGc`, `judgeFrozenGroup`, `probeFindsGroup`), `procShowsOwnPidSpace`, the verdict (`judgeProgramGroup`, `readGroupMembers`), and the kill and the probe (`stopProgramGroup`, `isProgramGroupAlive`, `processGroupTarget`, `isProcessGroupAlive` with `groupHasLiveProcess` and `procHidesOtherUsers`, `killProcessGroupBestEffort`, `signalProcessGroup`). +- `src/host/lifecycle.ts`: `allocateSession` (and the order of its `launch` call and first manifest write), `launchHost`, `isProcessAlive`, the host proof (`readSessionHost`, `psShowsSessionHost`, `isHostAlive`, `hostMatches`, `killHostBestEffort`), `cliRunsInsideProgramSession` with `ownLinuxSessionId`, `ownProcessGroupId`, `controllingTerminal` and `sharesControllingTerminal`, `reconcileSession`, and `destroySession` with its local `stopLeftoversThenRecordDestroyed` and `stopUnlessUnreadable` and its helpers `recordDestroyed`, `stopSessionProcesses`, `readSessionManifestOrThrow`, `waitForTerminalManifest`, `waitForProcessesToExit` and `killProcessBestEffort`, and `removeDeadHostSocket`, which `gc` and `destroySession` call. +- `src/host/programGroup.ts`: the token capture (`captureProgram`, `captureToken`, `readAutogroup`, `parseAutogroup`, `parseProcStat`), the `/proc` reads (`readProcFileIfExists`, `readLiveThreadState`, `readProcStat`, `readShownProcStat`, `isRefusedRead`, `readBootId`), the record (`writeProgramRecord`, `readProgramRecord`, `isUnreadableGroupError`, `readProvenProgramGroup`, `readProgramGroup`, `provenProgramGroupRuns` with its `GC_JUDGEMENTS` limit, `judgeGroupForGc`, `judgeFrozenGroup`, `probeFindsGroup`), `procShowsOwnPidSpace`, the verdict (`judgeProgramGroup`, `readGroupMembers`), and the kill and the probe (`stopProgramGroup`, `isProgramGroupAlive`, `processGroupTarget`, `isProcessGroupAlive` with `groupHasLiveProcess` and `procHidesOtherUsers`, `killProcessGroupBestEffort`, `signalProcessGroup`). - `src/host/hostMain.ts`: `waitForManifestFromCreate`, `isSessionCommandable`, and in `runHost` the start-up statements (the manifest wait, the `hostPid === process.pid` check, the `host.json` write with `captureHost` and `writeHostRecord`, `createSerialManifestWriter`, `EventLog.open`, the create-failed marker check, `createPty`, `setChildPid`, `captureProgram`), `hangUpProgram` with its kill timer and the `SHUTDOWN_KILL_GRACE_MS` constant, `startIdlePolling` (the idle time-out), `initiateShutdown`, `startShutdown`, `handlePtyExit` with its wait for the program's group, `pty.onExit`, the `SIGTERM` handler, the `resize` and `destroy` handlers, and the last `try` block (the `program.json` write, the start-up manifest write and `rpcServer.listen`). - `src/host/manifestWriter.ts` `createSerialManifestWriter`. - `src/cli/commands/gc.ts` `gcSessions` and `defaultDependencies`, `src/cli/commands/create.ts` `runCreateCommand` with `waitForReadyHost`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`. @@ -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. On a CI runner with 4 vCPUs and the default `CHECK_JOBS` of 4 it takes about an hour, so CI runs it in four shares. Ten runs explore more than 20 million distinct states each, so `CHECK_JOBS=79` 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. On a CI runner with 4 vCPUs and the default `CHECK_JOBS` of 4 it takes about an hour, so CI runs it in four shares. Ten runs explore more than 20 million distinct states each, so `CHECK_JOBS=84` 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-six 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 thirty-seven 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 79 times and prints one line per run. +3. It runs TLC 84 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. @@ -100,6 +100,11 @@ At the sync commit, the expected results are: | `witness-WitnessUnsharedDestroyCompletes-otherspace` | violated | A plain `destroy` from another pid space still reports success, because it trusts the host's `destroyed` record. | | `witness-WitnessUnsharedGcRemovesLeftover-otherspace` | violated | gc in another pid space cannot check the group, so it removes an exited session while a process that the program left runs. | | `mutant-UnsharedGroupReadsUnknown-otherspace`, `mutant-CreateRecordsHost-otherspace` | violated | R16: without the guard, the group reads gone where nothing shows it, and `destroy` of an exited session records destroyed while a process that the program left runs. | +| `current-checkfails`, the code as it is when every read of `program.json` by `destroy`, `list` and `gc` fails, every rule | pass | `CheckFails`: a read that fails with a system error (EACCES on `program.json`, EIO on `/proc`). gc and its reconcile skip the session, a plain `destroy` fails, and `destroy --force` records destroyed after it stopped the host alone. R11, R16 and R20 leave out a session that such a `destroy --force` recorded (the ghost `dblind`). | +| `witness-WitnessUncheckedForceDestroys-checkfails` | violated | `destroy --force` reports success for a session whose group it cannot read while a process that the program left runs. | +| `mutant-ForceSkipsUnreadableGroup-checkfails` | pass | Without the guard, `destroy --force` fails on the read like a plain `destroy`, so `WitnessUncheckedForceDestroys` is never reached, and no command removes the session. | +| `current-refused`, the code as it is when `/proc` of `destroy`, `list` and `gc` refuses the autogroup of the program's processes, every rule | pass | `Refused`: the group reads `unknown`, which reads alive while a process of it runs, and gets no kill. `destroy` then fails with `HOST_TIMEOUT` until the group ends, and gc reads the group not proven. R20 leaves `Refused` out. | +| `witness-WitnessRefusedGcRemovesLeftover-refused` | violated | gc that cannot check the group removes an exited session while a process that the program left runs. | | `mutant-HostChecksCreateFailed` | pass | Redundant off Windows: the SIGTERM of a `create` that gave up stops the host. | | `current-win32`, the code as it is on Windows, without a token and with a SIGTERM that ends the host at once, R1 to R14 and R17 to R19 | pass | `Win32`: `create` sends the SIGTERM only when the manifest names the program, and that SIGTERM is a host crash. | | `mutant-HostChecksCreateFailed-win32` | violated | R17: without the marker, a host that the manifest does not name yet keeps serving after `create` gave up. | @@ -485,6 +490,12 @@ node --import tsx src/cli/main.ts destroy "$id" --json node --import tsx src/cli/main.ts gc --json # removes the session ``` +### `ForceSkipsUnreadableGroup`: no command removes a session whose group cannot be read + +A read of the program's group that fails with a system error, such as `program.json` that refuses the read (EACCES) or a `/proc` scan that fails (EIO), fails every later read too. gc kept such a session, plain `destroy` failed on the same read, and so did `destroy --force`, so no command removed the session. No safety rule breaks then, because the model has no rule for a session that stays forever. + +Now `destroySession` runs every group read of a terminal session, and both rounds of `--force`, through its local `stopUnlessUnreadable`. That reads the group, stops it and waits for it. With `--force`, a read that `isUnreadableGroupError` names a system error makes it stop the host alone instead, and the wait then proves the host dead. A group that reads alive and a host that does not end still throw `HOST_TIMEOUT`. `recordDestroyed` then records destroyed, and a process that the program left can outlive it. gc names `destroy --force` in its skip reason for such a read. In the model, `CheckFails` makes every read of `program.json` by `destroy`, `list` and `gc` fail while the record exists, and the ghost `dblind` marks the destroyed record that such a `destroy --force` wrote. R11, R16 and R20 leave it out. `mutant-ForceSkipsUnreadableGroup-checkfails` expects pass, because without the guard `WitnessUncheckedForceDestroys` is never reached. The integration tests "destroy --force ends an exited session whose program.json it cannot read" and "destroy --force ends a session whose host died and whose program.json it cannot read" make `program.json` unreadable with `chmod 000`. + ### `CreateRecordsHost`: a CLI in another pid space reads a starting host dead (R2) A CLI in another pid namespace finds no process with the host's pid, so `judgeHost` reads the host dead unless `host.json` names it. The host wrote `host.json` only once it had read its manifest. A `list`, `inspect` or `gc` in another pid namespace that read the session between create's first manifest write and that record recorded a live host `failed`, and `gc` could then remove its folder. @@ -547,7 +558,7 @@ It assumes: - The kernel does not reuse a pid while a process group with that id exists, so a kill of the program's group id reaches only that group while a process of it runs. Once the whole group has ended, a new process can get that id and lead an unrelated group (case 5 of coder/agent-tty#203). The model lets that happen at any step after the group ended. With a token, `stopProgramGroup` kills only right after it read a live member that carries the token again, and the model takes that check and the kill as one step. No API holds a process group the way a pidfd holds one process, so a gap stays between the check and the `kill(2)`: from the start of the member's re-read to the kill call it took p50 24 µs, p99 69 µs and at most 81 µs over 300 kills at a load average of 43. A group that takes the id inside that gap needs every member to exit, the pid counter to wrap onto the id, and the new process to lead a group, all within those microseconds. - The program runs from the spawn on, but `program.json` names it only after `captureProgram` read its token and `writeProgramRecord` renamed the file, in the same synchronous block. A host death inside that block leaves a program that no file names, and R16 exempts it (case 2 of coder/agent-tty#203). Over 150 sequential `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, that took a median of 2.8 ms, a 90th percentile of 4.3 ms and at most 66 ms. A scratch build of `runHost` timed it with `performance.now()`. `captureProgram` took a median of 1.3 ms and at most 7.3 ms of that, so the long tail lies in the rest of the block and the write. node-pty returns before the child has called `setsid()`, so the capture polls for at most 250 ms until the child leads its own session. - `OtherPidSpace` changes only how `destroy`, `list` and `gc` see the program's group. Their view of the host stays as in the shared pid space. `CliHostAlive` gives their view of the host: `judgeHost` reads a host that `host.json` names in another pid space as `unknown`, also after the host ended, so they never record it failed, and `hostMatches` never proves it, so `destroy --force` kills no host there. Without `host.json` they probe the pid in their own pid space, where no process has it, and read the host dead. `create` writes `host.json` before the first manifest names the host, so only a capture that failed, which the model leaves out, leaves that window open. -- `current` describes Linux with autogroups, where the capture finds the token. The model reads every autogroup and the boot id. When `/proc` refuses the boot id, or shows no autogroup id for a live member in the program's session (a refused read, or an empty or malformed file), `judgeProgramGroup` gives `unknown`: no kill, and `isProgramGroupAlive` reads the group alive, so `destroy` ends with `HOST_TIMEOUT` and a reconcile writes nothing, as while a process of another user runs. A CLI that cannot list `/proc` at all, as in a chroot, sees no member. `judgeProgramGroup` then gives `gone`, so nothing gets the kill, and the probe of the group decides whether it reads alive. The model leaves those refused reads out. Without a token, `readProgramGroup` falls back to the childPid of the manifest, as before `program.json` existed: on macOS and Windows, on a kernel without `CONFIG_SCHED_AUTOGROUP`, when the capture read no autogroup or no boot id, and for a session that an older agent-tty created. There a reconcile and `destroy --force` kill that childPid as it is, `destroy` of a terminal session kills nothing, and a kill can still reach an unrelated group that took the id. `current-no-token` checks that fallback: the constant `Token` is FALSE there, so `program.json` names no group, and the host kills and probes the program's pid as it is. R15 and R16 do not hold on that path, so the run checks R1 to R14. The fallback kills only while the session folder exists. gc's real `rm` deletes file by file, so while it runs the folder can exist after `program.json` is gone, and a fallback kill in that moment can use a childPid that gc's removal made stale. +- `current` describes Linux with autogroups, where the capture finds the token. The model reads every autogroup and the boot id. When `/proc` refuses the boot id, or shows no autogroup id for a live member in the program's session (a refused read, or an empty or malformed file), `judgeProgramGroup` gives `unknown`: no kill, and `isProgramGroupAlive` reads the group alive, so `destroy` ends with `HOST_TIMEOUT` and a reconcile writes nothing, as while a process of another user runs. A CLI that cannot list `/proc` at all, as in a chroot, sees no member. `judgeProgramGroup` then gives `gone`, so nothing gets the kill, and the probe of the group decides whether it reads alive. `current-refused` checks a `/proc` that refuses the autogroups for `destroy`, `list` and `gc` (`Refused`): they never prove the group, gc removes the session, and R20 leaves that out. The host's own reads stay as in `current`, so the model leaves out a refused read that the host shares. Without a token, `readProgramGroup` falls back to the childPid of the manifest, as before `program.json` existed: on macOS and Windows, on a kernel without `CONFIG_SCHED_AUTOGROUP`, when the capture read no autogroup or no boot id, and for a session that an older agent-tty created. There a reconcile and `destroy --force` kill that childPid as it is, `destroy` of a terminal session kills nothing, and a kill can still reach an unrelated group that took the id. `current-no-token` checks that fallback: the constant `Token` is FALSE there, so `program.json` names no group, and the host kills and probes the program's pid as it is. R15 and R16 do not hold on that path, so the run checks R1 to R14. The fallback kills only while the session folder exists. gc's real `rm` deletes file by file, so while it runs the folder can exist after `program.json` is gone, and a fallback kill in that moment can use a childPid that gc's removal made stale. - A `program.json` that does not parse, or that another version wrote, proves nothing: it gets no kill, and reconcile and `destroy` do not throw. A missing one gets the childPid fallback above. - A manifest write is atomic, because `writeManifest` renames a temp file. A write that fails counts as a host crash or a failed command. That covers a host write into a removed folder, which only a state that already breaks R1 reaches. - The host waits for its manifest while the `create` process lives, so it gives up only when `create` dies before that write. That counts as a host crash, which R6 does not cover. diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index be1f0af1..529fd99b 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -1589,6 +1589,7 @@ const COVERED = [ ['src/host/programGroup.ts', 'provenProgramGroupRuns'], ['src/host/programGroup.ts', 'judgeGroupForGc'], ['src/host/programGroup.ts', 'judgeFrozenGroup'], + ['src/host/programGroup.ts', 'isUnreadableGroupError'], ['src/host/programGroup.ts', 'GC_JUDGEMENTS'], ['src/host/programGroup.ts', 'probeFindsGroup'], ['src/host/lifecycle.ts', 'allocateSession'], diff --git a/docs/USAGE.md b/docs/USAGE.md index a0b70efa..60d62a3d 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -316,6 +316,7 @@ agent-tty record diff --at-seq-a 0 --json 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. `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 a system error, 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. A plain `destroy` fails on the same read. `destroy --force` then stops the host alone, without the read, 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`. A group that reads alive, or a host that does not end (`HOST_TIMEOUT`), still fails it. `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`). A `destroy` that runs inside the session, such as one typed into the session's shell, runs again outside the session and prints its result once the session has ended. The session's terminal is closed by then, so redirect stdout to keep the result, for example `agent-tty destroy "$AGENT_TTY_SESSION_ID" --json > destroy.json`. From ace08738b66b1a589ea2e4698a9f34e4a86db0df Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 09:32:03 +0000 Subject: [PATCH 08/17] fix(gc): freeze a group again when the frozen group still reads gone Codex on #326: SIGSTOP does not nest, so another gc or a destroy can send SIGCONT before this gc judges the frozen group, and a fork chain then read gone and lost program.json. judgeFrozenGroup now reads a frozen group that still reads gone as inconclusive, so provenProgramGroupRuns freezes it again, and only GC_JUDGEMENTS such judgements read it ended. The model has one gc and does not change, so the record comes from facts.mjs at this commit. --- .../skills/verify-session-lifecycle/SKILL.md | 2 +- .../verify-session-lifecycle/coverage.json | 4 +- .../scripts/facts.mjs | 6 +- src/host/programGroup.ts | 9 +- test/unit/host/programGroup.test.ts | 92 ++++++++++++++----- 5 files changed, 82 insertions(+), 31 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 6a65632f..6c2cac10 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -474,7 +474,7 @@ node -e 'console.log(require(process.argv[1]).status)' "$d/session.json" Without the guard, `gcSessions` removed the folder of every collectable session. A program that exits on its own can leave a process in its group, such as `sleep 300 &` after `trap "" HUP`, and the host does not kill at a normal exit. The rm deleted `program.json` with the folder, and that record is the only proof that the process is the program's, so no later command could stop it. -Now `gcSessions` calls `provenProgramGroupRuns` after its other checks and before the rm. It judges the group that `readProvenProgramGroup` gives, as the waits of `destroy` do, and gc skips the session with the reason "the session's program group still runs (destroy ends it)" while it proves the group, also under `--dry-run`: a live member carries the token. A read that throws skips the session too, with the error as the reason. A member of a fork chain can end between its stat and its autogroup read (`unknown`), or show up only after the judge's scans, so `judgeGroupForGc` reads such a judgement as inconclusive, and gc judges again, at most ten times. gc does not check a destroyed session, because `destroy` records destroyed only after a wait that read the group gone. A record without a token proves nothing, so gc removes such a session as before. gc never keeps a session that no command can remove: a group that gc cannot check proves nothing, and gc removes its session as before. That covers another pid space, where the group reads `unshared` (as after a container restart that keeps the home, when `host.json` names a pid namespace that no longer exists), and a `/proc` that refuses the boot id or the autogroup of a live member (`unknown`). So R20 holds only for a gc in the host's pid space, and `witness-WitnessUnsharedGcRemovesLeftover-otherspace` shows that a gc in another one removes an exited session while a process that the program left runs. gc judges without a SIGSTOP first, so a fork chain that no scan shows reads gone to the judge. So `provenProgramGroupRuns` also counts the group as running while the probe `kill(-pgid, 0)` finds its id and no scan shows a member, live or zombie (`GcProbesUnseenGroup`). Under a PID 1 that never reaps, the chain also leaves zombies in view, so the scans show only zombies while its live member escapes them. Then `judgeFrozenGroup` sends SIGSTOP, as `stopProgramGroup` does, judges the stopped group, whose stopped member stays in view, and sends SIGCONT in a `finally` (`GcFreezesUnseenGroup`). It sends SIGSTOP only where `/proc` shows its own pid space. `mutant-GcFreezesUnseenGroup-unseen-zombies` must violate R20, and "gc keeps an exited session while a fork chain runs behind its zombies" in `test/integration/non-reaping-init.test.ts` covers it. An unrelated group that took the id is in view and reads `unproven`, so it does not keep the session. `mutant-GcProbesUnseenGroup-unseen` must violate R20. The integration tests "gc keeps an exited session while a process that the program left runs" and "... while a fork chain that the program left runs" in `test/integration/lifecycle.test.ts` cover both, and "gc removes an exited session whose host.json names another pid namespace" covers the restart. +Now `gcSessions` calls `provenProgramGroupRuns` after its other checks and before the rm. It judges the group that `readProvenProgramGroup` gives, as the waits of `destroy` do, and gc skips the session with the reason "the session's program group still runs (destroy ends it)" while it proves the group, also under `--dry-run`: a live member carries the token. A read that throws skips the session too, with the error as the reason. A member of a fork chain can end between its stat and its autogroup read (`unknown`), or show up only after the judge's scans, so `judgeGroupForGc` reads such a judgement as inconclusive, and gc judges again, at most ten times. gc does not check a destroyed session, because `destroy` records destroyed only after a wait that read the group gone. A record without a token proves nothing, so gc removes such a session as before. gc never keeps a session that no command can remove: a group that gc cannot check proves nothing, and gc removes its session as before. That covers another pid space, where the group reads `unshared` (as after a container restart that keeps the home, when `host.json` names a pid namespace that no longer exists), and a `/proc` that refuses the boot id or the autogroup of a live member (`unknown`). So R20 holds only for a gc in the host's pid space, and `witness-WitnessUnsharedGcRemovesLeftover-otherspace` shows that a gc in another one removes an exited session while a process that the program left runs. gc judges without a SIGSTOP first, so a fork chain that no scan shows reads gone to the judge. So `provenProgramGroupRuns` also counts the group as running while the probe `kill(-pgid, 0)` finds its id and no scan shows a member, live or zombie (`GcProbesUnseenGroup`). Under a PID 1 that never reaps, the chain also leaves zombies in view, so the scans show only zombies while its live member escapes them. Then `judgeFrozenGroup` sends SIGSTOP, as `stopProgramGroup` does, judges the stopped group, whose stopped member stays in view, and sends SIGCONT in a `finally` (`GcFreezesUnseenGroup`). Another gc or a `destroy` can send SIGCONT before that judgement, so a frozen group that still reads gone is judged again with another SIGSTOP, and only `GC_JUDGEMENTS` such judgements read it ended. The model has one gc, so it leaves that race out. It sends SIGSTOP only where `/proc` shows its own pid space. `mutant-GcFreezesUnseenGroup-unseen-zombies` must violate R20, and "gc keeps an exited session while a fork chain runs behind its zombies" in `test/integration/non-reaping-init.test.ts` covers it. An unrelated group that took the id is in view and reads `unproven`, so it does not keep the session. `mutant-GcProbesUnseenGroup-unseen` must violate R20. The integration tests "gc keeps an exited session while a process that the program left runs" and "... while a fork chain that the program left runs" in `test/integration/lifecycle.test.ts` cover both, and "gc removes an exited session whose host.json names another pid namespace" covers the restart. ```sh id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'trap "" HUP; sleep 300 & exit 0' | 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 1b903163..cafb794e 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -48,7 +48,7 @@ "src/cli/commands/gc.ts#defaultDependencies": "81a9894438cb5be7", "src/host/programGroup.ts#provenProgramGroupRuns": "7b50817618b4b769", "src/host/programGroup.ts#judgeGroupForGc": "fb133ba2739116d1", - "src/host/programGroup.ts#judgeFrozenGroup": "54e81ca84cfeabac", + "src/host/programGroup.ts#judgeFrozenGroup": "d18458e7d70a5664", "src/host/programGroup.ts#GC_JUDGEMENTS": "180a0af01a4b81c7", "src/host/programGroup.ts#probeFindsGroup": "31ea7b5e835c0509", "src/host/lifecycle.ts#allocateSession": "43819af8c6c271ec", @@ -140,7 +140,7 @@ "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", "skill:model/SessionLifecycle.tla": "77ec28d60359f635", - "skill:scripts/facts.mjs": "d44209b878acbb50", + "skill:scripts/facts.mjs": "eded6c52629e3523", "skill:scripts/check.sh": "e33db0960de216fe" }, "callSites": { diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 7b961476..05e181ee 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -1455,7 +1455,9 @@ function gcFacts() { const judgesGone = probes || (tail.length === 1 && tail[0] === 'return false;'); // judgeFrozenGroup sends SIGSTOP only where /proc shows this process's pid - // space, judges the stopped group, and sends SIGCONT in a finally. + // space, judges the stopped group, and sends SIGCONT in a finally. A + // frozen group that still reads gone is inconclusive, so gc freezes it + // again: another gc or a destroy can have resumed it. const freezes = probes && last === @@ -1463,7 +1465,7 @@ function gcFacts() { body('judgeFrozenGroup').join('\n') === [ "if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { return false; }", - "try { const { verdict } = judgeLiveGroup(group); return verdict === 'owned' ? true : verdict === 'unknown' ? null : false; } finally { signalProcessGroup(group.pid, 'SIGCONT'); }", + "try { const { verdict } = judgeLiveGroup(group); return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; } finally { signalProcessGroup(group.pid, 'SIGCONT'); }", ].join('\n'); return { GcSkipsNonCollectable: reconcile >= 0 && collectable > reconcile, diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index c4784cf3..3050a703 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -645,15 +645,18 @@ function judgeGroupForGc(group: ProvenRecord): boolean | null { // The scans show only zombies of the group while the probe finds its id. // Under a PID 1 that never reaps, the zombies of a fork chain stay, and its // live member can escape both scans. SIGSTOP freezes the group, as in -// stopProgramGroup, and a stopped member stays in view, so a judgement of -// the frozen group decides. The group gets SIGCONT, also when a scan throws. +// stopProgramGroup, and a stopped member stays in view. Another gc or a +// destroy can send SIGCONT before the judgement, so a frozen group that +// still reads gone is judged again, with another SIGSTOP. A group that +// ended reads gone each time, so the bounded loop of provenProgramGroupRuns +// then reads it ended. The group gets SIGCONT, also when a scan throws. function judgeFrozenGroup(group: ProvenRecord): boolean | null { if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { return false; } try { const { verdict } = judgeLiveGroup(group); - return verdict === 'owned' ? true : verdict === 'unknown' ? null : false; + return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; } finally { signalProcessGroup(group.pid, 'SIGCONT'); } diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index b9aa086b..c16572b6 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -986,31 +986,77 @@ describe('a program group with a token, as a faked /proc shows it', () => { // Under a PID 1 that never reaps, the zombies of a fork chain stay in // view while its live member escapes both scans. A stopped member stays // in view, so gc freezes the group and judges it again. - it.each([ - { frozen: ['Z', 'T'], runs: true }, - { frozen: ['Z'], runs: false }, - ])( - 'freezes a group whose scans show only zombies, and reads it running: $runs when the frozen group shows $frozen', - async ({ frozen, runs }) => { - const directory = await recordedSession(); - try { - procShowsTokenGroup('Z'); - const signals: unknown[] = []; - vi.spyOn(process, 'kill').mockImplementation((_pid, signal) => { - signals.push(signal); - if (signal === 'SIGSTOP') { - procShowsTokenGroup(...frozen); + it('freezes a group whose scans show only zombies, and keeps it when the frozen group shows a live member', async () => { + const directory = await recordedSession(); + try { + procShowsTokenGroup('Z'); + const signals: unknown[] = []; + vi.spyOn(process, 'kill').mockImplementation((_pid, signal) => { + signals.push(signal); + if (signal === 'SIGSTOP') { + procShowsTokenGroup('Z', 'T'); + } + return true; + }); + + expect(await provenProgramGroupRuns(directory)).toBe(true); + expect(signals).toEqual([0, 'SIGSTOP', 'SIGCONT']); + } finally { + await rm(directory, { recursive: true, force: true }); + } + }); + + // Another gc or a destroy can resume the group before the judgement. + it('freezes the group again when the frozen group still shows only zombies', async () => { + const directory = await recordedSession(); + try { + procShowsTokenGroup('Z'); + const signals: unknown[] = []; + let stops = 0; + vi.spyOn(process, 'kill').mockImplementation((_pid, signal) => { + signals.push(signal); + if (signal === 'SIGSTOP') { + stops += 1; + if (stops === 2) { + procShowsTokenGroup('Z', 'T'); } - return true; - }); + } + return true; + }); - expect(await provenProgramGroupRuns(directory)).toBe(runs); - expect(signals).toEqual([0, 'SIGSTOP', 'SIGCONT']); - } finally { - await rm(directory, { recursive: true, force: true }); - } - }, - ); + expect(await provenProgramGroupRuns(directory)).toBe(true); + expect(signals).toEqual([ + 0, + 'SIGSTOP', + 'SIGCONT', + 0, + 'SIGSTOP', + 'SIGCONT', + ]); + } finally { + await rm(directory, { recursive: true, force: true }); + } + }); + + // GC_JUDGEMENTS bounds the judgements of a group that ended. + it('reads a group that shows only zombies, also frozen, ended after ten judgements', async () => { + const directory = await recordedSession(); + try { + procShowsTokenGroup('Z'); + const signals: unknown[] = []; + vi.spyOn(process, 'kill').mockImplementation((_pid, signal) => { + signals.push(signal); + return true; + }); + + expect(await provenProgramGroupRuns(directory)).toBe(false); + expect(signals).toEqual( + Array.from({ length: 10 }, () => [0, 'SIGSTOP', 'SIGCONT']).flat(), + ); + } finally { + await rm(directory, { recursive: true, force: true }); + } + }); it('gives a frozen group SIGCONT when its judgement throws', async () => { const directory = await recordedSession(); From 878e73b32b7a8a3f9406ec9d5628052023a80d3c Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 09:49:06 +0000 Subject: [PATCH 09/17] fix(model): mark a blind destroy at its destroy marker, which a reconcile repairs to destroyed --- .../model/SessionLifecycle.tla | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index f23f0769..3d4e139b 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -277,8 +277,9 @@ VARIABLES \* "killed" (it died before it reported) dsaw, \* ghost: destroy wrote "destroyed" or read it last dkill, \* ghost: destroy --force killed a live host - dblind \* ghost: destroy --force recorded destroyed without a read - \* of the program's group (CheckFails) + dblind \* ghost: destroy --force wrote the destroy marker or + \* destroyed without a read of the program's group + \* (CheckFails); a reconcile then repairs to destroyed diskVars == <> @@ -1325,10 +1326,11 @@ DestroyMarksFolder == /\ DestroyAt({"tmark"}) /\ IF dir THEN /\ dmark' = TRUE /\ dpc' = "twrite" /\ UNCHANGED <> - ELSE /\ DestroyEnds("error") /\ UNCHANGED dmark + /\ dblind' = (dblind \/ drd.grp = "blind") + ELSE /\ DestroyEnds("error") /\ UNCHANGED <> /\ UNCHANGED <> \* recordDestroyed: writeManifest({ ...manifest, status: 'destroyed' }) from From 4756e7647de939c97c8af3c5331dd90116e255db Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 09:53:45 +0000 Subject: [PATCH 10/17] chore: sync the lifecycle coverage record for destroy --force without a readable group check.sh --update-coverage at 4e9707e0 gave 83/84 runs as expected: only current-checkfails broke R16, through the destroy marker. 878e73b3 fixes that, and current-checkfails, its witness and its mutant passed alone on the fixed model (12,444,472 distinct states for current-checkfails). The other runs never assign the blind kind, and every fact value is the same, so this record comes from facts.mjs at this commit. CI runs every run again. --- .../skills/verify-session-lifecycle/coverage.json | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index cafb794e..ca480fb5 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -18,6 +18,7 @@ "ShutdownChecksCommandable": true, "DestroyRecordsDestroyed": true, "DestroyKeepsExitCode": true, + "ForceSkipsUnreadableGroup": true, "DestroyStopsLeftovers": true, "ProvesHostPid": true, "ReconcileRepairsDestroyed": true, @@ -44,11 +45,12 @@ "src/cli/commands/create.ts#waitForReadyHost": "a7fd2ba345b6bfd6", "src/cli/commands/destroy.ts#runDestroyCommand": "ecaa8b1d572da7c6", "src/cli/commands/destroy.ts#rerunInNewSession": "cf32d7d082758522", - "src/cli/commands/gc.ts#gcSessions": "a2ac8bd10f100332", + "src/cli/commands/gc.ts#gcSessions": "18a7249df9349120", "src/cli/commands/gc.ts#defaultDependencies": "81a9894438cb5be7", "src/host/programGroup.ts#provenProgramGroupRuns": "7b50817618b4b769", "src/host/programGroup.ts#judgeGroupForGc": "fb133ba2739116d1", "src/host/programGroup.ts#judgeFrozenGroup": "d18458e7d70a5664", + "src/host/programGroup.ts#isUnreadableGroupError": "561c6a1108e60d06", "src/host/programGroup.ts#GC_JUDGEMENTS": "180a0af01a4b81c7", "src/host/programGroup.ts#probeFindsGroup": "31ea7b5e835c0509", "src/host/lifecycle.ts#allocateSession": "43819af8c6c271ec", @@ -82,7 +84,7 @@ "src/host/lifecycle.ts#stopSessionProcesses": "d1abb608b1d2160a", "src/host/lifecycle.ts#recordDestroyed": "d3a74237a9c8459c", "src/host/lifecycle.ts#removeDeadHostSocket": "34ce07ab7b7e8d7b", - "src/host/lifecycle.ts#destroySession": "d840dd07a0e481f5", + "src/host/lifecycle.ts#destroySession": "eb4a0bae82dc09a5", "src/host/lifecycle.ts#isMarkedDestroyed": "d178f4a63473915c", "src/host/lifecycle.ts#writeMarkedDestroyed": "4863c35f70699757", "src/host/lifecycle.ts#reconcileSession": "739c83bf945000c6", @@ -139,9 +141,9 @@ "src/host/hostMain.ts#runHost(final try)": "251f1e68a4ec17cc", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "77ec28d60359f635", - "skill:scripts/facts.mjs": "eded6c52629e3523", - "skill:scripts/check.sh": "e33db0960de216fe" + "skill:model/SessionLifecycle.tla": "f1bb5d457a8f2ba0", + "skill:scripts/facts.mjs": "81c2bebbe52aeff4", + "skill:scripts/check.sh": "0e998387e38d04c8" }, "callSites": { "writeManifest": [ From 9f2b1c7a4f9c087c5865d988cfbea8f3a7b5b48e Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 09:53:57 +0000 Subject: [PATCH 11/17] docs(lifecycle): count the eleven runs above 20 million states --- .agents/skills/verify-session-lifecycle/SKILL.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 45a5f7db..b2febb55 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -65,7 +65,7 @@ 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. On a CI runner with 4 vCPUs and the default `CHECK_JOBS` of 4 it takes about an hour, so CI runs it in four shares. Ten runs explore more than 20 million distinct states each, so `CHECK_JOBS=84` 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. On a CI runner with 4 vCPUs and the default `CHECK_JOBS` of 4 it takes about an hour, so CI runs it in four shares. Eleven runs explore more than 20 million distinct states each, so `CHECK_JOBS=84` 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: From c666628533162cd0d42f4f676e0d4afcdae477e5 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 10:10:28 +0000 Subject: [PATCH 12/17] perf(gc): read a group that shows only zombies, also frozen twice, ended in one pass Advisor on #326: a zombie-only ended session under a PID 1 that never reaps took ten passes of six /proc scans and ten SIGSTOP/SIGCONT pairs: about 2.5 s with 2,264 processes in /proc. judgeFrozenGroup now freezes and judges at most twice (FROZEN_JUDGEMENTS). The second freeze covers a SIGCONT from another gc or a destroy. When that judgement reads gone too, nothing live was in view to freeze, and the group reads ended: about 300 ms there, and 50 ms with 258 processes. Also from the advisor: unit tests for a frozen group whose live member is in another autogroup or session (ended, and resumed) and for a /proc/self of another pid (no SIGSTOP), and USAGE limit 5 says that gc keeps the session only when the frozen check proves the group. --- .../skills/verify-session-lifecycle/SKILL.md | 4 +- .../verify-session-lifecycle/coverage.json | 5 +- .../scripts/facts.mjs | 53 +++++++++++-- docs/USAGE.md | 2 +- src/host/programGroup.ts | 32 +++++--- test/unit/host/programGroup.test.ts | 78 +++++++++++++++++-- 6 files changed, 147 insertions(+), 27 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index b2febb55..81961194 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -42,7 +42,7 @@ The tool is TLC, the TLA+ model checker, pinned to release 1.7.4 by sha256. The Yes, when the diff changes any of these: - `src/host/lifecycle.ts`: `allocateSession` (and the order of its `launch` call and first manifest write), `launchHost`, `isProcessAlive`, the host proof (`readSessionHost`, `psShowsSessionHost`, `isHostAlive`, `hostMatches`, `killHostBestEffort`), `cliRunsInsideProgramSession` with `ownLinuxSessionId`, `ownProcessGroupId`, `controllingTerminal` and `sharesControllingTerminal`, `reconcileSession`, and `destroySession` with its local `stopLeftoversThenRecordDestroyed` and `stopUnlessUnreadable` and its helpers `recordDestroyed`, `stopSessionProcesses`, `readSessionManifestOrThrow`, `waitForTerminalManifest`, `waitForProcessesToExit` and `killProcessBestEffort`, and `removeDeadHostSocket`, which `gc` and `destroySession` call. -- `src/host/programGroup.ts`: the token capture (`captureProgram`, `captureToken`, `readAutogroup`, `parseAutogroup`, `parseProcStat`), the `/proc` reads (`readProcFileIfExists`, `readLiveThreadState`, `readProcStat`, `readShownProcStat`, `isRefusedRead`, `readBootId`), the record (`writeProgramRecord`, `readProgramRecord`, `isUnreadableGroupError`, `readProvenProgramGroup`, `readProgramGroup`, `provenProgramGroupRuns` with its `GC_JUDGEMENTS` limit, `judgeGroupForGc`, `judgeFrozenGroup`, `probeFindsGroup`), `procShowsOwnPidSpace`, the verdict (`judgeProgramGroup`, `readGroupMembers`), and the kill and the probe (`stopProgramGroup`, `isProgramGroupAlive`, `processGroupTarget`, `isProcessGroupAlive` with `groupHasLiveProcess` and `procHidesOtherUsers`, `killProcessGroupBestEffort`, `signalProcessGroup`). +- `src/host/programGroup.ts`: the token capture (`captureProgram`, `captureToken`, `readAutogroup`, `parseAutogroup`, `parseProcStat`), the `/proc` reads (`readProcFileIfExists`, `readLiveThreadState`, `readProcStat`, `readShownProcStat`, `isRefusedRead`, `readBootId`), the record (`writeProgramRecord`, `readProgramRecord`, `isUnreadableGroupError`, `readProvenProgramGroup`, `readProgramGroup`, `provenProgramGroupRuns` with its `GC_JUDGEMENTS` limit, `judgeGroupForGc`, `judgeFrozenGroup` with its `FROZEN_JUDGEMENTS` limit, `probeFindsGroup`), `procShowsOwnPidSpace`, the verdict (`judgeProgramGroup`, `readGroupMembers`), and the kill and the probe (`stopProgramGroup`, `isProgramGroupAlive`, `processGroupTarget`, `isProcessGroupAlive` with `groupHasLiveProcess` and `procHidesOtherUsers`, `killProcessGroupBestEffort`, `signalProcessGroup`). - `src/host/hostMain.ts`: `waitForManifestFromCreate`, `isSessionCommandable`, and in `runHost` the start-up statements (the manifest wait, the `hostPid === process.pid` check, the `host.json` write with `captureHost` and `writeHostRecord`, `createSerialManifestWriter`, `EventLog.open`, the create-failed marker check, `createPty`, `setChildPid`, `captureProgram`), `hangUpProgram` with its kill timer and the `SHUTDOWN_KILL_GRACE_MS` constant, `startIdlePolling` (the idle time-out), `initiateShutdown`, `startShutdown`, `handlePtyExit` with its wait for the program's group, `pty.onExit`, the `SIGTERM` handler, the `resize` and `destroy` handlers, and the last `try` block (the `program.json` write, the start-up manifest write and `rpcServer.listen`). - `src/host/manifestWriter.ts` `createSerialManifestWriter`. - `src/cli/commands/gc.ts` `gcSessions` and `defaultDependencies`, `src/cli/commands/create.ts` `runCreateCommand` with `waitForReadyHost`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`. @@ -479,7 +479,7 @@ node -e 'console.log(require(process.argv[1]).status)' "$d/session.json" Without the guard, `gcSessions` removed the folder of every collectable session. A program that exits on its own can leave a process in its group, such as `sleep 300 &` after `trap "" HUP`, and the host does not kill at a normal exit. The rm deleted `program.json` with the folder, and that record is the only proof that the process is the program's, so no later command could stop it. -Now `gcSessions` calls `provenProgramGroupRuns` after its other checks and before the rm. It judges the group that `readProvenProgramGroup` gives, as the waits of `destroy` do, and gc skips the session with the reason "the session's program group still runs (destroy ends it)" while it proves the group, also under `--dry-run`: a live member carries the token. A read that throws skips the session too, with the error as the reason. A member of a fork chain can end between its stat and its autogroup read (`unknown`), or show up only after the judge's scans, so `judgeGroupForGc` reads such a judgement as inconclusive, and gc judges again, at most ten times. gc does not check a destroyed session, because `destroy` records destroyed only after a wait that read the group gone. A record without a token proves nothing, so gc removes such a session as before. gc never keeps a session that no command can remove: a group that gc cannot check proves nothing, and gc removes its session as before. That covers another pid space, where the group reads `unshared` (as after a container restart that keeps the home, when `host.json` names a pid namespace that no longer exists), and a `/proc` that refuses the boot id or the autogroup of a live member (`unknown`). So R20 holds only for a gc in the host's pid space, and `witness-WitnessUnsharedGcRemovesLeftover-otherspace` shows that a gc in another one removes an exited session while a process that the program left runs. gc judges without a SIGSTOP first, so a fork chain that no scan shows reads gone to the judge. So `provenProgramGroupRuns` also counts the group as running while the probe `kill(-pgid, 0)` finds its id and no scan shows a member, live or zombie (`GcProbesUnseenGroup`). Under a PID 1 that never reaps, the chain also leaves zombies in view, so the scans show only zombies while its live member escapes them. Then `judgeFrozenGroup` sends SIGSTOP, as `stopProgramGroup` does, judges the stopped group, whose stopped member stays in view, and sends SIGCONT in a `finally` (`GcFreezesUnseenGroup`). Another gc or a `destroy` can send SIGCONT before that judgement, so a frozen group that still reads gone is judged again with another SIGSTOP, and only `GC_JUDGEMENTS` such judgements read it ended. The model has one gc, so it leaves that race out. It sends SIGSTOP only where `/proc` shows its own pid space. `mutant-GcFreezesUnseenGroup-unseen-zombies` must violate R20, and "gc keeps an exited session while a fork chain runs behind its zombies" in `test/integration/non-reaping-init.test.ts` covers it. An unrelated group that took the id is in view and reads `unproven`, so it does not keep the session. `mutant-GcProbesUnseenGroup-unseen` must violate R20. The integration tests "gc keeps an exited session while a process that the program left runs" and "... while a fork chain that the program left runs" in `test/integration/lifecycle.test.ts` cover both, and "gc removes an exited session whose host.json names another pid namespace" covers the restart. +Now `gcSessions` calls `provenProgramGroupRuns` after its other checks and before the rm. It judges the group that `readProvenProgramGroup` gives, as the waits of `destroy` do, and gc skips the session with the reason "the session's program group still runs (destroy ends it)" while it proves the group, also under `--dry-run`: a live member carries the token. A read that throws skips the session too, with the error as the reason. A member of a fork chain can end between its stat and its autogroup read (`unknown`), or show up only after the judge's scans, so `judgeGroupForGc` reads such a judgement as inconclusive, and gc judges again, at most ten times. gc does not check a destroyed session, because `destroy` records destroyed only after a wait that read the group gone. A record without a token proves nothing, so gc removes such a session as before. gc never keeps a session that no command can remove: a group that gc cannot check proves nothing, and gc removes its session as before. That covers another pid space, where the group reads `unshared` (as after a container restart that keeps the home, when `host.json` names a pid namespace that no longer exists), and a `/proc` that refuses the boot id or the autogroup of a live member (`unknown`). So R20 holds only for a gc in the host's pid space, and `witness-WitnessUnsharedGcRemovesLeftover-otherspace` shows that a gc in another one removes an exited session while a process that the program left runs. gc judges without a SIGSTOP first, so a fork chain that no scan shows reads gone to the judge. So `provenProgramGroupRuns` also counts the group as running while the probe `kill(-pgid, 0)` finds its id and no scan shows a member, live or zombie (`GcProbesUnseenGroup`). Under a PID 1 that never reaps, the chain also leaves zombies in view, so the scans show only zombies while its live member escapes them. Then `judgeFrozenGroup` sends SIGSTOP, as `stopProgramGroup` does, judges the stopped group, whose stopped member stays in view, and sends SIGCONT in a `finally` (`GcFreezesUnseenGroup`). Another gc or a `destroy` can send SIGCONT before that judgement, so a frozen group that still reads gone gets another SIGSTOP and judgement (`FROZEN_JUDGEMENTS`, two). When that one reads gone too, nothing live was in view to freeze, and the group reads ended. So an ended group costs one pass: under a subreaper that never reaps, with a zombie of the group and 2,264 processes in `/proc`, `provenProgramGroupRuns` took about 300 ms, against about 2.5 s for ten passes. The model has one gc, so it leaves that race out. It sends SIGSTOP only where `/proc` shows its own pid space. `mutant-GcFreezesUnseenGroup-unseen-zombies` must violate R20, and "gc keeps an exited session while a fork chain runs behind its zombies" in `test/integration/non-reaping-init.test.ts` covers it. An unrelated group that took the id is in view and reads `unproven`, so it does not keep the session. `mutant-GcProbesUnseenGroup-unseen` must violate R20. The integration tests "gc keeps an exited session while a process that the program left runs" and "... while a fork chain that the program left runs" in `test/integration/lifecycle.test.ts` cover both, and "gc removes an exited session whose host.json names another pid namespace" covers the restart. ```sh id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'trap "" HUP; sleep 300 & exit 0' | 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 ca480fb5..4acdfb4e 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -49,7 +49,8 @@ "src/cli/commands/gc.ts#defaultDependencies": "81a9894438cb5be7", "src/host/programGroup.ts#provenProgramGroupRuns": "7b50817618b4b769", "src/host/programGroup.ts#judgeGroupForGc": "fb133ba2739116d1", - "src/host/programGroup.ts#judgeFrozenGroup": "d18458e7d70a5664", + "src/host/programGroup.ts#judgeFrozenGroup": "ca600530eddb26b2", + "src/host/programGroup.ts#FROZEN_JUDGEMENTS": "d4eb06aa7addbaa9", "src/host/programGroup.ts#isUnreadableGroupError": "561c6a1108e60d06", "src/host/programGroup.ts#GC_JUDGEMENTS": "180a0af01a4b81c7", "src/host/programGroup.ts#probeFindsGroup": "31ea7b5e835c0509", @@ -142,7 +143,7 @@ "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", "skill:model/SessionLifecycle.tla": "f1bb5d457a8f2ba0", - "skill:scripts/facts.mjs": "81c2bebbe52aeff4", + "skill:scripts/facts.mjs": "222f471610f4a026", "skill:scripts/check.sh": "0e998387e38d04c8" }, "callSites": { diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 763f0bb5..c457187b 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -1398,6 +1398,52 @@ function rerunFacts() { }; } +// judgeFrozenGroup freezes and judges at most FROZEN_JUDGEMENTS times: SIGSTOP +// where /proc shows this process's pid space, a judgement, and SIGCONT in a +// finally. A frozen judgement other than gone decides; gone freezes again. +function frozenJudgesTwice() { + const module = 'src/host/programGroup.ts'; + const limit = requireDeclaration(module, 'FROZEN_JUDGEMENTS').initializer; + const statements = requireDeclaration(module, 'judgeFrozenGroup').body + .statements; + const loop = statements[0]; + if ( + limit === undefined || + !ts.isNumericLiteral(limit) || + !Number.isInteger(Number(limit.text)) || + Number(limit.text) < 1 || + statements.length !== 2 || + loop === undefined || + !ts.isForStatement(loop) || + !ts.isBlock(loop.statement) || + normalize(statements[1].getText()) !== 'return false;' + ) { + return false; + } + const head = normalize( + `${loop.initializer?.getText()}; ${loop.condition?.getText()}; ${loop.incrementor?.getText()}`, + ); + const [stop, declared, judged, decides, ...rest] = loop.statement.statements; + return ( + head === 'let frozen = 0; frozen < FROZEN_JUDGEMENTS; frozen += 1' && + rest.length === 0 && + normalize(stop?.getText() ?? '') === + "if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { return false; }" && + normalize(declared?.getText() ?? '') === + "let verdict: GroupJudgement['verdict'];" && + judged !== undefined && + ts.isTryStatement(judged) && + judged.catchClause === undefined && + judged.finallyBlock !== undefined && + statementsOf(judged.tryBlock).join('\n') === + 'verdict = judgeLiveGroup(group).verdict;' && + statementsOf(judged.finallyBlock).join('\n') === + "signalProcessGroup(group.pid, 'SIGCONT');" && + normalize(decides?.getText() ?? '') === + "if (verdict !== 'gone') { return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; }" + ); +} + function gcFacts() { const fn = requireDeclaration('src/cli/commands/gc.ts', 'gcSessions'); let loop; @@ -1530,11 +1576,7 @@ function gcFacts() { probes && last === 'return live === null ? true : live ? null : judgeFrozenGroup(group);' && - body('judgeFrozenGroup').join('\n') === - [ - "if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { return false; }", - "try { const { verdict } = judgeLiveGroup(group); return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; } finally { signalProcessGroup(group.pid, 'SIGCONT'); }", - ].join('\n'); + frozenJudgesTwice(); return { GcSkipsNonCollectable: reconcile >= 0 && collectable > reconcile, GcFinalCheck: finalCheck, @@ -1591,6 +1633,7 @@ const COVERED = [ ['src/host/programGroup.ts', 'provenProgramGroupRuns'], ['src/host/programGroup.ts', 'judgeGroupForGc'], ['src/host/programGroup.ts', 'judgeFrozenGroup'], + ['src/host/programGroup.ts', 'FROZEN_JUDGEMENTS'], ['src/host/programGroup.ts', 'isUnreadableGroupError'], ['src/host/programGroup.ts', 'GC_JUDGEMENTS'], ['src/host/programGroup.ts', 'probeFindsGroup'], diff --git a/docs/USAGE.md b/docs/USAGE.md index 60d62a3d..3200fed4 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -369,7 +369,7 @@ Limits: 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. 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. It then reports "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, 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. +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, at most twice, and it keeps the session only when such a check proves the group. 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, 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: - At the idle time-out, a host that cannot run the check kills nothing, but it still records the session as `exited` once the program has exited, while a process that the program left can still run. A later `destroy` then fails with `HOST_TIMEOUT`, and `gc` can remove the session folder. - When `/proc` hides the processes of other users (mounted with `hidepid=2`, `hidepid=4`, `hidepid=invisible` or `hidepid=ptraceable`), a group whose processes agent-tty cannot see counts as running. A `destroy` that cannot prove such a group gone fails with `HOST_TIMEOUT` and does not record the session as `destroyed`. diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index c1a902dc..30353a83 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -660,24 +660,34 @@ function judgeGroupForGc(group: ProvenRecord): boolean | null { return live === null ? true : live ? null : judgeFrozenGroup(group); } +// A frozen judgement that reads gone is judged frozen once more. +const FROZEN_JUDGEMENTS = 2; + // The scans show only zombies of the group while the probe finds its id. // Under a PID 1 that never reaps, the zombies of a fork chain stay, and its // live member can escape both scans. SIGSTOP freezes the group, as in // stopProgramGroup, and a stopped member stays in view. Another gc or a // destroy can send SIGCONT before the judgement, so a frozen group that -// still reads gone is judged again, with another SIGSTOP. A group that -// ended reads gone each time, so the bounded loop of provenProgramGroupRuns -// then reads it ended. The group gets SIGCONT, also when a scan throws. +// still reads gone gets another SIGSTOP and judgement. When that one reads +// gone too, nothing live was in view to freeze, and the group reads ended, +// so an ended group costs one pass of provenProgramGroupRuns, not +// GC_JUDGEMENTS. The group gets SIGCONT, also when a scan throws. function judgeFrozenGroup(group: ProvenRecord): boolean | null { - if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { - return false; - } - try { - const { verdict } = judgeLiveGroup(group); - return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; - } finally { - signalProcessGroup(group.pid, 'SIGCONT'); + for (let frozen = 0; frozen < FROZEN_JUDGEMENTS; frozen += 1) { + if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { + return false; + } + let verdict: GroupJudgement['verdict']; + try { + verdict = judgeLiveGroup(group).verdict; + } finally { + signalProcessGroup(group.pid, 'SIGCONT'); + } + if (verdict !== 'gone') { + return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; + } } + return false; } function probeFindsGroup(pgid: number): boolean { diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index 718dd726..ad40aa89 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -1031,7 +1031,6 @@ describe('a program group with a token, as a faked /proc shows it', () => { 0, 'SIGSTOP', 'SIGCONT', - 0, 'SIGSTOP', 'SIGCONT', ]); @@ -1040,8 +1039,8 @@ describe('a program group with a token, as a faked /proc shows it', () => { } }); - // GC_JUDGEMENTS bounds the judgements of a group that ended. - it('reads a group that shows only zombies, also frozen, ended after ten judgements', async () => { + // Nothing live was in view to freeze, so one pass reads the group ended. + it('reads a group that shows only zombies, also frozen twice, ended in one pass', async () => { const directory = await recordedSession(); try { procShowsTokenGroup('Z'); @@ -1052,9 +1051,76 @@ describe('a program group with a token, as a faked /proc shows it', () => { }); expect(await provenProgramGroupRuns(directory)).toBe(false); - expect(signals).toEqual( - Array.from({ length: 10 }, () => [0, 'SIGSTOP', 'SIGCONT']).flat(), - ); + expect(signals).toEqual([ + 0, + 'SIGSTOP', + 'SIGCONT', + 'SIGSTOP', + 'SIGCONT', + ]); + } finally { + await rm(directory, { recursive: true, force: true }); + } + }); + + // A member of another session or autogroup that took the id is not the + // program's, and it gets its SIGCONT. + it.each([ + { + member: 'another autogroup', + frozen: () => { + procShowsTokenGroup('Z', 'T'); + const read = autogroupFile.read; + autogroupFile.read = (file) => + file === '/proc/101/autogroup' + ? '/autogroup-9 nice 0\n' + : (read?.(file) ?? null); + }, + }, + { + member: 'another session', + frozen: () => { + procShowsTokenGroup('Z'); + procHooks.stat?.set( + '101', + `101 (a) T 1 ${String(CHILD_PID)} 4242 ${STAT_TAIL}`, + ); + }, + }, + ])( + 'reads a frozen group whose live member is in $member ended, and resumes it', + async ({ frozen }) => { + const directory = await recordedSession(); + try { + procShowsTokenGroup('Z'); + const signals: unknown[] = []; + vi.spyOn(process, 'kill').mockImplementation((_pid, signal) => { + signals.push(signal); + if (signal === 'SIGSTOP') { + frozen(); + } + return true; + }); + + expect(await provenProgramGroupRuns(directory)).toBe(false); + expect(signals).toEqual([0, 'SIGSTOP', 'SIGCONT']); + } finally { + await rm(directory, { recursive: true, force: true }); + } + }, + ); + + // A /proc that names another pid than this process's belongs to another + // pid namespace, so the group reads unshared and gc sends no signal. + it('sends no SIGSTOP when /proc/self names another pid', async () => { + const directory = await recordedSession(); + try { + procShowsTokenGroup('Z'); + procHooks.self = '1'; + const kill = vi.spyOn(process, 'kill').mockReturnValue(true); + + expect(await provenProgramGroupRuns(directory)).toBe(false); + expect(kill).not.toHaveBeenCalled(); } finally { await rm(directory, { recursive: true, force: true }); } From cf79ceeabbc8ecf4c5986411dae0e3ce634d41ff Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 11:29:28 +0000 Subject: [PATCH 13/17] fix(destroy): skip the group only when its first read fails for good destroy --force fell back to stopping the host alone for any system error inside stopSessionProcesses, so a group that had already read alive and then hit an errno on the witness re-read or in the wait got no SIGKILL and was recorded destroyed. The fallback now covers only the read of the group and its first judgement. A failure after that verdict fails the destroy. isUnreadableGroupError now accepts a listed set of errnos that a retry does not change (EACCES, EPERM, EIO, EISDIR, ENOTDIR, ELOOP, ENAMETOOLONG), also as the cause of a STORAGE_READ_ERROR. EMFILE, ENFILE, ENOMEM, EAGAIN and EINTR no longer skip the group. Also: a unit test that reaches the /proc/self guard inside judgeFrozenGroup, a USAGE limit for a SIGCONT from another gc or destroy before both frozen judgements, the forced fallback in src/host/README.md, and the SKILL and facts.mjs updates. The model is unchanged and every guard constant matches the last full check. --- .../skills/verify-session-lifecycle/SKILL.md | 8 +-- .../verify-session-lifecycle/coverage.json | 7 +-- .../scripts/facts.mjs | 35 ++++++++----- docs/USAGE.md | 4 +- src/host/README.md | 2 +- src/host/lifecycle.ts | 37 +++++++++----- src/host/programGroup.ts | 42 ++++++++++----- test/unit/host/lifecycle.test.ts | 41 +++++++++++++++ test/unit/host/programGroup.test.ts | 51 +++++++++++++++++-- 9 files changed, 173 insertions(+), 54 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 81961194..895cbb29 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -42,7 +42,7 @@ The tool is TLC, the TLA+ model checker, pinned to release 1.7.4 by sha256. The Yes, when the diff changes any of these: - `src/host/lifecycle.ts`: `allocateSession` (and the order of its `launch` call and first manifest write), `launchHost`, `isProcessAlive`, the host proof (`readSessionHost`, `psShowsSessionHost`, `isHostAlive`, `hostMatches`, `killHostBestEffort`), `cliRunsInsideProgramSession` with `ownLinuxSessionId`, `ownProcessGroupId`, `controllingTerminal` and `sharesControllingTerminal`, `reconcileSession`, and `destroySession` with its local `stopLeftoversThenRecordDestroyed` and `stopUnlessUnreadable` and its helpers `recordDestroyed`, `stopSessionProcesses`, `readSessionManifestOrThrow`, `waitForTerminalManifest`, `waitForProcessesToExit` and `killProcessBestEffort`, and `removeDeadHostSocket`, which `gc` and `destroySession` call. -- `src/host/programGroup.ts`: the token capture (`captureProgram`, `captureToken`, `readAutogroup`, `parseAutogroup`, `parseProcStat`), the `/proc` reads (`readProcFileIfExists`, `readLiveThreadState`, `readProcStat`, `readShownProcStat`, `isRefusedRead`, `readBootId`), the record (`writeProgramRecord`, `readProgramRecord`, `isUnreadableGroupError`, `readProvenProgramGroup`, `readProgramGroup`, `provenProgramGroupRuns` with its `GC_JUDGEMENTS` limit, `judgeGroupForGc`, `judgeFrozenGroup` with its `FROZEN_JUDGEMENTS` limit, `probeFindsGroup`), `procShowsOwnPidSpace`, the verdict (`judgeProgramGroup`, `readGroupMembers`), and the kill and the probe (`stopProgramGroup`, `isProgramGroupAlive`, `processGroupTarget`, `isProcessGroupAlive` with `groupHasLiveProcess` and `procHidesOtherUsers`, `killProcessGroupBestEffort`, `signalProcessGroup`). +- `src/host/programGroup.ts`: the token capture (`captureProgram`, `captureToken`, `readAutogroup`, `parseAutogroup`, `parseProcStat`), the `/proc` reads (`readProcFileIfExists`, `readLiveThreadState`, `readProcStat`, `readShownProcStat`, `isRefusedRead`, `readBootId`), the record (`writeProgramRecord`, `readProgramRecord`, `isUnreadableGroupError` with its `UNREADABLE_ERRNOS`, `readProvenProgramGroup`, `readProgramGroup`, `provenProgramGroupRuns` with its `GC_JUDGEMENTS` limit, `judgeGroupForGc`, `judgeFrozenGroup` with its `FROZEN_JUDGEMENTS` limit, `probeFindsGroup`), `procShowsOwnPidSpace`, the verdict (`judgeProgramGroup`, `readGroupMembers`), and the kill and the probe (`stopProgramGroup`, `isProgramGroupAlive`, `processGroupTarget`, `isProcessGroupAlive` with `groupHasLiveProcess` and `procHidesOtherUsers`, `killProcessGroupBestEffort`, `signalProcessGroup`). - `src/host/hostMain.ts`: `waitForManifestFromCreate`, `isSessionCommandable`, and in `runHost` the start-up statements (the manifest wait, the `hostPid === process.pid` check, the `host.json` write with `captureHost` and `writeHostRecord`, `createSerialManifestWriter`, `EventLog.open`, the create-failed marker check, `createPty`, `setChildPid`, `captureProgram`), `hangUpProgram` with its kill timer and the `SHUTDOWN_KILL_GRACE_MS` constant, `startIdlePolling` (the idle time-out), `initiateShutdown`, `startShutdown`, `handlePtyExit` with its wait for the program's group, `pty.onExit`, the `SIGTERM` handler, the `resize` and `destroy` handlers, and the last `try` block (the `program.json` write, the start-up manifest write and `rpcServer.listen`). - `src/host/manifestWriter.ts` `createSerialManifestWriter`. - `src/cli/commands/gc.ts` `gcSessions` and `defaultDependencies`, `src/cli/commands/create.ts` `runCreateCommand` with `waitForReadyHost`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`. @@ -479,7 +479,7 @@ node -e 'console.log(require(process.argv[1]).status)' "$d/session.json" Without the guard, `gcSessions` removed the folder of every collectable session. A program that exits on its own can leave a process in its group, such as `sleep 300 &` after `trap "" HUP`, and the host does not kill at a normal exit. The rm deleted `program.json` with the folder, and that record is the only proof that the process is the program's, so no later command could stop it. -Now `gcSessions` calls `provenProgramGroupRuns` after its other checks and before the rm. It judges the group that `readProvenProgramGroup` gives, as the waits of `destroy` do, and gc skips the session with the reason "the session's program group still runs (destroy ends it)" while it proves the group, also under `--dry-run`: a live member carries the token. A read that throws skips the session too, with the error as the reason. A member of a fork chain can end between its stat and its autogroup read (`unknown`), or show up only after the judge's scans, so `judgeGroupForGc` reads such a judgement as inconclusive, and gc judges again, at most ten times. gc does not check a destroyed session, because `destroy` records destroyed only after a wait that read the group gone. A record without a token proves nothing, so gc removes such a session as before. gc never keeps a session that no command can remove: a group that gc cannot check proves nothing, and gc removes its session as before. That covers another pid space, where the group reads `unshared` (as after a container restart that keeps the home, when `host.json` names a pid namespace that no longer exists), and a `/proc` that refuses the boot id or the autogroup of a live member (`unknown`). So R20 holds only for a gc in the host's pid space, and `witness-WitnessUnsharedGcRemovesLeftover-otherspace` shows that a gc in another one removes an exited session while a process that the program left runs. gc judges without a SIGSTOP first, so a fork chain that no scan shows reads gone to the judge. So `provenProgramGroupRuns` also counts the group as running while the probe `kill(-pgid, 0)` finds its id and no scan shows a member, live or zombie (`GcProbesUnseenGroup`). Under a PID 1 that never reaps, the chain also leaves zombies in view, so the scans show only zombies while its live member escapes them. Then `judgeFrozenGroup` sends SIGSTOP, as `stopProgramGroup` does, judges the stopped group, whose stopped member stays in view, and sends SIGCONT in a `finally` (`GcFreezesUnseenGroup`). Another gc or a `destroy` can send SIGCONT before that judgement, so a frozen group that still reads gone gets another SIGSTOP and judgement (`FROZEN_JUDGEMENTS`, two). When that one reads gone too, nothing live was in view to freeze, and the group reads ended. So an ended group costs one pass: under a subreaper that never reaps, with a zombie of the group and 2,264 processes in `/proc`, `provenProgramGroupRuns` took about 300 ms, against about 2.5 s for ten passes. The model has one gc, so it leaves that race out. It sends SIGSTOP only where `/proc` shows its own pid space. `mutant-GcFreezesUnseenGroup-unseen-zombies` must violate R20, and "gc keeps an exited session while a fork chain runs behind its zombies" in `test/integration/non-reaping-init.test.ts` covers it. An unrelated group that took the id is in view and reads `unproven`, so it does not keep the session. `mutant-GcProbesUnseenGroup-unseen` must violate R20. The integration tests "gc keeps an exited session while a process that the program left runs" and "... while a fork chain that the program left runs" in `test/integration/lifecycle.test.ts` cover both, and "gc removes an exited session whose host.json names another pid namespace" covers the restart. +Now `gcSessions` calls `provenProgramGroupRuns` after its other checks and before the rm. It judges the group that `readProvenProgramGroup` gives, as the waits of `destroy` do, and gc skips the session with the reason "the session's program group still runs (destroy ends it)" while it proves the group, also under `--dry-run`: a live member carries the token. A read that throws skips the session too, with the error as the reason. A member of a fork chain can end between its stat and its autogroup read (`unknown`), or show up only after the judge's scans, so `judgeGroupForGc` reads such a judgement as inconclusive, and gc judges again, at most ten times. gc does not check a destroyed session, because `destroy` records destroyed only after a wait that read the group gone. A record without a token proves nothing, so gc removes such a session as before. gc never keeps a session that no command can remove: a group that gc cannot check proves nothing, and gc removes its session as before. That covers another pid space, where the group reads `unshared` (as after a container restart that keeps the home, when `host.json` names a pid namespace that no longer exists), and a `/proc` that refuses the boot id or the autogroup of a live member (`unknown`). So R20 holds only for a gc in the host's pid space, and `witness-WitnessUnsharedGcRemovesLeftover-otherspace` shows that a gc in another one removes an exited session while a process that the program left runs. gc judges without a SIGSTOP first, so a fork chain that no scan shows reads gone to the judge. So `provenProgramGroupRuns` also counts the group as running while the probe `kill(-pgid, 0)` finds its id and no scan shows a member, live or zombie (`GcProbesUnseenGroup`). Under a PID 1 that never reaps, the chain also leaves zombies in view, so the scans show only zombies while its live member escapes them. Then `judgeFrozenGroup` sends SIGSTOP, as `stopProgramGroup` does, judges the stopped group, whose stopped member stays in view, and sends SIGCONT in a `finally` (`GcFreezesUnseenGroup`). Another gc or a `destroy` can send SIGCONT before that judgement, so a frozen group that still reads gone gets another SIGSTOP and judgement (`FROZEN_JUDGEMENTS`, two). When that one reads gone too, the group reads ended. So an ended group costs one pass: under a subreaper that never reaps, with a zombie of the group and 2,264 processes in `/proc`, `provenProgramGroupRuns` took about 300 ms, against about 2.5 s for ten passes. A SIGCONT from elsewhere before both judgements lets a live member escape both scans, and gc then reads the live chain ended and removes its folder. The model has one gc, so it leaves that race out. It sends SIGSTOP only where `/proc` shows its own pid space. `mutant-GcFreezesUnseenGroup-unseen-zombies` must violate R20, and "gc keeps an exited session while a fork chain runs behind its zombies" in `test/integration/non-reaping-init.test.ts` covers it. An unrelated group that took the id is in view and reads `unproven`, so it does not keep the session. `mutant-GcProbesUnseenGroup-unseen` must violate R20. The integration tests "gc keeps an exited session while a process that the program left runs" and "... while a fork chain that the program left runs" in `test/integration/lifecycle.test.ts` cover both, and "gc removes an exited session whose host.json names another pid namespace" covers the restart. ```sh id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'trap "" HUP; sleep 300 & exit 0' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))') @@ -492,9 +492,9 @@ node --import tsx src/cli/main.ts gc --json # removes the session ### `ForceSkipsUnreadableGroup`: no command removes a session whose group cannot be read -A read of the program's group that fails with a system error, such as `program.json` that refuses the read (EACCES) or a `/proc` scan that fails (EIO), fails every later read too. gc kept such a session, plain `destroy` failed on the same read, and so did `destroy --force`, so no command removed the session. No safety rule breaks then, because the model has no rule for a session that stays forever. +A read of the program's group that fails with an errno that a retry does not change, such as `program.json` that refuses the read (EACCES) or a `/proc` scan that fails (EIO), fails every later read too. `UNREADABLE_ERRNOS` lists them: EACCES, EPERM, EIO, EISDIR, ENOTDIR, ELOOP and ENAMETOOLONG. gc kept such a session, plain `destroy` failed on the same read, and so did `destroy --force`, so no command removed the session. No safety rule breaks then, because the model has no rule for a session that stays forever. -Now `destroySession` runs every group read of a terminal session, and both rounds of `--force`, through its local `stopUnlessUnreadable`. That reads the group, stops it and waits for it. With `--force`, a read that `isUnreadableGroupError` names a system error makes it stop the host alone instead, and the wait then proves the host dead. A group that reads alive and a host that does not end still throw `HOST_TIMEOUT`. `recordDestroyed` then records destroyed, and a process that the program left can outlive it. gc names `destroy --force` in its skip reason for such a read. In the model, `CheckFails` makes every read of `program.json` by `destroy`, `list` and `gc` fail while the record exists, and the ghost `dblind` marks the destroyed record that such a `destroy --force` wrote. R11, R16 and R20 leave it out. `mutant-ForceSkipsUnreadableGroup-checkfails` expects pass, because without the guard `WitnessUncheckedForceDestroys` is never reached. The integration tests "destroy --force ends an exited session whose program.json it cannot read" and "destroy --force ends a session whose host died and whose program.json it cannot read" make `program.json` unreadable with `chmod 000`. +Now `destroySession` runs every group read of a terminal session, and both rounds of `--force`, through its local `stopUnlessUnreadable`. That reads the group, stops it and waits for it. With `--force`, a read or a first judgement (`isProgramGroupAlive`) that fails with an error that `isUnreadableGroupError` accepts makes it stop the host alone instead, and the wait then proves the host dead. The stop runs after the `try`, so a read that fails after that first judgement, as in the wait, still throws, and a group that read alive gets its kill or fails the destroy. EMFILE, ENFILE, ENOMEM, EAGAIN and EINTR still throw, because a later read can succeed. A group that reads alive and a host that does not end still throw `HOST_TIMEOUT`. `recordDestroyed` then records destroyed, and a process that the program left can outlive it. gc names `destroy --force` in its skip reason for such a read. In the model, `CheckFails` makes every read of `program.json` by `destroy`, `list` and `gc` fail while the record exists, and the ghost `dblind` marks the destroyed record that such a `destroy --force` wrote. R11, R16 and R20 leave it out. The model has no read that succeeds and then fails: such a read only fails a destroy, and no rule forbids a destroy that fails. `mutant-ForceSkipsUnreadableGroup-checkfails` expects pass, because without the guard `WitnessUncheckedForceDestroys` is never reached. The integration tests "destroy --force ends an exited session whose program.json it cannot read" and "destroy --force ends a session whose host died and whose program.json it cannot read" make `program.json` unreadable with `chmod 000`. ### `CreateRecordsHost`: a CLI in another pid space reads a starting host dead (R2) diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 4acdfb4e..d588ce71 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -51,7 +51,8 @@ "src/host/programGroup.ts#judgeGroupForGc": "fb133ba2739116d1", "src/host/programGroup.ts#judgeFrozenGroup": "ca600530eddb26b2", "src/host/programGroup.ts#FROZEN_JUDGEMENTS": "d4eb06aa7addbaa9", - "src/host/programGroup.ts#isUnreadableGroupError": "561c6a1108e60d06", + "src/host/programGroup.ts#isUnreadableGroupError": "e2d852aa5b45cb53", + "src/host/programGroup.ts#UNREADABLE_ERRNOS": "24de7f719ccf14be", "src/host/programGroup.ts#GC_JUDGEMENTS": "180a0af01a4b81c7", "src/host/programGroup.ts#probeFindsGroup": "31ea7b5e835c0509", "src/host/lifecycle.ts#allocateSession": "43819af8c6c271ec", @@ -85,7 +86,7 @@ "src/host/lifecycle.ts#stopSessionProcesses": "d1abb608b1d2160a", "src/host/lifecycle.ts#recordDestroyed": "d3a74237a9c8459c", "src/host/lifecycle.ts#removeDeadHostSocket": "34ce07ab7b7e8d7b", - "src/host/lifecycle.ts#destroySession": "eb4a0bae82dc09a5", + "src/host/lifecycle.ts#destroySession": "ee53946fe51e4df1", "src/host/lifecycle.ts#isMarkedDestroyed": "d178f4a63473915c", "src/host/lifecycle.ts#writeMarkedDestroyed": "4863c35f70699757", "src/host/lifecycle.ts#reconcileSession": "739c83bf945000c6", @@ -143,7 +144,7 @@ "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", "skill:model/SessionLifecycle.tla": "f1bb5d457a8f2ba0", - "skill:scripts/facts.mjs": "222f471610f4a026", + "skill:scripts/facts.mjs": "e858a4c852cd0f68", "skill:scripts/check.sh": "0e998387e38d04c8" }, "callSites": { diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index c457187b..7d2e272c 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -729,8 +729,10 @@ function statementsOf(block) { function stopUnlessUnreadableFacts(arrows) { const st = arrows.get('stopUnlessUnreadable') ?? []; - const attempt = st[0]; + const [declared, attempt, ...after] = st; if ( + declared === undefined || + normalize(declared.getText()) !== 'let group: ProgramGroup | null;' || attempt === undefined || !ts.isTryStatement(attempt) || attempt.catchClause === undefined || @@ -738,30 +740,34 @@ function stopUnlessUnreadableFacts(arrows) { ) { return { stops: false, skipsUnreadable: false }; } + // The try reads the group and judges it once, with no kill. Only a read + // or a judgement that fails there can skip the group: the stop comes + // after the try, so a read that fails after a verdict fails the destroy. const tried = statementsOf(attempt.tryBlock).join('\n'); - const caught = statementsOf(attempt.catchClause.block).join('\n'); - const after = st.slice(1).map((s) => normalize(s.getText())); + const caught = statementsOf(attempt.catchClause.block); const stops = tried === - [ - 'const group = await readGroup();', - 'await stopSessionProcesses( sessionId, host, group, sessionDirectory, signal, );', - 'return group;', - ].join('\n'); + ['group = await readGroup();', 'isProgramGroupAlive(group);'].join( + '\n', + ) && + after.map((s) => normalize(s.getText())).join('\n') === + [ + 'await stopSessionProcesses( sessionId, host, group, sessionDirectory, signal, );', + 'return group;', + ].join('\n'); const skipsUnreadable = - caught === - 'if (force !== true || !isUnreadableGroupError(error)) { throw error; }' && - after.join('\n') === + caught.join('\n') === [ - 'await stopSessionProcesses(sessionId, host, null, sessionDirectory, signal);', + 'if (force !== true || !isUnreadableGroupError(error)) { throw error; }', + 'await stopSessionProcesses( sessionId, host, null, sessionDirectory, signal, );', 'return null;', ].join('\n') && bodyIs( 'isUnreadableGroupError', - "if (hasErrorCode(error, ERROR_CODES.STORAGE_READ_ERROR)) { return true; } const code: unknown = error instanceof Error ? (error as { code?: unknown }).code : undefined; return ( !(error instanceof CliError) && typeof code === 'string' && /^E[A-Z0-9]+$/.test(code) );", + "const cause = hasErrorCode(error, ERROR_CODES.STORAGE_READ_ERROR) ? (error as Error).cause : error; const code: unknown = cause instanceof Error ? (cause as { code?: unknown }).code : undefined; return ( !(cause instanceof CliError) && typeof code === 'string' && UNREADABLE_ERRNOS.has(code) );", ); return { - stops: stops && (caught === 'throw error;' || skipsUnreadable), + stops: stops && (caught.join('\n') === 'throw error;' || skipsUnreadable), skipsUnreadable: stops && skipsUnreadable, }; } @@ -1635,6 +1641,7 @@ const COVERED = [ ['src/host/programGroup.ts', 'judgeFrozenGroup'], ['src/host/programGroup.ts', 'FROZEN_JUDGEMENTS'], ['src/host/programGroup.ts', 'isUnreadableGroupError'], + ['src/host/programGroup.ts', 'UNREADABLE_ERRNOS'], ['src/host/programGroup.ts', 'GC_JUDGEMENTS'], ['src/host/programGroup.ts', 'probeFindsGroup'], ['src/host/lifecycle.ts', 'allocateSession'], diff --git a/docs/USAGE.md b/docs/USAGE.md index 3200fed4..a426c523 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -316,7 +316,7 @@ agent-tty record diff --at-seq-a 0 --json 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. `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 a system error, 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. A plain `destroy` fails on the same read. `destroy --force` then stops the host alone, without the read, 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`. A group that reads alive, or a host that does not end (`HOST_TIMEOUT`), still fails it. +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, `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`. 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. `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`). A `destroy` that runs inside the session, such as one typed into the session's shell, runs again outside the session and prints its result once the session has ended. The session's terminal is closed by then, so redirect stdout to keep the result, for example `agent-tty destroy "$AGENT_TTY_SESSION_ID" --json > destroy.json`. @@ -369,7 +369,7 @@ Limits: 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. 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, at most twice, and it keeps the session only when such a check proves the group. 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, 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. +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, at most twice, and it keeps the session only when such a check proves the group. Another `gc` or a `destroy` that runs at the same time can send SIGCONT before each of those checks. A live process of the chain can then escape both scans, and `gc` 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, 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: - At the idle time-out, a host that cannot run the check kills nothing, but it still records the session as `exited` once the program has exited, while a process that the program left can still run. A later `destroy` then fails with `HOST_TIMEOUT`, and `gc` can remove the session folder. - When `/proc` hides the processes of other users (mounted with `hidepid=2`, `hidepid=4`, `hidepid=invisible` or `hidepid=ptraceable`), a group whose processes agent-tty cannot see counts as running. A `destroy` that cannot prove such a group gone fails with `HOST_TIMEOUT` and does not record the session as `destroyed`. diff --git a/src/host/README.md b/src/host/README.md index 87bcc2f4..1175889d 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -55,7 +55,7 @@ - The `signal` handler accepts only `SIGTERM`, `SIGINT`, `SIGKILL`, `SIGHUP`, `SIGUSR1` and `SIGUSR2`, and throws `INVALID_SIGNAL` for others. [hostMain.ts:runHost] - The `run` handler waits 30,000 ms by default. The `wait` handler needs exactly one of `exit` or `idleMs`, else it throws `INVALID_DURATION`. `waitForRender` polls every `RENDER_WAIT_POLL_INTERVAL_MS` (200 ms, `src/renderWait/limits.ts`). [hostMain.ts:runHost] - `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. [lifecycle.ts:destroySession] +- `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` stops and waits 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. [lifecycle.ts:destroySession] [programGroup.ts:isUnreadableGroupError] - `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 or is 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] diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index a11fde16..1bba2fe1 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -911,32 +911,41 @@ export async function destroySession( } // destroy --force of a session whose host is gone also ends a session - // whose program group it cannot read: a read of program.json or /proc - // that fails with a system error. It then stops what it can without the - // group and records destroyed, so a process that the program left can - // outlive it. A group that reads alive, or a host that does not end - // (HOST_TIMEOUT), still fails the destroy. + // whose program group it cannot read: the read of program.json, or the + // first judgement of the group, fails with an errno that every later read + // repeats. It then stops what it can without the group and records + // destroyed, so a process that the program left can outlive it. A failed + // read after that first judgement, a group that reads alive, and a host + // that does not end (HOST_TIMEOUT) still fail the destroy. const stopUnlessUnreadable = async ( host: SessionHost | null, readGroup: () => Promise, ): Promise => { + let group: ProgramGroup | null; try { - const group = await readGroup(); + group = await readGroup(); + isProgramGroupAlive(group); + } catch (error) { + if (force !== true || !isUnreadableGroupError(error)) { + throw error; + } await stopSessionProcesses( sessionId, host, - group, + null, sessionDirectory, signal, ); - return group; - } catch (error) { - if (force !== true || !isUnreadableGroupError(error)) { - throw error; - } + return null; } - await stopSessionProcesses(sessionId, host, null, sessionDirectory, signal); - return null; + await stopSessionProcesses( + sessionId, + host, + group, + sessionDirectory, + signal, + ); + return group; }; const stopLeftoversThenRecordDestroyed = async ( diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index 30353a83..fa999dd0 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -297,20 +297,34 @@ async function readProgramRecord( } } -// Whether a read of the program's group failed with a system error: a read -// of program.json or host.json (STORAGE_READ_ERROR), or a read of /proc -// (an errno code such as EIO or EACCES). A verdict, HOST_TIMEOUT, an abort -// or a bug is none of these. +// The errnos of a read that a retry does not change: the permissions or the +// file system refuse it (EACCES, EPERM, EIO), or a path names no readable +// file (EISDIR, ENOTDIR, ELOOP, ENAMETOOLONG). EMFILE, ENFILE, ENOMEM, +// EAGAIN and EINTR pass, so a later read can succeed. +const UNREADABLE_ERRNOS = new Set([ + 'EACCES', + 'EPERM', + 'EIO', + 'EISDIR', + 'ENOTDIR', + 'ELOOP', + 'ENAMETOOLONG', +]); + +// Whether a read of the program's group failed in a way that every later +// read repeats: a read of program.json or host.json (STORAGE_READ_ERROR) or +// of /proc, with one of UNREADABLE_ERRNOS. A verdict, HOST_TIMEOUT, an +// abort or a bug is none of these. export function isUnreadableGroupError(error: unknown): boolean { - if (hasErrorCode(error, ERROR_CODES.STORAGE_READ_ERROR)) { - return true; - } + const cause = hasErrorCode(error, ERROR_CODES.STORAGE_READ_ERROR) + ? (error as Error).cause + : error; const code: unknown = - error instanceof Error ? (error as { code?: unknown }).code : undefined; + cause instanceof Error ? (cause as { code?: unknown }).code : undefined; return ( - !(error instanceof CliError) && + !(cause instanceof CliError) && typeof code === 'string' && - /^E[A-Z0-9]+$/.test(code) + UNREADABLE_ERRNOS.has(code) ); } @@ -669,9 +683,11 @@ const FROZEN_JUDGEMENTS = 2; // stopProgramGroup, and a stopped member stays in view. Another gc or a // destroy can send SIGCONT before the judgement, so a frozen group that // still reads gone gets another SIGSTOP and judgement. When that one reads -// gone too, nothing live was in view to freeze, and the group reads ended, -// so an ended group costs one pass of provenProgramGroupRuns, not -// GC_JUDGEMENTS. The group gets SIGCONT, also when a scan throws. +// gone too, the group reads ended, so an ended group costs one pass of +// provenProgramGroupRuns, not GC_JUDGEMENTS. That reads a live fork chain +// ended only when a SIGCONT from elsewhere came before both judgements and +// the chain's live member escaped both scans. The group gets SIGCONT, also +// when a scan throws. function judgeFrozenGroup(group: ProvenRecord): boolean | null { for (let frozen = 0; frozen < FROZEN_JUDGEMENTS; frozen += 1) { if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { diff --git a/test/unit/host/lifecycle.test.ts b/test/unit/host/lifecycle.test.ts index 4f6b57a5..3d11261e 100644 --- a/test/unit/host/lifecycle.test.ts +++ b/test/unit/host/lifecycle.test.ts @@ -971,6 +971,47 @@ describe('destroySession', () => { }); }); + // Only a read that fails before the first verdict on the group lets + // destroy --force record destroyed without it. After a verdict that + // the group runs, a failed read leaves the group running. + it('destroy --force fails, and records nothing, when a read fails after the group read owned', async () => { + const directory = await seedLeftover(); + const stat = `/proc/${String(group)}/stat`; + let reads = 0; + fsHooks.files = new (class extends Map { + override get(path: string): string | Error | undefined { + if (path !== stat) { + return undefined; + } + reads += 1; + return reads > 1 ? errno('EIO') : undefined; + } + })(); + const kill = vi.spyOn(process, 'kill'); + + await expect(destroySession('session-01', true)).rejects.toMatchObject({ + code: 'EIO', + }); + expect(kill).not.toHaveBeenCalledWith(-group, 'SIGKILL'); + expect(await readManifest(manifestPath(directory))).toEqual(exited); + expect(reads).toBeGreaterThan(1); + }); + + it('destroy --force records destroyed, and kills nothing, when the first read of the group fails', async () => { + const directory = await seedLeftover(); + fsHooks.files = new Map([ + [`/proc/${String(group)}/stat`, errno('EIO')], + ]); + const kill = vi.spyOn(process, 'kill'); + + await destroySession('session-01', true); + + expect(kill).not.toHaveBeenCalledWith(-group, 'SIGKILL'); + expect(await readManifest(manifestPath(directory))).toMatchObject({ + status: 'destroyed', + }); + }); + it('times out without recording destroyed while the group survives its kill', async () => { const directory = await seedLeftover(); const send = process.kill.bind(process); diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index ad40aa89..25411295 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -1112,7 +1112,7 @@ describe('a program group with a token, as a faked /proc shows it', () => { // A /proc that names another pid than this process's belongs to another // pid namespace, so the group reads unshared and gc sends no signal. - it('sends no SIGSTOP when /proc/self names another pid', async () => { + it('sends no signal when /proc/self names another pid', async () => { const directory = await recordedSession(); try { procShowsTokenGroup('Z'); @@ -1126,6 +1126,29 @@ describe('a program group with a token, as a faked /proc shows it', () => { } }); + // sharesHostPids read /proc/self as this process's pid a moment before, + // so only a /proc that changed since, such as one mounted over it, + // reaches the guard of the freeze. The probe changes it here. + it('sends no SIGSTOP when /proc/self names another pid at the freeze', async () => { + const directory = await recordedSession(); + try { + procShowsTokenGroup('Z'); + const signals: unknown[] = []; + vi.spyOn(process, 'kill').mockImplementation((_pid, signal) => { + signals.push(signal); + if (signal === 0) { + procHooks.self = '1'; + } + return true; + }); + + expect(await provenProgramGroupRuns(directory)).toBe(false); + expect(signals).toEqual([0]); + } finally { + await rm(directory, { recursive: true, force: true }); + } + }); + it('gives a frozen group SIGCONT when its judgement throws', async () => { const directory = await recordedSession(); try { @@ -1758,14 +1781,36 @@ describe.runIf(platform === 'linux')('a program record with a token', () => { // destroy --force ends a session without its group only after such a read. describe('isUnreadableGroupError', () => { + const refused = (code: string) => + makeCliError(ERROR_CODES.STORAGE_READ_ERROR, { cause: errno(code) }); it.each([ + ['a program.json that the read refuses', refused('EACCES'), true], [ - 'a program.json that the read refuses', - makeCliError(ERROR_CODES.STORAGE_READ_ERROR), + 'a program.json behind a file where a folder was', + refused('ENOTDIR'), true, ], ['a /proc scan that fails with EIO', errno('EIO'), true], ['a /proc read that fails with EACCES', errno('EACCES'), true], + ['a read that EPERM refuses', errno('EPERM'), true], + ['a path that loops', errno('ELOOP'), true], + ['a program.json that is a folder', refused('EISDIR'), true], + ['a name too long', errno('ENAMETOOLONG'), true], + [ + 'a program.json read that ran out of file descriptors', + refused('EMFILE'), + false, + ], + ['EMFILE', errno('EMFILE'), false], + ['ENFILE', errno('ENFILE'), false], + ['ENOMEM', errno('ENOMEM'), false], + ['EAGAIN', errno('EAGAIN'), false], + ['EINTR', errno('EINTR'), false], + [ + 'a STORAGE_READ_ERROR without a cause', + makeCliError(ERROR_CODES.STORAGE_READ_ERROR), + false, + ], ['HOST_TIMEOUT', makeCliError(ERROR_CODES.HOST_TIMEOUT), false], [ 'an assertion', From c1ef1d504dce6e39fccbd158416e3127443d1042 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 12:11:19 +0000 Subject: [PATCH 14/17] fix(gc): name destroy --force for a failed reconcile only when the group read fails Codex round 3 on #327: a reconcile also writes the manifest and removes the socket, so an EACCES from the socket unlink got the hint "destroy --force removes it" although destroy --force fails the same way. gc now asks forceSkipsGroup, the read and first judgement that destroy --force runs, and names destroy --force only when that read fails with an error that isUnreadableGroupError accepts. Also from Codex: isUnreadableGroupError no longer claims host.json reads. readHostRecord reads a failed read as missing, so the group reads unshared, destroy --force fails with HOST_TIMEOUT and gc removes the session. USAGE, the host README and SKILL say so. Only the gcSessions and defaultDependencies fingerprints changed, and every guard constant still matches the last full check. --- .../skills/verify-session-lifecycle/SKILL.md | 2 +- .../verify-session-lifecycle/coverage.json | 4 +- docs/USAGE.md | 4 +- src/cli/commands/gc.ts | 25 ++++++-- src/host/README.md | 4 +- src/host/programGroup.ts | 22 ++++++- test/unit/commands/gc.test.ts | 61 +++++++++++++++++++ test/unit/host/programGroup.test.ts | 18 ++++++ 8 files changed, 126 insertions(+), 14 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 895cbb29..7b0a22f7 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -494,7 +494,7 @@ node --import tsx src/cli/main.ts gc --json # removes the session A read of the program's group that fails with an errno that a retry does not change, such as `program.json` that refuses the read (EACCES) or a `/proc` scan that fails (EIO), fails every later read too. `UNREADABLE_ERRNOS` lists them: EACCES, EPERM, EIO, EISDIR, ENOTDIR, ELOOP and ENAMETOOLONG. gc kept such a session, plain `destroy` failed on the same read, and so did `destroy --force`, so no command removed the session. No safety rule breaks then, because the model has no rule for a session that stays forever. -Now `destroySession` runs every group read of a terminal session, and both rounds of `--force`, through its local `stopUnlessUnreadable`. That reads the group, stops it and waits for it. With `--force`, a read or a first judgement (`isProgramGroupAlive`) that fails with an error that `isUnreadableGroupError` accepts makes it stop the host alone instead, and the wait then proves the host dead. The stop runs after the `try`, so a read that fails after that first judgement, as in the wait, still throws, and a group that read alive gets its kill or fails the destroy. EMFILE, ENFILE, ENOMEM, EAGAIN and EINTR still throw, because a later read can succeed. A group that reads alive and a host that does not end still throw `HOST_TIMEOUT`. `recordDestroyed` then records destroyed, and a process that the program left can outlive it. gc names `destroy --force` in its skip reason for such a read. In the model, `CheckFails` makes every read of `program.json` by `destroy`, `list` and `gc` fail while the record exists, and the ghost `dblind` marks the destroyed record that such a `destroy --force` wrote. R11, R16 and R20 leave it out. The model has no read that succeeds and then fails: such a read only fails a destroy, and no rule forbids a destroy that fails. `mutant-ForceSkipsUnreadableGroup-checkfails` expects pass, because without the guard `WitnessUncheckedForceDestroys` is never reached. The integration tests "destroy --force ends an exited session whose program.json it cannot read" and "destroy --force ends a session whose host died and whose program.json it cannot read" make `program.json` unreadable with `chmod 000`. +Now `destroySession` runs every group read of a terminal session, and both rounds of `--force`, through its local `stopUnlessUnreadable`. That reads the group, stops it and waits for it. With `--force`, a read or a first judgement (`isProgramGroupAlive`) that fails with an error that `isUnreadableGroupError` accepts makes it stop the host alone instead, and the wait then proves the host dead. The stop runs after the `try`, so a read that fails after that first judgement, as in the wait, still throws, and a group that read alive gets its kill or fails the destroy. EMFILE, ENFILE, ENOMEM, EAGAIN and EINTR still throw, because a later read can succeed. A group that reads alive and a host that does not end still throw `HOST_TIMEOUT`. `recordDestroyed` then records destroyed, and a process that the program left can outlive it. gc names `destroy --force` in its skip reason for such a read. A reconcile also writes the manifest and removes the socket, so after a failed reconcile gc names it only when `forceSkipsGroup`, the read and first judgement of `destroy --force`, gets such an error too. A `host.json` that cannot be read counts as missing, so the group reads unshared: `destroy --force` fails with `HOST_TIMEOUT`, and gc removes the session. In the model, `CheckFails` makes every read of `program.json` by `destroy`, `list` and `gc` fail while the record exists, and the ghost `dblind` marks the destroyed record that such a `destroy --force` wrote. R11, R16 and R20 leave it out. The model has no read that succeeds and then fails: such a read only fails a destroy, and no rule forbids a destroy that fails. `mutant-ForceSkipsUnreadableGroup-checkfails` expects pass, because without the guard `WitnessUncheckedForceDestroys` is never reached. The integration tests "destroy --force ends an exited session whose program.json it cannot read" and "destroy --force ends a session whose host died and whose program.json it cannot read" make `program.json` unreadable with `chmod 000`. ### `CreateRecordsHost`: a CLI in another pid space reads a starting host dead (R2) diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index d588ce71..925b148c 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -45,8 +45,8 @@ "src/cli/commands/create.ts#waitForReadyHost": "a7fd2ba345b6bfd6", "src/cli/commands/destroy.ts#runDestroyCommand": "ecaa8b1d572da7c6", "src/cli/commands/destroy.ts#rerunInNewSession": "cf32d7d082758522", - "src/cli/commands/gc.ts#gcSessions": "18a7249df9349120", - "src/cli/commands/gc.ts#defaultDependencies": "81a9894438cb5be7", + "src/cli/commands/gc.ts#gcSessions": "4d996cc35406473a", + "src/cli/commands/gc.ts#defaultDependencies": "ae2347cdb778b488", "src/host/programGroup.ts#provenProgramGroupRuns": "7b50817618b4b769", "src/host/programGroup.ts#judgeGroupForGc": "fb133ba2739116d1", "src/host/programGroup.ts#judgeFrozenGroup": "ca600530eddb26b2", diff --git a/docs/USAGE.md b/docs/USAGE.md index a426c523..98fa92a6 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -316,7 +316,7 @@ agent-tty record diff --at-seq-a 0 --json 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. `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, `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`. 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. +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, `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`. 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`). A `destroy` that runs inside the session, such as one typed into the session's shell, runs again outside the session and prints its result once the session has ended. The session's terminal is closed by then, so redirect stdout to keep the result, for example `agent-tty destroy "$AGENT_TTY_SESSION_ID" --json > destroy.json`. @@ -369,7 +369,7 @@ Limits: 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. 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, at most twice, and it keeps the session only when such a check proves the group. Another `gc` or a `destroy` that runs at the same time can send SIGCONT before each of those checks. A live process of the chain can then escape both scans, and `gc` 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, 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. +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, at most twice, and it keeps the session only when such a check proves the group. Another `gc` or a `destroy` that runs at the same time can send SIGCONT before each of those checks. A live process of the chain can then escape both scans, and `gc` 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: - At the idle time-out, a host that cannot run the check kills nothing, but it still records the session as `exited` once the program has exited, while a process that the program left can still run. A later `destroy` then fails with `HOST_TIMEOUT`, and `gc` can remove the session folder. - When `/proc` hides the processes of other users (mounted with `hidepid=2`, `hidepid=4`, `hidepid=invisible` or `hidepid=ptraceable`), a group whose processes agent-tty cannot see counts as running. A `destroy` that cannot prove such a group gone fails with `HOST_TIMEOUT` and does not record the session as `destroyed`. diff --git a/src/cli/commands/gc.ts b/src/cli/commands/gc.ts index 49ecc14d..a793168a 100644 --- a/src/cli/commands/gc.ts +++ b/src/cli/commands/gc.ts @@ -9,6 +9,7 @@ import { removeDeadHostSocket, } from '../../host/lifecycle.js'; import { + forceSkipsGroup, isUnreadableGroupError, provenProgramGroupRuns, } from '../../host/programGroup.js'; @@ -101,6 +102,10 @@ export interface GcDependencies { manifest: SessionRecord, ) => Promise; provenProgramGroupRuns: (sessionDirectory: string) => Promise; + forceSkipsGroup: ( + sessionDirectory: string, + childPid: number | null, + ) => Promise; now: () => Date; } @@ -112,6 +117,7 @@ const defaultDependencies: GcDependencies = { reconcileSession, removeDeadHostSocket, provenProgramGroupRuns, + forceSkipsGroup, now: () => new Date(), }; @@ -292,10 +298,13 @@ export function parseDurationToMs(value: string): number { return durationMs; } -// A read of the program's group that fails with a system error fails every -// later check too. destroy --force ends such a session without the read. +// A read of the program's group that fails with one of UNREADABLE_ERRNOS +// fails every later check too. destroy --force ends such a session without +// the read. +const FORCE_HINT = ' (destroy --force removes it)'; + function forceRemovesIt(error: unknown): string { - return isUnreadableGroupError(error) ? ' (destroy --force removes it)' : ''; + return isUnreadableGroupError(error) ? FORCE_HINT : ''; } export async function gcSessions( @@ -377,9 +386,17 @@ export async function gcSessions( try { await dependencies.reconcileSession(sessionDirectory); } catch (error) { + // A reconcile also writes the manifest and removes the socket, so gc + // names destroy --force only when the read of the group fails too. + const skips = + isUnreadableGroupError(error) && + (await dependencies.forceSkipsGroup( + sessionDirectory, + manifestBefore.childPid, + )); result.skippedSessions.push({ sessionId: manifestBefore.sessionId, - reason: `failed to reconcile session${forceRemovesIt(error)}: ${getErrorMessage(error)}`, + reason: `failed to reconcile session${skips ? FORCE_HINT : ''}: ${getErrorMessage(error)}`, }); continue; } diff --git a/src/host/README.md b/src/host/README.md index 1175889d..ae44bf41 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -55,9 +55,9 @@ - The `signal` handler accepts only `SIGTERM`, `SIGINT`, `SIGKILL`, `SIGHUP`, `SIGUSR1` and `SIGUSR2`, and throws `INVALID_SIGNAL` for others. [hostMain.ts:runHost] - The `run` handler waits 30,000 ms by default. The `wait` handler needs exactly one of `exit` or `idleMs`, else it throws `INVALID_DURATION`. `waitForRender` polls every `RENDER_WAIT_POLL_INTERVAL_MS` (200 ms, `src/renderWait/limits.ts`). [hostMain.ts:runHost] - `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` stops and waits 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. [lifecycle.ts:destroySession] [programGroup.ts:isUnreadableGroupError] +- `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` stops and waits 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 or is 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. 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] - `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 fa999dd0..a4c743e0 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -312,9 +312,10 @@ const UNREADABLE_ERRNOS = new Set([ ]); // Whether a read of the program's group failed in a way that every later -// read repeats: a read of program.json or host.json (STORAGE_READ_ERROR) or -// of /proc, with one of UNREADABLE_ERRNOS. A verdict, HOST_TIMEOUT, an -// abort or a bug is none of these. +// read repeats: a read of program.json (STORAGE_READ_ERROR) or of /proc, +// with one of UNREADABLE_ERRNOS. A verdict, HOST_TIMEOUT, an abort or a bug +// is none of these. A host.json that cannot be read counts as missing, so +// its group reads unshared and throws nothing here. export function isUnreadableGroupError(error: unknown): boolean { const cause = hasErrorCode(error, ERROR_CODES.STORAGE_READ_ERROR) ? (error as Error).cause @@ -328,6 +329,21 @@ export function isUnreadableGroupError(error: unknown): boolean { ); } +// Whether destroy --force skips the program's group: the read of the group, +// or its first judgement, fails with an error that isUnreadableGroupError +// accepts. +export async function forceSkipsGroup( + sessionDirectory: string, + childPid: number | null, +): Promise { + try { + isProgramGroupAlive(await readProgramGroup(sessionDirectory, childPid)); + return false; + } catch (error) { + return isUnreadableGroupError(error); + } +} + export async function readProvenProgramGroup( sessionDirectory: string, ): Promise { diff --git a/test/unit/commands/gc.test.ts b/test/unit/commands/gc.test.ts index d083afcd..55995206 100644 --- a/test/unit/commands/gc.test.ts +++ b/test/unit/commands/gc.test.ts @@ -209,6 +209,7 @@ function createMockDependencies( }, provenProgramGroupRuns: (sessionDirectory: string) => Promise.resolve(runningGroups.has(sessionDirectory)), + forceSkipsGroup: () => Promise.resolve(false), }; return { @@ -485,6 +486,66 @@ describe('gc command helpers', () => { expect(removedPaths).toEqual([]); }); + it('names destroy --force for a failed reconcile only when the read of the group fails too', async () => { + const home = '/tmp/agent-tty'; + const running = (sessionId: string) => ({ + manifest: createSessionRecord({ + sessionId, + status: 'running', + createdAt: '2026-03-20T08:00:00.000Z', + }), + }); + const { dependencies, removedPaths } = createMockDependencies(home, { + 'socket-01': running('socket-01'), + 'unreadable-01': running('unreadable-01'), + 'transient-01': running('transient-01'), + }); + const failure = (code: string) => + Object.assign(new Error(`${code}: unlink of the socket failed`), { + code, + }); + dependencies.reconcileSession = (sessionDirectory: string) => + Promise.reject( + failure( + sessionDirectory.endsWith('transient-01') ? 'EMFILE' : 'EACCES', + ), + ); + const asked: string[] = []; + dependencies.forceSkipsGroup = (sessionDirectory, childPid) => { + asked.push(`${sessionDirectory} ${String(childPid)}`); + return Promise.resolve(sessionDirectory.endsWith('unreadable-01')); + }; + + const result = await gcSessions( + home, + { dryRun: false, staleOnly: false, olderThanMs: null }, + dependencies, + ); + + expect(result.skippedSessions).toEqual([ + { + sessionId: 'socket-01', + reason: + 'failed to reconcile session: EACCES: unlink of the socket failed', + }, + { + sessionId: 'unreadable-01', + reason: + 'failed to reconcile session (destroy --force removes it): EACCES: unlink of the socket failed', + }, + { + sessionId: 'transient-01', + reason: + 'failed to reconcile session: EMFILE: unlink of the socket failed', + }, + ]); + expect(asked).toEqual([ + `${home}/sessions/socket-01 456`, + `${home}/sessions/unreadable-01 456`, + ]); + expect(removedPaths).toEqual([]); + }); + it('reports removals in dry-run mode without deleting anything', async () => { const home = '/tmp/agent-tty'; const { dependencies, removedPaths, bytesBySession } = diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index 25411295..fa549ff5 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -18,6 +18,7 @@ import { afterEach, beforeEach, describe, expect, it, vi } from 'vitest'; import { captureProgram, + forceSkipsGroup, isProgramGroupAlive, isUnreadableGroupError, judgeProgramGroup, @@ -1746,6 +1747,23 @@ describe.runIf(platform === 'linux')('a program record with a token', () => { }); }); + // gc names destroy --force for a failed reconcile only after this check. + it('skips the group for destroy --force only when its first read fails for good', async () => { + recordHostIn(readlinkSync('/proc/self/ns/pid')); + expect(await forceSkipsGroup(directory, 4242)).toBe(false); + + procHooks.listError = errno('EMFILE'); + expect(await forceSkipsGroup(directory, 4242)).toBe(false); + + procHooks.listError = errno('EIO'); + expect(await forceSkipsGroup(directory, 4242)).toBe(true); + + procHooks.listError = undefined; + await rm(programRecordPath(directory)); + await mkdir(programRecordPath(directory)); + expect(await forceSkipsGroup(directory, 4242)).toBe(true); + }); + // Only an agent-tty version between program.json and host.json wrote a // token without host.json, and nothing names its pid space. it('reads alive and gets no kill without a host record', async () => { From bb4132c2cb66aec8720261c230262a61004e3504 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 12:19:32 +0000 Subject: [PATCH 15/17] fix(gc): judge a group again when both frozen judgements read gone Codex round 3 on #327 (P1) and the maintainer: reading a group ended after two frozen judgements that read gone was a regression from #326, which retried up to GC_JUDGEMENTS times. A SIGCONT from another gc or a destroy before both judgements let gc remove the folder of a live fork chain. judgeFrozenGroup now returns null (inconclusive) after both frozen judgements read gone, so provenProgramGroupRuns judges the group again. It keeps the two freezes per judgement, so a gc sends at most 10 x 2 SIGSTOP/SIGCONT pairs. An ended zombie-only group with about 2,300 processes in /proc now takes about 3.5 s at a load of 90, against about 2.5 s for #326's ten single freezes. New unit test: a live member that escapes both frozen judgements of one pass keeps the session (fails with the old return). facts.mjs expects the null return, and a false return turns GcFreezesUnseenGroup FALSE. USAGE limit 5 and SKILL state the cost and the remaining race (all 20 frozen judgements). --- .../skills/verify-session-lifecycle/SKILL.md | 2 +- .../verify-session-lifecycle/coverage.json | 4 +- .../scripts/facts.mjs | 5 ++- docs/USAGE.md | 2 +- src/host/programGroup.ts | 15 +++---- test/unit/host/programGroup.test.ts | 42 ++++++++++++++++++- 6 files changed, 55 insertions(+), 15 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 7b0a22f7..e88b6a52 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -479,7 +479,7 @@ node -e 'console.log(require(process.argv[1]).status)' "$d/session.json" Without the guard, `gcSessions` removed the folder of every collectable session. A program that exits on its own can leave a process in its group, such as `sleep 300 &` after `trap "" HUP`, and the host does not kill at a normal exit. The rm deleted `program.json` with the folder, and that record is the only proof that the process is the program's, so no later command could stop it. -Now `gcSessions` calls `provenProgramGroupRuns` after its other checks and before the rm. It judges the group that `readProvenProgramGroup` gives, as the waits of `destroy` do, and gc skips the session with the reason "the session's program group still runs (destroy ends it)" while it proves the group, also under `--dry-run`: a live member carries the token. A read that throws skips the session too, with the error as the reason. A member of a fork chain can end between its stat and its autogroup read (`unknown`), or show up only after the judge's scans, so `judgeGroupForGc` reads such a judgement as inconclusive, and gc judges again, at most ten times. gc does not check a destroyed session, because `destroy` records destroyed only after a wait that read the group gone. A record without a token proves nothing, so gc removes such a session as before. gc never keeps a session that no command can remove: a group that gc cannot check proves nothing, and gc removes its session as before. That covers another pid space, where the group reads `unshared` (as after a container restart that keeps the home, when `host.json` names a pid namespace that no longer exists), and a `/proc` that refuses the boot id or the autogroup of a live member (`unknown`). So R20 holds only for a gc in the host's pid space, and `witness-WitnessUnsharedGcRemovesLeftover-otherspace` shows that a gc in another one removes an exited session while a process that the program left runs. gc judges without a SIGSTOP first, so a fork chain that no scan shows reads gone to the judge. So `provenProgramGroupRuns` also counts the group as running while the probe `kill(-pgid, 0)` finds its id and no scan shows a member, live or zombie (`GcProbesUnseenGroup`). Under a PID 1 that never reaps, the chain also leaves zombies in view, so the scans show only zombies while its live member escapes them. Then `judgeFrozenGroup` sends SIGSTOP, as `stopProgramGroup` does, judges the stopped group, whose stopped member stays in view, and sends SIGCONT in a `finally` (`GcFreezesUnseenGroup`). Another gc or a `destroy` can send SIGCONT before that judgement, so a frozen group that still reads gone gets another SIGSTOP and judgement (`FROZEN_JUDGEMENTS`, two). When that one reads gone too, the group reads ended. So an ended group costs one pass: under a subreaper that never reaps, with a zombie of the group and 2,264 processes in `/proc`, `provenProgramGroupRuns` took about 300 ms, against about 2.5 s for ten passes. A SIGCONT from elsewhere before both judgements lets a live member escape both scans, and gc then reads the live chain ended and removes its folder. The model has one gc, so it leaves that race out. It sends SIGSTOP only where `/proc` shows its own pid space. `mutant-GcFreezesUnseenGroup-unseen-zombies` must violate R20, and "gc keeps an exited session while a fork chain runs behind its zombies" in `test/integration/non-reaping-init.test.ts` covers it. An unrelated group that took the id is in view and reads `unproven`, so it does not keep the session. `mutant-GcProbesUnseenGroup-unseen` must violate R20. The integration tests "gc keeps an exited session while a process that the program left runs" and "... while a fork chain that the program left runs" in `test/integration/lifecycle.test.ts` cover both, and "gc removes an exited session whose host.json names another pid namespace" covers the restart. +Now `gcSessions` calls `provenProgramGroupRuns` after its other checks and before the rm. It judges the group that `readProvenProgramGroup` gives, as the waits of `destroy` do, and gc skips the session with the reason "the session's program group still runs (destroy ends it)" while it proves the group, also under `--dry-run`: a live member carries the token. A read that throws skips the session too, with the error as the reason. A member of a fork chain can end between its stat and its autogroup read (`unknown`), or show up only after the judge's scans, so `judgeGroupForGc` reads such a judgement as inconclusive, and gc judges again, at most ten times. gc does not check a destroyed session, because `destroy` records destroyed only after a wait that read the group gone. A record without a token proves nothing, so gc removes such a session as before. gc never keeps a session that no command can remove: a group that gc cannot check proves nothing, and gc removes its session as before. That covers another pid space, where the group reads `unshared` (as after a container restart that keeps the home, when `host.json` names a pid namespace that no longer exists), and a `/proc` that refuses the boot id or the autogroup of a live member (`unknown`). So R20 holds only for a gc in the host's pid space, and `witness-WitnessUnsharedGcRemovesLeftover-otherspace` shows that a gc in another one removes an exited session while a process that the program left runs. gc judges without a SIGSTOP first, so a fork chain that no scan shows reads gone to the judge. So `provenProgramGroupRuns` also counts the group as running while the probe `kill(-pgid, 0)` finds its id and no scan shows a member, live or zombie (`GcProbesUnseenGroup`). Under a PID 1 that never reaps, the chain also leaves zombies in view, so the scans show only zombies while its live member escapes them. Then `judgeFrozenGroup` sends SIGSTOP, as `stopProgramGroup` does, judges the stopped group, whose stopped member stays in view, and sends SIGCONT in a `finally` (`GcFreezesUnseenGroup`). Another gc or a `destroy` can send SIGCONT before that judgement, so a frozen group that still reads gone gets another SIGSTOP and judgement (`FROZEN_JUDGEMENTS`, two). When that one reads gone too, the judgement stays inconclusive, and gc judges again, so an ended group reads ended only after ten passes of two frozen judgements each. Under a subreaper that never reaps, with a zombie of the group and about 2,300 processes in `/proc`, `provenProgramGroupRuns` then took about 3.5 s at a load of 90, against about 2.5 s for the ten single freezes of #326. Only a SIGCONT from elsewhere before each of those 20 judgements lets a live member escape them all, and gc then reads the live chain ended and removes its folder. The model has one gc, so it leaves that race out. It sends SIGSTOP only where `/proc` shows its own pid space. `mutant-GcFreezesUnseenGroup-unseen-zombies` must violate R20, and "gc keeps an exited session while a fork chain runs behind its zombies" in `test/integration/non-reaping-init.test.ts` covers it. An unrelated group that took the id is in view and reads `unproven`, so it does not keep the session. `mutant-GcProbesUnseenGroup-unseen` must violate R20. The integration tests "gc keeps an exited session while a process that the program left runs" and "... while a fork chain that the program left runs" in `test/integration/lifecycle.test.ts` cover both, and "gc removes an exited session whose host.json names another pid namespace" covers the restart. ```sh id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'trap "" HUP; sleep 300 & exit 0' | 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 925b148c..70aa3714 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -49,7 +49,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": "ca600530eddb26b2", + "src/host/programGroup.ts#judgeFrozenGroup": "e3a6c281e3f579fc", "src/host/programGroup.ts#FROZEN_JUDGEMENTS": "d4eb06aa7addbaa9", "src/host/programGroup.ts#isUnreadableGroupError": "e2d852aa5b45cb53", "src/host/programGroup.ts#UNREADABLE_ERRNOS": "24de7f719ccf14be", @@ -144,7 +144,7 @@ "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", "skill:model/SessionLifecycle.tla": "f1bb5d457a8f2ba0", - "skill:scripts/facts.mjs": "e858a4c852cd0f68", + "skill:scripts/facts.mjs": "e4dac7e26cc13dd4", "skill:scripts/check.sh": "0e998387e38d04c8" }, "callSites": { diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 7d2e272c..2ed2bc5f 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -1406,7 +1406,8 @@ function rerunFacts() { // judgeFrozenGroup freezes and judges at most FROZEN_JUDGEMENTS times: SIGSTOP // where /proc shows this process's pid space, a judgement, and SIGCONT in a -// finally. A frozen judgement other than gone decides; gone freezes again. +// finally. A frozen judgement other than gone decides; gone freezes again, +// and gone after the last freeze is inconclusive, so gc judges again. function frozenJudgesTwice() { const module = 'src/host/programGroup.ts'; const limit = requireDeclaration(module, 'FROZEN_JUDGEMENTS').initializer; @@ -1422,7 +1423,7 @@ function frozenJudgesTwice() { loop === undefined || !ts.isForStatement(loop) || !ts.isBlock(loop.statement) || - normalize(statements[1].getText()) !== 'return false;' + normalize(statements[1].getText()) !== 'return null;' ) { return false; } diff --git a/docs/USAGE.md b/docs/USAGE.md index 98fa92a6..572f79a3 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -369,7 +369,7 @@ Limits: 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. 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, at most twice, and it keeps the session only when such a check proves the group. Another `gc` or a `destroy` that runs at the same time can send SIGCONT before each of those checks. A live process of the chain can then escape both scans, and `gc` 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. +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, 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: - At the idle time-out, a host that cannot run the check kills nothing, but it still records the session as `exited` once the program has exited, while a process that the program left can still run. A later `destroy` then fails with `HOST_TIMEOUT`, and `gc` can remove the session folder. - When `/proc` hides the processes of other users (mounted with `hidepid=2`, `hidepid=4`, `hidepid=invisible` or `hidepid=ptraceable`), a group whose processes agent-tty cannot see counts as running. A `destroy` that cannot prove such a group gone fails with `HOST_TIMEOUT` and does not record the session as `destroyed`. diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index a4c743e0..118a53d4 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -690,7 +690,8 @@ function judgeGroupForGc(group: ProvenRecord): boolean | null { return live === null ? true : live ? null : judgeFrozenGroup(group); } -// A frozen judgement that reads gone is judged frozen once more. +// A frozen judgement that reads gone is judged frozen once more, so a gc +// sends at most GC_JUDGEMENTS * FROZEN_JUDGEMENTS SIGSTOP and SIGCONT pairs. const FROZEN_JUDGEMENTS = 2; // The scans show only zombies of the group while the probe finds its id. @@ -699,11 +700,11 @@ const FROZEN_JUDGEMENTS = 2; // stopProgramGroup, and a stopped member stays in view. Another gc or a // destroy can send SIGCONT before the judgement, so a frozen group that // still reads gone gets another SIGSTOP and judgement. When that one reads -// gone too, the group reads ended, so an ended group costs one pass of -// provenProgramGroupRuns, not GC_JUDGEMENTS. That reads a live fork chain -// ended only when a SIGCONT from elsewhere came before both judgements and -// the chain's live member escaped both scans. The group gets SIGCONT, also -// when a scan throws. +// gone too, the judgement stays inconclusive, and provenProgramGroupRuns +// judges the group again. So gc reads a live fork chain ended only when a +// SIGCONT from elsewhere came before each of its frozen judgements and the +// chain's live member escaped every scan. The group gets SIGCONT, also when +// a scan throws. function judgeFrozenGroup(group: ProvenRecord): boolean | null { for (let frozen = 0; frozen < FROZEN_JUDGEMENTS; frozen += 1) { if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { @@ -719,7 +720,7 @@ function judgeFrozenGroup(group: ProvenRecord): boolean | null { return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; } } - return false; + return null; } function probeFindsGroup(pgid: number): boolean { diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index fa549ff5..ec703008 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -1040,8 +1040,9 @@ describe('a program group with a token, as a faked /proc shows it', () => { } }); - // Nothing live was in view to freeze, so one pass reads the group ended. - it('reads a group that shows only zombies, also frozen twice, ended in one pass', async () => { + // Two frozen judgements that read gone stay inconclusive, so gc judges + // the group again, and reads it ended only after the last judgement. + it('reads a group that shows only zombies, frozen twice in each of ten judgements, ended', async () => { const directory = await recordedSession(); try { procShowsTokenGroup('Z'); @@ -1052,12 +1053,49 @@ describe('a program group with a token, as a faked /proc shows it', () => { }); expect(await provenProgramGroupRuns(directory)).toBe(false); + expect(signals).toEqual( + Array.from({ length: 10 }, () => [ + 0, + 'SIGSTOP', + 'SIGCONT', + 'SIGSTOP', + 'SIGCONT', + ]).flat(), + ); + } finally { + await rm(directory, { recursive: true, force: true }); + } + }); + + // A SIGCONT from another gc or a destroy before both frozen judgements + // lets the live member escape them. The next judgement still finds it. + it('keeps the session when a live member escapes both frozen judgements of one pass', async () => { + const directory = await recordedSession(); + try { + procShowsTokenGroup('Z'); + const signals: unknown[] = []; + let stops = 0; + vi.spyOn(process, 'kill').mockImplementation((_pid, signal) => { + signals.push(signal); + if (signal === 'SIGSTOP') { + stops += 1; + if (stops === 3) { + procShowsTokenGroup('Z', 'T'); + } + } + return true; + }); + + expect(await provenProgramGroupRuns(directory)).toBe(true); expect(signals).toEqual([ 0, 'SIGSTOP', 'SIGCONT', 'SIGSTOP', 'SIGCONT', + 0, + 'SIGSTOP', + 'SIGCONT', ]); } finally { await rm(directory, { recursive: true, force: true }); From 24e275f98081346eff7b1abdc4bf192622489a3f Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 12:31:11 +0000 Subject: [PATCH 16/17] fix(destroy): read an unreadable group again, 100 ms later, before destroy --force skips it Codex round 4 on #327 (P2): EIO, as on a network file system or from a one-off /proc read, need not repeat. destroy --force then skipped the group of a terminal session, recorded it destroyed, and the next gc deleted program.json while a leftover could still run. stopUnlessUnreadable now reads and judges the group again after DESTROY_POLL_INTERVAL_MS (100 ms, abortable) when the first read fails with an error that isUnreadableGroupError accepts. It skips the group only when that read fails the same way. A second read that passes stops the group as usual. The model is unchanged: CheckFails fails every read. New unit tests: EIO on the first read and a good second read gets the group its SIGKILL (fails on the previous head), and an abort between the two reads stops the destroy after one read (fails when the delay ignores the signal). facts.mjs reads the new statements, and a catch that skips the second read or the delay turns ForceSkipsUnreadableGroup FALSE. Also (P3): USAGE limit 5 says "up to twice in each of up to ten checks", because a frozen unknown judgement sends one pair. --- .../skills/verify-session-lifecycle/SKILL.md | 2 +- .../verify-session-lifecycle/coverage.json | 4 +- .../scripts/facts.mjs | 50 ++++++++++++----- docs/USAGE.md | 4 +- src/host/README.md | 2 +- src/host/lifecycle.ts | 43 ++++++++++----- test/unit/host/lifecycle.test.ts | 54 ++++++++++++++++++- 7 files changed, 126 insertions(+), 33 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index e88b6a52..86cc074d 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -494,7 +494,7 @@ node --import tsx src/cli/main.ts gc --json # removes the session A read of the program's group that fails with an errno that a retry does not change, such as `program.json` that refuses the read (EACCES) or a `/proc` scan that fails (EIO), fails every later read too. `UNREADABLE_ERRNOS` lists them: EACCES, EPERM, EIO, EISDIR, ENOTDIR, ELOOP and ENAMETOOLONG. gc kept such a session, plain `destroy` failed on the same read, and so did `destroy --force`, so no command removed the session. No safety rule breaks then, because the model has no rule for a session that stays forever. -Now `destroySession` runs every group read of a terminal session, and both rounds of `--force`, through its local `stopUnlessUnreadable`. That reads the group, stops it and waits for it. With `--force`, a read or a first judgement (`isProgramGroupAlive`) that fails with an error that `isUnreadableGroupError` accepts makes it stop the host alone instead, and the wait then proves the host dead. The stop runs after the `try`, so a read that fails after that first judgement, as in the wait, still throws, and a group that read alive gets its kill or fails the destroy. EMFILE, ENFILE, ENOMEM, EAGAIN and EINTR still throw, because a later read can succeed. A group that reads alive and a host that does not end still throw `HOST_TIMEOUT`. `recordDestroyed` then records destroyed, and a process that the program left can outlive it. gc names `destroy --force` in its skip reason for such a read. A reconcile also writes the manifest and removes the socket, so after a failed reconcile gc names it only when `forceSkipsGroup`, the read and first judgement of `destroy --force`, gets such an error too. A `host.json` that cannot be read counts as missing, so the group reads unshared: `destroy --force` fails with `HOST_TIMEOUT`, and gc removes the session. In the model, `CheckFails` makes every read of `program.json` by `destroy`, `list` and `gc` fail while the record exists, and the ghost `dblind` marks the destroyed record that such a `destroy --force` wrote. R11, R16 and R20 leave it out. The model has no read that succeeds and then fails: such a read only fails a destroy, and no rule forbids a destroy that fails. `mutant-ForceSkipsUnreadableGroup-checkfails` expects pass, because without the guard `WitnessUncheckedForceDestroys` is never reached. The integration tests "destroy --force ends an exited session whose program.json it cannot read" and "destroy --force ends a session whose host died and whose program.json it cannot read" make `program.json` unreadable with `chmod 000`. +Now `destroySession` runs every group read of a terminal session, and both rounds of `--force`, through its local `stopUnlessUnreadable`. That reads the group, stops it and waits for it. With `--force`, a read or a first judgement (`isProgramGroupAlive`, in `readAndJudge`) that fails with an error that `isUnreadableGroupError` accepts is run again after `pollDelay` (100 ms), and only a second such failure makes it stop the host alone instead, and the wait then proves the host dead. The stop runs after the `try`, so a read that fails after that first judgement, as in the wait, still throws, and a group that read alive gets its kill or fails the destroy. EMFILE, ENFILE, ENOMEM, EAGAIN and EINTR still throw, because a later read can succeed. A group that reads alive and a host that does not end still throw `HOST_TIMEOUT`. `recordDestroyed` then records destroyed, and a process that the program left can outlive it. gc names `destroy --force` in its skip reason for such a read. A reconcile also writes the manifest and removes the socket, so after a failed reconcile gc names it only when `forceSkipsGroup`, the read and first judgement of `destroy --force`, gets such an error too. A `host.json` that cannot be read counts as missing, so the group reads unshared: `destroy --force` fails with `HOST_TIMEOUT`, and gc removes the session. In the model, `CheckFails` makes every read of `program.json` by `destroy`, `list` and `gc` fail while the record exists, and the ghost `dblind` marks the destroyed record that such a `destroy --force` wrote. R11, R16 and R20 leave it out. The model has no read that succeeds and then fails: such a read only fails a destroy, and no rule forbids a destroy that fails. It has no read that fails once and then passes either, because `CheckFails` fails every read. A second read that passes leads to the stop of a readable group, which the model covers. `mutant-ForceSkipsUnreadableGroup-checkfails` expects pass, because without the guard `WitnessUncheckedForceDestroys` is never reached. The integration tests "destroy --force ends an exited session whose program.json it cannot read" and "destroy --force ends a session whose host died and whose program.json it cannot read" make `program.json` unreadable with `chmod 000`. ### `CreateRecordsHost`: a CLI in another pid space reads a starting host dead (R2) diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 70aa3714..2145a6b3 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -86,7 +86,7 @@ "src/host/lifecycle.ts#stopSessionProcesses": "d1abb608b1d2160a", "src/host/lifecycle.ts#recordDestroyed": "d3a74237a9c8459c", "src/host/lifecycle.ts#removeDeadHostSocket": "34ce07ab7b7e8d7b", - "src/host/lifecycle.ts#destroySession": "ee53946fe51e4df1", + "src/host/lifecycle.ts#destroySession": "05edb5d2825ed857", "src/host/lifecycle.ts#isMarkedDestroyed": "d178f4a63473915c", "src/host/lifecycle.ts#writeMarkedDestroyed": "4863c35f70699757", "src/host/lifecycle.ts#reconcileSession": "739c83bf945000c6", @@ -144,7 +144,7 @@ "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", "skill:model/SessionLifecycle.tla": "f1bb5d457a8f2ba0", - "skill:scripts/facts.mjs": "e4dac7e26cc13dd4", + "skill:scripts/facts.mjs": "c38cd6f59d124d76", "skill:scripts/check.sh": "0e998387e38d04c8" }, "callSites": { diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 2ed2bc5f..aa69ac11 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -729,8 +729,22 @@ function statementsOf(block) { function stopUnlessUnreadableFacts(arrows) { const st = arrows.get('stopUnlessUnreadable') ?? []; - const [declared, attempt, ...after] = st; + const [judge, declared, attempt, ...after] = st; + // readAndJudge reads the group and judges it once, with no kill. + const judges = + judge !== undefined && + ts.isVariableStatement(judge) && + judge.declarationList.declarations[0]?.name.getText() === 'readAndJudge' && + (arrows.get('readAndJudge') ?? []) + .map((s) => normalize(s.getText())) + .join('\n') === + [ + 'const group = await readGroup();', + 'isProgramGroupAlive(group);', + 'return group;', + ].join('\n'); if ( + !judges || declared === undefined || normalize(declared.getText()) !== 'let group: ProgramGroup | null;' || attempt === undefined || @@ -740,25 +754,35 @@ function stopUnlessUnreadableFacts(arrows) { ) { return { stops: false, skipsUnreadable: false }; } - // The try reads the group and judges it once, with no kill. Only a read - // or a judgement that fails there can skip the group: the stop comes - // after the try, so a read that fails after a verdict fails the destroy. + // Only a read or a judgement that fails in the try can skip the group: the + // stop comes after the try, so a read that fails after a verdict fails the + // destroy. With --force, an unreadable read is read again after a poll + // interval, and only a second unreadable read skips the group. const tried = statementsOf(attempt.tryBlock).join('\n'); - const caught = statementsOf(attempt.catchClause.block); + const caught = attempt.catchClause.block.statements; const stops = - tried === - ['group = await readGroup();', 'isProgramGroupAlive(group);'].join( - '\n', - ) && + tried === 'group = await readAndJudge();' && after.map((s) => normalize(s.getText())).join('\n') === [ 'await stopSessionProcesses( sessionId, host, group, sessionDirectory, signal, );', 'return group;', ].join('\n'); + const [rethrows, waits, again, ...more] = caught; const skipsUnreadable = - caught.join('\n') === + more.length === 0 && + normalize(rethrows?.getText() ?? '') === + 'if (force !== true || !isUnreadableGroupError(error)) { throw error; }' && + normalize(waits?.getText() ?? '') === + 'await pollDelay(DESTROY_POLL_INTERVAL_MS, signal);' && + again !== undefined && + ts.isTryStatement(again) && + again.catchClause !== undefined && + again.finallyBlock === undefined && + statementsOf(again.tryBlock).join('\n') === + 'group = await readAndJudge();' && + statementsOf(again.catchClause.block).join('\n') === [ - 'if (force !== true || !isUnreadableGroupError(error)) { throw error; }', + 'if (!isUnreadableGroupError(secondError)) { throw secondError; }', 'await stopSessionProcesses( sessionId, host, null, sessionDirectory, signal, );', 'return null;', ].join('\n') && @@ -766,8 +790,10 @@ function stopUnlessUnreadableFacts(arrows) { 'isUnreadableGroupError', "const cause = hasErrorCode(error, ERROR_CODES.STORAGE_READ_ERROR) ? (error as Error).cause : error; const code: unknown = cause instanceof Error ? (cause as { code?: unknown }).code : undefined; return ( !(cause instanceof CliError) && typeof code === 'string' && UNREADABLE_ERRNOS.has(code) );", ); + const rethrowsAll = + caught.map((s) => normalize(s.getText())).join('\n') === 'throw error;'; return { - stops: stops && (caught.join('\n') === 'throw error;' || skipsUnreadable), + stops: stops && (rethrowsAll || skipsUnreadable), skipsUnreadable: stops && skipsUnreadable, }; } diff --git a/docs/USAGE.md b/docs/USAGE.md index 572f79a3..4fc30b75 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -316,7 +316,7 @@ agent-tty record diff --at-seq-a 0 --json 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. `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, `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`. 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. +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`). A `destroy` that runs inside the session, such as one typed into the session's shell, runs again outside the session and prints its result once the session has ended. The session's terminal is closed by then, so redirect stdout to keep the result, for example `agent-tty destroy "$AGENT_TTY_SESSION_ID" --json > destroy.json`. @@ -369,7 +369,7 @@ Limits: 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. 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, 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. +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: - At the idle time-out, a host that cannot run the check kills nothing, but it still records the session as `exited` once the program has exited, while a process that the program left can still run. A later `destroy` then fails with `HOST_TIMEOUT`, and `gc` can remove the session folder. - When `/proc` hides the processes of other users (mounted with `hidepid=2`, `hidepid=4`, `hidepid=invisible` or `hidepid=ptraceable`), a group whose processes agent-tty cannot see counts as running. A `destroy` that cannot prove such a group gone fails with `HOST_TIMEOUT` and does not record the session as `destroyed`. diff --git a/src/host/README.md b/src/host/README.md index ae44bf41..09a9bef0 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -55,7 +55,7 @@ - The `signal` handler accepts only `SIGTERM`, `SIGINT`, `SIGKILL`, `SIGHUP`, `SIGUSR1` and `SIGUSR2`, and throws `INVALID_SIGNAL` for others. [hostMain.ts:runHost] - The `run` handler waits 30,000 ms by default. The `wait` handler needs exactly one of `exit` or `idleMs`, else it throws `INVALID_DURATION`. `waitForRender` polls every `RENDER_WAIT_POLL_INTERVAL_MS` (200 ms, `src/renderWait/limits.ts`). [hostMain.ts:runHost] - `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` stops and waits 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] +- `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] - `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] diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index 1bba2fe1..475ce849 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -913,30 +913,45 @@ export async function destroySession( // destroy --force of a session whose host is gone also ends a session // whose program group it cannot read: the read of program.json, or the // first judgement of the group, fails with an errno that every later read - // repeats. It then stops what it can without the group and records - // destroyed, so a process that the program left can outlive it. A failed - // read after that first judgement, a group that reads alive, and a host - // that does not end (HOST_TIMEOUT) still fail the destroy. + // repeats, twice, 100 ms apart. It then stops what it can without the + // group and records destroyed, so a process that the program left can + // outlive it. A failed read after that first judgement, a group that reads + // alive, and a host that does not end (HOST_TIMEOUT) still fail the + // destroy. const stopUnlessUnreadable = async ( host: SessionHost | null, readGroup: () => Promise, ): Promise => { + const readAndJudge = async (): Promise => { + const group = await readGroup(); + isProgramGroupAlive(group); + return group; + }; let group: ProgramGroup | null; try { - group = await readGroup(); - isProgramGroupAlive(group); + group = await readAndJudge(); } catch (error) { if (force !== true || !isUnreadableGroupError(error)) { throw error; } - await stopSessionProcesses( - sessionId, - host, - null, - sessionDirectory, - signal, - ); - return null; + // A read that fails once, as on a network file system, can pass the + // next time. + await pollDelay(DESTROY_POLL_INTERVAL_MS, signal); + try { + group = await readAndJudge(); + } catch (secondError) { + if (!isUnreadableGroupError(secondError)) { + throw secondError; + } + await stopSessionProcesses( + sessionId, + host, + null, + sessionDirectory, + signal, + ); + return null; + } } await stopSessionProcesses( sessionId, diff --git a/test/unit/host/lifecycle.test.ts b/test/unit/host/lifecycle.test.ts index 3d11261e..cc9cf83f 100644 --- a/test/unit/host/lifecycle.test.ts +++ b/test/unit/host/lifecycle.test.ts @@ -997,7 +997,7 @@ describe('destroySession', () => { expect(reads).toBeGreaterThan(1); }); - it('destroy --force records destroyed, and kills nothing, when the first read of the group fails', async () => { + it('destroy --force records destroyed, and kills nothing, when the first read of the group fails twice', async () => { const directory = await seedLeftover(); fsHooks.files = new Map([ [`/proc/${String(group)}/stat`, errno('EIO')], @@ -1012,6 +1012,58 @@ describe('destroySession', () => { }); }); + // A read can fail once, as on a network file system, and pass the + // next time, 100 ms later. + it('destroy --force kills the group when only the first read of the group fails', async () => { + const directory = await seedLeftover(); + const stat = `/proc/${String(group)}/stat`; + let reads = 0; + fsHooks.files = new (class extends Map { + override get(path: string): string | Error | undefined { + if (path !== stat) { + return undefined; + } + reads += 1; + return reads === 1 ? errno('EIO') : undefined; + } + })(); + const kill = vi.spyOn(process, 'kill'); + + await destroySession('session-01', true); + + expect(kill).toHaveBeenCalledWith(-group, 'SIGKILL'); + expect(await readManifest(manifestPath(directory))).toMatchObject({ + status: 'destroyed', + }); + expect(reads).toBeGreaterThan(1); + }); + + it('destroy --force stops at an abort between the two reads of the group', async () => { + const directory = await seedLeftover(); + const controller = new AbortController(); + const reason = new Error('destroy aborted'); + const stat = `/proc/${String(group)}/stat`; + let reads = 0; + fsHooks.files = new (class extends Map { + override get(path: string): string | Error | undefined { + if (path !== stat) { + return undefined; + } + reads += 1; + controller.abort(reason); + return errno('EIO'); + } + })(); + const kill = vi.spyOn(process, 'kill'); + + await expect( + destroySession('session-01', true, { signal: controller.signal }), + ).rejects.toBe(reason); + expect(reads).toBe(1); + expect(kill).not.toHaveBeenCalledWith(-group, 'SIGKILL'); + expect(await readManifest(manifestPath(directory))).toEqual(exited); + }); + it('times out without recording destroyed while the group survives its kill', async () => { const directory = await seedLeftover(); const send = process.kill.bind(process); From 53c0fe19da1b3536296f0b073c13815250d5d746 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 17:09:37 +0000 Subject: [PATCH 17/17] chore(lifecycle): record the coverage of the merge with #324 check.sh --update-coverage rewrote coverage.json from facts.mjs at the merge of main (#324) into #327. All 41 constants hold, and the 39 guards read TRUE. 77 of the 90 TLC runs finished locally as expected before the host rebooted. CI runs all 90. --- .../verify-session-lifecycle/coverage.json | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 94b58db2..ed8dd56b 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -20,6 +20,7 @@ "ShutdownChecksCommandable": true, "DestroyRecordsDestroyed": true, "DestroyKeepsExitCode": true, + "ForceSkipsUnreadableGroup": true, "DestroyStopsLeftovers": true, "ProvesHostPid": true, "ReconcileRepairsDestroyed": true, @@ -48,11 +49,14 @@ "src/cli/commands/create.ts#hostRuns": "b80eac3bb9523aaf", "src/cli/commands/destroy.ts#runDestroyCommand": "ecaa8b1d572da7c6", "src/cli/commands/destroy.ts#rerunInNewSession": "cf32d7d082758522", - "src/cli/commands/gc.ts#gcSessions": "a2ac8bd10f100332", - "src/cli/commands/gc.ts#defaultDependencies": "81a9894438cb5be7", + "src/cli/commands/gc.ts#gcSessions": "4d996cc35406473a", + "src/cli/commands/gc.ts#defaultDependencies": "ae2347cdb778b488", "src/host/programGroup.ts#provenProgramGroupRuns": "7b50817618b4b769", "src/host/programGroup.ts#judgeGroupForGc": "fb133ba2739116d1", - "src/host/programGroup.ts#judgeFrozenGroup": "d18458e7d70a5664", + "src/host/programGroup.ts#judgeFrozenGroup": "e3a6c281e3f579fc", + "src/host/programGroup.ts#FROZEN_JUDGEMENTS": "d4eb06aa7addbaa9", + "src/host/programGroup.ts#isUnreadableGroupError": "e2d852aa5b45cb53", + "src/host/programGroup.ts#UNREADABLE_ERRNOS": "24de7f719ccf14be", "src/host/programGroup.ts#GC_JUDGEMENTS": "180a0af01a4b81c7", "src/host/programGroup.ts#probeFindsGroup": "31ea7b5e835c0509", "src/host/lifecycle.ts#allocateSession": "43819af8c6c271ec", @@ -86,7 +90,7 @@ "src/host/lifecycle.ts#stopSessionProcesses": "d1abb608b1d2160a", "src/host/lifecycle.ts#recordDestroyed": "d3a74237a9c8459c", "src/host/lifecycle.ts#removeDeadHostSocket": "34ce07ab7b7e8d7b", - "src/host/lifecycle.ts#destroySession": "d840dd07a0e481f5", + "src/host/lifecycle.ts#destroySession": "05edb5d2825ed857", "src/host/lifecycle.ts#isMarkedDestroyed": "d178f4a63473915c", "src/host/lifecycle.ts#writeMarkedDestroyed": "4863c35f70699757", "src/host/lifecycle.ts#reconcileSession": "739c83bf945000c6", @@ -143,9 +147,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": "7f1c6dd7943968c3", - "skill:scripts/facts.mjs": "6ee4da3ef9b6bac3", - "skill:scripts/check.sh": "b48bc5fd343aefb5" + "skill:model/SessionLifecycle.tla": "cd8639012467f13e", + "skill:scripts/facts.mjs": "2de6761bed77fb19", + "skill:scripts/check.sh": "fe2da7911682462a" }, "callSites": { "writeManifest": [