diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 01a783c3..8ea09871 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, or while the host has yet to check for the create-failed marker. | `create` fails with `HOST_UNREACHABLE`, but the session runs, and `list --all` shows it running. | | R18 `DestroyedStaysDestroyed` | Once `destroy` reported success, the manifest says destroyed while the session folder exists, except while a reconcile that wrote over it has yet to write destroyed again. | `destroy` reports `destroyed: true`, and the session then reads `failed`. | | R19 `NoUnrelatedHostKilled` | No kill of `destroy --force` reaches a process that took the host's pid after the host ended. | `destroy --force` sends SIGKILL to an unrelated process that got the crashed host's pid. | +| R20 `RemovedSessionStopped` | gc in the host's pid space removes a session folder, and with it `program.json`, only once no process of the program's group runs, also none that the program left when it exited on its own. | A process of the session keeps running, and nothing can prove or stop it later. | `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`), `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`, `src/cli/commands/create.ts` `runCreateCommand` with `waitForReadyHost`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`. +- `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`. - `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` and `writeCreateFailedMarker` with `writeEmptyMarker`. @@ -54,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. 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 From the repo root: @@ -62,14 +65,14 @@ 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. Ten runs explore more than 20 million distinct states each, so `CHECK_JOBS=75` 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: -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. +1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the thirty-five guards that the rules depend on and the status sets of the policy table, and it hashes each covered function with comments and layout removed. 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 75 times and prints one line per run. -4. It compares the hashes and call sites with `coverage.json`. +3. It runs TLC 78 times and prints one line per run. +4. It compares the guard values, the status sets, the hashes and the call sites with `coverage.json`. Exit codes: 0 means every run gave the expected result and the covered code matches the sync record. 1 means at least one run gave an unexpected result; the line says `UNEXPECTED`. 3 means every result was as expected, but covered code changed since the sync commit; that is not a pass, so follow "When you change covered code on purpose". 2 means a tool could not run. When both 1 and 3 apply, the exit code is 1. @@ -77,27 +80,28 @@ 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, a reconcile's first read writes destroyed over a marked terminal manifest, `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-ReconcileRepairsMarked` | pass | Without the guard, a reconcile skips a marked `failed` as it skips any terminal manifest. The reconcile that wrote that `failed` always repairs it in the model, because the model has no crash of a reconciling process, so no rule breaks. The unit tests in `test/unit/host/lifecycle.test.ts` cover the crash. | -| `mutant-ReconcileSkipsTerminal` | pass | The re-read in `reconcileSession` also returns on a terminal manifest, so the first terminal return alone is redundant. | -| `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`, `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. | -| `mutant-HostChecksCreateFailed-win32` | violated | R17: without the marker, a host that the manifest does not name yet keeps serving after `create` gave up. | +| 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, a reconcile's first read writes destroyed over a marked terminal manifest, `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`, `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-ReconcileRepairsMarked` | pass | Without the guard, a reconcile skips a marked `failed` as it skips any terminal manifest. The reconcile that wrote that `failed` always repairs it in the model, because the model has no crash of a reconciling process, so no rule breaks. The unit tests in `test/unit/host/lifecycle.test.ts` cover the crash. | +| `mutant-ReconcileSkipsTerminal` | pass | The re-read in `reconcileSession` also returns on a terminal manifest, so the first terminal return alone is redundant. | +| `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. | +| `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. | +| `mutant-HostChecksCreateFailed-win32` | violated | R17: without the marker, a host that the manifest does not name yet keeps serving after `create` gave up. | 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`. @@ -465,6 +469,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 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))') +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 +``` + ### `CreateRecordsHost`: a CLI in another pid space reads a starting host dead (R2) A CLI in another pid namespace finds no process with the host's pid, so `judgeHost` reads the host dead unless `host.json` names it. The host wrote `host.json` only once it had read its manifest. A `list`, `inspect` or `gc` in another pid namespace that read the session between create's first manifest write and that record recorded a live host `failed`, and `gc` could then remove its folder. @@ -519,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: @@ -554,7 +573,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/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 9275b847..cfb65dd6 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -1,10 +1,54 @@ { + "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#GC_JUDGEMENTS": "180a0af01a4b81c7", + "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 +137,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": "4aff1bce5c8ba086", + "skill:scripts/check.sh": "0e69ddb1068b5df4" }, "callSites": { "writeManifest": [ diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index 76a11572..7a96a5ff 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -44,6 +44,12 @@ 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 + 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 @@ -77,7 +83,8 @@ CONSTANTS \* AGENT_TTY_SESSION_ID before it reads the \* manifest RecordsProgramSync, \* hostMain.ts: program.json is written in the - \* synchronous block that spawns the program + \* synchronous block that spawns the program, + \* with a token only beside host.json ProvesGroupOwnership, \* programGroup.ts: every group kill goes \* through stopProgramGroup, which kills only \* while a live member carries the token @@ -142,7 +149,9 @@ ASSUME Token \in BOOLEAN ASSUME Unseen \in BOOLEAN ASSUME OtherPidSpace \in BOOLEAN ASSUME Win32 \in BOOLEAN -ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, ReconcileSkipsTerminal, +ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, GcKeepsLiveGroup, + GcProbesUnseenGroup, + ReconcileSkipsTerminal, ReconcileSkipsLiveHost, CreateRecordsHostPid, HostWaitsForManifest, ReconcileRereads, HostSerializesWrites, HostStopsAfterTerminalWrite, @@ -571,7 +580,10 @@ StartShutdown(ahead) == \* missing manifest without the wait, or a status other than "running", \* throws, and the host exits. Right after the read, with no await between, \* the host writes host.json with writeHostRecord: its pid, the boot id and -\* its start time from /proc/self/stat. +\* its start time from /proc/self/stat. The model leaves out a capture that +\* fails (a refused read of the stat, the boot id or the pid namespace), +\* after which the host writes no host.json and records no token +\* (RecordsProgramSync). HostReadsManifest == /\ hostAlive /\ hpc = "boot" /\ ~(HostWaitsForManifest /\ mst = "none") @@ -1069,6 +1081,31 @@ 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, but it counts only a group that it proves: a live +\* member carries the token. gc sends no SIGSTOP, so with Unseen no scan +\* shows the program's processes, and with GcProbesUnseenGroup the probe +\* kill(-pgid, 0) then finds them. An unrelated group that took the id is +\* in view and reads unproven. With OtherPidSpace gc cannot check the group +\* and reads it not proven, so that a session whose pid space is gone, as +\* after a container restart, does not stay forever. With GcKeepsLiveGroup +\* gc skips a session that is not destroyed while it proves the group +\* ("the session's program group still runs"). The code tests the status +\* of manifestAfter, which cannot turn from destroyed back, so this current +\* status skips no more often. +GcSeesGroup == + /\ ~OtherPidSpace + /\ \/ GroupSeen("proven") + \/ GcProbesUnseenGroup /\ Unseen /\ (prog \/ left) + +GcChecksGroup == + /\ pc["gc"] = "group" + /\ IF GcKeepsLiveGroup /\ mst # "destroyed" /\ rec /\ GcSeesGroup 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. @@ -1590,4 +1637,9 @@ 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: the +\* state that R20 leaves out. +WitnessUnsharedGcRemovesLeftover == + ~(OtherPidSpace /\ gres = "removed" /\ ~diedUnrecorded /\ left) ============================================================================= diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index 399c57bb..fcb6ab42 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 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. @@ -16,19 +19,25 @@ # # 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 +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) @@ -36,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" @@ -59,22 +69,28 @@ 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" -# `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" @@ -88,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}`); } @@ -114,6 +147,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 +166,7 @@ TERMINAL=$(node -e ' const c = JSON.parse(require("node:fs").readFileSync(process.argv[1], "utf8")).constants; console.log("{" + c.Terminal.map((s) => JSON.stringify(s)).join(", ") + "}"); ' "$OUT/facts.json") -GUARDS="GcSkipsNonCollectable GcFinalCheck ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed ReconcileRepairsMarked CreateStopsOnGiveUp HostChecksCreateFailed TokenNamesProgram ReusedIdReadsGone ProvesHostPid CreateRecordsHost 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 ReconcileRepairsMarked CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid CreateRecordsHost FreezesUnseenGroup UnsharedGroupReadsUnknown HostChecksCreateFailed" # One "Guard=TRUE|FALSE" word per guard, read from the code by facts.mjs. FACTS_LINE=$(node -e ' const c = JSON.parse(require("node:fs").readFileSync(process.argv[1], "utf8")).constants; @@ -133,8 +177,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 WitnessMarkedRepaired WitnessWaitPassesReusedId WitnessReusedHostMeetsKill" @@ -217,6 +262,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 @@ -226,6 +272,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 @@ -233,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 @@ -256,6 +304,26 @@ write_run current-win32 pass "$NO_TOKEN_RULES" "" "the code on Windows: R1 to R1 write_run mutant-HostChecksCreateFailed-win32 violated FailedCreateStopped "HostChecksCreateFailed=FALSE" "without the marker, a host that the manifest does not name yet keeps serving after create gave up" FailedCreateStopped WIN32=FALSE +# 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) @@ -266,11 +334,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 @@ -320,6 +397,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/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 0bd9da5d..6ff06fa3 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -972,11 +972,14 @@ function noAwaitIn(statements) { } // runHost captures the program's token right after setChildPid, only when it -// wrote host.json, and writes -// program.json as the first statement of its last try, before -// `await persistManifest()`, and no statement between createPty and that try -// awaits. So the record is written in the synchronous block that spawns the -// program. +// wrote host.json, and writes program.json as the first statement of its last +// try, before `await persistManifest()`, and no statement between createPty +// and that try awaits. So the record is written in the synchronous block that +// spawns the program. The fact also guards that a token lies only beside +// host.json: a CLI counts the group of a token without host.json as running, +// so a destroy of such a session after its program exited fails with +// HOST_TIMEOUT. The model leaves out a host that cannot write host.json, so no +// run checks that part. function programRecordFacts() { const body = requireDeclaration('src/host/hostMain.ts', 'runHost').body; const spawn = indexOfStatement(body, /= createPty\(/); @@ -1005,8 +1008,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'); @@ -1057,13 +1061,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)'); } }); } @@ -1077,7 +1086,7 @@ function ownershipFacts() { checkedKill && judgesToken && rawKills > 0 && - targets === 3 && + targets === 4 && signalParam === "signal: 'SIGSTOP' | 'SIGCONT'" && !stray, FreezesUnseenGroup: freezeFacts(stop.body), @@ -1350,9 +1359,103 @@ 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 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) && + 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 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. + // 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);' && + runs[1] === + "if (group === null || 'unshared' in group) { return false; }" && + 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 && + tail.join('\n') === probeTail.join('\n') && + normalize( + requireDeclaration( + 'src/host/programGroup.ts', + 'probeFindsGroup', + ).body.getText(), + ) === + "{ try { process.kill(processGroupTarget(pgid), 0); return true; } catch (error) { if (hasErrorCode(error, 'ESRCH')) { return false; } if (hasErrorCode(error, 'EPERM')) { return true; } throw error; } }"; + const judgesGone = + probes || (tail.length === 1 && tail[0] === 'return false;'); return { GcSkipsNonCollectable: reconcile >= 0 && collectable > reconcile, GcFinalCheck: finalCheck, + GcKeepsLiveGroup: + groupRead > collectable && + groupSkip === groupRead + 1 && + loop.statements.indexOf(removal) > groupSkip && + wired && + judges && + judgesGone, + GcProbesUnseenGroup: probes, }; } @@ -1393,6 +1496,11 @@ 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/programGroup.ts', 'judgeGroupForGc'], + ['src/host/programGroup.ts', 'GC_JUDGEMENTS'], + ['src/host/programGroup.ts', 'probeFindsGroup'], ['src/host/lifecycle.ts', 'allocateSession'], ['src/host/lifecycle.ts', 'launchHost'], ['src/host/lifecycle.ts', 'isProcessAlive'], diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0e485800..2852aa39 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -219,6 +219,58 @@ 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. 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 + 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 + 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 + if: matrix.shard == 1 + 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' + CHECK_SHARD: ${{ matrix.shard }}/4 + run: .agents/skills/verify-session-lifecycle/scripts/check.sh + quality-gates: runs-on: ubuntu-latest timeout-minutes: 5 @@ -228,6 +280,7 @@ jobs: - test-integration - test-e2e - proc-isolation + - lifecycle-model if: ${{ always() }} steps: - name: Report Linux quality gate results @@ -237,6 +290,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') }} diff --git a/docs/USAGE.md b/docs/USAGE.md index bee6eb1c..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), 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), 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. @@ -356,7 +356,7 @@ Reconcile counts the host as ended only when no process has its pid, when that p Reconcile then records the session as `failed`. `destroy --force` sends the host SIGKILL only when the boot id and the start time of the process match `host.json`, so it does not signal a process that got the pid before that check. The check and the kill are two system calls. A process that gets the pid between them still gets the signal, which needs the host to end, be reaped and its pid to go to a new process in that gap. When agent-tty cannot read `/proc` or `host.json`, it counts a host whose pid exists as running and does not kill it. With `host.json` but an unreadable `/proc/self/ns/pid`, it counts the host as running even when no process has its pid. -When it runs in another pid namespace than the one that `host.json` names, or on another machine (another machine id), where the recorded pid can name an unrelated process, it counts the host as running and kills nothing, whatever that pid shows. Without a session token, it also kills no process group through the program's recorded pid there. +When it runs in another pid namespace than the one that `host.json` names, or on another machine (another machine id), where the recorded pid can name an unrelated process, it counts the host as running and kills nothing, whatever that pid shows. A CLI whose `/proc` belongs to another pid namespace (`/proc/self` names another pid than its own) counts the host as running in the same way, so its `destroy --force` can fail with `HOST_TIMEOUT` (item 7 under Limits). Without a session token, it also kills no process group through the program's recorded pid there. In another time namespace than the host's, `/proc` shows start times with another boottime offset. There agent-tty counts the host as ended only when no process has its pid or that process is a zombie, and it does not kill the host. Without `host.json`, as for a session that an agent-tty version without it started, agent-tty cannot tell that it runs in another pid namespace. There a pid that no process has, or a zombie, reads as an ended host, and a kill without a session token goes to the group that the program's recorded pid names there. A session with an autogroup record but no `host.json`, which only unreleased development builds wrote, counts as out of the CLI's pid space: its group counts as running and gets no signal. A `hostPid` in `session.json` that differs from the pid in `host.json` never matches, so the session stays `running` and `destroy --force` kills nothing until `session.json` names the host again. That does not happen in normal use, because the host checks that `session.json` names its own pid. @@ -368,11 +368,11 @@ 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` 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` 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` 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, 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. +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`). 9. A host that has ended reads as running forever when the machine id in its `host.json` differs from this machine's, for example after `/etc/machine-id` changed or in a cloned image that got a new one. `list` keeps the session `running`, `destroy --force` fails with `HOST_TIMEOUT`, and `gc` keeps the folder. First check, on the machine that started the session, that the host is gone: `ps -p ` with the Host PID that `inspect` shows prints no `_host` process for that session. `ps` sees only the processes of its own machine, and when you delete `host.json` while the session still runs on another machine, `gc` can remove its folder. Then delete `host.json` from the session folder (`/sessions//host.json`). The next `list` records the session as `failed`, and `gc` can remove it. If another process now has that pid, the session stays `running`, and you can remove the session folder yourself. 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 6f0681f5..798127ae 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -595,6 +595,68 @@ 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 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 (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); + 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 { + 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 { if (group === null) { return; diff --git a/test/integration/lifecycle.test.ts b/test/integration/lifecycle.test.ts index 9395091a..06046646 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', @@ -1013,6 +1031,90 @@ 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 ({ 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 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 }, + }); + }, + ); + + // 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)( @@ -1141,6 +1243,48 @@ 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 ({ skip }) => { + const beat = join(testHome, 'beat'); + const sessionId = createSession(testHome, [ + '/bin/sh', + '-c', + `trap "" HUP; python3 '${forkChain}' 60 0.002 '${beat}' & ${untilRecorded()}; 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); + } + 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 }); + 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, + }); + // 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); + }, + ); + 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/commands/gc.test.ts b/test/unit/commands/gc.test.ts index c2f2aa92..754941d1 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,88 @@ 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('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 b976eeca..6d6f4460 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'; @@ -881,6 +886,130 @@ 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. 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); + 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 }); + } + }, + ); + + // 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 }); + } + }); + + // 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'])( 'is alive and gets the kill when a live member carries the token and another process refuses its read with %s', (readError) => {