From 5ebe5da12d8ce4aa6864cddde253bbdef54340cb Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 08:08:23 +0000 Subject: [PATCH 1/4] 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 2/4] 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 3/4] 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 ace08738b66b1a589ea2e4698a9f34e4a86db0df Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 09:32:03 +0000 Subject: [PATCH 4/4] 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();