From faa14b11fcbdb0996da58cbc25dab2a31d2d2daa Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 20:02:09 +0000 Subject: [PATCH 01/17] test: gc keeps an exited session whose program group still runs --- test/integration/lifecycle.test.ts | 47 ++++++++++++++++++++++++++++++ test/unit/commands/gc.test.ts | 46 +++++++++++++++++++++++++++++ 2 files changed, 93 insertions(+) diff --git a/test/integration/lifecycle.test.ts b/test/integration/lifecycle.test.ts index ef1f64fa..4b63a436 100644 --- a/test/integration/lifecycle.test.ts +++ b/test/integration/lifecycle.test.ts @@ -1011,6 +1011,53 @@ describe('lifecycle integration', { timeout: 30000 }, () => { }, ); + // gc would delete program.json, the only record that proves the group. + it.runIf(capturesToken)( + 'gc keeps an exited session while a process that the program left runs', + async () => { + const sessionId = await createProgram( + 'trap "" HUP; sleep 300 & touch "$0"; exit 0', + ); + const deadline = Date.now() + 10_000; + while (inspectSession(testHome, sessionId).status !== 'exited') { + 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, + homes: [ + { + skippedSessions: [ + { + sessionId, + reason: expect.stringContaining('destroy') as string, + }, + ], + }, + ], + }, + }); + expect(inspectSession(testHome, sessionId).status).toBe('exited'); + expect(isGroupAlive(pgid)).toBe(true); + + const destroyed = runCli(['destroy', sessionId, '--json'], { + AGENT_TTY_HOME: testHome, + }); + expect(JSON.parse(destroyed.stdout)).toMatchObject({ ok: true }); + expect(await groupEnds(pgid)).toBe(true); + const removed = runCli(['gc', '--json'], { AGENT_TTY_HOME: testHome }); + expect(JSON.parse(removed.stdout)).toMatchObject({ + ok: true, + result: { removedSessionCount: 1 }, + }); + }, + ); + // Only a session with a token checks the autogroup. it.runIf(capturesToken)( 'destroy times out while it cannot read the autogroup of a process that the program left', diff --git a/test/unit/commands/gc.test.ts b/test/unit/commands/gc.test.ts index c2f2aa92..729d043b 100644 --- a/test/unit/commands/gc.test.ts +++ b/test/unit/commands/gc.test.ts @@ -37,6 +37,7 @@ interface MockSessionState { manifestReads?: Array; reconciledManifest?: SessionRecord | null; isDirectory?: boolean; + groupRuns?: boolean; } function createSessionRecord(options: { @@ -86,6 +87,7 @@ function createMockDependencies( const manifestStore = new Map(); const manifestReadSequences = new Map>(); const reconcileStore = new Map(); + const runningGroups = new Set(); const removedPaths: string[] = []; const socketCleanups: string[] = []; const bytesBySession = new Map(); @@ -142,6 +144,9 @@ function createMockDependencies( if ('reconciledManifest' in sessionState) { reconcileStore.set(sessionDirectory, sessionState.reconciledManifest); } + if (sessionState.groupRuns === true) { + runningGroups.add(sessionDirectory); + } } const dependencies: GcDependencies = { @@ -202,6 +207,8 @@ function createMockDependencies( socketCleanups.push(`${sessionDirectory} ${manifest.status}`); return Promise.resolve(); }, + provenProgramGroupRuns: (sessionDirectory: string) => + Promise.resolve(runningGroups.has(sessionDirectory)), }; return { @@ -362,6 +369,45 @@ describe('gc command helpers', () => { expect(removedPaths).toEqual([]); }); + it('keeps a terminal session whose proven program group still runs', async () => { + const home = '/tmp/agent-tty'; + const exitedManifest = createSessionRecord({ + sessionId: 'leftover-01', + status: 'exited', + createdAt: '2026-03-20T08:00:00.000Z', + }); + const { dependencies, removedPaths, socketCleanups } = + createMockDependencies(home, { + 'leftover-01': { manifest: exitedManifest, groupRuns: true }, + 'destroyed-01': { + manifest: { + ...exitedManifest, + sessionId: 'destroyed-01', + status: 'destroyed', + }, + groupRuns: true, + }, + }); + + for (const dryRun of [true, false]) { + const result = await gcSessions( + home, + { dryRun, staleOnly: false, olderThanMs: null }, + dependencies, + ); + + expect(result.skippedSessions).toEqual([ + { + sessionId: 'leftover-01', + reason: "the session's program group still runs (destroy ends it)", + }, + ]); + expect(result.removedSessions).toEqual(['destroyed-01']); + } + expect(removedPaths).toEqual([`${home}/sessions/destroyed-01`]); + expect(socketCleanups).toEqual([`${home}/sessions/destroyed-01 destroyed`]); + }); + it('reports removals in dry-run mode without deleting anything', async () => { const home = '/tmp/agent-tty'; const { dependencies, removedPaths, bytesBySession } = From 6a5e989df529762d3b99ef6518a97d4d3bcb504e Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 20:06:18 +0000 Subject: [PATCH 02/17] fix(gc): keep a session whose proven program group still runs gc deleted program.json with the folder of an exited session while a process that the program left still ran, so nothing could prove or stop that process later. gc now skips such a session until destroy ends the group. The lifecycle model gets the GcKeepsLiveGroup guard, rule R20 RemovedSessionStopped and the mutant run that breaks it. check.sh gains --drift-only and a job pool. --- .../skills/verify-session-lifecycle/SKILL.md | 60 +++++++++------ .../model/SessionLifecycle.tla | 30 +++++++- .../verify-session-lifecycle/scripts/check.sh | 73 +++++++++++++------ .../scripts/facts.mjs | 46 ++++++++++++ docs/USAGE.md | 4 +- src/cli/commands/gc.ts | 26 +++++++ src/host/programGroup.ts | 6 ++ 7 files changed, 198 insertions(+), 47 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index a6d2c87c..8517cf81 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -33,6 +33,7 @@ The tool is TLC, the TLA+ model checker, pinned to release 1.7.4 by sha256. The | 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. | `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 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. | `TypeOK` also runs in every run. When it breaks, the model is wrong, not the code. @@ -41,10 +42,10 @@ 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`), 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`), 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`, `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`, `src/cli/commands/create.ts` `runCreateCommand`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`. +- `src/cli/commands/gc.ts` `gcSessions` and `defaultDependencies`, `src/cli/commands/create.ts` `runCreateCommand`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`. - `src/host/sessionState.ts` `setDimensions`, `requestDestroy`, `recordDestroyed` and `recordExit`, `src/host/eventLog.ts` `EventLog.open`, `src/host/rpcServer.ts` `listen` and `close`, `src/host/rpcClient.ts` `toTransportCliError` (which socket errors read as `HOST_UNREACHABLE`). - `src/host/hostRecord.ts`: `captureHost`, `writeHostRecord`, `readHostRecord`, `pidExists`, `judgeHost`, `inPidNamespace`, `readTimeNamespace`, `inTimeNamespace`, `readMachineId`, `inHostPidSpace` and `sharesHostPids`. - `src/storage/manifests.ts` `readValidatedJsonFile`, `replaceFileAtomic`, `replaceFileAtomicSync`, `writeValidatedJsonFileSync`, `writeManifest`, `writeDestroyMarker`. @@ -62,13 +63,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 this repo it takes about eleven minutes with the default `CHECK_JOBS` of 4. Eight runs explore the whole model, so `CHECK_JOBS=69` 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 this repo it takes about eleven minutes with the default `CHECK_JOBS` of 4. Eight runs explore the whole model, so `CHECK_JOBS=70` 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 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-one 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 69 times and prints one line per run. +3. It runs TLC 70 times and prints one line per run. 4. It compares the hashes and 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. @@ -77,23 +78,23 @@ Exit codes: 0 means every run gave the expected result and the covered code matc At the sync commit, the expected results are: -| Runs | Expected | Why | -| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -| `current`, the code as it is with the program's session token, every rule | pass | No order of the modelled steps breaks a rule. This is the run that catches a new bug. | -| `current-no-token`, the code as it is without a token, R1 to R14 and R17 to R19 | pass | The same for a session whose `program.json` holds no token: on macOS, on a kernel without autogroups, when the capture read none, and for a session that an older agent-tty created. Every kill then falls back to the id that a manifest or the host's own record names. R15 and R16 are what the token adds, so this run leaves them out (see Scope). | -| `current-unseen`, the code as it is with a token and a program that no scan of `/proc` shows, every rule | pass | A fork chain: each process of the program forks its successor and ends between scans, so the kill through the token sees a member only once the group is frozen. | -| `witness-*` without a suffix | violated | Each witness is a state that must be reachable: a `create` that gave up recorded the session destroyed, gc removes a session, a session serves, a resize lands, a clean exit is recorded, a crash is reconciled, a plain destroy completes, a SIGTERM shutdown is recorded, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` (which ends with `HOST_TIMEOUT` and leaves the session destroying) and `destroy --force` (which ends with `HOST_TIMEOUT` too), a process that the program left meets the kill of `destroy`, an unrelated group has the program's group id when `destroy --force` kills, `destroy --force` stops a program that only `program.json` names, a program whose host died before `program.json` named it outlives `destroy`, a wait of `destroy` through `program.json` reads the group gone while an unrelated group holds its id, a reconcile writes destroyed again over the failed that it wrote, `destroy --force` reaches its kill while a process that took the ended host's pid runs, and `destroy --force` reaches its kill while a live host has not written `host.json` yet. A witness that passes means the model can no longer reach that state, and the passing rules prove nothing. | -| `witness-*-no-token` | violated | Eight of those states without a token: a `create` that gave up recorded the session destroyed, a crash is reconciled, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` and `destroy --force`, and a reconcile writes destroyed again over the failed that it wrote. They show that `current-no-token` reaches the fallback kill and the EPERM probe. | -| `mutant-CreateRecordsHostPid`, `mutant-HostWaitsForManifest`, `mutant-ReconcileRereads`, `mutant-HostSerializesWrites`, `mutant-ReconcileSkipsLiveHost`, `mutant-HostStopsAfterTerminalWrite`, `mutant-DestroyRecordsDestroyed`, `mutant-DestroyKeepsExitCode`, `mutant-ManifestWriteNeedsFolder`, `mutant-KillsProgramGroup`, `mutant-HostWaitsForGroup`, `mutant-ReconcileWaitsForGroup`, `mutant-ReRunsInNewSession`, `mutant-InsideCheckReadsEnv`, `mutant-RecordsProgramSync`, `mutant-ProvesGroupOwnership`, `mutant-DestroyStopsLeftovers`, `mutant-FallbackNeedsFolder`, `mutant-ReconcileRepairsDestroyed`, `mutant-CreateStopsOnGiveUp`, `mutant-TokenNamesProgram`, `mutant-ProvesHostPid`, `mutant-GcBothChecks`, `mutant-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` | 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-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-ReconcileSkipsTerminal` | pass | The re-read in `reconcileSession` also returns on a terminal manifest, so the first terminal return alone is redundant. | -| `mutant-GcSkipsNonCollectable`, `mutant-GcFinalCheck` | pass | gc checks "collectable" twice. One check alone still keeps R1, so removing one is safe. Removing both is not. | -| `mutant-ShutdownChecksCommandable` | pass | `initiateShutdown` requests destroy only while the session is commandable, and the writer writes nothing after a terminal record. Either one alone keeps R3. Removing both is not safe. | -| `current-otherspace`, the code as it is with `destroy`, `list` and `gc` in another pid space than the host, every rule | pass | `OtherPidSpace`: no scan and no probe of those commands shows the program's processes, as without `/proc`, with an empty `/proc`, in another pid namespace or on another machine. | -| `witness-WitnessUnsharedDestroyCompletes-otherspace` | violated | A plain `destroy` from another pid space still reports success, because it trusts the host's `destroyed` record. | -| `mutant-UnsharedGroupReadsUnknown-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. | +| Runs | Expected | Why | +| ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | -------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `current`, the code as it is with the program's session token, every rule | pass | No order of the modelled steps breaks a rule. This is the run that catches a new bug. | +| `current-no-token`, the code as it is without a token, R1 to R14 and R17 to R19 | pass | The same for a session whose `program.json` holds no token: on macOS, on a kernel without autogroups, when the capture read none, and for a session that an older agent-tty created. Every kill then falls back to the id that a manifest or the host's own record names. R15 and R16 are what the token adds, so this run leaves them out (see Scope). | +| `current-unseen`, the code as it is with a token and a program that no scan of `/proc` shows, every rule | pass | A fork chain: each process of the program forks its successor and ends between scans, so the kill through the token sees a member only once the group is frozen. | +| `witness-*` without a suffix | violated | Each witness is a state that must be reachable: a `create` that gave up recorded the session destroyed, gc removes a session, a session serves, a resize lands, a clean exit is recorded, a crash is reconciled, a plain destroy completes, a SIGTERM shutdown is recorded, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` (which ends with `HOST_TIMEOUT` and leaves the session destroying) and `destroy --force` (which ends with `HOST_TIMEOUT` too), a process that the program left meets the kill of `destroy`, an unrelated group has the program's group id when `destroy --force` kills, `destroy --force` stops a program that only `program.json` names, a program whose host died before `program.json` named it outlives `destroy`, a wait of `destroy` through `program.json` reads the group gone while an unrelated group holds its id, a reconcile writes destroyed again over the failed that it wrote, `destroy --force` reaches its kill while a process that took the ended host's pid runs, and `destroy --force` reaches its kill while a live host has not written `host.json` yet. A witness that passes means the model can no longer reach that state, and the passing rules prove nothing. | +| `witness-*-no-token` | violated | Eight of those states without a token: a `create` that gave up recorded the session destroyed, a crash is reconciled, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` and `destroy --force`, and a reconcile writes destroyed again over the failed that it wrote. They show that `current-no-token` reaches the fallback kill and the EPERM probe. | +| `mutant-CreateRecordsHostPid`, `mutant-HostWaitsForManifest`, `mutant-ReconcileRereads`, `mutant-HostSerializesWrites`, `mutant-ReconcileSkipsLiveHost`, `mutant-HostStopsAfterTerminalWrite`, `mutant-DestroyRecordsDestroyed`, `mutant-DestroyKeepsExitCode`, `mutant-ManifestWriteNeedsFolder`, `mutant-KillsProgramGroup`, `mutant-HostWaitsForGroup`, `mutant-ReconcileWaitsForGroup`, `mutant-ReRunsInNewSession`, `mutant-InsideCheckReadsEnv`, `mutant-RecordsProgramSync`, `mutant-ProvesGroupOwnership`, `mutant-DestroyStopsLeftovers`, `mutant-FallbackNeedsFolder`, `mutant-ReconcileRepairsDestroyed`, `mutant-CreateStopsOnGiveUp`, `mutant-TokenNamesProgram`, `mutant-ProvesHostPid`, `mutant-GcBothChecks`, `mutant-GcKeepsLiveGroup`, `mutant-ShutdownBothChecks` | violated | Each run removes a guard from the model and checks only the rule that the guard protects. That rule must break, which shows the check can fail. | +| `mutant-ProbeCountsDeniedGroup-no-token`, `mutant-KillsProgramGroup-no-token`, `mutant-HostWaitsForGroup-no-token`, `mutant-ReconcileWaitsForGroup-no-token` | violated | The same without a token. The fallback depends on these guards as the code before `program.json` did. With a token, the token check reads a process of another user in view, so only this path checks `ProbeCountsDeniedGroup`. | +| `mutant-FreezesUnseenGroup-unseen` | 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-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-ReconcileSkipsTerminal` | pass | The re-read in `reconcileSession` also returns on a terminal manifest, so the first terminal return alone is redundant. | +| `mutant-GcSkipsNonCollectable`, `mutant-GcFinalCheck` | pass | gc checks "collectable" twice. One check alone still keeps R1, so removing one is safe. Removing both is not. | +| `mutant-ShutdownChecksCommandable` | pass | `initiateShutdown` requests destroy only while the session is commandable, and the writer writes nothing after a terminal record. Either one alone keeps R3. Removing both is not safe. | +| `current-otherspace`, the code as it is with `destroy`, `list` and `gc` in another pid space than the host, every rule | pass | `OtherPidSpace`: no scan and no probe of those commands shows the program's processes, as without `/proc`, with an empty `/proc`, in another pid namespace or on another machine. | +| `witness-WitnessUnsharedDestroyCompletes-otherspace` | violated | A plain `destroy` from another pid space still reports success, because it trusts the host's `destroyed` record. | +| `mutant-UnsharedGroupReadsUnknown-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. | Read `current` first. The witness and mutant runs use the same facts from the code, so a code change that breaks `current` can also turn them `UNEXPECTED`. @@ -437,6 +438,21 @@ AGENT_TTY_TEST_OTHER_PIDS=1 NODE_OPTIONS=--import=./test/fixtures/no-proc.ts nod node -e 'console.log(require(process.argv[1]).status)' "$d/session.json" # before: destroyed; now: exited ``` +### `GcKeepsLiveGroup`: gc removes the record of a process that the program left (R20) + +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 that group reads alive, also under `--dry-run`. A failed read skips it too. 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. In another pid space the group reads alive, so gc keeps every session with a token there that is not destroyed. gc sends no SIGSTOP, so a fork chain that no scan shows reads gone, and R20 does not cover the `Unseen` runs. + +```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))') +d="$AGENT_TTY_HOME/sessions/$id" +until [ "$(node -e 'console.log(require(process.argv[1]).status)' "$d/session.json")" = exited ]; do sleep 0.1; done +node --import tsx src/cli/main.ts gc --json # skipped: the session's program group still runs +node --import tsx src/cli/main.ts destroy "$id" --json +node --import tsx src/cli/main.ts gc --json # removes the session +``` + ### `ReusedIdReadsGone`: a wait that never ends while an unrelated group holds the id `isProgramGroupAlive` reads a group with a token alive while the check finds a live member with the token (`owned`), while it cannot run (`unknown`), and while it finds no live member and the probe of the id reads alive. A group whose live members carry another autogroup (`unproven`) reads gone. Without the guard, a group that took the program's id after the program's group ended read alive. `destroy` of the exited session then waited until it ended with `HOST_TIMEOUT`, and every reconcile waited and wrote nothing, until that unrelated group ended. diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index 36b6735e..4cadecfe 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -44,6 +44,9 @@ CONSTANTS Terminal, \* statuses whose policy says terminal GcSkipsNonCollectable, \* gc.ts: skip when manifestAfter is not collectable GcFinalCheck, \* gc.ts: re-read before rm, skip if not collectable + GcKeepsLiveGroup, \* gc.ts: skip a session that is not destroyed + \* while program.json proves that its group + \* runs 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 @@ -127,7 +130,8 @@ ASSUME MaxListReconciles \in 1..3 ASSUME Token \in BOOLEAN ASSUME Unseen \in BOOLEAN ASSUME OtherPidSpace \in BOOLEAN -ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, ReconcileSkipsTerminal, +ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, GcKeepsLiveGroup, + ReconcileSkipsTerminal, ReconcileSkipsLiveHost, CreateRecordsHostPid, HostWaitsForManifest, ReconcileRereads, HostSerializesWrites, HostStopsAfterTerminalWrite, @@ -970,6 +974,20 @@ GcReadsManifest == GcReadsReconciled == /\ pc["gc"] = "readafter" /\ IF mst = "none" \/ (GcSkipsNonCollectable /\ mst \notin Collectable) + THEN GcSkips + ELSE GcGoesTo("group") + /\ UNCHANGED <> + +\* provenProgramGroupRuns reads program.json and judges the group, as the +\* waits of destroy do. With GcKeepsLiveGroup gc skips a session that is not +\* destroyed while that group reads alive ("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. +GcChecksGroup == + /\ pc["gc"] = "group" + /\ IF GcKeepsLiveGroup /\ mst # "destroyed" /\ rec + /\ CliGroupSeen("proven") THEN GcSkips ELSE GcGoesTo("final") /\ UNCHANGED < ~(GroupAlive \/ left) + \* Witnesses. check.sh expects TLC to report each one VIOLATED, which shows \* that the model reaches the state: the rules above are not true only \* because the model can never get there. diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index b80959ee..4d2fce45 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/check.sh +++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh @@ -3,7 +3,10 @@ # reconcileSession, gc, and destroy, all acting on one session at the same # time. # -# .agents/skills/verify-session-lifecycle/scripts/check.sh [--update-coverage] +# .agents/skills/verify-session-lifecycle/scripts/check.sh [--update-coverage | --drift-only] +# +# --drift-only compares the covered code with coverage.json and runs no TLC, +# so it needs no Java: exit 0 or 3 as below. # # Exit 0: every TLC run gave the expected result and the covered code is # unchanged since the last sync. @@ -20,15 +23,19 @@ set -euo pipefail UPDATE_COVERAGE=0 +DRIFT_ONLY=0 for arg in "$@"; do case "$arg" in --update-coverage) UPDATE_COVERAGE=1 ;; + --drift-only) DRIFT_ONLY=1 ;; *) - echo "usage: $0 [--update-coverage]" >&2 + echo "usage: $0 [--update-coverage | --drift-only]" >&2 exit 2 ;; esac done +[ $((UPDATE_COVERAGE + DRIFT_ONLY)) -le 1 ] || + { echo "usage: $0 [--update-coverage | --drift-only]" >&2; exit 2; } SKILL_DIR=$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd) REPO=$(git -C "$SKILL_DIR" rev-parse --show-toplevel) @@ -60,21 +67,23 @@ case "$JOBS" in *[!0-9]* | 0*) die "CHECK_JOBS must be a positive integer, not '$JOBS'" ;; esac command -v node >/dev/null 2>&1 || die "node is not on PATH" -# `java -version` prints `version "11.0.2"`, or `version "1.8.0_292"` for Java 8. -java_out=$("$JAVA" -version 2>&1) || die "Java 11+ is needed (set JAVA=/path/to/java)" -java_version=$(sed -n 's/.* version "\([^"]*\)".*/\1/p' <<<"$java_out" | head -1) -[ -n "$java_version" ] || die "Java 11+ is needed (set JAVA=/path/to/java)" -java_major=${java_version#1.} -java_major=${java_major%%[!0-9]*} -[ -n "$java_major" ] && [ "$java_major" -ge 11 ] || - die "Java 11+ is needed, $JAVA is version $java_version (set JAVA=/path/to/java)" -if [ ! -f "$JAR" ]; then - mkdir -p "$(dirname "$JAR")" - echo "Fetching TLC $TLC_VERSION into $JAR" - curl -fsSL -o "$JAR.part" "$TLC_URL" || die "could not download $TLC_URL" - mv "$JAR.part" "$JAR" +if [ "$DRIFT_ONLY" -eq 0 ]; then + # `java -version` prints `version "11.0.2"`, or `version "1.8.0_292"` for Java 8. + java_out=$("$JAVA" -version 2>&1) || die "Java 11+ is needed (set JAVA=/path/to/java)" + java_version=$(sed -n 's/.* version "\([^"]*\)".*/\1/p' <<<"$java_out" | head -1) + [ -n "$java_version" ] || die "Java 11+ is needed (set JAVA=/path/to/java)" + java_major=${java_version#1.} + java_major=${java_major%%[!0-9]*} + [ -n "$java_major" ] && [ "$java_major" -ge 11 ] || + die "Java 11+ is needed, $JAVA is version $java_version (set JAVA=/path/to/java)" + if [ ! -f "$JAR" ]; then + mkdir -p "$(dirname "$JAR")" + echo "Fetching TLC $TLC_VERSION into $JAR" + curl -fsSL -o "$JAR.part" "$TLC_URL" || die "could not download $TLC_URL" + mv "$JAR.part" "$JAR" fi [ "$(sha256 "$JAR")" = "$TLC_SHA256" ] || die "$JAR does not match the pinned sha256 of TLC $TLC_VERSION" +fi OUT=${CHECK_OUT:-$(mktemp -d "${TMPDIR:-/tmp}/session-lifecycle-check.XXXXXX")} mkdir -p "$OUT" @@ -114,6 +123,17 @@ node -e ' } ' "$OUT/facts.json" "$COVERAGE" >"$OUT/drift.txt" +if [ "$DRIFT_ONLY" -eq 1 ]; then + if [ -s "$OUT/drift.txt" ]; then + echo "STALE: covered code changed since the last sync. Re-read each item," + echo "update the model if it no longer describes the code, then run with --update-coverage:" + sed 's/^/ /' "$OUT/drift.txt" + exit 3 + fi + echo "Covered code matches the sync record." + exit 0 +fi + COLLECTABLE=$(node -e ' const c = JSON.parse(require("node:fs").readFileSync(process.argv[1], "utf8")).constants; console.log("{" + c.Collectable.map((s) => JSON.stringify(s)).join(", ") + "}"); @@ -122,7 +142,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 ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid FreezesUnseenGroup UnsharedGroupReadsUnknown" +GUARDS="GcSkipsNonCollectable GcFinalCheck GcKeepsLiveGroup ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid FreezesUnseenGroup UnsharedGroupReadsUnknown" # 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; @@ -133,8 +153,9 @@ FACTS_LINE=$(node -e ' ' "$OUT/facts.json" $GUARDS) || die "facts.json lacks a guard fact" NO_TOKEN_RULES="NoLiveSessionDeleted HostDeathOnlyWhenDead TerminalIsFinal RecordedExitKept RunningSessionReachable HostStartsWhenCreated TerminalIsLastWrite DestroyedOnlyWhenEnded DestroyEndsDestroyed RemovedFolderStaysRemoved DestroyedProgramStopped LiveGroupStaysNamed DestroyOutlivesProgram FailedCreateStopped DestroyedStaysDestroyed NoUnrelatedHostKilled" -# R15 and R16 are what the token adds, so only the runs with Token check them. -RULES="$NO_TOKEN_RULES NoUnrelatedGroupKilled DestroyedSessionStopped" +# R15, R16 and R20 are what the token adds, so only the runs with Token +# check them. +RULES="$NO_TOKEN_RULES NoUnrelatedGroupKilled DestroyedSessionStopped RemovedSessionStopped" NO_TOKEN_WITNESSES="WitnessCreateGivesUp WitnessCrashReconciled WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessReconcileRepairs" WITNESSES="WitnessGcRemovesSession WitnessCreateGivesUp WitnessSessionServes WitnessResizeLands WitnessCleanExitRecorded WitnessCrashReconciled WitnessDestroyCompletes WitnessSigtermRecorded WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessLeftoverMeetsDestroy WitnessReusedIdMeetsKill WitnessRecordNamesProgram WitnessUnrecordedProgramOutlives WitnessReconcileRepairs WitnessWaitPassesReusedId WitnessReusedHostMeetsKill WitnessUnrecordedHostMeetsKill" @@ -211,6 +232,7 @@ write_run mutant-ReconcileSkipsTerminal pass RecordedExitKept "ReconcileSkipsTer write_run mutant-GcSkipsNonCollectable pass NoLiveSessionDeleted "GcSkipsNonCollectable=FALSE" "redundant: the final check still skips" write_run mutant-GcFinalCheck pass NoLiveSessionDeleted "GcFinalCheck=FALSE" "redundant: the first check still skips" write_run mutant-GcBothChecks violated NoLiveSessionDeleted "GcSkipsNonCollectable=FALSE GcFinalCheck=FALSE" "with neither gc check, gc removes live sessions" NoLiveSessionDeleted +write_run mutant-GcKeepsLiveGroup violated RemovedSessionStopped "GcKeepsLiveGroup=FALSE" "without the group check, gc removes program.json while a process that the program left runs" RemovedSessionStopped write_run mutant-ShutdownChecksCommandable pass TerminalIsFinal "ShutdownChecksCommandable=FALSE" "redundant: the writer writes nothing after a terminal record" write_run mutant-ShutdownBothChecks violated TerminalIsFinal "ShutdownChecksCommandable=FALSE HostStopsAfterTerminalWrite=FALSE" "with neither, shutdown writes destroying over an exit record" TerminalIsFinal @@ -252,11 +274,20 @@ run_tlc() { echo "$rc" >"$dir/rc" } -count=0 +# A pool: a new run starts as soon as one ends. The bash 3.2 of macOS has +# no `wait -n`, so there each batch of $JOBS runs waits for its slowest. +running=0 for name in $RUNS; do run_tlc "$name" & - count=$((count + 1)) - if [ $((count % JOBS)) -eq 0 ]; then wait; fi + running=$((running + 1)) + if [ "$running" -ge "$JOBS" ]; then + if wait -n 2>/dev/null; then + running=$((running - 1)) + else + wait + running=0 + fi + fi done wait diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index e59d599f..d265127b 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -1244,9 +1244,53 @@ function gcFacts() { const rm = indexOfStatement(inner, /dependencies\.rm\(sessionDirectory/); finalCheck = check >= 0 && rm > check; } + // After the collectable guard and before the removal, gc reads whether + // program.json proves a live group for a session that is not destroyed, + // and skips the session when it does or when the read throws. The + // default dependency is provenProgramGroupRuns, which judges the group + // that readProvenProgramGroup gives as isProgramGroupAlive does. + const groupRead = loop.statements.findIndex( + (s) => + ts.isTryStatement(s) && + normalize(s.tryBlock.getText()) === + "{ groupRuns = manifestAfter.status !== 'destroyed' && (await dependencies.provenProgramGroupRuns(sessionDirectory)); }" && + s.catchClause !== undefined && + returnsOrContinues(s.catchClause.block, ts.SyntaxKind.ContinueStatement), + ); + const groupSkip = guardIndex( + loop, + 'groupRuns', + ts.SyntaxKind.ContinueStatement, + ); + const defaults = requireDeclaration( + 'src/cli/commands/gc.ts', + 'defaultDependencies', + ).initializer; + const wired = + defaults !== undefined && + ts.isObjectLiteralExpression(defaults) && + defaults.properties.some( + (p) => + ts.isShorthandPropertyAssignment(p) && + p.name.text === 'provenProgramGroupRuns', + ); + const judges = + normalize( + requireDeclaration( + 'src/host/programGroup.ts', + 'provenProgramGroupRuns', + ).body.getText(), + ) === + '{ return isProgramGroupAlive(await readProvenProgramGroup(sessionDirectory)); }'; return { GcSkipsNonCollectable: reconcile >= 0 && collectable > reconcile, GcFinalCheck: finalCheck, + GcKeepsLiveGroup: + groupRead > collectable && + groupSkip === groupRead + 1 && + loop.statements.indexOf(removal) > groupSkip && + wired && + judges, }; } @@ -1286,6 +1330,8 @@ const COVERED = [ ['src/cli/commands/destroy.ts', 'runDestroyCommand'], ['src/cli/commands/destroy.ts', 'rerunInNewSession'], ['src/cli/commands/gc.ts', 'gcSessions'], + ['src/cli/commands/gc.ts', 'defaultDependencies'], + ['src/host/programGroup.ts', 'provenProgramGroupRuns'], ['src/host/lifecycle.ts', 'allocateSession'], ['src/host/lifecycle.ts', 'launchHost'], ['src/host/lifecycle.ts', 'isProcessAlive'], diff --git a/docs/USAGE.md b/docs/USAGE.md index 06ca6ecc..6ac7ef74 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -337,7 +337,7 @@ If no process passes the check, agent-tty kills nothing, for example when an unr If `/proc` refuses to show the boot id, or shows no autogroup id for a live process whose group and session id are the program's pid (it refuses the read, or the file is empty or malformed), agent-tty cannot run the check. It then kills nothing and counts the group as running. When the CLI cannot list `/proc` at all, as in a chroot or a container without it, it sees no process of the group, and nothing proves a kill. For a session without an autogroup record or without `host.json`, the group then counts as running while `kill(-pgid, 0)` finds a process. A plain `destroy` still ends a live session through its host, and `destroy --force` of a session with an autogroup record fails with `HOST_TIMEOUT`. End it with a plain `destroy`, or run `destroy --force` from a process that can read `/proc`. -On Linux, a CLI that cannot prove that it shares the host's pid space cannot prove that the program's group ended either: it cannot read `/proc/self/ns/pid` (no `/proc`, or an empty one), or `host.json` names another pid namespace or another machine. For a session with an autogroup record and a `host.json`, such a CLI counts the group as running and sends it no signal. On the host's machine, a plain `destroy` of a live session still ends it through its host. From another machine the host's socket does not answer, so a plain `destroy` fails with `HOST_UNREACHABLE`: run it on the machine that started the session. A `destroy` of a session whose program exited fails with `HOST_TIMEOUT` and keeps the session `exited`, also when no process of the group is left. This trade-off keeps `destroy` from recording `destroyed` while a process that the program left runs where the CLI cannot see it. Run such a `destroy` from a process in the host's pid namespace that can read `/proc`. `gc` still removes the folder of an `exited` session, as it does on every system. +On Linux, a CLI that cannot prove that it shares the host's pid space cannot prove that the program's group ended either: it cannot read `/proc/self/ns/pid` (no `/proc`, or an empty one), or `host.json` names another pid namespace or another machine. For a session with an autogroup record and a `host.json`, such a CLI counts the group as running and sends it no signal. On the host's machine, a plain `destroy` of a live session still ends it through its host. From another machine the host's socket does not answer, so a plain `destroy` fails with `HOST_UNREACHABLE`: run it on the machine that started the session. A `destroy` of a session whose program exited fails with `HOST_TIMEOUT` and keeps the session `exited`, also when no process of the group is left. This trade-off keeps `destroy` from recording `destroyed` while a process that the program left runs where the CLI cannot see it. Run such a `destroy` from a process in the host's pid namespace that can read `/proc`. Such a CLI's `gc` keeps the folder of every session with an autogroup record that is not `destroyed`, because it cannot tell whether the group ended. If the proven group, or a group that agent-tty cannot check, does not end within the destroy wait (about 5 s), `destroy` fails with `HOST_TIMEOUT` and does not record the session as `destroyed`. `destroy --force` and reconcile also check the host's pid from `session.json` before they trust it. @@ -358,7 +358,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 or the boot id 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 the check and SIGCONT when the check fails. 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` removes `program.json` with the session folder, and `gc` kills nothing. 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` while the autogroup record in `program.json` proves that a process of the program's group runs, and reports "the session's program group still runs (destroy ends it)". Without an autogroup record (see item 2), `gc` cannot prove the group, so it removes `program.json` with the folder, and a process that the program left can 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 b301ae09..d1bb1134 100644 --- a/src/cli/commands/gc.ts +++ b/src/cli/commands/gc.ts @@ -8,6 +8,7 @@ import { reconcileSession, removeDeadHostSocket, } from '../../host/lifecycle.js'; +import { provenProgramGroupRuns } from '../../host/programGroup.js'; import { ERROR_CODES, makeCliError } from '../../protocol/errors.js'; import { isCollectableSessionStatus, @@ -96,6 +97,7 @@ export interface GcDependencies { sessionDirectory: string, manifest: SessionRecord, ) => Promise; + provenProgramGroupRuns: (sessionDirectory: string) => Promise; now: () => Date; } @@ -106,6 +108,7 @@ const defaultDependencies: GcDependencies = { readManifestIfExists, reconcileSession, removeDeadHostSocket, + provenProgramGroupRuns, now: () => new Date(), }; @@ -420,6 +423,29 @@ export async function gcSessions( continue; } + // The rm deletes program.json, the only proof of the program's group, so + // a process that the program left would run on out of destroy's reach. + // A destroyed session's group read gone before destroy recorded it. + let groupRuns: boolean; + try { + groupRuns = + manifestAfter.status !== 'destroyed' && + (await dependencies.provenProgramGroupRuns(sessionDirectory)); + } catch (error) { + result.skippedSessions.push({ + sessionId, + reason: `failed to check the session's program group: ${getErrorMessage(error)}`, + }); + continue; + } + if (groupRuns) { + result.skippedSessions.push({ + sessionId, + reason: "the session's program group still runs (destroy ends it)", + }); + continue; + } + const sessionBytes = await measurePathBytes( sessionDirectory, dependencies, diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index c460268a..01b1e916 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -575,6 +575,12 @@ export function isProgramGroupAlive(group: ProgramGroup | null): boolean { ); } +export async function provenProgramGroupRuns( + sessionDirectory: string, +): Promise { + return isProgramGroupAlive(await readProvenProgramGroup(sessionDirectory)); +} + export function stopProgramGroup(group: ProgramGroup | null): void { if (group === null) { return; From abc2982364f3ec42c331ed46c0d4d8546f45127e Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 20:26:33 +0000 Subject: [PATCH 03/17] ci: model-check the session lifecycle The lifecycle-model job runs check.sh --drift-only on every run, and the whole check when coverage.json differs from the base. coverage.json syncs the model with gc's group check. --- .../skills/verify-session-lifecycle/SKILL.md | 4 +- .../verify-session-lifecycle/coverage.json | 14 ++++-- .github/workflows/ci.yml | 46 +++++++++++++++++++ 3 files changed, 58 insertions(+), 6 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 8517cf81..32b50fa9 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -55,6 +55,8 @@ Yes, when the diff changes any of these: You do not have to judge this by hand. The check prints `STALE` when any of these changed since the sync commit. +CI runs the check in the `lifecycle-model` job. Every run of it calls `scripts/check.sh --drift-only`, which compares the covered code with `coverage.json` and needs no Java, and fails on `STALE`. The whole check runs only when `coverage.json` differs from the base of the pull request or merge group. + ## Run it From the repo root: @@ -501,7 +503,7 @@ To bring the check back in line after changes that skipped it, use `/maintain-fo ## Scope -The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 23,479,528 distinct states, and without one 22,893,820. The check prints both counts. +The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 25,302,052 distinct states, and without one 24,834,276. The check prints both counts. It assumes: diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index c6b3ea55..3903eae0 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -3,7 +3,9 @@ "src/cli/commands/create.ts#runCreateCommand": "5135dd8d24063c90", "src/cli/commands/destroy.ts#runDestroyCommand": "ecaa8b1d572da7c6", "src/cli/commands/destroy.ts#rerunInNewSession": "cf32d7d082758522", - "src/cli/commands/gc.ts#gcSessions": "667e4ebc3ca3029c", + "src/cli/commands/gc.ts#gcSessions": "a2ac8bd10f100332", + "src/cli/commands/gc.ts#defaultDependencies": "81a9894438cb5be7", + "src/host/programGroup.ts#provenProgramGroupRuns": "80ea01be23763792", "src/host/lifecycle.ts#allocateSession": "77dab09b34fedce5", "src/host/lifecycle.ts#launchHost": "597a5a6b9eb58cc8", "src/host/lifecycle.ts#isProcessAlive": "1ca1fe6ad6c41711", @@ -87,9 +89,9 @@ "src/host/hostMain.ts#runHost(final try)": "16789dd4e2534bc7", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "25bc78980b0d67cd", - "skill:scripts/facts.mjs": "86ec94456c10cb37", - "skill:scripts/check.sh": "422878fda4460ac0" + "skill:model/SessionLifecycle.tla": "f6e5e97a2a5defc1", + "skill:scripts/facts.mjs": "c859e87c2e9ac81a", + "skill:scripts/check.sh": "8f5abb45097333f2" }, "callSites": { "writeManifest": [ @@ -146,7 +148,9 @@ "src/host/lifecycle.ts#destroySession", "src/host/lifecycle.ts#listSessions" ], - "writeProgramRecord": ["src/host/hostMain.ts#runHost"], + "writeProgramRecord": [ + "src/host/hostMain.ts#runHost" + ], "stopProgramGroup": [ "src/host/hostMain.ts#runHost>handlePtyExit", "src/host/hostMain.ts#runHost>handlePtyExit", diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 43fe9eca..78cadfd2 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -216,6 +216,50 @@ jobs: sh -c '"$@" & wait $!' sh \ npx vitest run --maxWorkers=1 --retry=2 test/integration/lifecycle.test.ts test/integration/gc.test.ts test/integration/other-user-group.test.ts + # Model-checks the session lifecycle with the verify-session-lifecycle + # skill. Every run checks that coverage.json matches the covered code. The + # TLC runs take about two CPU-hours, so they run only when coverage.json + # differs from the base, which every change to the model, its scripts or + # the covered code needs. + lifecycle-model: + runs-on: ubuntu-latest + timeout-minutes: 75 + steps: + - name: Check out repository + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6 + with: + persist-credentials: false + fetch-depth: 0 + + - name: Set up mise + uses: jdx/mise-action@5228313ee0372e111a38da051671ca30fc5a96db # v3.6.3 + with: + install_args: --locked node python aube + + - name: Install CI dependencies + run: mise run bootstrap-ci + + - name: Check that coverage.json matches the covered code + run: .agents/skills/verify-session-lifecycle/scripts/check.sh --drift-only + + - name: Decide whether the model checker must run + id: inputs + env: + BASE: ${{ github.event.pull_request.base.sha || github.event.merge_group.base_sha || github.event.before }} + run: | + if [ -n "$BASE" ] && git cat-file -e "$BASE^{commit}" 2>/dev/null && + git diff --quiet "$BASE" HEAD -- .agents/skills/verify-session-lifecycle/coverage.json; then + echo "tlc=false" >> "$GITHUB_OUTPUT" + else + echo "tlc=true" >> "$GITHUB_OUTPUT" + fi + + - name: Model-check the session lifecycle + if: steps.inputs.outputs.tlc == 'true' + env: + CHECK_JOBS: '4' + run: .agents/skills/verify-session-lifecycle/scripts/check.sh + quality-gates: runs-on: ubuntu-latest timeout-minutes: 5 @@ -225,6 +269,7 @@ jobs: - test-integration - test-e2e - proc-isolation + - lifecycle-model if: ${{ always() }} steps: - name: Report Linux quality gate results @@ -234,6 +279,7 @@ jobs: echo "test-integration: ${{ needs.test-integration.result }}" echo "test-e2e: ${{ needs.test-e2e.result }}" echo "proc-isolation: ${{ needs.proc-isolation.result }}" + echo "lifecycle-model: ${{ needs.lifecycle-model.result }}" - name: Fail if any Linux quality gate failed if: ${{ contains(needs.*.result, 'failure') || contains(needs.*.result, 'cancelled') || contains(needs.*.result, 'skipped') }} From 9a3716504bc9f18e9863e656f2fda34d071439c0 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 21:14:37 +0000 Subject: [PATCH 04/17] chore: format the lifecycle coverage record --- .agents/skills/verify-session-lifecycle/coverage.json | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 3903eae0..ba0e2fd7 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -148,9 +148,7 @@ "src/host/lifecycle.ts#destroySession", "src/host/lifecycle.ts#listSessions" ], - "writeProgramRecord": [ - "src/host/hostMain.ts#runHost" - ], + "writeProgramRecord": ["src/host/hostMain.ts#runHost"], "stopProgramGroup": [ "src/host/hostMain.ts#runHost>handlePtyExit", "src/host/hostMain.ts#runHost>handlePtyExit", From 2bb0655c9d18d865275c97d7e414688785afd465 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 21:36:17 +0000 Subject: [PATCH 05/17] fix(gc): keep a session while the probe finds a group that no scan shows Codex on #302: gc sends no SIGSTOP, so a fork chain that the program left read gone and gc removed program.json while it ran. A group id that kill(-pgid, 0) finds while no scan shows a member, live or zombie, now keeps the session. The model gets GcProbesUnseenGroup, R20 covers the Unseen runs, and mutant-GcProbesUnseenGroup-unseen must violate it. --- .../skills/verify-session-lifecycle/SKILL.md | 12 ++-- .../model/SessionLifecycle.tla | 28 ++++++--- .../verify-session-lifecycle/scripts/check.sh | 3 +- .../scripts/facts.mjs | 33 ++++++++-- docs/USAGE.md | 2 +- src/host/programGroup.ts | 30 ++++++++- test/integration/lifecycle.test.ts | 36 +++++++++++ test/unit/host/programGroup.test.ts | 61 ++++++++++++++++++- 8 files changed, 180 insertions(+), 25 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 32b50fa9..f6915f6e 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`), 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`, `probeFindsGroup`), 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`, `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`, 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 this repo it takes about eleven minutes with the default `CHECK_JOBS` of 4. Eight runs explore the whole model, so `CHECK_JOBS=70` 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 this repo it takes about eleven minutes with the default `CHECK_JOBS` of 4. Eight runs explore the whole model, so `CHECK_JOBS=71` 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-one 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-two 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 70 times and prints one line per run. +3. It runs TLC 71 times and prints one line per run. 4. It compares the hashes and call sites with `coverage.json`. Exit codes: 0 means every run gave the expected result and the covered code matches the sync record. 1 means at least one run gave an unexpected result; the line says `UNEXPECTED`. 3 means every result was as expected, but covered code changed since the sync commit; that is not a pass, so follow "When you change covered code on purpose". 2 means a tool could not run. When both 1 and 3 apply, the exit code is 1. @@ -89,7 +89,7 @@ At the sync commit, the expected results are: | `witness-*-no-token` | violated | Eight of those states without a token: a `create` that gave up recorded the session destroyed, a crash is reconciled, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` and `destroy --force`, and a reconcile writes destroyed again over the failed that it wrote. They show that `current-no-token` reaches the fallback kill and the EPERM probe. | | `mutant-CreateRecordsHostPid`, `mutant-HostWaitsForManifest`, `mutant-ReconcileRereads`, `mutant-HostSerializesWrites`, `mutant-ReconcileSkipsLiveHost`, `mutant-HostStopsAfterTerminalWrite`, `mutant-DestroyRecordsDestroyed`, `mutant-DestroyKeepsExitCode`, `mutant-ManifestWriteNeedsFolder`, `mutant-KillsProgramGroup`, `mutant-HostWaitsForGroup`, `mutant-ReconcileWaitsForGroup`, `mutant-ReRunsInNewSession`, `mutant-InsideCheckReadsEnv`, `mutant-RecordsProgramSync`, `mutant-ProvesGroupOwnership`, `mutant-DestroyStopsLeftovers`, `mutant-FallbackNeedsFolder`, `mutant-ReconcileRepairsDestroyed`, `mutant-CreateStopsOnGiveUp`, `mutant-TokenNamesProgram`, `mutant-ProvesHostPid`, `mutant-GcBothChecks`, `mutant-GcKeepsLiveGroup`, `mutant-ShutdownBothChecks` | violated | Each run removes a guard from the model and checks only the rule that the guard protects. That rule must break, which shows the check can fail. | | `mutant-ProbeCountsDeniedGroup-no-token`, `mutant-KillsProgramGroup-no-token`, `mutant-HostWaitsForGroup-no-token`, `mutant-ReconcileWaitsForGroup-no-token` | violated | The same without a token. The fallback depends on these guards as the code before `program.json` did. With a token, the token check reads a process of another user in view, so only this path checks `ProbeCountsDeniedGroup`. | -| `mutant-FreezesUnseenGroup-unseen` | 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-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-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-ReconcileSkipsTerminal` | pass | The re-read in `reconcileSession` also returns on a terminal manifest, so the first terminal return alone is redundant. | | `mutant-GcSkipsNonCollectable`, `mutant-GcFinalCheck` | pass | gc checks "collectable" twice. One check alone still keeps R1, so removing one is safe. Removing both is not. | @@ -444,7 +444,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 that group reads alive, also under `--dry-run`. A failed read skips it too. 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. In another pid space the group reads alive, so gc keeps every session with a token there that is not destroyed. gc sends no SIGSTOP, so a fork chain that no scan shows reads gone, and R20 does not cover the `Unseen` runs. +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 that group reads alive, also under `--dry-run`. A failed read skips it too. 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. In another pid space the group reads alive, so gc keeps every session with a token there that is not destroyed. 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. ```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 4cadecfe..11de5000 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -47,6 +47,9 @@ CONSTANTS GcKeepsLiveGroup, \* gc.ts: skip a session that is not destroyed \* while program.json proves that its group \* runs + GcProbesUnseenGroup, \* programGroup.ts: provenProgramGroupRuns also + \* counts a group id that the probe finds + \* while no scan shows a member 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 @@ -131,6 +134,7 @@ ASSUME Token \in BOOLEAN ASSUME Unseen \in BOOLEAN ASSUME OtherPidSpace \in BOOLEAN ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, GcKeepsLiveGroup, + GcProbesUnseenGroup, ReconcileSkipsTerminal, ReconcileSkipsLiveHost, CreateRecordsHostPid, HostWaitsForManifest, ReconcileRereads, @@ -980,14 +984,21 @@ GcReadsReconciled == lruns, destroyVars, groupVars>> \* provenProgramGroupRuns reads program.json and judges the group, as the -\* waits of destroy do. With GcKeepsLiveGroup gc skips a session that is not -\* destroyed while that group reads alive ("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. +\* waits of destroy do. 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 GcKeepsLiveGroup gc skips a session that +\* is not destroyed while that group reads alive ("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 == + \/ CliGroupSeen("proven") + \/ GcProbesUnseenGroup /\ Unseen /\ (prog \/ left) + GcChecksGroup == /\ pc["gc"] = "group" - /\ IF GcKeepsLiveGroup /\ mst # "destroyed" /\ rec - /\ CliGroupSeen("proven") + /\ IF GcKeepsLiveGroup /\ mst # "destroyed" /\ rec /\ GcSeesGroup THEN GcSkips ELSE GcGoesTo("final") /\ UNCHANGED < ~(GroupAlive \/ left) + (gres = "removed" /\ ~diedUnrecorded) => ~(GroupAlive \/ left) \* Witnesses. check.sh expects TLC to report each one VIOLATED, which shows \* that the model reaches the state: the rules above are not true only diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index 4d2fce45..177800a7 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/check.sh +++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh @@ -142,7 +142,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 ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid FreezesUnseenGroup UnsharedGroupReadsUnknown" +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 CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid FreezesUnseenGroup UnsharedGroupReadsUnknown" # 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; @@ -242,6 +242,7 @@ write_run mutant-ShutdownBothChecks violated TerminalIsFinal "ShutdownChecksComm 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 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 d265127b..9e110b66 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -907,8 +907,9 @@ function programRecordFacts() { // Every group kill goes through stopProgramGroup. It is synchronous, and // 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, and only -// stopProgramGroup sends the SIGSTOP and SIGCONT of signalProcessGroup. +// 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. function ownershipFacts() { const module = 'src/host/programGroup.ts'; const stop = requireDeclaration(module, 'stopProgramGroup'); @@ -959,13 +960,18 @@ function ownershipFacts() { } if (isCall(node, 'processGroupTarget')) { targets += 1; + const owner = ownerPath(node); stray ||= file !== module || ![ 'isProcessGroupAlive', + 'probeFindsGroup', 'killProcessGroupBestEffort', 'signalProcessGroup', - ].includes(ownerPath(node)); + ].includes(owner) || + (['isProcessGroupAlive', 'probeFindsGroup'].includes(owner) && + normalize(node.parent.getText()) !== + 'process.kill(processGroupTarget(pgid), 0)'); } }); } @@ -979,7 +985,7 @@ function ownershipFacts() { checkedKill && judgesToken && rawKills > 0 && - targets === 3 && + targets === 4 && signalParam === "signal: 'SIGSTOP' | 'SIGCONT'" && !stray, FreezesUnseenGroup: freezeFacts(stop.body), @@ -1274,14 +1280,27 @@ function gcFacts() { ts.isShorthandPropertyAssignment(p) && p.name.text === 'provenProgramGroupRuns', ); + const runs = requireDeclaration( + 'src/host/programGroup.ts', + 'provenProgramGroupRuns', + ).body.statements.map((s) => normalize(s.getText())); const judges = + runs[0] === + 'const group = await readProvenProgramGroup(sessionDirectory);' && + runs[1] === 'if (isProgramGroupAlive(group)) { return true; }'; + // Then a group that reads gone, whose id the probe finds while no scan + // shows a member, live or zombie, counts as running too. + const probes = + judges && + runs[2] === + "return ( group !== null && !('unshared' in group) && judgeLiveGroup(group).verdict === 'gone' && probeFindsGroup(group.pid) && groupHasLiveProcess(group.pid) === null );" && normalize( requireDeclaration( 'src/host/programGroup.ts', - 'provenProgramGroupRuns', + 'probeFindsGroup', ).body.getText(), ) === - '{ return isProgramGroupAlive(await readProvenProgramGroup(sessionDirectory)); }'; + "{ try { process.kill(processGroupTarget(pgid), 0); return true; } catch (error) { if (hasErrorCode(error, 'ESRCH')) { return false; } if (hasErrorCode(error, 'EPERM')) { return true; } throw error; } }"; return { GcSkipsNonCollectable: reconcile >= 0 && collectable > reconcile, GcFinalCheck: finalCheck, @@ -1291,6 +1310,7 @@ function gcFacts() { loop.statements.indexOf(removal) > groupSkip && wired && judges, + GcProbesUnseenGroup: probes, }; } @@ -1332,6 +1352,7 @@ const COVERED = [ ['src/cli/commands/gc.ts', 'gcSessions'], ['src/cli/commands/gc.ts', 'defaultDependencies'], ['src/host/programGroup.ts', 'provenProgramGroupRuns'], + ['src/host/programGroup.ts', 'probeFindsGroup'], ['src/host/lifecycle.ts', 'allocateSession'], ['src/host/lifecycle.ts', 'launchHost'], ['src/host/lifecycle.ts', 'isProcessAlive'], diff --git a/docs/USAGE.md b/docs/USAGE.md index 6ac7ef74..4e3348a3 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -358,7 +358,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 or the boot id 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 the check and SIGCONT when the check fails. 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` while the autogroup record in `program.json` proves that a process of the program's group runs, and reports "the session's program group still runs (destroy ends it)". Without an autogroup record (see item 2), `gc` cannot prove the group, so it removes `program.json` with the folder, and a process that the program left can 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` while the autogroup record in `program.json` proves that a process of the program's group runs, or while the group id still names a process that no scan of `/proc` shows, such as a fast fork chain. It reports "the session's program group still runs (destroy ends it)". Without an autogroup record (see item 2), `gc` cannot prove the group, so it removes `program.json` with the folder, and a process that the program left can 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 01b1e916..0655dd1f 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -575,10 +575,38 @@ export function isProgramGroupAlive(group: ProgramGroup | null): boolean { ); } +// Whether gc must keep the session. gc sends no SIGSTOP, so a fork chain +// that no scan shows reads gone: a group id that the probe finds while no +// scan shows a member of the group, not even a zombie, also counts. export async function provenProgramGroupRuns( sessionDirectory: string, ): Promise { - return isProgramGroupAlive(await readProvenProgramGroup(sessionDirectory)); + const group = await readProvenProgramGroup(sessionDirectory); + if (isProgramGroupAlive(group)) { + return true; + } + return ( + group !== null && + !('unshared' in group) && + judgeLiveGroup(group).verdict === 'gone' && + probeFindsGroup(group.pid) && + groupHasLiveProcess(group.pid) === null + ); +} + +function probeFindsGroup(pgid: number): boolean { + try { + process.kill(processGroupTarget(pgid), 0); + return true; + } catch (error) { + if (hasErrorCode(error, 'ESRCH')) { + return false; + } + if (hasErrorCode(error, 'EPERM')) { + return true; + } + throw error; + } } export function stopProgramGroup(group: ProgramGroup | null): void { diff --git a/test/integration/lifecycle.test.ts b/test/integration/lifecycle.test.ts index 4b63a436..2539607c 100644 --- a/test/integration/lifecycle.test.ts +++ b/test/integration/lifecycle.test.ts @@ -1149,6 +1149,42 @@ describe('lifecycle integration', { timeout: 30000 }, () => { }, ); + // gc sends no SIGSTOP, so only the probe of the group id finds the chain. + it.runIf(capturesToken)( + 'gc keeps an exited session while a fork chain that the program left runs', + async () => { + const beat = join(testHome, 'beat'); + const sessionId = createSession(testHome, [ + '/bin/sh', + '-c', + `trap "" HUP; python3 '${forkChain}' 60 0.002 '${beat}' & exit 0`, + ]); + pgid = inspectSession(testHome, sessionId).childPid as number; + const deadline = Date.now() + 10_000; + while ( + !existsSync(beat) || + inspectSession(testHome, sessionId).status !== 'exited' + ) { + expect(Date.now()).toBeLessThan(deadline); + await sleep(100); + } + expect(await chainRuns(beat)).toBe(true); + + const kept = runCli(['gc', '--json'], { AGENT_TTY_HOME: testHome }); + expect(JSON.parse(kept.stdout)).toMatchObject({ + ok: true, + result: { removedSessionCount: 0 }, + }); + expect(inspectSession(testHome, sessionId).status).toBe('exited'); + + const destroyed = runCli(['destroy', sessionId, '--json'], { + AGENT_TTY_HOME: testHome, + }); + expect(JSON.parse(destroyed.stdout)).toMatchObject({ ok: true }); + expect(await chainRuns(beat)).toBe(false); + }, + ); + it('a reconcile after a host crash ends the program and its background process', async () => { const sessionId = await createProgram( 'trap "" TERM HUP; sleep 300 & touch "$0"; wait', diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index 279e5f3a..ed09954a 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -22,6 +22,7 @@ import { judgeProgramGroup, parseAutogroup, parseProcStat, + provenProgramGroupRuns, readProgramGroup, readProvenProgramGroup, stopProgramGroup, @@ -33,7 +34,11 @@ import { programRecordPath, sessionDir, } from '../../../src/storage/sessionPaths.js'; -import { captureHost, writeHostRecord } from '../../../src/host/hostRecord.js'; +import { + captureHost, + writeHostRecord, + type HostRecord, +} from '../../../src/host/hostRecord.js'; import { capturesToken } from '../../helpers.js'; import type * as Fs from 'node:fs'; @@ -869,6 +874,60 @@ describe('a program group with a token, as a faked /proc shows it', () => { : null; } + // gc sends no SIGSTOP, so a fork chain that no scan shows reads gone. + describe('provenProgramGroupRuns', () => { + async function recordedSession(): Promise { + const directory = await mkdtemp(join(tmpdir(), 'agent-tty-runs-')); + writeProgramRecord(directory, group); + writeHostRecord(directory, captureHost(process.pid) as HostRecord); + return directory; + } + + it.each([ + { + when: 'no scan shows a member and the probe finds the id', + states: [], + probe: 'ok', + runs: true, + }, + { + when: 'only zombies are left', + states: ['Z'], + probe: 'ok', + runs: false, + }, + { + when: 'the probe finds no process', + states: [], + probe: 'ESRCH', + runs: false, + }, + { + when: 'a live member carries the token', + states: ['S'], + probe: 'ok', + runs: true, + }, + ] as const)( + 'when $when, reads the group running: $runs', + async ({ states, probe, runs }) => { + const directory = await recordedSession(); + try { + procShowsTokenGroup(...states); + if (probe === 'ok') { + probeEnds('ok'); + } else { + killFailsWith(probe); + } + + expect(await provenProgramGroupRuns(directory)).toBe(runs); + } finally { + await rm(directory, { recursive: true, force: true }); + } + }, + ); + }); + it.each(['EPERM', 'EACCES'])( 'is alive and gets the kill when a live member carries the token and another process refuses its read with %s', (readError) => { From 8b4deb2d0dfe205a1ea4abb61e39540cc1c8e207 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 22:03:27 +0000 Subject: [PATCH 06/17] chore: sync the lifecycle coverage record after the main merge --- .../skills/verify-session-lifecycle/SKILL.md | 2 +- .../verify-session-lifecycle/coverage.json | 19 ++++++++++++------- 2 files changed, 13 insertions(+), 8 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index faf8b068..a28898d6 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -522,7 +522,7 @@ To bring the check back in line after changes that skipped it, use `/maintain-fo ## Scope -The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 25,534,376 distinct states, and without one 24,675,744. The check prints both counts. +The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 27,654,252 distinct states, and without one 26,870,672. The check prints both counts. It assumes: diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index ba0e2fd7..cdfa985d 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -5,7 +5,8 @@ "src/cli/commands/destroy.ts#rerunInNewSession": "cf32d7d082758522", "src/cli/commands/gc.ts#gcSessions": "a2ac8bd10f100332", "src/cli/commands/gc.ts#defaultDependencies": "81a9894438cb5be7", - "src/host/programGroup.ts#provenProgramGroupRuns": "80ea01be23763792", + "src/host/programGroup.ts#provenProgramGroupRuns": "c59ef5d6c37a049e", + "src/host/programGroup.ts#probeFindsGroup": "31ea7b5e835c0509", "src/host/lifecycle.ts#allocateSession": "77dab09b34fedce5", "src/host/lifecycle.ts#launchHost": "597a5a6b9eb58cc8", "src/host/lifecycle.ts#isProcessAlive": "1ca1fe6ad6c41711", @@ -36,9 +37,11 @@ "src/host/lifecycle.ts#waitForProcessesToExit": "bdab1d674a6856b8", "src/host/lifecycle.ts#stopSessionProcesses": "d1abb608b1d2160a", "src/host/lifecycle.ts#recordDestroyed": "d3a74237a9c8459c", - "src/host/lifecycle.ts#removeDeadHostSocket": "e4044ea706544ff8", + "src/host/lifecycle.ts#removeDeadHostSocket": "34ce07ab7b7e8d7b", "src/host/lifecycle.ts#destroySession": "d840dd07a0e481f5", - "src/host/lifecycle.ts#reconcileSession": "c2904456d54b87c8", + "src/host/lifecycle.ts#isMarkedDestroyed": "d178f4a63473915c", + "src/host/lifecycle.ts#writeMarkedDestroyed": "4863c35f70699757", + "src/host/lifecycle.ts#reconcileSession": "4e5dac8144a0d9fb", "src/host/hostMain.ts#waitForManifestFromCreate": "fd500651f83683eb", "src/host/hostMain.ts#isSessionCommandable": "260060f07b068ec1", "src/host/hostMain.ts#SHUTDOWN_KILL_GRACE_MS": "51171d9c5aa6c510", @@ -89,16 +92,17 @@ "src/host/hostMain.ts#runHost(final try)": "16789dd4e2534bc7", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "f6e5e97a2a5defc1", - "skill:scripts/facts.mjs": "c859e87c2e9ac81a", - "skill:scripts/check.sh": "8f5abb45097333f2" + "skill:model/SessionLifecycle.tla": "57342e142bf3b9fe", + "skill:scripts/facts.mjs": "c4733ce37c35ff33", + "skill:scripts/check.sh": "55930dbbd5a93ef3" }, "callSites": { "writeManifest": [ "src/host/lifecycle.ts#allocateSession", "src/host/lifecycle.ts#reconcileSession", "src/host/lifecycle.ts#reconcileSession", - "src/host/lifecycle.ts#recordDestroyed" + "src/host/lifecycle.ts#recordDestroyed", + "src/host/lifecycle.ts#writeMarkedDestroyed" ], "persistManifest": [ "src/host/hostMain.ts#runHost", @@ -144,6 +148,7 @@ "reconcileSession": [ "src/cli/commands/gc.ts#gcSessions", "src/cli/commands/inspect.ts#runInspectCommand", + "src/cli/commands/inspect.ts#runInspectCommand", "src/host/lifecycle.ts#destroySession", "src/host/lifecycle.ts#destroySession", "src/host/lifecycle.ts#listSessions" From 701af730d5c3befbe5babb6fb47846e09416214c Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 22:45:08 +0000 Subject: [PATCH 07/17] test: run the provenProgramGroupRuns tests on Linux only; docs: gc keeps a group it cannot check Codex on #302: an exited session whose group reads unknown stays after gc, and USAGE said gc could remove it. --- docs/USAGE.md | 4 ++-- test/unit/host/programGroup.test.ts | 5 +++-- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/docs/USAGE.md b/docs/USAGE.md index 8423d349..889e1b0c 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -358,9 +358,9 @@ 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 or the boot id 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 the check and SIGCONT when the check fails. 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` while the autogroup record in `program.json` proves that a process of the program's group runs, or while the group id still names a process that no scan of `/proc` shows, such as a fast fork chain. It reports "the session's program group still runs (destroy ends it)". Without an autogroup record (see item 2), `gc` cannot prove the group, so it removes `program.json` with the folder, and a process that the program left can 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` while the autogroup record in `program.json` proves that a process of the program's group runs, or while the group id still names a process that no scan of `/proc` shows, such as a fast fork chain. It also keeps it while it cannot check the group, for example when `/proc` refuses the autogroup of a live member, because such a group counts as running. It reports "the session's program group still runs (destroy ends it)". Without an autogroup record (see item 2), `gc` cannot prove the group, so it removes `program.json` with the folder, and a process that the program left can 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. + - 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` keeps the session folder until the group has ended or agent-tty can check it again. - 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`. 7. Off Linux, reconcile counts the host as alive while any process has its pid. A crashed host that stays a zombie, or a process that got its pid, keeps the session `running`, and `destroy --force` kills nothing and fails with `HOST_TIMEOUT`. On Linux, the same happens when `/proc` is not mounted or refuses to show the host, and for a session that an agent-tty version without `host.json` started. On Windows, `destroy --force` never kills the host: it kills the program, and a host that hangs makes it fail with `HOST_TIMEOUT`. End such a host yourself with the Host PID that `inspect` shows (`taskkill /pid /f`), then run `destroy --force` again. When agent-tty cannot judge the host (another pid namespace or machine, or a refused read of `/proc/self/ns/pid`), `destroy --force` cannot see the host end either. It can fail with `HOST_TIMEOUT` although the host has recorded the session as `exited`, and a second `destroy --force` then records it as `destroyed`. When `/proc` is mounted but refuses to show the host and the program's processes (a security module that hides processes of the same user), `destroy --force` kills nothing and fails with `HOST_TIMEOUT` also for a healthy host. 8. A Home that several machines share, for example over NFS, works only from the machine that started each session. From another machine, agent-tty counts the host as running and kills nothing, because the machine id differs. Machines without a machine id (an empty, missing or `uninitialized` `/etc/machine-id`, as in many container images), or with the same one (a cloned image), cannot tell each other apart. agent-tty takes a machine id only when it is 32 lowercase hex characters, so it also reads any other value, such as a UUID with dashes or uppercase hex, as no id. There the boot id differs, so the other machine counts a live host as ended, records the session as `failed`, and `gc` can then remove its folder. Remote sessions are out of scope (see `RELEASE.md`). diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index ed09954a..a1dabfb2 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -874,8 +874,9 @@ describe('a program group with a token, as a faked /proc shows it', () => { : null; } - // gc sends no SIGSTOP, so a fork chain that no scan shows reads gone. - describe('provenProgramGroupRuns', () => { + // gc sends no SIGSTOP, so a fork chain that no scan shows reads gone. The + // records name this process's pid space, which only Linux records. + describe.runIf(platform === 'linux')('provenProgramGroupRuns', () => { async function recordedSession(): Promise { const directory = await mkdtemp(join(tmpdir(), 'agent-tty-runs-')); writeProgramRecord(directory, group); From d16a34fc5c73f63b986da8f6ae01bf4da60ce3dc Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 23:10:56 +0000 Subject: [PATCH 08/17] ci: run the lifecycle model check in four shares One job of 4 vCPUs took 63 min for the 73 TLC runs. check.sh gains CHECK_SHARD=/, which takes every n-th run that expects pass and every n-th of the rest, and the lifecycle-model job runs four shares. --- .../skills/verify-session-lifecycle/SKILL.md | 2 +- .../verify-session-lifecycle/coverage.json | 2 +- .../verify-session-lifecycle/scripts/check.sh | 30 ++++++++++++++++++- .github/workflows/ci.yml | 14 ++++++--- 4 files changed, 41 insertions(+), 7 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index a28898d6..8d53c8f2 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -55,7 +55,7 @@ Yes, when the diff changes any of these: You do not have to judge this by hand. The check prints `STALE` when any of these changed since the sync commit. -CI runs the check in the `lifecycle-model` job. Every run of it calls `scripts/check.sh --drift-only`, which compares the covered code with `coverage.json` and needs no Java, and fails on `STALE`. The whole check runs only when `coverage.json` differs from the base of the pull request or merge group. +CI runs the check in the `lifecycle-model` job. Every run of it calls `scripts/check.sh --drift-only`, which compares the covered code with `coverage.json` and needs no Java, and fails on `STALE`. The whole check runs only when `coverage.json` differs from the base of the pull request or merge group, in four jobs with `CHECK_SHARD=/4`. Each job runs every fourth run that expects pass and every fourth of the rest, because the runs that expect pass explore the whole model and take most of the time. ## Run it diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index cdfa985d..9bf3e0af 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -94,7 +94,7 @@ "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", "skill:model/SessionLifecycle.tla": "57342e142bf3b9fe", "skill:scripts/facts.mjs": "c4733ce37c35ff33", - "skill:scripts/check.sh": "55930dbbd5a93ef3" + "skill:scripts/check.sh": "0b31e02e391b203f" }, "callSites": { "writeManifest": [ diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index a42bedae..2c2f8b99 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/check.sh +++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh @@ -19,7 +19,9 @@ # # Needs: node (the repo's), Java 11 or newer, and the network once, to fetch # the pinned TLC jar. Env: JAVA (default java), TLA2TOOLS_JAR (use this jar), -# CHECK_OUT (keep the results in this folder), CHECK_JOBS (default 4). +# CHECK_OUT (keep the results in this folder), CHECK_JOBS (default 4), +# CHECK_SHARD=/ (run only the i-th of n shares of the runs; CI runs +# the shares in parallel jobs). set -euo pipefail UPDATE_COVERAGE=0 @@ -43,6 +45,7 @@ SPEC="$SKILL_DIR/model/SessionLifecycle.tla" COVERAGE="$SKILL_DIR/coverage.json" JAVA=${JAVA:-java} JOBS=${CHECK_JOBS:-4} +SHARD=${CHECK_SHARD:-1/1} TLC_VERSION=1.7.4 TLC_SHA256=936a262061c914694dfd669a543be24573c45d5aa0ff20a8b96b23d01e050e88 TLC_URL="https://github.com/tlaplus/tlaplus/releases/download/v$TLC_VERSION/tla2tools.jar" @@ -66,6 +69,10 @@ sha256() { case "$JOBS" in *[!0-9]* | 0*) die "CHECK_JOBS must be a positive integer, not '$JOBS'" ;; esac +SHARD_INDEX=${SHARD%%/*} +SHARD_COUNT=${SHARD#*/} +[[ $SHARD =~ ^[1-9][0-9]*/[1-9][0-9]*$ ]] && [ "$SHARD_INDEX" -le "$SHARD_COUNT" ] || + die "CHECK_SHARD must be / with 1 <= i <= n, not '$SHARD'" command -v node >/dev/null 2>&1 || die "node is not on PATH" if [ "$DRIFT_ONLY" -eq 0 ]; then # `java -version` prints `version "11.0.2"`, or `version "1.8.0_292"` for Java 8. @@ -266,6 +273,26 @@ write_run mutant-KillsProgramGroup-no-token violated DestroyedProgramStopped "Ki write_run mutant-HostWaitsForGroup-no-token violated DestroyedProgramStopped "HostWaitsForGroup=FALSE" "without a token, the host records destroyed while a process of another user runs" DestroyedProgramStopped write_run mutant-ReconcileWaitsForGroup-no-token violated LiveGroupStaysNamed "ReconcileWaitsForGroup=FALSE" "without a token, reconcile drops childPid while the group runs" LiveGroupStaysNamed +# A run that expects pass explores the whole model and takes minutes, and a +# run that expects a violation stops at the first one, mostly in seconds. So +# a share takes every n-th run of each kind, which spreads the long runs. +if [ "$SHARD_COUNT" -gt 1 ]; then + passes=0 + others=0 + share="" + for name in $RUNS; do + if [ "$(cut -f1 "$OUT/$name/expect.txt")" = pass ]; then + [ $((passes % SHARD_COUNT + 1)) -eq "$SHARD_INDEX" ] && share="$share $name" + passes=$((passes + 1)) + else + [ $((others % SHARD_COUNT + 1)) -eq "$SHARD_INDEX" ] && share="$share $name" + others=$((others + 1)) + fi + done + RUNS=$share + echo "Share $SHARD of the runs:$RUNS" +fi + run_tlc() { local dir rc=0 dir=$(cd "$OUT/$1" && pwd) @@ -339,6 +366,7 @@ echo echo "Facts: $FACTS_LINE" echo " Collectable=$COLLECTABLE Terminal=$TERMINAL" for name in current current-no-token; do + case " $RUNS " in *" $name "*) ;; *) continue ;; esac echo "Distinct states of $name: $(sed -n 's/.* \([0-9]*\) distinct states found.*/\1/p' "$OUT/$name/tlc.out" | tail -1)." done echo "A violated run stops at its first violation." diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 78cadfd2..cf072df1 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -218,12 +218,17 @@ jobs: # Model-checks the session lifecycle with the verify-session-lifecycle # skill. Every run checks that coverage.json matches the covered code. The - # TLC runs take about two CPU-hours, so they run only when coverage.json - # differs from the base, which every change to the model, its scripts or - # the covered code needs. + # TLC runs took 63 min in one job of 4 vCPUs, so they run in 4 shares, and + # only when coverage.json differs from the base, which every change to the + # model, its scripts or the covered code needs. lifecycle-model: runs-on: ubuntu-latest - timeout-minutes: 75 + timeout-minutes: 50 + strategy: + fail-fast: false + matrix: + shard: [1, 2, 3, 4] + name: lifecycle-model (${{ matrix.shard }}/4) steps: - name: Check out repository uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6 @@ -258,6 +263,7 @@ jobs: if: steps.inputs.outputs.tlc == 'true' env: CHECK_JOBS: '4' + CHECK_SHARD: ${{ matrix.shard }}/4 run: .agents/skills/verify-session-lifecycle/scripts/check.sh quality-gates: From b0c2b8d46cc45cd6222feecc079b5c68ff92d913 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 01:07:32 +0000 Subject: [PATCH 09/17] ci: note the measured shard times of the lifecycle model check --- .github/workflows/ci.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index cf072df1..f0dec2df 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -218,9 +218,9 @@ jobs: # Model-checks the session lifecycle with the verify-session-lifecycle # skill. Every run checks that coverage.json matches the covered code. The - # TLC runs took 63 min in one job of 4 vCPUs, so they run in 4 shares, and - # only when coverage.json differs from the base, which every change to the - # model, its scripts or the covered code needs. + # TLC runs took 63 min in one job of 4 vCPUs and take 10 to 17 min in each + # of 4 shares. They run only when coverage.json differs from the base, + # which every change to the model, its scripts or the covered code needs. lifecycle-model: runs-on: ubuntu-latest timeout-minutes: 50 From dd7a3a77fd4d727a9cf1aeee28cd183f2ae071ce Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 03:04:20 +0000 Subject: [PATCH 10/17] ci: fail the lifecycle drift check when a guard value changes coverage.json now records the facts (every guard and status set) that facts.mjs read at the sync, and check.sh --drift-only compares them. The facts come from the source text with its comments while the hashes leave comments out, so one new comment in reconcileSession's repair block turned ReconcileRepairsDestroyed FALSE and the drift check still passed. --- .../skills/verify-session-lifecycle/SKILL.md | 6 ++--- .../verify-session-lifecycle/scripts/check.sh | 25 ++++++++++++++++--- 2 files changed, 24 insertions(+), 7 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 8d53c8f2..02fe973e 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -55,7 +55,7 @@ Yes, when the diff changes any of these: You do not have to judge this by hand. The check prints `STALE` when any of these changed since the sync commit. -CI runs the check in the `lifecycle-model` job. Every run of it calls `scripts/check.sh --drift-only`, which compares the covered code with `coverage.json` and needs no Java, and fails on `STALE`. The whole check runs only when `coverage.json` differs from the base of the pull request or merge group, in four jobs with `CHECK_SHARD=/4`. Each job runs every fourth run that expects pass and every fourth of the rest, because the runs that expect pass explore the whole model and take most of the time. +CI runs the check in the `lifecycle-model` job. Every run of it calls `scripts/check.sh --drift-only`, which compares the guard values and the covered code with `coverage.json` and needs no Java, and fails on `STALE`. The whole check runs only when `coverage.json` differs from the base of the pull request or merge group, in four jobs with `CHECK_SHARD=/4`. Each job runs every fourth run that expects pass and every fourth of the rest, because the runs that expect pass explore the whole model and take most of the time. ## Run it @@ -72,7 +72,7 @@ What it does: 1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the thirty-three 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 73 times and prints one line per run. -4. It compares the hashes and call sites with `coverage.json`. +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. @@ -556,7 +556,7 @@ The artifact commands never create the session folder (coder/agent-tty#198). `en ## Coverage record -The sync commit is the last commit that changed `coverage.json`. `check.sh` prints it, and `git log -1 --format=%h -- .agents/skills/verify-session-lifecycle/coverage.json` shows it too. In that commit, someone read the covered code above and confirmed that the model describes it. `coverage.json` holds the hash of each covered function, of the model and of the two check scripts, and the list of call sites at that commit. The check compares them with the code on every run. +The sync commit is the last commit that changed `coverage.json`. `check.sh` prints it, and `git log -1 --format=%h -- .agents/skills/verify-session-lifecycle/coverage.json` shows it too. In that commit, someone read the covered code above and confirmed that the model describes it. `coverage.json` holds the value of each guard and status set that `scripts/facts.mjs` read, the hash of each covered function, of the model and of the two check scripts, and the list of call sites at that commit. The check compares them with the code on every run. The guards come from the source text with its comments, and the hashes leave comments out. So a new comment inside a guarded block can turn a guard FALSE while every hash stays the same, and the check then prints `fact changed: was true, now false`. Change `coverage.json` (with `check.sh --update-coverage`) only in the same commit as a confirmed model, or after you have confirmed that the model still describes the changed code. Because the sync commit comes from git, a squash merge keeps it correct. diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index 2c2f8b99..e077dab7 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/check.sh +++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh @@ -5,8 +5,8 @@ # # .agents/skills/verify-session-lifecycle/scripts/check.sh [--update-coverage | --drift-only] # -# --drift-only compares the covered code with coverage.json and runs no TLC, -# so it needs no Java: exit 0 or 3 as below. +# --drift-only compares the facts and the covered code with coverage.json +# and runs no TLC, so it needs no Java: exit 0 or 3 as below. # # Exit 0: every TLC run gave the expected result and the covered code is # unchanged since the last sync. @@ -104,18 +104,35 @@ if [ "$UPDATE_COVERAGE" -eq 1 ]; then node -e ' const fs = require("node:fs"); const facts = JSON.parse(fs.readFileSync(process.argv[1], "utf8")); - const record = { fingerprints: facts.fingerprints, callSites: facts.callSites }; + const record = { + constants: facts.constants, + fingerprints: facts.fingerprints, + callSites: facts.callSites, + }; fs.writeFileSync(process.argv[2], JSON.stringify(record, null, 2) + "\n"); ' "$OUT/facts.json" "$COVERAGE" echo "Rewrote $COVERAGE. Commit it only after you have confirmed that the model" echo "describes the code: that commit becomes the sync commit." fi -# Prints one line per covered function or call site that changed. +# Prints one line per fact, covered function or call site that changed. The +# facts come from the source text with its comments, and the hashes leave +# comments out, so a new comment in a guarded block can turn a guard FALSE +# while every hash stays the same. node -e ' const fs = require("node:fs"); const facts = JSON.parse(fs.readFileSync(process.argv[1], "utf8")); const record = JSON.parse(fs.readFileSync(process.argv[2], "utf8")); + const recorded = record.constants ?? {}; + for (const [key, value] of Object.entries(facts.constants)) { + const before = key in recorded ? JSON.stringify(recorded[key]) : "not recorded"; + if (before !== JSON.stringify(value)) { + console.log(`fact ${key} changed: was ${before}, now ${JSON.stringify(value)}`); + } + } + for (const key of Object.keys(recorded)) { + if (!(key in facts.constants)) console.log(`fact ${key} is no longer read`); + } for (const [key, value] of Object.entries(facts.fingerprints)) { if (record.fingerprints[key] !== value) console.log(`changed: ${key}`); } From b4e1b8341f540b2145abc55120b9f7cf6eff59e7 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 04:15:37 +0000 Subject: [PATCH 11/17] chore: sync the lifecycle coverage record with its facts after the main merge check.sh --update-coverage at c9dd5be5 gave 74/74 runs as expected. The record now holds the facts. current has 26,798,236 distinct states and current-no-token 26,648,756. --- .../skills/verify-session-lifecycle/SKILL.md | 4 +- .../verify-session-lifecycle/coverage.json | 49 +++++++++++++++++-- 2 files changed, 47 insertions(+), 6 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index eb72c3b0..8a892fa9 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 this repo it takes about eleven minutes with the default `CHECK_JOBS` of 4. Eight runs explore the whole model, so `CHECK_JOBS=74` 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 this repo it takes about eleven minutes with the default `CHECK_JOBS` of 4. Ten runs explore the whole model, so `CHECK_JOBS=74` 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: @@ -528,7 +528,7 @@ To bring the check back in line after changes that skipped it, use `/maintain-fo ## Scope -The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 27,654,252 distinct states, and without one 26,870,672. The check prints both counts. +The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 26,798,236 distinct states, and without one 26,648,756. The check prints both counts. It assumes: diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 0eab56ff..fc00c36a 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -1,10 +1,51 @@ { + "constants": { + "ReconcileSkipsTerminal": true, + "ReconcileSkipsLiveHost": true, + "ReconcileRereads": true, + "GcSkipsNonCollectable": true, + "GcFinalCheck": true, + "GcKeepsLiveGroup": true, + "GcProbesUnseenGroup": true, + "CreateRecordsHostPid": true, + "CreateRecordsHost": true, + "CreateStopsOnGiveUp": true, + "HostWaitsForManifest": true, + "HostSerializesWrites": true, + "HostStopsAfterTerminalWrite": true, + "ShutdownChecksCommandable": true, + "DestroyRecordsDestroyed": true, + "DestroyKeepsExitCode": true, + "DestroyStopsLeftovers": true, + "ProvesHostPid": true, + "ReconcileRepairsDestroyed": true, + "ReconcileRepairsMarked": true, + "ManifestWriteNeedsFolder": true, + "KillsProgramGroup": true, + "ProbeCountsDeniedGroup": true, + "HostWaitsForGroup": true, + "ReconcileWaitsForGroup": true, + "RecordsProgramSync": true, + "ProvesGroupOwnership": true, + "FreezesUnseenGroup": true, + "FallbackNeedsFolder": true, + "UnsharedGroupReadsUnknown": true, + "TokenNamesProgram": true, + "ReusedIdReadsGone": true, + "ReRunsInNewSession": true, + "InsideCheckReadsEnv": true, + "Collectable": ["destroyed", "exited", "failed"], + "Terminal": ["destroyed", "exited", "failed"] + }, "fingerprints": { "src/cli/commands/create.ts#runCreateCommand": "635715a49fa0273e", "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": "667e4ebc3ca3029c", + "src/cli/commands/gc.ts#gcSessions": "a2ac8bd10f100332", + "src/cli/commands/gc.ts#defaultDependencies": "81a9894438cb5be7", + "src/host/programGroup.ts#provenProgramGroupRuns": "c59ef5d6c37a049e", + "src/host/programGroup.ts#probeFindsGroup": "31ea7b5e835c0509", "src/host/lifecycle.ts#allocateSession": "43819af8c6c271ec", "src/host/lifecycle.ts#launchHost": "597a5a6b9eb58cc8", "src/host/lifecycle.ts#isProcessAlive": "1ca1fe6ad6c41711", @@ -91,9 +132,9 @@ "src/host/hostMain.ts#runHost(final try)": "16789dd4e2534bc7", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "7986bb289034aa6c", - "skill:scripts/facts.mjs": "ea6bebdccb255054", - "skill:scripts/check.sh": "66a765237f244773" + "skill:model/SessionLifecycle.tla": "acab1ebdb1d93654", + "skill:scripts/facts.mjs": "5275ba91a44f3cd6", + "skill:scripts/check.sh": "f2164c27c0ae4b30" }, "callSites": { "writeManifest": [ From 477c40e0a071f88d8f15f0accc9374589236ba6b Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 05:12:36 +0000 Subject: [PATCH 12/17] fix(gc): keep a session only while gc proves its group runs A group that gc cannot check proved nothing but kept its session forever. After a container restart that keeps the home, host.json names a pid namespace that no longer exists, the group reads unshared, and no destroy can prove it gone. provenProgramGroupRuns now counts only a live member that carries the token, or the probe of a fork chain that no scan shows. In another pid space, or behind a refused read of /proc, gc removes the session as main did. The model reads the group not proven in another pid space, R20 covers a gc in the host's pid space, and witness-WitnessUnsharedGcRemovesLeftover-otherspace shows the trade-off. The gc integration tests now let the program exit only once program.json is in place, and skip when the host captured no token: /bin/sh could exit before the capture under load. A unit test covers the gc skip when the group check throws. SKILL.md gives the measured time of a whole run. --- .../skills/verify-session-lifecycle/SKILL.md | 7 +- .../model/SessionLifecycle.tla | 39 +++++++---- .../verify-session-lifecycle/scripts/check.sh | 1 + .../scripts/facts.mjs | 19 ++++-- docs/USAGE.md | 6 +- src/host/programGroup.ts | 27 +++++--- test/integration/lifecycle.test.ts | 66 +++++++++++++++++-- test/unit/commands/gc.test.ts | 43 ++++++++++++ test/unit/host/programGroup.test.ts | 43 ++++++++++++ 9 files changed, 211 insertions(+), 40 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index f8467d59..a0d0f240 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -33,7 +33,7 @@ The tool is TLC, the TLA+ model checker, pinned to release 1.7.4 by sha256. The | 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 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. | +| 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. | `TypeOK` also runs in every run. When it breaks, the model is wrong, not the code. @@ -55,7 +55,7 @@ Yes, when the diff changes any of these: You do not have to judge this by hand. The check prints `STALE` when any of these changed since the sync commit. -CI runs the check in the `lifecycle-model` job. Every run of it calls `scripts/check.sh --drift-only`, which compares the guard values and the covered code with `coverage.json` and needs no Java, and fails on `STALE`. The whole check runs only when `coverage.json` differs from the base of the pull request or merge group, in four jobs with `CHECK_SHARD=/4`. Each job runs every fourth run that expects pass and every fourth of the rest, because the runs that expect pass explore the whole model and take most of the time. +CI runs the check in the `lifecycle-model` job. Its first share calls `scripts/check.sh --drift-only`, which compares the guard values and the covered code with `coverage.json` and needs no Java, and fails on `STALE`. The whole check runs only when `coverage.json` differs from the base of the pull request or merge group, in four jobs with `CHECK_SHARD=/4`. Each job runs every fourth run that expects pass and every fourth of the rest, because the runs that expect pass explore the whole model and take most of the time. ## Run it @@ -97,6 +97,7 @@ At the sync commit, the expected results are: | `mutant-ShutdownChecksCommandable` | pass | `initiateShutdown` requests destroy only while the session is commandable, and the writer writes nothing after a terminal record. Either one alone keeps R3. Removing both is not safe. | | `current-otherspace`, the code as it is with `destroy`, `list` and `gc` in another pid space than the host, every rule | pass | `OtherPidSpace`: no scan and no probe of those commands shows the program's processes, as without `/proc`, with an empty `/proc`, in another pid namespace or on another machine. | | `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. | | `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. | @@ -472,7 +473,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 that group reads alive, also under `--dry-run`. A failed read skips it too. 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. In another pid space the group reads alive, so gc keeps every session with a token there that is not destroyed. 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. +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. 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. ```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 21415a25..876d6e8a 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -1087,17 +1087,21 @@ GcReadsReconciled == lruns, destroyVars, groupVars>> \* provenProgramGroupRuns reads program.json and judges the group, as the -\* waits of destroy do. gc sends no SIGSTOP, so with Unseen no scan shows -\* the program's processes, and with GcProbesUnseenGroup the probe +\* 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 GcKeepsLiveGroup gc skips a session that -\* is not destroyed while that group reads alive ("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. +\* 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 == - \/ CliGroupSeen("proven") - \/ GcProbesUnseenGroup /\ Unseen /\ (prog \/ left) + /\ ~OtherPidSpace + /\ \/ GroupSeen("proven") + \/ GcProbesUnseenGroup /\ Unseen /\ (prog \/ left) GcChecksGroup == /\ pc["gc"] = "group" @@ -1578,12 +1582,15 @@ DestroyedStaysDestroyed == \* pid after the host ended. NoUnrelatedHostKilled == ~hitUnrelatedHost -\* R20: gc removes the 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. It does not count a program that no -\* program.json named (see R16). +\* R20: gc in the host's pid space removes the 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. It does not count +\* a program that no program.json named (see R16). A gc in another pid +\* space cannot check the group, and it removes the folder as it does +\* without a token (WitnessUnsharedGcRemovesLeftover). RemovedSessionStopped == - (gres = "removed" /\ ~diedUnrecorded) => ~(GroupAlive \/ left) + (gres = "removed" /\ ~diedUnrecorded /\ ~OtherPidSpace) + => ~(GroupAlive \/ left) \* Witnesses. check.sh expects TLC to report each one VIOLATED, which shows \* that the model reaches the state: the rules above are not true only @@ -1630,4 +1637,8 @@ WitnessWaitPassesReusedId == ~passedReused \* destroyed record. WitnessUnsharedDestroyCompletes == ~(OtherPidSpace /\ ~dforce /\ wasNamed /\ dres = "ok") +\* With OtherPidSpace gc removes an exited session while a process that +\* the program left runs, because it cannot check the group there. +WitnessUnsharedGcRemovesLeftover == + ~(OtherPidSpace /\ rec /\ left /\ gres = "removed") ============================================================================= diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index e2c3c1de..fcb6ab42 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/check.sh +++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh @@ -280,6 +280,7 @@ UNSEEN=FALSE OTHER=TRUE write_run current-otherspace pass "$RULES" "" "the code with destroy, list and gc in another pid space: every rule holds" write_run witness-WitnessUnsharedDestroyCompletes-otherspace violated WitnessUnsharedDestroyCompletes "" "a plain destroy from another pid space still succeeds" +write_run witness-WitnessUnsharedGcRemovesLeftover-otherspace violated WitnessUnsharedGcRemovesLeftover "" "gc in another pid space cannot check the group, so it removes an exited session while a process that the program left runs" write_run mutant-UnsharedGroupReadsUnknown-otherspace violated DestroyedSessionStopped "UnsharedGroupReadsUnknown=FALSE" "with the group read gone where no scan or probe shows it, destroy of an exited session records destroyed while a process it left runs" DestroyedSessionStopped 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 diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 7838d72e..e7064157 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -1363,7 +1363,9 @@ function gcFacts() { // program.json proves a live group for a session that is not destroyed, // and skips the session when it does or when the read throws. The // default dependency is provenProgramGroupRuns, which judges the group - // that readProvenProgramGroup gives as isProgramGroupAlive does. + // that readProvenProgramGroup gives and counts it only when a live member + // carries the token. A group in another pid space reads unshared there, + // and gc does not count it. const groupRead = loop.statements.findIndex( (s) => ts.isTryStatement(s) && @@ -1393,16 +1395,21 @@ function gcFacts() { 'src/host/programGroup.ts', 'provenProgramGroupRuns', ).body.statements.map((s) => normalize(s.getText())); + const owned = "verdict === 'owned'"; + // Or a group that reads gone, whose id the probe finds while no scan + // shows a member, live or zombie. + const withProbe = `return ( ${owned} || (verdict === 'gone' && probeFindsGroup(group.pid) && groupHasLiveProcess(group.pid) === null) );`; const judges = + runs.length === 4 && runs[0] === 'const group = await readProvenProgramGroup(sessionDirectory);' && - runs[1] === 'if (isProgramGroupAlive(group)) { return true; }'; - // Then a group that reads gone, whose id the probe finds while no scan - // shows a member, live or zombie, counts as running too. + runs[1] === + "if (group === null || 'unshared' in group) { return false; }" && + runs[2] === 'const { verdict } = judgeLiveGroup(group);' && + (runs[3] === `return ${owned};` || runs[3] === withProbe); const probes = judges && - runs[2] === - "return ( group !== null && !('unshared' in group) && judgeLiveGroup(group).verdict === 'gone' && probeFindsGroup(group.pid) && groupHasLiveProcess(group.pid) === null );" && + runs[3] === withProbe && normalize( requireDeclaration( 'src/host/programGroup.ts', diff --git a/docs/USAGE.md b/docs/USAGE.md index f9bb1cdc..93de8a69 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -347,7 +347,7 @@ If no process passes the check, agent-tty kills nothing, for example when an unr If `/proc` refuses to show the boot id, or shows no autogroup id for a live process whose group and session id are the program's pid (it refuses the read, or the file is empty or malformed), agent-tty cannot run the check. It then kills nothing and counts the group as running. When the CLI cannot list `/proc` at all, as in a chroot or a container without it, it sees no process of the group, and nothing proves a kill. For a session without an autogroup record, the group then counts as running while `kill(-pgid, 0)` finds a process. A session with an autogroup record but without `host.json` counts as running whatever the probe finds. A plain `destroy` still ends a live session through its host, and `destroy --force` of a session with an autogroup record fails with `HOST_TIMEOUT`. End it with a plain `destroy`, or run `destroy --force` from a process that can read `/proc`. -On Linux, a CLI that cannot prove that it shares the host's pid space cannot prove that the program's group ended either: it cannot read `/proc/self/ns/pid` (no `/proc`, or an empty one), its `/proc` belongs to another pid namespace (`/proc/self` names another pid than its own), or `host.json` names another pid namespace or another machine. For a session with an autogroup record and a `host.json`, such a CLI counts the group as running and sends it no signal. On the host's machine, a plain `destroy` of a live session still ends it through its host. From another machine the host's socket does not answer, so a plain `destroy` fails with `HOST_UNREACHABLE`: run it on the machine that started the session. A `destroy` of a session whose program exited fails with `HOST_TIMEOUT` and keeps the session `exited`, also when no process of the group is left. This trade-off keeps `destroy` from recording `destroyed` while a process that the program left runs where the CLI cannot see it. Run such a `destroy` from a process in the host's pid namespace that can read `/proc`. Such a CLI's `gc` keeps the folder of every session with an autogroup record that is not `destroyed`, because it cannot tell whether the group ended. +On Linux, a CLI that cannot prove that it shares the host's pid space cannot prove that the program's group ended either: it cannot read `/proc/self/ns/pid` (no `/proc`, or an empty one), its `/proc` belongs to another pid namespace (`/proc/self` names another pid than its own), or `host.json` names another pid namespace or another machine. For a session with an autogroup record and a `host.json`, such a CLI counts the group as running and sends it no signal. On the host's machine, a plain `destroy` of a live session still ends it through its host. From another machine the host's socket does not answer, so a plain `destroy` fails with `HOST_UNREACHABLE`: run it on the machine that started the session. A `destroy` of a session whose program exited fails with `HOST_TIMEOUT` and keeps the session `exited`, also when no process of the group is left. This trade-off keeps `destroy` from recording `destroyed` while a process that the program left runs where the CLI cannot see it. Run such a `destroy` from a process in the host's pid namespace that can read `/proc`. `gc` still removes the folder of an `exited` session, as it does on every system. If the proven group, or a group that agent-tty cannot check, does not end within the destroy wait (about 5 s), `destroy` fails with `HOST_TIMEOUT` and does not record the session as `destroyed`. `destroy --force` and reconcile also check the host's pid from `session.json` before they trust it. @@ -368,9 +368,9 @@ 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. 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` while the autogroup record in `program.json` proves that a process of the program's group runs, or while the group id still names a process that no scan of `/proc` shows, such as a fast fork chain. It also keeps it while it cannot check the group, for example when `/proc` refuses the autogroup of a live member, because such a group counts as running. It reports "the session's program group still runs (destroy ends it)". Without an autogroup record (see item 2), `gc` cannot prove the group, so it removes `program.json` with the folder, and a process that the program left can 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. 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` keeps the session folder until the group has ended or agent-tty can check it again. + - 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`. 7. Off Linux, reconcile counts the host as alive while any process has its pid. A crashed host that stays a zombie, or a process that got its pid, keeps the session `running`, and `destroy --force` kills nothing and fails with `HOST_TIMEOUT`. On Linux, the same happens when `/proc` is not mounted or refuses to show the host, and for a session that an agent-tty version without `host.json` started. On Windows, `destroy --force` never kills the host: it kills the program, and a host that hangs makes it fail with `HOST_TIMEOUT`. End such a host yourself with the Host PID that `inspect` shows (`taskkill /pid /f`), then run `destroy --force` again. When agent-tty cannot judge the host (another pid namespace or machine, a `/proc` of another pid namespace, or a refused read of `/proc/self/ns/pid`), `destroy --force` cannot see the host end either. It can fail with `HOST_TIMEOUT` although the host has recorded the session as `exited`, and a second `destroy --force` then records it as `destroyed`. When `/proc` is mounted but refuses to show the host and the program's processes (a security module that hides processes of the same user), `destroy --force` kills nothing and fails with `HOST_TIMEOUT` also for a healthy host. 8. A Home that several machines share, for example over NFS, works only from the machine that started each session. From another machine, agent-tty counts the host as running and kills nothing, because the machine id differs. Machines without a machine id (an empty, missing or `uninitialized` `/etc/machine-id`, as in many container images), or with the same one (a cloned image), cannot tell each other apart. agent-tty takes a machine id only when it is 32 lowercase hex characters, so it also reads any other value, such as a UUID with dashes or uppercase hex, as no id. There the boot id differs, so the other machine counts a live host as ended, records the session as `failed`, and `gc` can then remove its folder. Remote sessions are out of scope (see `RELEASE.md`). diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index e23c5194..a46b5952 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -595,22 +595,29 @@ export function isProgramGroupAlive(group: ProgramGroup | null): boolean { ); } -// Whether gc must keep the session. gc sends no SIGSTOP, so a fork chain -// that no scan shows reads gone: a group id that the probe finds while no -// scan shows a member of the group, not even a zombie, also counts. +// Whether gc must keep the session. gc keeps it only while it proves that +// the group runs, so that destroy can end it: a live member carries the +// token. gc sends no SIGSTOP, so a fork chain that no scan shows reads gone: +// a group id that the probe finds while no scan shows a member of the +// group, not even a zombie, also counts. A group that gc cannot check, in +// another pid space or behind a refused read of /proc, proves nothing, and +// gc removes the session as it does one without a token. Else such a +// session would stay forever, for example after a container restart that +// keeps the home, when host.json names a pid namespace that no longer +// exists. export async function provenProgramGroupRuns( sessionDirectory: string, ): Promise { const group = await readProvenProgramGroup(sessionDirectory); - if (isProgramGroupAlive(group)) { - return true; + if (group === null || 'unshared' in group) { + return false; } + const { verdict } = judgeLiveGroup(group); return ( - group !== null && - !('unshared' in group) && - judgeLiveGroup(group).verdict === 'gone' && - probeFindsGroup(group.pid) && - groupHasLiveProcess(group.pid) === null + verdict === 'owned' || + (verdict === 'gone' && + probeFindsGroup(group.pid) && + groupHasLiveProcess(group.pid) === null) ); } diff --git a/test/integration/lifecycle.test.ts b/test/integration/lifecycle.test.ts index 09fb1f72..da524bc0 100644 --- a/test/integration/lifecycle.test.ts +++ b/test/integration/lifecycle.test.ts @@ -949,6 +949,24 @@ describe('lifecycle integration', { timeout: 60_000 }, () => { return sessionId; } + // The host captures the session token only while the program runs, so a + // program that would exit at once first waits until program.json is in + // place. A capture that still found no token leaves gc nothing to prove, + // so a test of gc's group check skips then. + function untilRecorded(): string { + return `until [ -f "${testHome}/sessions/$AGENT_TTY_SESSION_ID/program.json" ]; do sleep 0.01; done`; + } + + async function recordsToken(sessionId: string): Promise { + const record = JSON.parse( + await readFile( + join(testHome, 'sessions', sessionId, 'program.json'), + 'utf8', + ), + ) as { bootId: unknown }; + return record.bootId !== null; + } + it('destroy ends it within the destroy wait', async () => { const sessionId = await createProgram( 'trap "" TERM HUP; touch "$0"; exec sleep 300', @@ -1016,15 +1034,18 @@ describe('lifecycle integration', { timeout: 60_000 }, () => { // gc would delete program.json, the only record that proves the group. it.runIf(capturesToken)( 'gc keeps an exited session while a process that the program left runs', - async () => { + async ({ skip }) => { const sessionId = await createProgram( - 'trap "" HUP; sleep 300 & touch "$0"; exit 0', + `trap "" HUP; sleep 300 & ${untilRecorded()}; touch "$0"; exit 0`, ); const deadline = Date.now() + 10_000; while (inspectSession(testHome, sessionId).status !== 'exited') { expect(Date.now()).toBeLessThan(deadline); await sleep(100); } + if (!(await recordsToken(sessionId))) { + skip('the host captured no session token'); + } const kept = runCli(['gc', '--json'], { AGENT_TTY_HOME: testHome }); expect(kept.status).toBe(0); @@ -1060,6 +1081,40 @@ describe('lifecycle integration', { timeout: 60_000 }, () => { }, ); + // After a container restart that keeps the home, host.json names a pid + // namespace that no longer exists. gc cannot check the group there, and + // no destroy can prove it gone, so gc removes the session. + it.runIf(capturesToken)( + 'gc removes an exited session whose host.json names another pid namespace', + async ({ skip }) => { + const sessionId = await createProgram( + `trap "" HUP; sleep 300 & ${untilRecorded()}; touch "$0"; exit 0`, + ); + const deadline = Date.now() + 10_000; + while (inspectSession(testHome, sessionId).status !== 'exited') { + expect(Date.now()).toBeLessThan(deadline); + await sleep(100); + } + if (!(await recordsToken(sessionId))) { + skip('the host captured no session token'); + } + const hostFile = join(testHome, 'sessions', sessionId, 'host.json'); + const host = JSON.parse(await readFile(hostFile, 'utf8')) as object; + await writeFile( + hostFile, + JSON.stringify({ ...host, pidNamespace: 'pid:[1]' }), + ); + + const removed = runCli(['gc', '--json'], { AGENT_TTY_HOME: testHome }); + expect(removed.status).toBe(0); + expect(JSON.parse(removed.stdout)).toMatchObject({ + ok: true, + result: { removedSessionCount: 1 }, + }); + expect(isGroupAlive(pgid)).toBe(true); + }, + ); + // 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)( @@ -1191,12 +1246,12 @@ describe('lifecycle integration', { timeout: 60_000 }, () => { // gc sends no SIGSTOP, so only the probe of the group id finds the chain. it.runIf(capturesToken)( 'gc keeps an exited session while a fork chain that the program left runs', - async () => { + async ({ skip }) => { const beat = join(testHome, 'beat'); const sessionId = createSession(testHome, [ '/bin/sh', '-c', - `trap "" HUP; python3 '${forkChain}' 60 0.002 '${beat}' & exit 0`, + `trap "" HUP; python3 '${forkChain}' 60 0.002 '${beat}' & ${untilRecorded()}; exit 0`, ]); pgid = inspectSession(testHome, sessionId).childPid as number; const deadline = Date.now() + 10_000; @@ -1207,6 +1262,9 @@ describe('lifecycle integration', { timeout: 60_000 }, () => { expect(Date.now()).toBeLessThan(deadline); await sleep(100); } + if (!(await recordsToken(sessionId))) { + skip('the host captured no session token'); + } expect(await chainRuns(beat)).toBe(true); const kept = runCli(['gc', '--json'], { AGENT_TTY_HOME: testHome }); diff --git a/test/unit/commands/gc.test.ts b/test/unit/commands/gc.test.ts index 729d043b..754941d1 100644 --- a/test/unit/commands/gc.test.ts +++ b/test/unit/commands/gc.test.ts @@ -408,6 +408,49 @@ describe('gc command helpers', () => { expect(socketCleanups).toEqual([`${home}/sessions/destroyed-01 destroyed`]); }); + it('keeps a session whose program group check throws, and reports why', async () => { + const home = '/tmp/agent-tty'; + const exitedManifest = createSessionRecord({ + sessionId: 'unchecked-01', + status: 'exited', + createdAt: '2026-03-20T08:00:00.000Z', + }); + const { dependencies, removedPaths, socketCleanups } = + createMockDependencies(home, { + 'unchecked-01': { manifest: exitedManifest }, + 'exited-01': { + manifest: { ...exitedManifest, sessionId: 'exited-01' }, + }, + }); + const checked: string[] = []; + dependencies.provenProgramGroupRuns = (sessionDirectory: string) => { + checked.push(sessionDirectory); + return sessionDirectory.endsWith('/unchecked-01') + ? Promise.reject(new Error('EIO: i/o error, scandir /proc')) + : Promise.resolve(false); + }; + + for (const dryRun of [true, false]) { + const result = await gcSessions( + home, + { dryRun, staleOnly: false, olderThanMs: null }, + dependencies, + ); + + expect(result.skippedSessions).toEqual([ + { + sessionId: 'unchecked-01', + reason: + "failed to check the session's program group: EIO: i/o error, scandir /proc", + }, + ]); + expect(result.removedSessions).toEqual(['exited-01']); + } + expect(checked).toContain(`${home}/sessions/unchecked-01`); + expect(removedPaths).toEqual([`${home}/sessions/exited-01`]); + expect(socketCleanups).toEqual([`${home}/sessions/exited-01 exited`]); + }); + 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 a2e13360..f801dec9 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -939,6 +939,49 @@ describe('a program group with a token, as a faked /proc shows it', () => { } }, ); + + // gc keeps only a group that it proves, so that destroy can end it. A + // group that it cannot check would keep the session forever, as after a + // container restart that keeps the home: host.json then names a pid + // namespace that no longer exists. + it.each([ + { + when: 'host.json names another pid namespace', + setUp: (directory: string) => { + const host = captureHost(process.pid) as HostRecord; + writeHostRecord(directory, { ...host, pidNamespace: 'pid:[1]' }); + procShowsTokenGroup('S'); + probeEnds('ok'); + }, + }, + { + when: 'a live member of the session shows no autogroup', + setUp: () => { + procShowsTokenGroup('S'); + const read = autogroupFile.read; + autogroupFile.read = (file) => + /^\/proc\/\d+\/autogroup$/.test(file) ? '' : (read?.(file) ?? null); + probeEnds('ok'); + }, + }, + { + when: '/proc hides the processes of other users and the probe finds the id', + setUp: () => { + procHooks.mountinfo = procMount('rw,hidepid=2'); + procShowsTokenGroup(); + probeEnds('EPERM'); + }, + }, + ])('when $when, reads the group not proven', async ({ setUp }) => { + const directory = await recordedSession(); + try { + setUp(directory); + + expect(await provenProgramGroupRuns(directory)).toBe(false); + } finally { + await rm(directory, { recursive: true, force: true }); + } + }); }); it.each(['EPERM', 'EACCES'])( From cf58b7320b18b317c10a71e19da40495fe67e1b9 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 05:12:36 +0000 Subject: [PATCH 13/17] ci: check the lifecycle coverage record in the first share only --- .github/workflows/ci.yml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 159768c9..2852aa39 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -220,10 +220,11 @@ jobs: npx vitest run --maxWorkers=1 --retry=2 test/integration/lifecycle.test.ts test/integration/gc.test.ts test/integration/other-user-group.test.ts # Model-checks the session lifecycle with the verify-session-lifecycle - # skill. Every run checks that coverage.json matches the covered code. The - # TLC runs took 63 min in one job of 4 vCPUs and take 10 to 17 min in each - # of 4 shares. They run only when coverage.json differs from the base, - # which every change to the model, its scripts or the covered code needs. + # skill. Share 1 checks that coverage.json matches the facts and the + # covered code. The TLC runs took 63 min in one job of 4 vCPUs and take 13 + # to 17 min in each of 4 shares. They run only when coverage.json differs + # from the base, which every change to the model, its scripts, the covered + # code or a fact needs. lifecycle-model: runs-on: ubuntu-latest timeout-minutes: 50 @@ -248,6 +249,7 @@ jobs: run: mise run bootstrap-ci - name: Check that coverage.json matches the covered code + if: matrix.shard == 1 run: .agents/skills/verify-session-lifecycle/scripts/check.sh --drift-only - name: Decide whether the model checker must run From dcbf0c8e91665df0be08dbd9055b0524353a6b9e Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 06:17:53 +0000 Subject: [PATCH 14/17] fix(model): state the unshared gc witness without the removed record GcRemoves clears rec in the same step, so the witness asks for the state that R20 leaves out instead: a gc in another pid space removed the session while a process that the program left runs. --- .agents/skills/verify-session-lifecycle/SKILL.md | 4 ++-- .../verify-session-lifecycle/model/SessionLifecycle.tla | 5 +++-- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index a0d0f240..d1fdb62e 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. Eleven 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=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). What it does: @@ -538,7 +538,7 @@ To bring the check back in line after changes that skipped it, use `/maintain-fo ## Scope -The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 27,013,946 distinct states, and without one 26,822,518. The check prints both counts. +The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 29,309,460 distinct states, and without one 29,186,546. The check prints both counts. It assumes: diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index 876d6e8a..7a96a5ff 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -1638,7 +1638,8 @@ WitnessWaitPassesReusedId == ~passedReused WitnessUnsharedDestroyCompletes == ~(OtherPidSpace /\ ~dforce /\ wasNamed /\ dres = "ok") \* With OtherPidSpace gc removes an exited session while a process that -\* the program left runs, because it cannot check the group there. +\* the program left runs, because it cannot check the group there: the +\* state that R20 leaves out. WitnessUnsharedGcRemovesLeftover == - ~(OtherPidSpace /\ rec /\ left /\ gres = "removed") + ~(OtherPidSpace /\ gres = "removed" /\ ~diedUnrecorded /\ left) ============================================================================= From 983fb02d7bfc495f76727f24406ab5542dd92c24 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 07:13:53 +0000 Subject: [PATCH 15/17] fix(gc): judge a fork chain again while a judgement is inconclusive CI at dcbf0c8e: gc removed a session whose fork chain ran. A member can end between its stat and its autogroup read (unknown), or show up only after the judge's scans, and both now read false. judgeGroupForGc reads them as inconclusive, and provenProgramGroupRuns judges again, at most ten times. A judgement that stays inconclusive, as behind a refused read of /proc, still proves nothing, so gc removes that session. --- .../skills/verify-session-lifecycle/SKILL.md | 4 +- .../scripts/facts.mjs | 43 +++++++++++++----- src/host/programGroup.ts | 45 ++++++++++++++----- test/integration/lifecycle.test.ts | 5 ++- test/unit/host/programGroup.test.ts | 26 +++++++++++ 5 files changed, 96 insertions(+), 27 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index d1fdb62e..19aeae22 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`, `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`, `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/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`. @@ -473,7 +473,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. 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 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. ```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/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index e7064157..eefe4236 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -1391,25 +1391,40 @@ function gcFacts() { ts.isShorthandPropertyAssignment(p) && p.name.text === 'provenProgramGroupRuns', ); - const runs = requireDeclaration( - 'src/host/programGroup.ts', - 'provenProgramGroupRuns', - ).body.statements.map((s) => normalize(s.getText())); - const owned = "verdict === 'owned'"; - // Or a group that reads gone, whose id the probe finds while no scan - // shows a member, live or zombie. - const withProbe = `return ( ${owned} || (verdict === 'gone' && probeFindsGroup(group.pid) && groupHasLiveProcess(group.pid) === null) );`; + const body = (name) => + requireDeclaration('src/host/programGroup.ts', name).body.statements.map( + (s) => normalize(s.getText()), + ); + const runs = body('provenProgramGroupRuns'); + const judge = body('judgeGroupForGc'); + // provenProgramGroupRuns gives false for a group that gc cannot check in + // another pid space, and judges the group again while judgeGroupForGc + // reads it inconclusive. That counts only a live member that carries the + // token, and treats unknown as inconclusive. const judges = runs.length === 4 && runs[0] === 'const group = await readProvenProgramGroup(sessionDirectory);' && runs[1] === "if (group === null || 'unshared' in group) { return false; }" && - runs[2] === 'const { verdict } = judgeLiveGroup(group);' && - (runs[3] === `return ${owned};` || runs[3] === withProbe); + runs[2] === + 'for (let judged = 0; judged < GC_JUDGEMENTS; judged += 1) { const runs = judgeGroupForGc(group); if (runs !== null) { return runs; } }' && + runs[3] === 'return false;' && + judge[0] === 'const { verdict } = judgeLiveGroup(group);' && + judge[1] === + "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 = [ + 'if (!probeFindsGroup(group.pid)) { return false; }', + 'const live = groupHasLiveProcess(group.pid);', + 'return live === null ? true : live ? null : false;', + ]; + const tail = judge.slice(2); const probes = judges && - runs[3] === withProbe && + tail.join('\n') === probeTail.join('\n') && normalize( requireDeclaration( 'src/host/programGroup.ts', @@ -1417,6 +1432,8 @@ function gcFacts() { ).body.getText(), ) === "{ try { process.kill(processGroupTarget(pgid), 0); return true; } catch (error) { if (hasErrorCode(error, 'ESRCH')) { return false; } if (hasErrorCode(error, 'EPERM')) { return true; } throw error; } }"; + const judgesGone = + probes || (tail.length === 1 && tail[0] === 'return false;'); return { GcSkipsNonCollectable: reconcile >= 0 && collectable > reconcile, GcFinalCheck: finalCheck, @@ -1425,7 +1442,8 @@ function gcFacts() { groupSkip === groupRead + 1 && loop.statements.indexOf(removal) > groupSkip && wired && - judges, + judges && + judgesGone, GcProbesUnseenGroup: probes, }; } @@ -1469,6 +1487,7 @@ const COVERED = [ ['src/cli/commands/gc.ts', 'gcSessions'], ['src/cli/commands/gc.ts', 'defaultDependencies'], ['src/host/programGroup.ts', 'provenProgramGroupRuns'], + ['src/host/programGroup.ts', 'judgeGroupForGc'], ['src/host/programGroup.ts', 'probeFindsGroup'], ['src/host/lifecycle.ts', 'allocateSession'], ['src/host/lifecycle.ts', 'launchHost'], diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index a46b5952..798127ae 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -595,13 +595,14 @@ export function isProgramGroupAlive(group: ProgramGroup | null): boolean { ); } +// gc judges the group again at most this many times while a judgement +// stays inconclusive. +const GC_JUDGEMENTS = 10; + // Whether gc must keep the session. gc keeps it only while it proves that -// the group runs, so that destroy can end it: a live member carries the -// token. gc sends no SIGSTOP, so a fork chain that no scan shows reads gone: -// a group id that the probe finds while no scan shows a member of the -// group, not even a zombie, also counts. A group that gc cannot check, in -// another pid space or behind a refused read of /proc, proves nothing, and -// gc removes the session as it does one without a token. Else such a +// the group runs, so that destroy can end it. A group that gc cannot check, +// in another pid space or behind a refused read of /proc, proves nothing, +// and gc removes the session as it does one without a token. Else such a // session would stay forever, for example after a container restart that // keeps the home, when host.json names a pid namespace that no longer // exists. @@ -612,13 +613,33 @@ export async function provenProgramGroupRuns( if (group === null || 'unshared' in group) { return false; } + for (let judged = 0; judged < GC_JUDGEMENTS; judged += 1) { + const runs = judgeGroupForGc(group); + if (runs !== null) { + return runs; + } + } + return false; +} + +// true: a live member carries the token. false: the group ended, or the +// live members are not the program's. null: inconclusive. 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. A refused read of /proc stays +// inconclusive. +function judgeGroupForGc(group: ProvenRecord): boolean | null { const { verdict } = judgeLiveGroup(group); - return ( - verdict === 'owned' || - (verdict === 'gone' && - probeFindsGroup(group.pid) && - groupHasLiveProcess(group.pid) === null) - ); + if (verdict !== 'gone') { + return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; + } + // gc sends no SIGSTOP, so a fork chain that no scan shows reads gone: a + // group id that the probe finds while no scan shows a member of the + // group, not even a zombie, counts. + if (!probeFindsGroup(group.pid)) { + return false; + } + const live = groupHasLiveProcess(group.pid); + return live === null ? true : live ? null : false; } function probeFindsGroup(pgid: number): boolean { diff --git a/test/integration/lifecycle.test.ts b/test/integration/lifecycle.test.ts index da524bc0..06046646 100644 --- a/test/integration/lifecycle.test.ts +++ b/test/integration/lifecycle.test.ts @@ -1277,7 +1277,10 @@ describe('lifecycle integration', { timeout: 60_000 }, () => { const destroyed = runCli(['destroy', sessionId, '--json'], { AGENT_TTY_HOME: testHome, }); - expect(JSON.parse(destroyed.stdout)).toMatchObject({ ok: true }); + // The error, when there is one, names why the chain outlived destroy. + expect( + (JSON.parse(destroyed.stdout) as { error?: unknown }).error, + ).toBeUndefined(); expect(await chainRuns(beat)).toBe(false); }, ); diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index f801dec9..6d6f4460 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -982,6 +982,32 @@ describe('a program group with a token, as a faked /proc shows it', () => { 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 () => { + const directory = await recordedSession(); + try { + procShowsTokenGroup('S'); + const read = autogroupFile.read; + let autogroupReads = 0; + autogroupFile.read = (file) => { + if (/^\/proc\/\d+\/autogroup$/.test(file)) { + autogroupReads += 1; + if (autogroupReads === 1) { + return ''; + } + } + return read?.(file) ?? null; + }; + probeEnds('ok'); + + expect(await provenProgramGroupRuns(directory)).toBe(true); + expect(autogroupReads).toBe(2); + } finally { + await rm(directory, { recursive: true, force: true }); + } + }); }); it.each(['EPERM', 'EACCES'])( From a31fe8973c114a8eada78652ff1ccad7d8bbdcdc Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 07:13:53 +0000 Subject: [PATCH 16/17] chore: sync the lifecycle coverage record after the gc fix check.sh --update-coverage at dcbf0c8e gave 78/78 runs as expected in 3,304 s. The model and check.sh are unchanged since, and facts.mjs reads the same values, so this record comes from facts.mjs at this commit. current has 29,309,460 distinct states and current-no-token 29,186,546. --- .../verify-session-lifecycle/coverage.json | 51 +++++++++++++++++-- 1 file changed, 47 insertions(+), 4 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 9275b847..3e9ca452 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -1,10 +1,53 @@ { + "constants": { + "ReconcileSkipsTerminal": true, + "ReconcileSkipsLiveHost": true, + "ReconcileRereads": true, + "GcSkipsNonCollectable": true, + "GcFinalCheck": true, + "GcKeepsLiveGroup": true, + "GcProbesUnseenGroup": true, + "CreateRecordsHostPid": true, + "CreateRecordsHost": true, + "CreateStopsOnGiveUp": true, + "HostChecksCreateFailed": true, + "HostWaitsForManifest": true, + "HostSerializesWrites": true, + "HostStopsAfterTerminalWrite": true, + "ShutdownChecksCommandable": true, + "DestroyRecordsDestroyed": true, + "DestroyKeepsExitCode": true, + "DestroyStopsLeftovers": true, + "ProvesHostPid": true, + "ReconcileRepairsDestroyed": true, + "ReconcileRepairsMarked": true, + "ManifestWriteNeedsFolder": true, + "KillsProgramGroup": true, + "ProbeCountsDeniedGroup": true, + "HostWaitsForGroup": true, + "ReconcileWaitsForGroup": true, + "RecordsProgramSync": true, + "ProvesGroupOwnership": true, + "FreezesUnseenGroup": true, + "FallbackNeedsFolder": true, + "UnsharedGroupReadsUnknown": true, + "TokenNamesProgram": true, + "ReusedIdReadsGone": true, + "ReRunsInNewSession": true, + "InsideCheckReadsEnv": true, + "Collectable": ["destroyed", "exited", "failed"], + "Terminal": ["destroyed", "exited", "failed"] + }, "fingerprints": { "src/cli/commands/create.ts#runCreateCommand": "131d2707818ea283", "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": "667e4ebc3ca3029c", + "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#probeFindsGroup": "31ea7b5e835c0509", "src/host/lifecycle.ts#allocateSession": "43819af8c6c271ec", "src/host/lifecycle.ts#launchHost": "597a5a6b9eb58cc8", "src/host/lifecycle.ts#isProcessAlive": "1ca1fe6ad6c41711", @@ -93,9 +136,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": "320f9c8a26340aeb", - "skill:scripts/facts.mjs": "0f4e240431fb0fcd", - "skill:scripts/check.sh": "606573a67217656e" + "skill:model/SessionLifecycle.tla": "19775a9a74c5ca9a", + "skill:scripts/facts.mjs": "d0d36f49e4ad735e", + "skill:scripts/check.sh": "0e69ddb1068b5df4" }, "callSites": { "writeManifest": [ From f263f56d6ece25cfab23a5e4fd434ab5d8616148 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 07:37:48 +0000 Subject: [PATCH 17/17] chore(lifecycle): record the gc judgement limit Codex on #302: GC_JUDGEMENTS = 0 would skip every judgement, so gc would keep no session, and no fact or hash changed. facts.mjs now reads GcKeepsLiveGroup FALSE unless the limit is a positive integer literal, and coverage.json hashes the declaration. The model, check.sh and every fact value are unchanged since the 78/78 check at dcbf0c8e. --- .agents/skills/verify-session-lifecycle/SKILL.md | 2 +- .../skills/verify-session-lifecycle/coverage.json | 3 ++- .../verify-session-lifecycle/scripts/facts.mjs | 12 ++++++++++++ 3 files changed, 15 insertions(+), 2 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 19aeae22..8ea09871 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`, `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`, `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`. diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 3e9ca452..cfb65dd6 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -47,6 +47,7 @@ "src/cli/commands/gc.ts#defaultDependencies": "81a9894438cb5be7", "src/host/programGroup.ts#provenProgramGroupRuns": "7b50817618b4b769", "src/host/programGroup.ts#judgeGroupForGc": "e0cd1b46a60eb1fe", + "src/host/programGroup.ts#GC_JUDGEMENTS": "180a0af01a4b81c7", "src/host/programGroup.ts#probeFindsGroup": "31ea7b5e835c0509", "src/host/lifecycle.ts#allocateSession": "43819af8c6c271ec", "src/host/lifecycle.ts#launchHost": "597a5a6b9eb58cc8", @@ -137,7 +138,7 @@ "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": "d0d36f49e4ad735e", + "skill:scripts/facts.mjs": "4aff1bce5c8ba086", "skill:scripts/check.sh": "0e69ddb1068b5df4" }, "callSites": { diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index eefe4236..6ff06fa3 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -1401,7 +1401,18 @@ function gcFacts() { // another pid space, and judges the group again while judgeGroupForGc // reads it inconclusive. That counts only a live member that carries the // token, and treats unknown as inconclusive. + // The loop runs at least once only with a positive GC_JUDGEMENTS. + const limit = requireDeclaration( + 'src/host/programGroup.ts', + 'GC_JUDGEMENTS', + ).initializer; + const judgesAtAll = + limit !== undefined && + ts.isNumericLiteral(limit) && + Number.isInteger(Number(limit.text)) && + Number(limit.text) >= 1; const judges = + judgesAtAll && runs.length === 4 && runs[0] === 'const group = await readProvenProgramGroup(sessionDirectory);' && @@ -1488,6 +1499,7 @@ const COVERED = [ ['src/cli/commands/gc.ts', 'defaultDependencies'], ['src/host/programGroup.ts', 'provenProgramGroupRuns'], ['src/host/programGroup.ts', 'judgeGroupForGc'], + ['src/host/programGroup.ts', 'GC_JUDGEMENTS'], ['src/host/programGroup.ts', 'probeFindsGroup'], ['src/host/lifecycle.ts', 'allocateSession'], ['src/host/lifecycle.ts', 'launchHost'],