diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index fc3d465d..c3a678ad 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -13,27 +13,27 @@ The tool is TLC, the TLA+ model checker, pinned to release 1.7.4 by sha256. The ## The rules -| Rule | What must hold | Harm when it breaks | -| ------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | -| R1 `NoLiveSessionDeleted` | gc never removes the folder of a session whose host can still write to it. | A running or starting session loses its manifest and event log. | -| R2 `HostDeathOnlyWhenDead` | The manifest says "failed, host died" only when the host process is dead. | `list` and `inspect` show a live session as failed. Commands refuse it. | -| R3 `TerminalIsFinal` | Once the manifest shows exited, failed or destroyed, it never shows running again. | A finished session looks running, and the next reconcile marks it failed. | -| R4 `RecordedExitKept` | Once the manifest records that the program exited, only `destroy` changes it, to destroyed, and keeps the exit code. | A program that exited 0 is reported as failed, with its exit code lost. | -| R5 `RunningSessionReachable` | While the host serves a running program, the socket file exists. | The session runs, but no command can reach it. | -| R6 `HostStartsWhenCreated` | A host never fails to start because another process removed or rewrote its files. | `create` fails with `HOST_UNREACHABLE` for a session nobody touched. | -| R7 `TerminalIsLastWrite` | Once the manifest shows exited, failed or destroyed, the host has no write left to make. | gc removes the folder while the host still writes to it, and the host's write then fails. | -| R8 `DestroyedOnlyWhenEnded` | While the host lives, the manifest says destroyed only after the host saw the program end. | `list` hides a program that still runs, and gc removes its folder. | -| R9 `DestroyEndsDestroyed` | `destroy` reports success only after it wrote destroyed or read it. | `destroy` says `destroyed: true`, but the session reads failed, "host process died unexpectedly", until a second `destroy`. | -| R10 `RemovedFolderStaysRemoved` | Once gc removed the session folder, no write brings it back. | A late write creates the folder again with only `session.json`. `list --all` shows that stub session until the next gc removes it. | -| R11 `DestroyedProgramStopped` | When the manifest says destroyed, no process of the program's process group runs, unless the program exited on its own first or no manifest named its pid. | A process of the session keeps running, `list` hides it, and nothing stops it later. | -| R13 `LiveGroupStaysNamed` | While a process of the program's process group runs, a manifest that named the program still names it. | The session reads failed or destroyed without `childPid`, so no later `destroy` or reconcile can stop the process that still runs. | -| R14 `DestroyOutlivesProgram` | `destroy` is never killed before it reports, also when it runs inside the program's session. | `destroy` prints nothing. With `--force` it kills its own group, and the session reads exited, not destroyed. | -| R15 `NoUnrelatedGroupKilled` | No kill reaches a process group that took the program's group id after the program's group ended. | `destroy`, `destroy --force`, a reconcile or the host's shutdown sends SIGKILL to an unrelated group, such as the program of another session. | -| R16 `DestroyedSessionStopped` | When the manifest says destroyed, no process of the program's group runs, also none that the program left when it exited on its own, unless the host died before `program.json` named the program. | `destroy` reports `destroyed: true` while a process of the session runs, `list` hides it, and nothing stops it later. | -| R17 `FailedCreateStopped` | Once `create` gave up on its host, the host keeps the session `running` only while `create`'s SIGTERM is on its way to it, or while the host has yet to check for the create-failed marker. A `create` on Windows whose marker writes all failed is outside R17 (see Scope). | `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, or, after that reconcile died, until the next reconcile reads the manifest. | `destroy` reports `destroyed: true`, and the session then reads `failed`. | -| R19 `NoUnrelatedHostKilled` | No kill of `destroy --force` reaches a process that took the host's pid after the host ended. | `destroy --force` sends SIGKILL to an unrelated process that got the crashed host's pid. | -| R20 `RemovedSessionStopped` | gc in the host's pid space removes a session folder, and with it `program.json`, only once no process of the program's group runs, also none that the program left when it exited on its own. | A process of the session keeps running, and nothing can prove or stop it later. | +| Rule | What must hold | Harm when it breaks | +| ------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | +| R1 `NoLiveSessionDeleted` | gc never removes the folder of a session whose host can still write to it. | A running or starting session loses its manifest and event log. | +| R2 `HostDeathOnlyWhenDead` | The manifest says "failed, host died" only when the host process is dead. | `list` and `inspect` show a live session as failed. Commands refuse it. | +| R3 `TerminalIsFinal` | Once the manifest shows exited, failed or destroyed, it never shows running again. | A finished session looks running, and the next reconcile marks it failed. | +| R4 `RecordedExitKept` | Once the manifest records that the program exited, only `destroy` changes it, to destroyed, and keeps the exit code. | A program that exited 0 is reported as failed, with its exit code lost. | +| R5 `RunningSessionReachable` | While the host serves a running program, the socket file exists. | The session runs, but no command can reach it. | +| R6 `HostStartsWhenCreated` | A host never fails to start because another process removed or rewrote its files. | `create` fails with `HOST_UNREACHABLE` for a session nobody touched. | +| R7 `TerminalIsLastWrite` | Once the manifest shows exited, failed or destroyed, the host has no write left to make. | gc removes the folder while the host still writes to it, and the host's write then fails. | +| R8 `DestroyedOnlyWhenEnded` | While the host lives, the manifest says destroyed only after the host saw the program end. | `list` hides a program that still runs, and gc removes its folder. | +| R9 `DestroyEndsDestroyed` | `destroy` reports success only after it wrote destroyed or read it. | `destroy` says `destroyed: true`, but the session reads failed, "host process died unexpectedly", until a second `destroy`. | +| R10 `RemovedFolderStaysRemoved` | Once gc removed the session folder, no write brings it back. | A late write creates the folder again with only `session.json`. `list --all` shows that stub session until the next gc removes it. | +| R11 `DestroyedProgramStopped` | When the manifest says destroyed, no process of the program's process group runs, unless the program exited on its own first, no manifest named its pid, or `destroy --force` could not read the group. | A process of the session keeps running, `list` hides it, and nothing stops it later. | +| R13 `LiveGroupStaysNamed` | While a process of the program's process group runs, a manifest that named the program still names it. | The session reads failed or destroyed without `childPid`, so no later `destroy` or reconcile can stop the process that still runs. | +| R14 `DestroyOutlivesProgram` | `destroy` is never killed before it reports, also when it runs inside the program's session. | `destroy` prints nothing. With `--force` it kills its own group, and the session reads exited, not destroyed. | +| R15 `NoUnrelatedGroupKilled` | No kill reaches a process group that took the program's group id after the program's group ended. | `destroy`, `destroy --force`, a reconcile or the host's shutdown sends SIGKILL to an unrelated group, such as the program of another session. | +| R16 `DestroyedSessionStopped` | When the manifest says destroyed, no process of the program's group runs, also none that the program left when it exited on its own, unless the host died before `program.json` named the program or `destroy --force` could not read the group. | `destroy` reports `destroyed: true` while a process of the session runs, `list` hides it, and nothing stops it later. | +| R17 `FailedCreateStopped` | Once `create` gave up on its host, the host keeps the session `running` only while `create`'s SIGTERM is on its way to it, or while the host has yet to check for the create-failed marker. A `create` on Windows whose marker writes all failed is outside R17 (see Scope). | `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, or, after that reconcile died, until the next reconcile reads the manifest. | `destroy` reports `destroyed: true`, and the session then reads `failed`. | +| R19 `NoUnrelatedHostKilled` | No kill of `destroy --force` reaches a process that took the host's pid after the host ended. | `destroy --force` sends SIGKILL to an unrelated process that got the crashed host's pid. | +| R20 `RemovedSessionStopped` | gc in the host's pid space, with a `/proc` that shows the autogroups, removes a session folder, and with it `program.json`, only once no process of the program's group runs, also none that the program left when it exited on its own, unless `destroy --force` could not read the group. | A process of the session keeps running, and nothing can prove or stop it later. | `TypeOK` also runs in every run. When it breaks, the model is wrong, not the code. @@ -41,8 +41,8 @@ The tool is TLC, the TLA+ model checker, pinned to release 1.7.4 by sha256. The Yes, when the diff changes any of these: -- `src/host/lifecycle.ts`: `allocateSession` (and the order of its `launch` call and first manifest write), `launchHost`, `isProcessAlive`, the host proof (`readSessionHost`, `psShowsSessionHost`, `isHostAlive`, `hostMatches`, `killHostBestEffort`), `cliRunsInsideProgramSession` with `ownLinuxSessionId`, `ownProcessGroupId`, `controllingTerminal` and `sharesControllingTerminal`, `reconcileSession`, and `destroySession` with its local `stopLeftoversThenRecordDestroyed` and its helpers `recordDestroyed`, `stopSessionProcesses`, `readSessionManifestOrThrow`, `waitForTerminalManifest`, `waitForProcessesToExit` and `killProcessBestEffort`, and `removeDeadHostSocket`, which `gc` and `destroySession` call. -- `src/host/programGroup.ts`: the token capture (`captureProgram`, `captureToken`, `readAutogroup`, `parseAutogroup`, `parseProcStat`), the `/proc` reads (`readProcFileIfExists`, `readLiveThreadState`, `readProcStat`, `readShownProcStat`, `isRefusedRead`, `readBootId`), the record (`writeProgramRecord`, `readProgramRecord`, `readProvenProgramGroup`, `readProgramGroup`, `provenProgramGroupRuns` with its `GC_JUDGEMENTS` limit, `judgeGroupForGc`, `judgeFrozenGroup`, `probeFindsGroup`), `procShowsOwnPidSpace`, the verdict (`judgeProgramGroup`, `readGroupMembers`), and the kill and the probe (`stopProgramGroup`, `isProgramGroupAlive`, `processGroupTarget`, `isProcessGroupAlive` with `groupHasLiveProcess` and `procHidesOtherUsers`, `killProcessGroupBestEffort`, `signalProcessGroup`). +- `src/host/lifecycle.ts`: `allocateSession` (and the order of its `launch` call and first manifest write), `launchHost`, `isProcessAlive`, the host proof (`readSessionHost`, `psShowsSessionHost`, `isHostAlive`, `hostMatches`, `killHostBestEffort`), `cliRunsInsideProgramSession` with `ownLinuxSessionId`, `ownProcessGroupId`, `controllingTerminal` and `sharesControllingTerminal`, `reconcileSession`, and `destroySession` with its local `stopLeftoversThenRecordDestroyed` and `stopUnlessUnreadable` and its helpers `recordDestroyed`, `stopSessionProcesses`, `readSessionManifestOrThrow`, `waitForTerminalManifest`, `waitForProcessesToExit` and `killProcessBestEffort`, and `removeDeadHostSocket`, which `gc` and `destroySession` call. +- `src/host/programGroup.ts`: the token capture (`captureProgram`, `captureToken`, `readAutogroup`, `parseAutogroup`, `parseProcStat`), the `/proc` reads (`readProcFileIfExists`, `readLiveThreadState`, `readProcStat`, `readShownProcStat`, `isRefusedRead`, `readBootId`), the record (`writeProgramRecord`, `readProgramRecord`, `isUnreadableGroupError` with its `UNREADABLE_ERRNOS`, `readProvenProgramGroup`, `readProgramGroup`, `provenProgramGroupRuns` with its `GC_JUDGEMENTS` limit, `judgeGroupForGc`, `judgeFrozenGroup` with its `FROZEN_JUDGEMENTS` limit, `probeFindsGroup`), `procShowsOwnPidSpace`, the verdict (`judgeProgramGroup`, `readGroupMembers`), and the kill and the probe (`stopProgramGroup`, `isProgramGroupAlive`, `processGroupTarget`, `isProcessGroupAlive` with `groupHasLiveProcess` and `procHidesOtherUsers`, `killProcessGroupBestEffort`, `signalProcessGroup`). - `src/host/hostMain.ts`: `waitForManifestFromCreate`, `isSessionCommandable`, and in `runHost` the start-up statements (the manifest wait, the `hostPid === process.pid` check, the `host.json` write with `captureHost` and `writeHostRecord`, `createSerialManifestWriter`, `EventLog.open`, the create-failed marker check, `createPty`, `setChildPid`, `captureProgram`, `watchCreateFailed`), `hangUpProgram` with its kill timer and the `SHUTDOWN_KILL_GRACE_MS` constant, `startIdlePolling` (the idle time-out), `initiateShutdown`, `startShutdown`, `handlePtyExit` with its wait for the program's group, `pty.onExit`, the `SIGTERM` handler, the `resize` and `destroy` handlers, and the last `try` block (the `program.json` write, the start-up manifest write and `rpcServer.listen`). - `src/host/manifestWriter.ts` `createSerialManifestWriter`. - `src/cli/commands/gc.ts` `gcSessions` and `defaultDependencies`, `src/cli/commands/create.ts` `runCreateCommand` with `waitForReadyHost`, `writeMarkerOrLog` and `hostRuns`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`. @@ -65,13 +65,13 @@ From the repo root: .agents/skills/verify-session-lifecycle/scripts/check.sh ``` -It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. On a CI runner with 4 vCPUs and the default `CHECK_JOBS` of 4 it takes about an hour, so CI runs it in four shares. Eleven runs explore more than 20 million distinct states each, so `CHECK_JOBS=85` starts every run at once and takes about as long as the longest run. `JAVA=/path/to/java` picks another Java. `TLA2TOOLS_JAR=/path/to/tla2tools.jar` uses a jar you already have, which must be the same 1.7.4 build. `CHECK_OUT=` keeps the results in that folder (default: a new temp folder, printed at the end). +It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. On a CI runner with 4 vCPUs and the default `CHECK_JOBS` of 4 it takes about an hour, so CI runs it in four shares. Eleven runs explore more than 20 million distinct states each, so `CHECK_JOBS=90` starts every run at once and takes about as long as the longest run. `JAVA=/path/to/java` picks another Java. `TLA2TOOLS_JAR=/path/to/tla2tools.jar` uses a jar you already have, which must be the same 1.7.4 build. `CHECK_OUT=` keeps the results in that folder (default: a new temp folder, printed at the end). What it does: -1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the thirty-eight 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-nine guards that the rules depend on and the status sets of the policy table, and it hashes each covered function with comments and layout removed. 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 85 times and prints one line per run. +3. It runs TLC 90 times and prints one line per run. 4. It compares the guard values, the status sets, the hashes and the call sites with `coverage.json`. Exit codes: 0 means every run gave the expected result and the covered code matches the sync record. 1 means at least one run gave an unexpected result; the line says `UNEXPECTED`. 3 means every result was as expected, but covered code changed since the sync commit; that is not a pass, so follow "When you change covered code on purpose". 2 means a tool could not run. When both 1 and 3 apply, the exit code is 1. @@ -100,6 +100,11 @@ At the sync commit, the expected results are: | `witness-WitnessUnsharedDestroyCompletes-otherspace` | violated | A plain `destroy` from another pid space still reports success, because it trusts the host's `destroyed` record. | | `witness-WitnessUnsharedGcRemovesLeftover-otherspace` | violated | gc in another pid space cannot check the group, so it removes an exited session while a process that the program left runs. | | `mutant-UnsharedGroupReadsUnknown-otherspace`, `mutant-CreateRecordsHost-otherspace` | violated | R16: without the guard, the group reads gone where nothing shows it, and `destroy` of an exited session records destroyed while a process that the program left runs. | +| `current-checkfails`, the code as it is when every read of `program.json` by `destroy`, `list` and `gc` fails, every rule | pass | `CheckFails`: a read that fails with a system error (EACCES on `program.json`, EIO on `/proc`). gc and its reconcile skip the session, a plain `destroy` fails, and `destroy --force` records destroyed after it stopped the host alone. R11, R16 and R20 leave out a session that such a `destroy --force` recorded (the ghost `dblind`). | +| `witness-WitnessUncheckedForceDestroys-checkfails` | violated | `destroy --force` reports success for a session whose group it cannot read while a process that the program left runs. | +| `mutant-ForceSkipsUnreadableGroup-checkfails` | pass | Without the guard, `destroy --force` fails on the read like a plain `destroy`, so `WitnessUncheckedForceDestroys` is never reached, and no command removes the session. | +| `current-refused`, the code as it is when `/proc` of `destroy`, `list` and `gc` refuses the autogroup of the program's processes, every rule | pass | `Refused`: the group reads `unknown`, which reads alive while a process of it runs, and gets no kill. `destroy` then fails with `HOST_TIMEOUT` until the group ends, and gc reads the group not proven. R20 leaves `Refused` out. | +| `witness-WitnessRefusedGcRemovesLeftover-refused` | violated | gc that cannot check the group removes an exited session while a process that the program left runs. | | `mutant-HostChecksCreateFailed` | pass | Redundant off Windows: the SIGTERM of a `create` that gave up stops the host. | | `current-win32`, the code as it is on Windows, without a token and with a SIGTERM that ends the host at once, R1 to R14 and R17 to R19 | pass | `Win32`: `create` sends the SIGTERM only when the manifest names the program, and that SIGTERM is a host crash. | | `mutant-HostChecksCreateFailed-win32` | violated | R17: without the marker, a host that the manifest does not name yet keeps serving after `create` gave up. | @@ -492,7 +497,7 @@ node -e 'console.log(require(process.argv[1]).status)' "$d/session.json" Without the guard, `gcSessions` removed the folder of every collectable session. A program that exits on its own can leave a process in its group, such as `sleep 300 &` after `trap "" HUP`, and the host does not kill at a normal exit. The rm deleted `program.json` with the folder, and that record is the only proof that the process is the program's, so no later command could stop it. -Now `gcSessions` calls `provenProgramGroupRuns` after its other checks and before the rm. It judges the group that `readProvenProgramGroup` gives, as the waits of `destroy` do, and gc skips the session with the reason "the session's program group still runs (destroy ends it)" while it proves the group, also under `--dry-run`: a live member carries the token. A read that throws skips the session too, with the error as the reason. A member of a fork chain can end between its stat and its autogroup read (`unknown`), or show up only after the judge's scans, so `judgeGroupForGc` reads such a judgement as inconclusive, and gc judges again, at most ten times. gc does not check a destroyed session, because `destroy` records destroyed only after a wait that read the group gone. A record without a token proves nothing, so gc removes such a session as before. gc never keeps a session that no command can remove: a group that gc cannot check proves nothing, and gc removes its session as before. That covers another pid space, where the group reads `unshared` (as after a container restart that keeps the home, when `host.json` names a pid namespace that no longer exists), and a `/proc` that refuses the boot id or the autogroup of a live member (`unknown`). So R20 holds only for a gc in the host's pid space, and `witness-WitnessUnsharedGcRemovesLeftover-otherspace` shows that a gc in another one removes an exited session while a process that the program left runs. gc judges without a SIGSTOP first, so a fork chain that no scan shows reads gone to the judge. So `provenProgramGroupRuns` also counts the group as running while the probe `kill(-pgid, 0)` finds its id and no scan shows a member, live or zombie (`GcProbesUnseenGroup`). Under a PID 1 that never reaps, the chain also leaves zombies in view, so the scans show only zombies while its live member escapes them. Then `judgeFrozenGroup` sends SIGSTOP, as `stopProgramGroup` does, judges the stopped group, whose stopped member stays in view, and sends SIGCONT in a `finally` (`GcFreezesUnseenGroup`). Another gc or a `destroy` can send SIGCONT before that judgement, so a frozen group that still reads gone is judged again with another SIGSTOP, and only `GC_JUDGEMENTS` such judgements read it ended. The model has one gc, so it leaves that race out. It sends SIGSTOP only where `/proc` shows its own pid space. `mutant-GcFreezesUnseenGroup-unseen-zombies` must violate R20, and "gc keeps an exited session while a fork chain runs behind its zombies" in `test/integration/non-reaping-init.test.ts` covers it. An unrelated group that took the id is in view and reads `unproven`, so it does not keep the session. `mutant-GcProbesUnseenGroup-unseen` must violate R20. The integration tests "gc keeps an exited session while a process that the program left runs" and "... while a fork chain that the program left runs" in `test/integration/lifecycle.test.ts` cover both, and "gc removes an exited session whose host.json names another pid namespace" covers the restart. +Now `gcSessions` calls `provenProgramGroupRuns` after its other checks and before the rm. It judges the group that `readProvenProgramGroup` gives, as the waits of `destroy` do, and gc skips the session with the reason "the session's program group still runs (destroy ends it)" while it proves the group, also under `--dry-run`: a live member carries the token. A read that throws skips the session too, with the error as the reason. A member of a fork chain can end between its stat and its autogroup read (`unknown`), or show up only after the judge's scans, so `judgeGroupForGc` reads such a judgement as inconclusive, and gc judges again, at most ten times. gc does not check a destroyed session, because `destroy` records destroyed only after a wait that read the group gone. A record without a token proves nothing, so gc removes such a session as before. gc never keeps a session that no command can remove: a group that gc cannot check proves nothing, and gc removes its session as before. That covers another pid space, where the group reads `unshared` (as after a container restart that keeps the home, when `host.json` names a pid namespace that no longer exists), and a `/proc` that refuses the boot id or the autogroup of a live member (`unknown`). So R20 holds only for a gc in the host's pid space, and `witness-WitnessUnsharedGcRemovesLeftover-otherspace` shows that a gc in another one removes an exited session while a process that the program left runs. gc judges without a SIGSTOP first, so a fork chain that no scan shows reads gone to the judge. So `provenProgramGroupRuns` also counts the group as running while the probe `kill(-pgid, 0)` finds its id and no scan shows a member, live or zombie (`GcProbesUnseenGroup`). Under a PID 1 that never reaps, the chain also leaves zombies in view, so the scans show only zombies while its live member escapes them. Then `judgeFrozenGroup` sends SIGSTOP, as `stopProgramGroup` does, judges the stopped group, whose stopped member stays in view, and sends SIGCONT in a `finally` (`GcFreezesUnseenGroup`). Another gc or a `destroy` can send SIGCONT before that judgement, so a frozen group that still reads gone gets another SIGSTOP and judgement (`FROZEN_JUDGEMENTS`, two). When that one reads gone too, the judgement stays inconclusive, and gc judges again, so an ended group reads ended only after ten passes of two frozen judgements each. Under a subreaper that never reaps, with a zombie of the group and about 2,300 processes in `/proc`, `provenProgramGroupRuns` then took about 3.5 s at a load of 90, against about 2.5 s for the ten single freezes of #326. Only a SIGCONT from elsewhere before each of those 20 judgements lets a live member escape them all, and gc then reads the live chain ended and removes its folder. The model has one gc, so it leaves that race out. It sends SIGSTOP only where `/proc` shows its own pid space. `mutant-GcFreezesUnseenGroup-unseen-zombies` must violate R20, and "gc keeps an exited session while a fork chain runs behind its zombies" in `test/integration/non-reaping-init.test.ts` covers it. An unrelated group that took the id is in view and reads `unproven`, so it does not keep the session. `mutant-GcProbesUnseenGroup-unseen` must violate R20. The integration tests "gc keeps an exited session while a process that the program left runs" and "... while a fork chain that the program left runs" in `test/integration/lifecycle.test.ts` cover both, and "gc removes an exited session whose host.json names another pid namespace" covers the restart. ```sh id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'trap "" HUP; sleep 300 & exit 0' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))') @@ -503,6 +508,12 @@ node --import tsx src/cli/main.ts destroy "$id" --json node --import tsx src/cli/main.ts gc --json # removes the session ``` +### `ForceSkipsUnreadableGroup`: no command removes a session whose group cannot be read + +A read of the program's group that fails with an errno that a retry does not change, such as `program.json` that refuses the read (EACCES) or a `/proc` scan that fails (EIO), fails every later read too. `UNREADABLE_ERRNOS` lists them: EACCES, EPERM, EIO, EISDIR, ENOTDIR, ELOOP and ENAMETOOLONG. gc kept such a session, plain `destroy` failed on the same read, and so did `destroy --force`, so no command removed the session. No safety rule breaks then, because the model has no rule for a session that stays forever. + +Now `destroySession` runs every group read of a terminal session, and both rounds of `--force`, through its local `stopUnlessUnreadable`. That reads the group, stops it and waits for it. With `--force`, a read or a first judgement (`isProgramGroupAlive`, in `readAndJudge`) that fails with an error that `isUnreadableGroupError` accepts is run again after `pollDelay` (100 ms), and only a second such failure makes it stop the host alone instead, and the wait then proves the host dead. The stop runs after the `try`, so a read that fails after that first judgement, as in the wait, still throws, and a group that read alive gets its kill or fails the destroy. EMFILE, ENFILE, ENOMEM, EAGAIN and EINTR still throw, because a later read can succeed. A group that reads alive and a host that does not end still throw `HOST_TIMEOUT`. `recordDestroyed` then records destroyed, and a process that the program left can outlive it. gc names `destroy --force` in its skip reason for such a read. A reconcile also writes the manifest and removes the socket, so after a failed reconcile gc names it only when `forceSkipsGroup`, the read and first judgement of `destroy --force`, gets such an error too. A `host.json` that cannot be read counts as missing, so the group reads unshared: `destroy --force` fails with `HOST_TIMEOUT`, and gc removes the session. In the model, `CheckFails` makes every read of `program.json` by `destroy`, `list` and `gc` fail while the record exists, and the ghost `dblind` marks the destroyed record that such a `destroy --force` wrote. R11, R16 and R20 leave it out. The model has no read that succeeds and then fails: such a read only fails a destroy, and no rule forbids a destroy that fails. It has no read that fails once and then passes either, because `CheckFails` fails every read. A second read that passes leads to the stop of a readable group, which the model covers. `mutant-ForceSkipsUnreadableGroup-checkfails` expects pass, because without the guard `WitnessUncheckedForceDestroys` is never reached. The integration tests "destroy --force ends an exited session whose program.json it cannot read" and "destroy --force ends a session whose host died and whose program.json it cannot read" make `program.json` unreadable with `chmod 000`. + ### `CreateRecordsHost`: a CLI in another pid space reads a starting host dead (R2) 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. @@ -565,7 +576,7 @@ It assumes: - The kernel does not reuse a pid while a process group with that id exists, so a kill of the program's group id reaches only that group while a process of it runs. Once the whole group has ended, a new process can get that id and lead an unrelated group (case 5 of coder/agent-tty#203). The model lets that happen at any step after the group ended. With a token, `stopProgramGroup` kills only right after it read a live member that carries the token again, and the model takes that check and the kill as one step. No API holds a process group the way a pidfd holds one process, so a gap stays between the check and the `kill(2)`: from the start of the member's re-read to the kill call it took p50 24 µs, p99 69 µs and at most 81 µs over 300 kills at a load average of 43. A group that takes the id inside that gap needs every member to exit, the pid counter to wrap onto the id, and the new process to lead a group, all within those microseconds. - The program runs from the spawn on, but `program.json` names it only after `captureProgram` read its token and `writeProgramRecord` renamed the file, in the same synchronous block. A host death inside that block leaves a program that no file names, and R16 exempts it (case 2 of coder/agent-tty#203). Over 150 sequential `create` calls on Linux, from the return of node-pty's spawn to the renamed `program.json`, at 1-minute load averages of 38 to 83, that took a median of 2.8 ms, a 90th percentile of 4.3 ms and at most 66 ms. A scratch build of `runHost` timed it with `performance.now()`. `captureProgram` took a median of 1.3 ms and at most 7.3 ms of that, so the long tail lies in the rest of the block and the write. node-pty returns before the child has called `setsid()`, so the capture polls for at most 250 ms until the child leads its own session. - `OtherPidSpace` changes only how `destroy`, `list` and `gc` see the program's group. Their view of the host stays as in the shared pid space. `CliHostAlive` gives their view of the host: `judgeHost` reads a host that `host.json` names in another pid space as `unknown`, also after the host ended, so they never record it failed, and `hostMatches` never proves it, so `destroy --force` kills no host there. Without `host.json` they probe the pid in their own pid space, where no process has it, and read the host dead. `create` writes `host.json` before the first manifest names the host, so only a capture that failed, which the model leaves out, leaves that window open. -- `current` describes Linux with autogroups, where the capture finds the token. The model reads every autogroup and the boot id. When `/proc` refuses the boot id, or shows no autogroup id for a live member in the program's session (a refused read, or an empty or malformed file), `judgeProgramGroup` gives `unknown`: no kill, and `isProgramGroupAlive` reads the group alive, so `destroy` ends with `HOST_TIMEOUT` and a reconcile writes nothing, as while a process of another user runs. A CLI that cannot list `/proc` at all, as in a chroot, sees no member. `judgeProgramGroup` then gives `gone`, so nothing gets the kill, and the probe of the group decides whether it reads alive. The model leaves those refused reads out. Without a token, `readProgramGroup` falls back to the childPid of the manifest, as before `program.json` existed: on macOS and Windows, on a kernel without `CONFIG_SCHED_AUTOGROUP`, when the capture read no autogroup or no boot id, and for a session that an older agent-tty created. There a reconcile and `destroy --force` kill that childPid as it is, `destroy` of a terminal session kills nothing, and a kill can still reach an unrelated group that took the id. `current-no-token` checks that fallback: the constant `Token` is FALSE there, so `program.json` names no group, and the host kills and probes the program's pid as it is. R15 and R16 do not hold on that path, so the run checks R1 to R14. The fallback kills only while the session folder exists. gc's real `rm` deletes file by file, so while it runs the folder can exist after `program.json` is gone, and a fallback kill in that moment can use a childPid that gc's removal made stale. +- `current` describes Linux with autogroups, where the capture finds the token. The model reads every autogroup and the boot id. When `/proc` refuses the boot id, or shows no autogroup id for a live member in the program's session (a refused read, or an empty or malformed file), `judgeProgramGroup` gives `unknown`: no kill, and `isProgramGroupAlive` reads the group alive, so `destroy` ends with `HOST_TIMEOUT` and a reconcile writes nothing, as while a process of another user runs. A CLI that cannot list `/proc` at all, as in a chroot, sees no member. `judgeProgramGroup` then gives `gone`, so nothing gets the kill, and the probe of the group decides whether it reads alive. `current-refused` checks a `/proc` that refuses the autogroups for `destroy`, `list` and `gc` (`Refused`): they never prove the group, gc removes the session, and R20 leaves that out. The host's own reads stay as in `current`, so the model leaves out a refused read that the host shares. Without a token, `readProgramGroup` falls back to the childPid of the manifest, as before `program.json` existed: on macOS and Windows, on a kernel without `CONFIG_SCHED_AUTOGROUP`, when the capture read no autogroup or no boot id, and for a session that an older agent-tty created. There a reconcile and `destroy --force` kill that childPid as it is, `destroy` of a terminal session kills nothing, and a kill can still reach an unrelated group that took the id. `current-no-token` checks that fallback: the constant `Token` is FALSE there, so `program.json` names no group, and the host kills and probes the program's pid as it is. R15 and R16 do not hold on that path, so the run checks R1 to R14. The fallback kills only while the session folder exists. gc's real `rm` deletes file by file, so while it runs the folder can exist after `program.json` is gone, and a fallback kill in that moment can use a childPid that gc's removal made stale. - A `program.json` that does not parse, or that another version wrote, proves nothing: it gets no kill, and reconcile and `destroy` do not throw. A missing one gets the childPid fallback above. - A manifest write is atomic, because `writeManifest` renames a temp file. A write that fails counts as a host crash or a failed command. That covers a host write into a removed folder, which only a state that already breaks R1 reaches. - The host waits for its manifest while the `create` process lives, so it gives up only when `create` dies before that write. That counts as a host crash, which R6 does not cover. diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 94b58db2..ed8dd56b 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -20,6 +20,7 @@ "ShutdownChecksCommandable": true, "DestroyRecordsDestroyed": true, "DestroyKeepsExitCode": true, + "ForceSkipsUnreadableGroup": true, "DestroyStopsLeftovers": true, "ProvesHostPid": true, "ReconcileRepairsDestroyed": true, @@ -48,11 +49,14 @@ "src/cli/commands/create.ts#hostRuns": "b80eac3bb9523aaf", "src/cli/commands/destroy.ts#runDestroyCommand": "ecaa8b1d572da7c6", "src/cli/commands/destroy.ts#rerunInNewSession": "cf32d7d082758522", - "src/cli/commands/gc.ts#gcSessions": "a2ac8bd10f100332", - "src/cli/commands/gc.ts#defaultDependencies": "81a9894438cb5be7", + "src/cli/commands/gc.ts#gcSessions": "4d996cc35406473a", + "src/cli/commands/gc.ts#defaultDependencies": "ae2347cdb778b488", "src/host/programGroup.ts#provenProgramGroupRuns": "7b50817618b4b769", "src/host/programGroup.ts#judgeGroupForGc": "fb133ba2739116d1", - "src/host/programGroup.ts#judgeFrozenGroup": "d18458e7d70a5664", + "src/host/programGroup.ts#judgeFrozenGroup": "e3a6c281e3f579fc", + "src/host/programGroup.ts#FROZEN_JUDGEMENTS": "d4eb06aa7addbaa9", + "src/host/programGroup.ts#isUnreadableGroupError": "e2d852aa5b45cb53", + "src/host/programGroup.ts#UNREADABLE_ERRNOS": "24de7f719ccf14be", "src/host/programGroup.ts#GC_JUDGEMENTS": "180a0af01a4b81c7", "src/host/programGroup.ts#probeFindsGroup": "31ea7b5e835c0509", "src/host/lifecycle.ts#allocateSession": "43819af8c6c271ec", @@ -86,7 +90,7 @@ "src/host/lifecycle.ts#stopSessionProcesses": "d1abb608b1d2160a", "src/host/lifecycle.ts#recordDestroyed": "d3a74237a9c8459c", "src/host/lifecycle.ts#removeDeadHostSocket": "34ce07ab7b7e8d7b", - "src/host/lifecycle.ts#destroySession": "d840dd07a0e481f5", + "src/host/lifecycle.ts#destroySession": "05edb5d2825ed857", "src/host/lifecycle.ts#isMarkedDestroyed": "d178f4a63473915c", "src/host/lifecycle.ts#writeMarkedDestroyed": "4863c35f70699757", "src/host/lifecycle.ts#reconcileSession": "739c83bf945000c6", @@ -143,9 +147,9 @@ "src/host/hostMain.ts#runHost(final try)": "e0615a9709fefb67", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "7f1c6dd7943968c3", - "skill:scripts/facts.mjs": "6ee4da3ef9b6bac3", - "skill:scripts/check.sh": "b48bc5fd343aefb5" + "skill:model/SessionLifecycle.tla": "cd8639012467f13e", + "skill:scripts/facts.mjs": "2de6761bed77fb19", + "skill:scripts/check.sh": "fe2da7911682462a" }, "callSites": { "writeManifest": [ diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index 5bc325c5..7906292c 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -120,6 +120,10 @@ CONSTANTS \* create writes the marker again and reads \* the manifest after each write, up to 50 \* times, while the host runs + ForceSkipsUnreadableGroup, \* lifecycle.ts: destroy --force of a session + \* whose host is gone records destroyed also + \* when the read of the group fails with a + \* system error, after it stops the host alone TokenNamesProgram, \* programGroup.ts: captureToken records an \* autogroup only once the program leads its \* own session in an autogroup other than the @@ -157,6 +161,13 @@ CONSTANTS Win32, \* the environment: Windows, where SIGTERM ends \* the host at once, so create sends it only \* when the manifest names the program + CheckFails, \* the environment: while program.json names + \* the program, every read of it by destroy, + \* list and gc fails with a system error (EACCES, + \* or EIO on /proc), as does every judgement + Refused, \* the environment: /proc of destroy, list and gc + \* refuses the autogroup of the program's + \* processes, so no judgement proves the group MaxListReconciles \* how many times the "list" process reconciles ASSUME MaxListReconciles \in 1..3 @@ -165,6 +176,8 @@ ASSUME Unseen \in BOOLEAN ASSUME ZombiesInView \in BOOLEAN ASSUME OtherPidSpace \in BOOLEAN ASSUME Win32 \in BOOLEAN +ASSUME CheckFails \in BOOLEAN +ASSUME Refused \in BOOLEAN ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, GcKeepsLiveGroup, GcProbesUnseenGroup, GcFreezesUnseenGroup, ReconcileSkipsTerminal, @@ -180,7 +193,7 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, GcKeepsLiveGroup, ProvesGroupOwnership, DestroyStopsLeftovers, FallbackNeedsFolder, CreateStopsOnGiveUp, HostChecksCreateFailed, HostPollsCreateFailed, - CreateRetriesMarker, + CreateRetriesMarker, ForceSkipsUnreadableGroup, ReconcileRepairsDestroyed, ReconcileRepairsMarked, TokenNamesProgram, ReusedIdReadsGone, ProvesHostPid, CreateRecordsHost, @@ -189,8 +202,10 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, GcKeepsLiveGroup, Readers == {"gc", "list"} \* the two processes that run reconcileSession \* The group that a kill went through, and that the wait after it probes: \* "proven" (program.json with a token), "numeric" (a childPid without a -\* token), "bare" (the host's own record without a token) or "none". -GroupKinds == {"none", "proven", "numeric", "bare"} +\* token), "bare" (the host's own record without a token), "blind" (destroy +\* --force could not read the group, see ForceSkipsUnreadableGroup) or +\* "none". +GroupKinds == {"none", "proven", "numeric", "bare", "blind"} NoRead == [pid |-> FALSE, origin |-> "none", code |-> FALSE, child |-> FALSE, grp |-> "none"] @@ -280,7 +295,10 @@ VARIABLES dres, \* what destroy reported: "pending", "ok", "error", or \* "killed" (it died before it reported) dsaw, \* ghost: destroy wrote "destroyed" or read it last - dkill \* ghost: destroy --force killed a live host + dkill, \* ghost: destroy --force killed a live host + dblind \* ghost: destroy --force wrote the destroy marker or + \* destroyed without a read of the program's group + \* (CheckFails); a reconcile then repairs to destroyed diskVars == <> @@ -291,7 +309,7 @@ groupVars == <> shutVars == <> readerVars == <> -destroyVars == <> +destroyVars == <> vars == <> @@ -319,7 +337,7 @@ Init == /\ lruns = 0 /\ dpc = "check" /\ dforce \in BOOLEAN /\ dinside = FALSE /\ drd = NoRead /\ dres = "pending" - /\ dsaw = FALSE /\ dkill = FALSE + /\ dsaw = FALSE /\ dkill = FALSE /\ dblind = FALSE \* writeManifest in src/storage/manifests.ts: write a temp file in the session \* directory and rename it over session.json. The rename is the visible step. @@ -441,12 +459,23 @@ GroupSeen(kind) == \* readProgramGroup and readProvenProgramGroup give a group with a token \* that reads alive instead, so their waits time out. The host always runs \* in its own pid space, so it keeps GroupSeen and HostKill. CliHostAlive -\* gives the CLI's view of the host. +\* gives the CLI's view of the host. With Refused a live member of the +\* program's session shows no autogroup, so a group with a token reads +\* unknown, which reads alive, while a process of it runs, and it gets no +\* kill, because nothing proves it. CliGroupSeen(kind) == IF OtherPidSpace THEN kind = "proven" /\ UnsharedGroupReadsUnknown + ELSE IF Refused /\ kind = "proven" + THEN KillsProgramGroup /\ (prog \/ left \/ foreign) ELSE GroupSeen(kind) -CliKillThrough(named) == IF OtherPidSpace THEN NoKill ELSE KillThrough(named) +CliKillThrough(named) == + IF OtherPidSpace \/ (Refused /\ rec) THEN NoKill ELSE KillThrough(named) + +\* With CheckFails every read of program.json by destroy, list and gc fails +\* while the record exists, and so does every judgement of the group that +\* it names. +Unreadable == CheckFails /\ rec \* The host fails to start because its files are missing or were rewritten. HostFailsToStart == @@ -1044,13 +1073,22 @@ ReconcileRereadsManifest(p) == \* `const group = await readProgramGroup(sessionDirectory, \* current.childPid)` reads program.json, then stopProgramGroup(group). +\* With Unreadable the read throws, and so does reconcileSession: gc skips +\* the session ("failed to reconcile session (destroy --force removes it)"), +\* and list goes on. ReconcileReadsRecord(p) == /\ pc[p] = "r_record" - /\ CliKillThrough(rd[p].child) - /\ rd' = [rd EXCEPT ![p].grp = KindThrough(rd[p].child)] - /\ pc' = [pc EXCEPT ![p] = AfterGroupKill] + /\ IF Unreadable + THEN /\ NoKill /\ UNCHANGED rd + /\ pc' = [pc EXCEPT ![p] = IF p = "gc" THEN "done" + ELSE AfterReconcile(p)] + /\ gres' = IF p = "gc" THEN "skipped" ELSE gres + ELSE /\ CliKillThrough(rd[p].child) + /\ rd' = [rd EXCEPT ![p].grp = KindThrough(rd[p].child)] + /\ pc' = [pc EXCEPT ![p] = AfterGroupKill] + /\ UNCHANGED gres /\ UNCHANGED <> @@ -1201,14 +1239,15 @@ GcReadsReconciled == \* cannot turn from destroyed back, so this current status skips no more \* often. GcSeesGroup == - /\ ~OtherPidSpace + /\ ~OtherPidSpace /\ ~Refused /\ \/ GroupSeen("proven") \/ /\ GcProbesUnseenGroup /\ Unseen /\ (prog \/ left) /\ (~ZombiesInView \/ GcFreezesUnseenGroup) GcChecksGroup == /\ pc["gc"] = "group" - /\ IF GcKeepsLiveGroup /\ mst # "destroyed" /\ rec /\ GcSeesGroup + /\ IF GcKeepsLiveGroup /\ mst # "destroyed" + /\ (Unreadable \/ (rec /\ GcSeesGroup)) THEN GcSkips ELSE GcGoesTo("final") /\ UNCHANGED <> + readerVars, dforce, dinside, dsaw, dkill, dblind, + groupVars>> \* runDestroyCommand: cliRunsInsideProgramSession first compares \* AGENT_TTY_SESSION_ID, which the program and its processes inherit at @@ -1295,7 +1335,8 @@ DestroyChecksSession == /\ (InsideCheckReadsEnv \/ mchild))) /\ dpc' = "read" /\ UNCHANGED <> + readerVars, dforce, drd, dres, dsaw, dkill, dblind, + groupVars>> ReadCopy == [pid |-> mpid, origin |-> morigin, code |-> mcode, child |-> mchild, grp |-> "none"] @@ -1346,7 +1387,7 @@ DestroyReads == ELSE /\ dpc' = "rpc" /\ UNCHANGED <> /\ sock' = (sock /\ (mst # "destroyed" \/ (mpid /\ CliHostAlive))) /\ UNCHANGED <> + readerVars, dforce, dinside, dkill, dblind, groupVars>> \* stopLeftoversThenRecordDestroyed: stopSessionProcesses(sessionId, null, \* await readProvenProgramGroup(sessionDirectory), ...). The program.json @@ -1355,12 +1396,18 @@ DestroyReads == \* Then waitForProcessesToExit (DestroyPollsGroup, at "twait"). DestroyKillsLeftovers == /\ DestroyAt({"tkill"}) - /\ IF rec /\ ~OtherPidSpace THEN ProvenKill ELSE NoKill - /\ drd' = [drd EXCEPT !.grp = IF rec THEN "proven" ELSE "none"] - /\ dpc' = "twait" + /\ IF Unreadable /\ ~(dforce /\ ForceSkipsUnreadableGroup) + THEN /\ NoKill /\ DestroyEnds("error") + ELSE /\ IF rec /\ ~OtherPidSpace /\ ~Refused /\ ~Unreadable + THEN ProvenKill ELSE NoKill + /\ drd' = [drd EXCEPT !.grp = IF Unreadable THEN "blind" + ELSE IF rec THEN "proven" + ELSE "none"] + /\ dpc' = "twait" + /\ UNCHANGED dres /\ UNCHANGED <> \* recordDestroyed: writeDestroyMarker, an empty file written with no mkdir. @@ -1370,7 +1417,8 @@ DestroyMarksFolder == /\ DestroyAt({"tmark"}) /\ IF dir THEN /\ dmark' = TRUE /\ dpc' = "twrite" /\ UNCHANGED <> - ELSE /\ DestroyEnds("error") /\ UNCHANGED dmark + /\ dblind' = (dblind \/ drd.grp = "blind") + ELSE /\ DestroyEnds("error") /\ UNCHANGED <> /\ UNCHANGED <> /\ UNCHANGED <> @@ -1397,7 +1446,7 @@ DestroyUnlinksSocket == /\ sock' = FALSE /\ dpc' = "done" /\ dres' = "ok" /\ UNCHANGED <> + dforce, dinside, drd, dsaw, dkill, dblind, groupVars>> \* killHostBestEffort(host) of the copy that destroy read. With \* ProvesHostPid it kills only a host that hostMatches proves: the live host @@ -1423,13 +1472,19 @@ KillsHost == \* wait ("rkill"). DestroyKills == /\ DestroyAt({"kill", "rkill"}) - /\ CliKillThrough(drd.child) - /\ KillsHost - /\ drd' = [drd EXCEPT !.grp = KindThrough(drd.child)] - /\ dpc' = IF dpc = "kill" THEN "kwait" ELSE "rwait" + /\ IF Unreadable /\ ~ForceSkipsUnreadableGroup + THEN /\ NoKill /\ DestroyEnds("error") + /\ UNCHANGED <> + ELSE /\ IF Unreadable THEN NoKill ELSE CliKillThrough(drd.child) + /\ KillsHost + /\ drd' = [drd EXCEPT !.grp = IF Unreadable THEN "blind" + ELSE KindThrough(drd.child)] + /\ dpc' = IF dpc = "kill" THEN "kwait" ELSE "rwait" + /\ UNCHANGED dres /\ UNCHANGED <> + readerVars, dforce, dinside, dsaw, dblind, rec, reused, + hrec, hreused, passedReused>> \* waitForProcessesToExit in stopSessionProcesses polls until the host is \* dead and isProgramGroupAlive(group) reads false. A host that the kill @@ -1453,7 +1508,7 @@ DestroyPollsGroup == THEN /\ dpc' = "tunlink" /\ drd' = NoRead /\ UNCHANGED <> ELSE /\ dpc' = Records /\ UNCHANGED <> /\ UNCHANGED <> @@ -1468,7 +1523,7 @@ DestroyRereads == /\ dsaw' = (mst = "destroyed") /\ UNCHANGED dres /\ UNCHANGED <> + readerVars, dforce, dinside, dkill, dblind, groupVars>> \* sendRpc(socketFile, 'destroy') reaches the host, whose destroy handler \* calls startShutdown and answers. The host does the work, so this is one @@ -1478,7 +1533,7 @@ DestroySendsRpc == /\ StartShutdown(WriteQueued) /\ dpc' = "poll" /\ UNCHANGED <> \* No socket file, or nobody listens on it: HOST_UNREACHABLE. destroy then @@ -1487,7 +1542,7 @@ DestroyRpcFails == /\ DestroyAt({"rpc"}) /\ ~(sock /\ hostAlive) /\ dpc' = "final" /\ UNCHANGED <> \* waitForTerminalManifest: readManifest until it is terminal. A missing @@ -1501,7 +1556,7 @@ DestroyPolls == THEN DestroyFinishes ELSE /\ dpc' = "final" /\ UNCHANGED <> /\ UNCHANGED <> + readerVars, dforce, dinside, dkill, dblind, groupVars>> \* readSessionManifestOrThrow after destroy's own reconcile: terminal means \* success, anything else throws. @@ -1509,7 +1564,7 @@ DestroyFinalRead == /\ DestroyAt({"final"}) /\ IF mst \in Terminal THEN DestroyFinishes ELSE DestroyEnds("error") /\ UNCHANGED <> + readerVars, dforce, dinside, dkill, dblind, groupVars>> \* Every process is finished. This step keeps TLC from reporting the end \* states as deadlocks. Any other state without a step is a model error. @@ -1560,7 +1615,8 @@ TypeOK == /\ {dir, mpid, mchild, wasTerminal, wasExited, wasNamed, dmark, cmark, startFailed, readRepaired, lostRepair, diedBeforeRepair, polled, sock, - hostAlive, prog, foreign, sig, dforce, dinside, dsaw, dkill, rec, left, + hostAlive, prog, foreign, sig, dforce, dinside, dsaw, dkill, dblind, + rec, left, reused, hitUnrelated, diedUnrecorded, passedReused, hrec, hreused, hitUnrelatedHost} \subseteq BOOLEAN @@ -1646,7 +1702,8 @@ RemovedFolderStaysRemoved == gres = "removed" => ~dir \* process that a program left when it exited on its own (`left`, which R16 \* covers), nor a program that no manifest named: its host died before the \* start-up write (see the Scope section of SKILL.md). -DestroyedProgramStopped == (mst = "destroyed" /\ wasNamed) => ~GroupAlive +DestroyedProgramStopped == + (mst = "destroyed" /\ wasNamed /\ ~dblind) => ~GroupAlive \* R13: while a process of the program's group runs, a manifest that named \* the program still names it, so a later destroy or reconcile can still @@ -1666,7 +1723,7 @@ NoUnrelatedGroupKilled == ~hitUnrelated \* the host died after it started the program and before program.json named \* it (see the Scope section of SKILL.md). DestroyedSessionStopped == - (mst = "destroyed" /\ ~diedUnrecorded) => ~(GroupAlive \/ left) + (mst = "destroyed" /\ ~diedUnrecorded /\ ~dblind) => ~(GroupAlive \/ left) \* R17: once create gave up, its host keeps the session "running" only \* while create's SIGTERM is still on its way to it, or while the host has @@ -1701,7 +1758,8 @@ NoUnrelatedHostKilled == ~hitUnrelatedHost \* space cannot check the group, and it removes the folder as it does \* without a token (WitnessUnsharedGcRemovesLeftover). RemovedSessionStopped == - (gres = "removed" /\ ~diedUnrecorded /\ ~OtherPidSpace) + (gres = "removed" /\ ~diedUnrecorded /\ ~OtherPidSpace /\ ~Refused + /\ ~dblind) => ~(GroupAlive \/ left) \* Witnesses. check.sh expects TLC to report each one VIOLATED, which shows @@ -1756,6 +1814,9 @@ WitnessUnsharedDestroyCompletes == \* With OtherPidSpace gc removes an exited session while a process that \* the program left runs, because it cannot check the group there: the \* state that R20 leaves out. +WitnessUncheckedForceDestroys == ~(dblind /\ dres = "ok" /\ left) +WitnessRefusedGcRemovesLeftover == + ~(Refused /\ gres = "removed" /\ ~diedUnrecorded /\ left) WitnessUnsharedGcRemovesLeftover == ~(OtherPidSpace /\ gres = "removed" /\ ~diedUnrecorded /\ left) ============================================================================= diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index 061e278c..ff17ea33 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/check.sh +++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh @@ -166,7 +166,7 @@ TERMINAL=$(node -e ' const c = JSON.parse(require("node:fs").readFileSync(process.argv[1], "utf8")).constants; console.log("{" + c.Terminal.map((s) => JSON.stringify(s)).join(", ") + "}"); ' "$OUT/facts.json") -GUARDS="GcSkipsNonCollectable GcFinalCheck GcKeepsLiveGroup GcProbesUnseenGroup GcFreezesUnseenGroup ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed ReconcileRepairsMarked CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid CreateRecordsHost FreezesUnseenGroup UnsharedGroupReadsUnknown HostChecksCreateFailed HostPollsCreateFailed CreateRetriesMarker" +GUARDS="GcSkipsNonCollectable GcFinalCheck GcKeepsLiveGroup GcProbesUnseenGroup GcFreezesUnseenGroup ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed ReconcileRepairsMarked CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid CreateRecordsHost FreezesUnseenGroup UnsharedGroupReadsUnknown HostChecksCreateFailed HostPollsCreateFailed CreateRetriesMarker ForceSkipsUnreadableGroup" # One "Guard=TRUE|FALSE" word per guard, read from the code by facts.mjs. FACTS_LINE=$(node -e ' const c = JSON.parse(require("node:fs").readFileSync(process.argv[1], "utf8")).constants; @@ -199,6 +199,11 @@ ZOMBIES=FALSE OTHER=FALSE # WIN32: whether SIGTERM ends the host at once, as on Windows. WIN32=FALSE +# CHECKFAILS: whether destroy, list and gc fail every read of program.json. +CHECKFAILS=FALSE +# REFUSED: whether /proc of destroy, list and gc refuses the program's +# autogroup. +REFUSED=FALSE write_run() { local name=$1 expect=$2 invariants=$3 overrides=$4 note=$5 must=${6:-} local dir="$OUT/$name" fact guard value @@ -222,6 +227,8 @@ write_run() { echo " ZombiesInView = $ZOMBIES" echo " OtherPidSpace = $OTHER" echo " Win32 = $WIN32" + echo " CheckFails = $CHECKFAILS" + echo " Refused = $REFUSED" echo " MaxListReconciles = 2" echo "SPECIFICATION Spec" echo "CHECK_DEADLOCK TRUE" @@ -295,6 +302,22 @@ write_run mutant-UnsharedGroupReadsUnknown-otherspace violated DestroyedSessionS write_run mutant-CreateRecordsHost-otherspace violated HostDeathOnlyWhenDead "CreateRecordsHost=FALSE" "without the record from create, a reconcile in another pid space reads the starting host dead and records it failed" HostDeathOnlyWhenDead OTHER=FALSE +# destroy, list and gc cannot read program.json (EACCES), or /proc fails with +# a system error. gc keeps the session, and destroy --force ends it without +# the read. +CHECKFAILS=TRUE +write_run current-checkfails pass "$RULES" "" "the code with program.json unreadable for destroy, list and gc: every rule holds" +write_run witness-WitnessUncheckedForceDestroys-checkfails violated WitnessUncheckedForceDestroys "" "destroy --force ends a session whose group it cannot read while a process that the program left runs" +write_run mutant-ForceSkipsUnreadableGroup-checkfails pass WitnessUncheckedForceDestroys "ForceSkipsUnreadableGroup=FALSE" "without the fallback, destroy --force fails on the read, so no command removes the session" +CHECKFAILS=FALSE + +# /proc of destroy, list and gc refuses the autogroup of the program's +# processes. gc cannot check the group, and destroy cannot prove it. +REFUSED=TRUE +write_run current-refused pass "$RULES" "" "the code with a /proc that refuses the program's autogroup: every rule holds" +write_run witness-WitnessRefusedGcRemovesLeftover-refused violated WitnessRefusedGcRemovesLeftover "" "gc cannot check the group, so it removes an exited session while a process that the program left runs" +REFUSED=FALSE + # Without a token every kill falls back to the id that a manifest or the # host's own record names, as before program.json existed. TOKEN=FALSE diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 525f9858..0c4c4b6e 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -704,7 +704,7 @@ function destroyFacts() { const block = force.thenStatement; const first = indexOfStatement( block, - /^await stopSessionProcesses\(\s*sessionId,\s*await readSessionHost\(sessionDirectory, manifest\),\s*await readProgramGroup\(/, + /^await stopUnlessUnreadable\(\s*await readSessionHost\(sessionDirectory, manifest\),\s*\(\) => readProgramGroup\(sessionDirectory, manifest\.childPid\),?\s*\);$/, ); const reread = indexOfStatement( block, @@ -712,11 +712,7 @@ function destroyFacts() { ); const group = indexOfStatement( block, - /^const group = await readProgramGroup\(/, - ); - const second = indexOfStatement( - block, - /^await stopSessionProcesses\(\s*sessionId,\s*await readSessionHost\(sessionDirectory, current\),\s*group,/, + /^const group = await stopUnlessUnreadable\(\s*await readSessionHost\(sessionDirectory, current\),\s*\(\) => readProgramGroup\(sessionDirectory, current\.childPid\),?\s*\);$/, ); const records = indexOfStatement( block, @@ -726,8 +722,8 @@ function destroyFacts() { first >= 0 && reread > first && group > reread && - second > group && - records > second && + records > group && + stopsThenRecords.stops && calls(block, 'reconcileSession').length === 0; } const stop = requireDeclaration( @@ -757,6 +753,7 @@ function destroyFacts() { stopWaits && waitsForProcessesOnly, DestroyKeepsExitCode: keepsExitCode, + ForceSkipsUnreadableGroup: forceRecords && stopsThenRecords.skipsUnreadable, DestroyStopsLeftovers: stopsThenRecords.records && stopsThenRecords.stops && @@ -771,52 +768,155 @@ function destroyFacts() { }; } -// The statements of destroySession's local stopLeftoversThenRecordDestroyed: -// with DestroyStopsLeftovers it stops the group that program.json proves, -// waits for it, and only then records destroyed. readProvenProgramGroup -// returns the record whenever it has a token, or the unshared group when -// this process cannot prove that it shares the host's pid space. A session -// that a process which saw the group recorded destroyed gets no wait for an -// unshared group (trustsDestroyed). +// destroySession's local stopLeftoversThenRecordDestroyed hands +// stopUnlessUnreadable the read of program.json, and only then records +// destroyed. readProvenProgramGroup returns the record whenever it has a +// token, or the unshared group when this process cannot prove that it +// shares the host's pid space. A session that a process which saw the +// group recorded destroyed gets no wait for an unshared group +// (trustsDestroyed). stopUnlessUnreadable reads the group, stops it and +// waits. With skipsUnreadable, destroy --force that cannot read the group +// (a system error) stops the host alone instead. const UNSHARED_RETURN = 'return (await sharesHostPids(sessionDirectory, false)) ? record : UNSHARED_GROUP;'; -const STOP_UNLESS_TRUSTED = - "await stopSessionProcesses( sessionId, null, terminal.status === 'destroyed' && group !== null && 'unshared' in group ? null : group, sessionDirectory, signal, );"; -const STOP_ALWAYS = - 'await stopSessionProcesses( sessionId, null, group, sessionDirectory, signal, );'; +const RETURN_UNLESS_TRUSTED = + "return terminal.status === 'destroyed' && group !== null && 'unshared' in group ? null : group;"; -function stopLeftoversThenRecordDestroyed(destroy) { - let found = []; +function localArrows(destroy) { + const out = new Map(); walk(destroy.body, (node) => { if ( ts.isVariableDeclaration(node) && - node.name.getText() === 'stopLeftoversThenRecordDestroyed' && node.initializer !== undefined && ts.isArrowFunction(node.initializer) && ts.isBlock(node.initializer.body) ) { - found = node.initializer.body.statements.map((st) => - normalize(st.getText()), - ); + out.set(node.name.getText(), node.initializer.body.statements); } }); + return out; +} + +function statementsOf(block) { + return block.statements.map((st) => normalize(st.getText())); +} + +function stopUnlessUnreadableFacts(arrows) { + const st = arrows.get('stopUnlessUnreadable') ?? []; + const [judge, declared, attempt, ...after] = st; + // readAndJudge reads the group and judges it once, with no kill. + const judges = + judge !== undefined && + ts.isVariableStatement(judge) && + judge.declarationList.declarations[0]?.name.getText() === 'readAndJudge' && + (arrows.get('readAndJudge') ?? []) + .map((s) => normalize(s.getText())) + .join('\n') === + [ + 'const group = await readGroup();', + 'isProgramGroupAlive(group);', + 'return group;', + ].join('\n'); + if ( + !judges || + declared === undefined || + normalize(declared.getText()) !== 'let group: ProgramGroup | null;' || + attempt === undefined || + !ts.isTryStatement(attempt) || + attempt.catchClause === undefined || + attempt.finallyBlock !== undefined + ) { + return { stops: false, skipsUnreadable: false }; + } + // Only a read or a judgement that fails in the try can skip the group: the + // stop comes after the try, so a read that fails after a verdict fails the + // destroy. With --force, an unreadable read is read again after a poll + // interval, and only a second unreadable read skips the group. + const tried = statementsOf(attempt.tryBlock).join('\n'); + const caught = attempt.catchClause.block.statements; + const stops = + tried === 'group = await readAndJudge();' && + after.map((s) => normalize(s.getText())).join('\n') === + [ + 'await stopSessionProcesses( sessionId, host, group, sessionDirectory, signal, );', + 'return group;', + ].join('\n'); + const [rethrows, waits, again, ...more] = caught; + const skipsUnreadable = + more.length === 0 && + normalize(rethrows?.getText() ?? '') === + 'if (force !== true || !isUnreadableGroupError(error)) { throw error; }' && + normalize(waits?.getText() ?? '') === + 'await pollDelay(DESTROY_POLL_INTERVAL_MS, signal);' && + again !== undefined && + ts.isTryStatement(again) && + again.catchClause !== undefined && + again.finallyBlock === undefined && + statementsOf(again.tryBlock).join('\n') === + 'group = await readAndJudge();' && + statementsOf(again.catchClause.block).join('\n') === + [ + 'if (!isUnreadableGroupError(secondError)) { throw secondError; }', + 'await stopSessionProcesses( sessionId, host, null, sessionDirectory, signal, );', + 'return null;', + ].join('\n') && + bodyIs( + 'isUnreadableGroupError', + "const cause = hasErrorCode(error, ERROR_CODES.STORAGE_READ_ERROR) ? (error as Error).cause : error; const code: unknown = cause instanceof Error ? (cause as { code?: unknown }).code : undefined; return ( !(cause instanceof CliError) && typeof code === 'string' && UNREADABLE_ERRNOS.has(code) );", + ); + const rethrowsAll = + caught.map((s) => normalize(s.getText())).join('\n') === 'throw error;'; + return { + stops: stops && (rethrowsAll || skipsUnreadable), + skipsUnreadable: stops && skipsUnreadable, + }; +} + +function stopLeftoversThenRecordDestroyed(destroy) { + const arrows = localArrows(destroy); + const found = arrows.get('stopLeftoversThenRecordDestroyed') ?? []; + const first = found[0]; + let read = []; + if ( + first !== undefined && + ts.isExpressionStatement(first) && + ts.isAwaitExpression(first.expression) && + ts.isCallExpression(first.expression.expression) + ) { + const call = first.expression.expression; + const reader = call.arguments[1]; + if ( + call.expression.getText() === 'stopUnlessUnreadable' && + call.arguments.length === 2 && + call.arguments[0].getText() === 'null' && + reader !== undefined && + ts.isArrowFunction(reader) && + ts.isBlock(reader.body) + ) { + read = statementsOf(reader.body); + } + } + const unless = stopUnlessUnreadableFacts(arrows); return { records: found.length > 0 && /^await recordDestroyed\(manifestFile, socketFile, terminal, null\);$/.test( - found.at(-1), + normalize(found.at(-1).getText()), ), stops: - found.length === 3 && - found[0] === + found.length === 2 && + read.length === 2 && + read[0] === 'const group = await readProvenProgramGroup(sessionDirectory);' && - [STOP_UNLESS_TRUSTED, STOP_ALWAYS].includes(found[1]) && + [RETURN_UNLESS_TRUSTED, 'return group;'].includes(read[1]) && + unless.stops && bodyIs( 'readProvenProgramGroup', `const record = await readProgramRecord(sessionDirectory); if (typeof record !== 'object' || !hasToken(record)) { return null; } ${UNSHARED_RETURN}`, ) && bodyIs('hasToken', 'return record.bootId !== null;'), - trustsDestroyed: found[1] === STOP_UNLESS_TRUSTED, + trustsDestroyed: read[1] === RETURN_UNLESS_TRUSTED, + skipsUnreadable: unless.skipsUnreadable, }; } @@ -1404,6 +1504,53 @@ function rerunFacts() { }; } +// judgeFrozenGroup freezes and judges at most FROZEN_JUDGEMENTS times: SIGSTOP +// where /proc shows this process's pid space, a judgement, and SIGCONT in a +// finally. A frozen judgement other than gone decides; gone freezes again, +// and gone after the last freeze is inconclusive, so gc judges again. +function frozenJudgesTwice() { + const module = 'src/host/programGroup.ts'; + const limit = requireDeclaration(module, 'FROZEN_JUDGEMENTS').initializer; + const statements = requireDeclaration(module, 'judgeFrozenGroup').body + .statements; + const loop = statements[0]; + if ( + limit === undefined || + !ts.isNumericLiteral(limit) || + !Number.isInteger(Number(limit.text)) || + Number(limit.text) < 1 || + statements.length !== 2 || + loop === undefined || + !ts.isForStatement(loop) || + !ts.isBlock(loop.statement) || + normalize(statements[1].getText()) !== 'return null;' + ) { + return false; + } + const head = normalize( + `${loop.initializer?.getText()}; ${loop.condition?.getText()}; ${loop.incrementor?.getText()}`, + ); + const [stop, declared, judged, decides, ...rest] = loop.statement.statements; + return ( + head === 'let frozen = 0; frozen < FROZEN_JUDGEMENTS; frozen += 1' && + rest.length === 0 && + normalize(stop?.getText() ?? '') === + "if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { return false; }" && + normalize(declared?.getText() ?? '') === + "let verdict: GroupJudgement['verdict'];" && + judged !== undefined && + ts.isTryStatement(judged) && + judged.catchClause === undefined && + judged.finallyBlock !== undefined && + statementsOf(judged.tryBlock).join('\n') === + 'verdict = judgeLiveGroup(group).verdict;' && + statementsOf(judged.finallyBlock).join('\n') === + "signalProcessGroup(group.pid, 'SIGCONT');" && + normalize(decides?.getText() ?? '') === + "if (verdict !== 'gone') { return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; }" + ); +} + function gcFacts() { const fn = requireDeclaration('src/cli/commands/gc.ts', 'gcSessions'); let loop; @@ -1536,11 +1683,7 @@ function gcFacts() { probes && last === 'return live === null ? true : live ? null : judgeFrozenGroup(group);' && - body('judgeFrozenGroup').join('\n') === - [ - "if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { return false; }", - "try { const { verdict } = judgeLiveGroup(group); return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; } finally { signalProcessGroup(group.pid, 'SIGCONT'); }", - ].join('\n'); + frozenJudgesTwice(); return { GcSkipsNonCollectable: reconcile >= 0 && collectable > reconcile, GcFinalCheck: finalCheck, @@ -1599,6 +1742,9 @@ const COVERED = [ ['src/host/programGroup.ts', 'provenProgramGroupRuns'], ['src/host/programGroup.ts', 'judgeGroupForGc'], ['src/host/programGroup.ts', 'judgeFrozenGroup'], + ['src/host/programGroup.ts', 'FROZEN_JUDGEMENTS'], + ['src/host/programGroup.ts', 'isUnreadableGroupError'], + ['src/host/programGroup.ts', 'UNREADABLE_ERRNOS'], ['src/host/programGroup.ts', 'GC_JUDGEMENTS'], ['src/host/programGroup.ts', 'probeFindsGroup'], ['src/host/lifecycle.ts', 'allocateSession'], diff --git a/docs/USAGE.md b/docs/USAGE.md index 9ec4760b..c7a7da90 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -316,6 +316,7 @@ agent-tty record diff --at-seq-a 0 --json On Linux it also ends those processes when the program has already exited or the session has failed. A group whose processes each fork their successor and end too fast for any scan of `/proc` to show one, a fork chain, gets SIGSTOP first. Its stopped processes stay in view, so `destroy` can prove the group and kill it. A frozen group that agent-tty cannot prove is the session's gets SIGCONT. `destroy --force` kills the host and the program's group without asking the host first. +When a read of the program's group fails with an error that every later read repeats, such as `program.json` that refuses the read (EACCES) or a `/proc` scan that fails (EIO), `gc` keeps the session and reports "failed to check the session's program group (destroy --force removes it)", or "failed to reconcile session (destroy --force removes it)" for a session whose host died. Those errors are EACCES, EPERM, EIO, EISDIR, ENOTDIR, ELOOP and ENAMETOOLONG. A plain `destroy` fails on the same read. When the read of `program.json` or the first check of the group fails that way twice, 100 ms apart, `destroy --force` stops the host alone, without the group, and records the session as `destroyed` once the host has ended, so the next `gc` removes it. A process that the program left can outlive such a `destroy --force`. When the second read passes, `destroy --force` stops the group as usual. A read that fails after that first check, a group that reads alive, or a host that does not end (`HOST_TIMEOUT`) still fails it. Other errors, such as EMFILE, ENOMEM or EAGAIN, can pass, so `gc` gives no such hint and `destroy --force` fails on them too. A `host.json` that cannot be read counts as missing, so the group reads as out of view: `destroy --force` fails with `HOST_TIMEOUT`, and `gc` removes the session, as in another pid namespace. `list`, `inspect`, `destroy` and `gc` reconcile a session whose host died: they kill the program's group and record the session as `failed` (or `exited` or `destroyed`). A `destroy` that runs inside the session, such as one typed into the session's shell, runs again outside the session and prints its result once the session has ended. The session's terminal is closed by then, so redirect stdout to keep the result, for example `agent-tty destroy "$AGENT_TTY_SESSION_ID" --json > destroy.json`. @@ -368,7 +369,7 @@ Limits: 2. Some sessions have no autogroup record: sessions on macOS and Windows, on Linux kernels without autogroups (`/proc/self/autogroup` is missing), on Linux when `/proc` refuses to show the autogroup, the boot id or the host's pid namespace at start-up, and sessions that an agent-tty version without `program.json` created. For these sessions, `destroy --force`, reconcile and the host's own kill at shutdown or at the idle time-out kill the process group (on Windows, the process) that `session.json` names, without the check, so such a kill can reach an unrelated process that took the group id after the program's group ended. `destroy` of a session whose program has already exited kills nothing. A `program.json` that agent-tty cannot read as a record, for example one that a newer version wrote, proves nothing: `destroy` and reconcile kill nothing for that session. 3. The check and the kill are separate system calls, a few microseconds apart. If every process of the group exits and an unrelated process takes the group id in that time, the kill reaches the unrelated process. No system call kills a process group through a handle, so this window remains. A group that no scan shows gets SIGSTOP before each check and SIGCONT when the checks fail. `gc` sends the same two signals to a group whose scans show only zombies while its id still names a process (see item 5). A CLI whose `/proc` belongs to another pid namespace sends no SIGSTOP. If the unrelated group is a job of an interactive shell, the shell reports the job as stopped, and after the SIGCONT the job runs in the background. If agent-tty itself dies between the two signals (SIGKILL, SIGINT, SIGTERM, SIGHUP, or the out-of-memory killer), an unrelated group that took the id stays stopped, and a later `destroy` does not resume it. Resume it with `kill -CONT -- -`, where `` is the Child PID that `inspect` shows. 4. The host writes `program.json` a few milliseconds after it starts the program. We timed 150 `create` calls on Linux, from the return of node-pty's spawn to the renamed `program.json`, at 1-minute load averages of 38 to 83: the median was 2.8 ms, the 90th percentile 4.3 ms, and the longest 66 ms. If the host dies in that window and the program ignores the hang-up signal, no file names the program, and `destroy` cannot end it. -5. `gc` kills nothing. It keeps the folder of a session that is not `destroyed` only while it proves that the program's group runs: the autogroup record in `program.json` proves that a live process of the group is the program's, or the group id still names a process that no scan of `/proc` shows, such as a fast fork chain. When the scans show only zombies of the group while its id still names a process, as for a fork chain under a PID 1 that never reaps, `gc` sends the group SIGSTOP, checks it again, and sends SIGCONT. It then reports "the session's program group still runs (destroy ends it)". When `gc` cannot check the group, it removes `program.json` with the folder, as it does without an autogroup record (see item 2). That happens in another pid namespace than the one that `host.json` names, for example after a container restart that keeps the agent-tty home, and when `/proc` refuses the boot id or the autogroup of a live process of the group, or hides the processes of other users. Otherwise such a session would stay forever, because no `destroy` can prove its group gone. A process that the program left can then no longer be stopped by agent-tty. Run `destroy` before `gc` when a program can leave processes behind. +5. `gc` kills nothing. It keeps the folder of a session that is not `destroyed` only while it proves that the program's group runs: the autogroup record in `program.json` proves that a live process of the group is the program's, or the group id still names a process that no scan of `/proc` shows, such as a fast fork chain. When the scans show only zombies of the group while its id still names a process, as for a fork chain under a PID 1 that never reaps, `gc` sends the group SIGSTOP, checks it again, and sends SIGCONT, up to twice in each of up to ten checks of the group, and it keeps the session only when such a check proves the group. A group that has ended gets all 20 frozen checks: with about 2,300 processes in `/proc`, they took about 3.5 s at a load of 90. Another `gc` or a `destroy` that runs at the same time can send SIGCONT before a frozen check. Only when that happens before all 20 of them can a live process of the chain escape every scan, and `gc` then removes the folder of a session whose group still runs. A kept session gets the reason "the session's program group still runs (destroy ends it)". When `gc` cannot check the group, it removes `program.json` with the folder, as it does without an autogroup record (see item 2). That happens in another pid namespace than the one that `host.json` names, for example after a container restart that keeps the agent-tty home, when `host.json` cannot be read, and when `/proc` refuses the boot id or the autogroup of a live process of the group, or hides the processes of other users. Otherwise such a session would stay forever, because no `destroy` can prove its group gone. A process that the program left can then no longer be stopped by agent-tty. Run `destroy` before `gc` when a program can leave processes behind. 6. Two cases where agent-tty cannot run the check end differently from a session that stays running: - At the idle time-out, a host that cannot run the check kills nothing, but it still records the session as `exited` once the program has exited, while a process that the program left can still run. A later `destroy` then fails with `HOST_TIMEOUT`, and `gc` can remove the session folder. - When `/proc` hides the processes of other users (mounted with `hidepid=2`, `hidepid=4`, `hidepid=invisible` or `hidepid=ptraceable`), a group whose processes agent-tty cannot see counts as running. A `destroy` that cannot prove such a group gone fails with `HOST_TIMEOUT` and does not record the session as `destroyed`. diff --git a/src/cli/commands/gc.ts b/src/cli/commands/gc.ts index d1bb1134..a793168a 100644 --- a/src/cli/commands/gc.ts +++ b/src/cli/commands/gc.ts @@ -8,7 +8,11 @@ import { reconcileSession, removeDeadHostSocket, } from '../../host/lifecycle.js'; -import { provenProgramGroupRuns } from '../../host/programGroup.js'; +import { + forceSkipsGroup, + isUnreadableGroupError, + provenProgramGroupRuns, +} from '../../host/programGroup.js'; import { ERROR_CODES, makeCliError } from '../../protocol/errors.js'; import { isCollectableSessionStatus, @@ -98,6 +102,10 @@ export interface GcDependencies { manifest: SessionRecord, ) => Promise; provenProgramGroupRuns: (sessionDirectory: string) => Promise; + forceSkipsGroup: ( + sessionDirectory: string, + childPid: number | null, + ) => Promise; now: () => Date; } @@ -109,6 +117,7 @@ const defaultDependencies: GcDependencies = { reconcileSession, removeDeadHostSocket, provenProgramGroupRuns, + forceSkipsGroup, now: () => new Date(), }; @@ -289,6 +298,15 @@ export function parseDurationToMs(value: string): number { return durationMs; } +// A read of the program's group that fails with one of UNREADABLE_ERRNOS +// fails every later check too. destroy --force ends such a session without +// the read. +const FORCE_HINT = ' (destroy --force removes it)'; + +function forceRemovesIt(error: unknown): string { + return isUnreadableGroupError(error) ? FORCE_HINT : ''; +} + export async function gcSessions( home: string, options: GcExecutionOptions, @@ -368,9 +386,17 @@ export async function gcSessions( try { await dependencies.reconcileSession(sessionDirectory); } catch (error) { + // A reconcile also writes the manifest and removes the socket, so gc + // names destroy --force only when the read of the group fails too. + const skips = + isUnreadableGroupError(error) && + (await dependencies.forceSkipsGroup( + sessionDirectory, + manifestBefore.childPid, + )); result.skippedSessions.push({ sessionId: manifestBefore.sessionId, - reason: `failed to reconcile session: ${getErrorMessage(error)}`, + reason: `failed to reconcile session${skips ? FORCE_HINT : ''}: ${getErrorMessage(error)}`, }); continue; } @@ -434,7 +460,7 @@ export async function gcSessions( } catch (error) { result.skippedSessions.push({ sessionId, - reason: `failed to check the session's program group: ${getErrorMessage(error)}`, + reason: `failed to check the session's program group${forceRemovesIt(error)}: ${getErrorMessage(error)}`, }); continue; } diff --git a/src/host/README.md b/src/host/README.md index e52580d3..95238824 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -55,9 +55,9 @@ - The `signal` handler accepts only `SIGTERM`, `SIGINT`, `SIGKILL`, `SIGHUP`, `SIGUSR1` and `SIGUSR2`, and throws `INVALID_SIGNAL` for others. [hostMain.ts:runHost] - The `run` handler waits 30,000 ms by default. The `wait` handler needs exactly one of `exit` or `idleMs`, else it throws `INVALID_DURATION`. `waitForRender` polls every `RENDER_WAIT_POLL_INTERVAL_MS` (200 ms, `src/renderWait/limits.ts`). [hostMain.ts:runHost] - `runHost` handles PTY exit once. If the status is `destroying` it records `destroyed`, else `exited`. Shutdown runs once. [hostMain.ts:runHost] -- `destroySession` throws `SESSION_NOT_FOUND` when there is no manifest, or when the session directory is gone at its `destroyed` write, and `SESSION_ALREADY_DESTROYED` for a destroyed session. When it records `destroyed` itself, `recordDestroyed` first writes the empty `/destroyed` marker with `writeDestroyMarker`. Before it records a terminal session as `destroyed`, it calls `stopProgramGroup` with the group from `readProvenProgramGroup`, so only a group with a token gets a signal, and it throws `HOST_TIMEOUT` while that group lives. A session already recorded `destroyed` with the unshared group gets no wait, because only a process that saw the group recorded it, after its wait. A running session gets the `destroy` RPC. With `force` it gets `SIGKILL` for the program's group and, only when `hostMatches` proves the host, for the host: on Linux `judgeHost` must return `alive`, elsewhere `/bin/ps` must show `_host `, and on Windows the host gets no signal. It polls every 100 ms for at most 50 attempts and throws `HOST_TIMEOUT` if the status is still not terminal. [lifecycle.ts:destroySession] +- `destroySession` throws `SESSION_NOT_FOUND` when there is no manifest, or when the session directory is gone at its `destroyed` write, and `SESSION_ALREADY_DESTROYED` for a destroyed session. When it records `destroyed` itself, `recordDestroyed` first writes the empty `/destroyed` marker with `writeDestroyMarker`. Before it records a terminal session as `destroyed`, it calls `stopProgramGroup` with the group from `readProvenProgramGroup`, so only a group with a token gets a signal, and it throws `HOST_TIMEOUT` while that group lives. A session already recorded `destroyed` with the unshared group gets no wait, because only a process that saw the group recorded it, after its wait. A running session gets the `destroy` RPC. With `force` it gets `SIGKILL` for the program's group and, only when `hostMatches` proves the host, for the host: on Linux `judgeHost` must return `alive`, elsewhere `/bin/ps` must show `_host `, and on Windows the host gets no signal. It polls every 100 ms for at most 50 attempts and throws `HOST_TIMEOUT` if the status is still not terminal. With `force`, when the read of `program.json` or the first `isProgramGroupAlive` of the group throws an error that `isUnreadableGroupError` accepts (a `STORAGE_READ_ERROR` whose cause, or a `/proc` read whose code, is in `UNREADABLE_ERRNOS`), `stopUnlessUnreadable` waits `DESTROY_POLL_INTERVAL_MS` (100 ms, abortable) and reads and judges the group again. Only when that read throws such an error too does it stop and wait for the host alone, and `destroySession` records `destroyed` once the host has ended. An error after that first judgement, as in the wait, still throws. `forceSkipsGroup` runs that read and first judgement and returns whether such an error came, so `gcSessions` names `destroy --force` for a failed reconcile only then. [lifecycle.ts:destroySession] [programGroup.ts:isUnreadableGroupError] [programGroup.ts:forceSkipsGroup] - `reconcileSession` writes `destroyed` (both PIDs `null`, the exit code kept, no failure fields) over a terminal manifest other than `destroyed` when the destroy marker exists (`writeMarkedDestroyed`). It then unlinks the socket, removes the Home's socket directory if it is empty, removes the old socket at `legacySocketPath` when `isOwnLegacySocket` accepts it, and returns. Otherwise it does nothing when the manifest is missing, the status is terminal or the host can be alive: `judgeHost` with the record from `host.json` does not return `dead`. A null `hostPid` counts as a dead host. `allocateSession` writes the host PID into the first manifest, so a new session already has a `hostPid`. After the liveness check, `reconcileSession` reads the manifest again and does nothing when it is now missing or terminal. Otherwise it maps the status it read again: `running` to `failed` (failure origin `host-death`), `exiting` to `exited`, `destroying` to `destroyed` and any other status to `failed` (origin `unknown`), and sets both PIDs to `null`. Right after that write, when its status was not `destroyed` and the destroy marker exists, it writes `destroyed` again from the same copy, with both PIDs `null` and no failure fields. When the session directory is gone at any of these writes, it returns. [lifecycle.ts:reconcileSession] [lifecycle.ts:writeMarkedDestroyed] -- Every kill of the program's process group goes through `stopProgramGroup`. For a record with a token, `judgeProgramGroup` returns `owned` only when a process that is not a zombie (a process whose main thread exited is not one while another of its threads runs) has the program's pid as its process group and session id, and the recorded autogroup on the recorded boot. A scan that finds no live member runs once more, because a member can fork and end after the scan listed `/proc`. `stopProgramGroup` reads that process again right before the kill. `unproven` (another boot id, or only members with another session id or autogroup) and `unknown` kill nothing. `gone` (no live member) sends the group SIGSTOP with `signalProcessGroup`, because a fork chain whose members each live about 2 ms is never in view, and a stopped member is. The judge then runs again, up to 5 times, and each judgement that reads `gone` sends SIGSTOP again, for a member that a SIGCONT from elsewhere resumed. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace and no SIGSTOP goes out. A frozen group that gets no kill gets SIGCONT, also when a scan throws. So a group id that an unrelated group took, whose members no scan shows either, gets a SIGSTOP and a SIGCONT. `unknown` means that `/proc` refused the boot id, or showed a member with the program's session id but no autogroup, so `isProgramGroupAlive` reads it alive. A record without a token gets the kill of its `pid`. A `{ childPid, sessionDirectory }` group gets the kill of `childPid`, and reads alive, only while `sessionDirectory` exists, checked in the same synchronous block. The unshared group `{ unshared: true }`, which a record with a token gives when `host.json` names another pid space or is missing, gets no signal and reads alive. [programGroup.ts:stopProgramGroup] [programGroup.ts:judgeProgramGroup] +- Every kill of the program's process group goes through `stopProgramGroup`. For a record with a token, `judgeProgramGroup` returns `owned` only when a process that is not a zombie (a process whose main thread exited is not one while another of its threads runs) has the program's pid as its process group and session id, and the recorded autogroup on the recorded boot. A scan that finds no live member runs once more, because a member can fork and end after the scan listed `/proc`. `stopProgramGroup` reads that process again right before the kill. `unproven` (another boot id, or only members with another session id or autogroup) and `unknown` kill nothing. `gone` (no live member) sends the group SIGSTOP with `signalProcessGroup`, because a fork chain whose members each live about 2 ms is never in view, and a stopped member is. The judge then runs again, up to 5 times, and each judgement that reads `gone` sends SIGSTOP again, for a member that a SIGCONT from elsewhere resumed. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace and no SIGSTOP goes out. A frozen group that gets no kill gets SIGCONT, also when a scan throws. So a group id that an unrelated group took, whose members no scan shows either, gets a SIGSTOP and a SIGCONT. `unknown` means that `/proc` refused the boot id, or showed a member with the program's session id but no autogroup, so `isProgramGroupAlive` reads it alive. A record without a token gets the kill of its `pid`. A `{ childPid, sessionDirectory }` group gets the kill of `childPid`, and reads alive, only while `sessionDirectory` exists, checked in the same synchronous block. The unshared group `{ unshared: true }`, which a record with a token gives when `host.json` names another pid space, is missing or cannot be read (`readHostRecord` reads a failed read as missing), gets no signal and reads alive. [programGroup.ts:stopProgramGroup] [programGroup.ts:judgeProgramGroup] - `captureProgram` records a token only on Linux, for its own child that leads its own session and has an autogroup other than the host's, within 250 ms, and only when `/proc` shows the boot id. `runHost` calls it right after `createPty` and writes the record before its first manifest write, with no `await` in between. [programGroup.ts:captureProgram] [hostMain.ts:runHost] - `allocateSession` throws `INVALID_DIMENSIONS` for non-positive `cols` or `rows`, `STORAGE_READ_ERROR` when `cwd` is not a directory and `INVALID_INPUT` when the shell path is not a file. An empty `command` defaults to the shell path. It creates the session directory and calls `launch` only after these checks pass. [lifecycle.ts:allocateSession] - `buildReplayInput` validates the manifest with `SessionRecordSchema` and requires its `sessionId` to match. It validates the events with `validateEventRecords` unless `trustValidated` is set. `targetSeq` is -1 for no events, else from 0 to the last `seq`. [replay.ts:buildReplayInput] diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index 5f7a184a..20510e35 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -35,6 +35,7 @@ import { invariant } from '../util/assert.js'; import { hasErrorCode } from '../util/hasErrorCode.js'; import { isProgramGroupAlive, + isUnreadableGroupError, parseProcStat, readProgramGroup, readProvenProgramGroup, @@ -910,22 +911,73 @@ export async function destroySession( }); } - const stopLeftoversThenRecordDestroyed = async ( - terminal: SessionRecord, - ): Promise => { - const group = await readProvenProgramGroup(sessionDirectory); - // Only a process that sees the program's group records destroyed, after - // a wait that read the group gone. So a destroyed record needs no wait - // for a group out of view. + // destroy --force of a session whose host is gone also ends a session + // whose program group it cannot read: the read of program.json, or the + // first judgement of the group, fails with an errno that every later read + // repeats, twice, 100 ms apart. It then stops what it can without the + // group and records destroyed, so a process that the program left can + // outlive it. A failed read after that first judgement, a group that reads + // alive, and a host that does not end (HOST_TIMEOUT) still fail the + // destroy. + const stopUnlessUnreadable = async ( + host: SessionHost | null, + readGroup: () => Promise, + ): Promise => { + const readAndJudge = async (): Promise => { + const group = await readGroup(); + isProgramGroupAlive(group); + return group; + }; + let group: ProgramGroup | null; + try { + group = await readAndJudge(); + } catch (error) { + if (force !== true || !isUnreadableGroupError(error)) { + throw error; + } + // A read that fails once, as on a network file system, can pass the + // next time. + await pollDelay(DESTROY_POLL_INTERVAL_MS, signal); + try { + group = await readAndJudge(); + } catch (secondError) { + if (!isUnreadableGroupError(secondError)) { + throw secondError; + } + await stopSessionProcesses( + sessionId, + host, + null, + sessionDirectory, + signal, + ); + return null; + } + } await stopSessionProcesses( sessionId, - null, - terminal.status === 'destroyed' && group !== null && 'unshared' in group - ? null - : group, + host, + group, sessionDirectory, signal, ); + return group; + }; + + const stopLeftoversThenRecordDestroyed = async ( + terminal: SessionRecord, + ): Promise => { + await stopUnlessUnreadable(null, async () => { + const group = await readProvenProgramGroup(sessionDirectory); + // Only a process that sees the program's group records destroyed, + // after a wait that read the group gone. So a destroyed record needs no + // wait for a group out of view. + return terminal.status === 'destroyed' && + group !== null && + 'unshared' in group + ? null + : group; + }); await recordDestroyed(manifestFile, socketFile, terminal, null); }; @@ -935,23 +987,16 @@ export async function destroySession( } if (force === true) { - await stopSessionProcesses( - sessionId, + await stopUnlessUnreadable( await readSessionHost(sessionDirectory, manifest), - await readProgramGroup(sessionDirectory, manifest.childPid), - sessionDirectory, - signal, + () => readProgramGroup(sessionDirectory, manifest.childPid), ); // The host is dead now, so this read is final. It can name a child that // the first read did not. const current = await readSessionManifestOrThrow(sessionId, manifestFile); - const group = await readProgramGroup(sessionDirectory, current.childPid); - await stopSessionProcesses( - sessionId, + const group = await stopUnlessUnreadable( await readSessionHost(sessionDirectory, current), - group, - sessionDirectory, - signal, + () => readProgramGroup(sessionDirectory, current.childPid), ); await recordDestroyed(manifestFile, socketFile, current, group); return; diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index 3050a703..118a53d4 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -3,6 +3,7 @@ import process from 'node:process'; import { z } from 'zod'; +import { CliError } from '../cli/errors.js'; import { ERROR_CODES, makeCliError } from '../protocol/errors.js'; import { readValidatedJsonFile, @@ -296,6 +297,53 @@ async function readProgramRecord( } } +// The errnos of a read that a retry does not change: the permissions or the +// file system refuse it (EACCES, EPERM, EIO), or a path names no readable +// file (EISDIR, ENOTDIR, ELOOP, ENAMETOOLONG). EMFILE, ENFILE, ENOMEM, +// EAGAIN and EINTR pass, so a later read can succeed. +const UNREADABLE_ERRNOS = new Set([ + 'EACCES', + 'EPERM', + 'EIO', + 'EISDIR', + 'ENOTDIR', + 'ELOOP', + 'ENAMETOOLONG', +]); + +// Whether a read of the program's group failed in a way that every later +// read repeats: a read of program.json (STORAGE_READ_ERROR) or of /proc, +// with one of UNREADABLE_ERRNOS. A verdict, HOST_TIMEOUT, an abort or a bug +// is none of these. A host.json that cannot be read counts as missing, so +// its group reads unshared and throws nothing here. +export function isUnreadableGroupError(error: unknown): boolean { + const cause = hasErrorCode(error, ERROR_CODES.STORAGE_READ_ERROR) + ? (error as Error).cause + : error; + const code: unknown = + cause instanceof Error ? (cause as { code?: unknown }).code : undefined; + return ( + !(cause instanceof CliError) && + typeof code === 'string' && + UNREADABLE_ERRNOS.has(code) + ); +} + +// Whether destroy --force skips the program's group: the read of the group, +// or its first judgement, fails with an error that isUnreadableGroupError +// accepts. +export async function forceSkipsGroup( + sessionDirectory: string, + childPid: number | null, +): Promise { + try { + isProgramGroupAlive(await readProgramGroup(sessionDirectory, childPid)); + return false; + } catch (error) { + return isUnreadableGroupError(error); + } +} + export async function readProvenProgramGroup( sessionDirectory: string, ): Promise { @@ -642,24 +690,37 @@ function judgeGroupForGc(group: ProvenRecord): boolean | null { return live === null ? true : live ? null : judgeFrozenGroup(group); } +// A frozen judgement that reads gone is judged frozen once more, so a gc +// sends at most GC_JUDGEMENTS * FROZEN_JUDGEMENTS SIGSTOP and SIGCONT pairs. +const FROZEN_JUDGEMENTS = 2; + // The scans show only zombies of the group while the probe finds its id. // Under a PID 1 that never reaps, the zombies of a fork chain stay, and its // live member can escape both scans. SIGSTOP freezes the group, as in // stopProgramGroup, and a stopped member stays in view. Another gc or a // destroy can send SIGCONT before the judgement, so a frozen group that -// still reads gone is judged again, with another SIGSTOP. A group that -// ended reads gone each time, so the bounded loop of provenProgramGroupRuns -// then reads it ended. The group gets SIGCONT, also when a scan throws. +// still reads gone gets another SIGSTOP and judgement. When that one reads +// gone too, the judgement stays inconclusive, and provenProgramGroupRuns +// judges the group again. So gc reads a live fork chain ended only when a +// SIGCONT from elsewhere came before each of its frozen judgements and the +// chain's live member escaped every scan. The group gets SIGCONT, also when +// a scan throws. function judgeFrozenGroup(group: ProvenRecord): boolean | null { - if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { - return false; - } - try { - const { verdict } = judgeLiveGroup(group); - return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; - } finally { - signalProcessGroup(group.pid, 'SIGCONT'); + for (let frozen = 0; frozen < FROZEN_JUDGEMENTS; frozen += 1) { + if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { + return false; + } + let verdict: GroupJudgement['verdict']; + try { + verdict = judgeLiveGroup(group).verdict; + } finally { + signalProcessGroup(group.pid, 'SIGCONT'); + } + if (verdict !== 'gone') { + return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; + } } + return null; } function probeFindsGroup(pgid: number): boolean { diff --git a/test/integration/lifecycle.test.ts b/test/integration/lifecycle.test.ts index 868284fe..6acafec8 100644 --- a/test/integration/lifecycle.test.ts +++ b/test/integration/lifecycle.test.ts @@ -1115,6 +1115,129 @@ describe('lifecycle integration', { timeout: 60_000 }, () => { }, ); + // A read of program.json that fails with EACCES fails every later + // check too. destroy --force ends such a session without the read, so + // gc does not keep it forever. Root reads any file, so these tests skip + // under root. + async function statusOf(sessionId: string): Promise { + const manifest = JSON.parse( + await readFile( + join(testHome, 'sessions', sessionId, 'session.json'), + 'utf8', + ), + ) as { status: string }; + return manifest.status; + } + + it.runIf(process.getuid?.() !== 0)( + 'destroy --force ends an exited session whose program.json it cannot read', + async () => { + const sessionId = await createProgram( + `trap "" HUP; sleep 300 & ${untilRecorded()}; touch "$0"; exit 0`, + ); + const deadline = Date.now() + 10_000; + while ((await statusOf(sessionId)) !== 'exited') { + expect(Date.now()).toBeLessThan(deadline); + await sleep(100); + } + await chmod(join(testHome, 'sessions', sessionId, 'program.json'), 0); + + const kept = runCli(['gc', '--json'], { AGENT_TTY_HOME: testHome }); + expect(JSON.parse(kept.stdout)).toMatchObject({ + ok: true, + result: { + removedSessionCount: 0, + homes: [ + { + skippedSessions: [ + { + sessionId, + reason: expect.stringContaining( + 'destroy --force removes it', + ) as string, + }, + ], + }, + ], + }, + }); + const plain = runCli(['destroy', sessionId, '--json'], { + AGENT_TTY_HOME: testHome, + }); + expect(JSON.parse(plain.stdout)).toMatchObject({ ok: false }); + expect(await statusOf(sessionId)).toBe('exited'); + + const forced = runCli(['destroy', sessionId, '--force', '--json'], { + AGENT_TTY_HOME: testHome, + }); + expect( + (JSON.parse(forced.stdout) as { error?: unknown }).error, + ).toBeUndefined(); + expect(await statusOf(sessionId)).toBe('destroyed'); + // The documented trade-off: the process that the program left runs on. + expect(isGroupAlive(pgid)).toBe(true); + const removed = runCli(['gc', '--json'], { AGENT_TTY_HOME: testHome }); + expect(JSON.parse(removed.stdout)).toMatchObject({ + ok: true, + result: { removedSessionCount: 1 }, + }); + }, + ); + + it.runIf(process.getuid?.() !== 0)( + 'destroy --force ends a session whose host died and whose program.json it cannot read', + async () => { + const sessionId = await createProgram( + `trap "" HUP; ${untilRecorded()}; touch "$0"; exec sleep 300`, + ); + const sessionFile = join( + testHome, + 'sessions', + sessionId, + 'session.json', + ); + const { hostPid } = JSON.parse(await readFile(sessionFile, 'utf8')) as { + hostPid: number; + }; + process.kill(hostPid, 'SIGKILL'); + const deadline = Date.now() + 10_000; + while (isProcessAlive(hostPid)) { + expect(Date.now()).toBeLessThan(deadline); + await sleep(50); + } + await chmod(join(testHome, 'sessions', sessionId, 'program.json'), 0); + + const kept = runCli(['gc', '--json'], { AGENT_TTY_HOME: testHome }); + expect(JSON.parse(kept.stdout)).toMatchObject({ + ok: true, + result: { + removedSessionCount: 0, + homes: [ + { + skippedSessions: [ + { + sessionId, + reason: expect.stringContaining( + 'destroy --force removes it', + ) as string, + }, + ], + }, + ], + }, + }); + expect(await statusOf(sessionId)).toBe('running'); + + const forced = runCli(['destroy', sessionId, '--force', '--json'], { + AGENT_TTY_HOME: testHome, + }); + expect( + (JSON.parse(forced.stdout) as { error?: unknown }).error, + ).toBeUndefined(); + expect(await statusOf(sessionId)).toBe('destroyed'); + }, + ); + // A token proves the group only beside host.json, which names its pid // space, so a host that cannot record itself records no token. it.runIf(capturesToken)( diff --git a/test/unit/commands/gc.test.ts b/test/unit/commands/gc.test.ts index 754941d1..55995206 100644 --- a/test/unit/commands/gc.test.ts +++ b/test/unit/commands/gc.test.ts @@ -209,6 +209,7 @@ function createMockDependencies( }, provenProgramGroupRuns: (sessionDirectory: string) => Promise.resolve(runningGroups.has(sessionDirectory)), + forceSkipsGroup: () => Promise.resolve(false), }; return { @@ -451,6 +452,100 @@ describe('gc command helpers', () => { expect(socketCleanups).toEqual([`${home}/sessions/exited-01 exited`]); }); + it('names destroy --force when a read of the group fails with a system error', async () => { + const home = '/tmp/agent-tty'; + const { dependencies, removedPaths } = createMockDependencies(home, { + 'unreadable-01': { + manifest: createSessionRecord({ + sessionId: 'unreadable-01', + status: 'exited', + createdAt: '2026-03-20T08:00:00.000Z', + }), + }, + }); + dependencies.provenProgramGroupRuns = () => + Promise.reject( + Object.assign(new Error('EIO: i/o error, scandir /proc'), { + code: 'EIO', + }), + ); + + const result = await gcSessions( + home, + { dryRun: false, staleOnly: false, olderThanMs: null }, + dependencies, + ); + + expect(result.skippedSessions).toEqual([ + { + sessionId: 'unreadable-01', + reason: + "failed to check the session's program group (destroy --force removes it): EIO: i/o error, scandir /proc", + }, + ]); + expect(removedPaths).toEqual([]); + }); + + it('names destroy --force for a failed reconcile only when the read of the group fails too', async () => { + const home = '/tmp/agent-tty'; + const running = (sessionId: string) => ({ + manifest: createSessionRecord({ + sessionId, + status: 'running', + createdAt: '2026-03-20T08:00:00.000Z', + }), + }); + const { dependencies, removedPaths } = createMockDependencies(home, { + 'socket-01': running('socket-01'), + 'unreadable-01': running('unreadable-01'), + 'transient-01': running('transient-01'), + }); + const failure = (code: string) => + Object.assign(new Error(`${code}: unlink of the socket failed`), { + code, + }); + dependencies.reconcileSession = (sessionDirectory: string) => + Promise.reject( + failure( + sessionDirectory.endsWith('transient-01') ? 'EMFILE' : 'EACCES', + ), + ); + const asked: string[] = []; + dependencies.forceSkipsGroup = (sessionDirectory, childPid) => { + asked.push(`${sessionDirectory} ${String(childPid)}`); + return Promise.resolve(sessionDirectory.endsWith('unreadable-01')); + }; + + const result = await gcSessions( + home, + { dryRun: false, staleOnly: false, olderThanMs: null }, + dependencies, + ); + + expect(result.skippedSessions).toEqual([ + { + sessionId: 'socket-01', + reason: + 'failed to reconcile session: EACCES: unlink of the socket failed', + }, + { + sessionId: 'unreadable-01', + reason: + 'failed to reconcile session (destroy --force removes it): EACCES: unlink of the socket failed', + }, + { + sessionId: 'transient-01', + reason: + 'failed to reconcile session: EMFILE: unlink of the socket failed', + }, + ]); + expect(asked).toEqual([ + `${home}/sessions/socket-01 456`, + `${home}/sessions/unreadable-01 456`, + ]); + expect(removedPaths).toEqual([]); + }); + it('reports removals in dry-run mode without deleting anything', async () => { const home = '/tmp/agent-tty'; const { dependencies, removedPaths, bytesBySession } = diff --git a/test/unit/host/lifecycle.test.ts b/test/unit/host/lifecycle.test.ts index 4f6b57a5..cc9cf83f 100644 --- a/test/unit/host/lifecycle.test.ts +++ b/test/unit/host/lifecycle.test.ts @@ -971,6 +971,99 @@ describe('destroySession', () => { }); }); + // Only a read that fails before the first verdict on the group lets + // destroy --force record destroyed without it. After a verdict that + // the group runs, a failed read leaves the group running. + it('destroy --force fails, and records nothing, when a read fails after the group read owned', async () => { + const directory = await seedLeftover(); + const stat = `/proc/${String(group)}/stat`; + let reads = 0; + fsHooks.files = new (class extends Map { + override get(path: string): string | Error | undefined { + if (path !== stat) { + return undefined; + } + reads += 1; + return reads > 1 ? errno('EIO') : undefined; + } + })(); + const kill = vi.spyOn(process, 'kill'); + + await expect(destroySession('session-01', true)).rejects.toMatchObject({ + code: 'EIO', + }); + expect(kill).not.toHaveBeenCalledWith(-group, 'SIGKILL'); + expect(await readManifest(manifestPath(directory))).toEqual(exited); + expect(reads).toBeGreaterThan(1); + }); + + it('destroy --force records destroyed, and kills nothing, when the first read of the group fails twice', async () => { + const directory = await seedLeftover(); + fsHooks.files = new Map([ + [`/proc/${String(group)}/stat`, errno('EIO')], + ]); + const kill = vi.spyOn(process, 'kill'); + + await destroySession('session-01', true); + + expect(kill).not.toHaveBeenCalledWith(-group, 'SIGKILL'); + expect(await readManifest(manifestPath(directory))).toMatchObject({ + status: 'destroyed', + }); + }); + + // A read can fail once, as on a network file system, and pass the + // next time, 100 ms later. + it('destroy --force kills the group when only the first read of the group fails', async () => { + const directory = await seedLeftover(); + const stat = `/proc/${String(group)}/stat`; + let reads = 0; + fsHooks.files = new (class extends Map { + override get(path: string): string | Error | undefined { + if (path !== stat) { + return undefined; + } + reads += 1; + return reads === 1 ? errno('EIO') : undefined; + } + })(); + const kill = vi.spyOn(process, 'kill'); + + await destroySession('session-01', true); + + expect(kill).toHaveBeenCalledWith(-group, 'SIGKILL'); + expect(await readManifest(manifestPath(directory))).toMatchObject({ + status: 'destroyed', + }); + expect(reads).toBeGreaterThan(1); + }); + + it('destroy --force stops at an abort between the two reads of the group', async () => { + const directory = await seedLeftover(); + const controller = new AbortController(); + const reason = new Error('destroy aborted'); + const stat = `/proc/${String(group)}/stat`; + let reads = 0; + fsHooks.files = new (class extends Map { + override get(path: string): string | Error | undefined { + if (path !== stat) { + return undefined; + } + reads += 1; + controller.abort(reason); + return errno('EIO'); + } + })(); + const kill = vi.spyOn(process, 'kill'); + + await expect( + destroySession('session-01', true, { signal: controller.signal }), + ).rejects.toBe(reason); + expect(reads).toBe(1); + expect(kill).not.toHaveBeenCalledWith(-group, 'SIGKILL'); + expect(await readManifest(manifestPath(directory))).toEqual(exited); + }); + it('times out without recording destroyed while the group survives its kill', async () => { const directory = await seedLeftover(); const send = process.kill.bind(process); diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index c16572b6..ec703008 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -18,7 +18,9 @@ import { afterEach, beforeEach, describe, expect, it, vi } from 'vitest'; import { captureProgram, + forceSkipsGroup, isProgramGroupAlive, + isUnreadableGroupError, judgeProgramGroup, parseAutogroup, parseProcStat, @@ -30,6 +32,7 @@ import { type ProcessRow, type ProgramRecord, } from '../../../src/host/programGroup.js'; +import { ERROR_CODES, makeCliError } from '../../../src/protocol/errors.js'; import { programRecordPath, sessionDir, @@ -1029,7 +1032,6 @@ describe('a program group with a token, as a faked /proc shows it', () => { 0, 'SIGSTOP', 'SIGCONT', - 0, 'SIGSTOP', 'SIGCONT', ]); @@ -1038,8 +1040,9 @@ describe('a program group with a token, as a faked /proc shows it', () => { } }); - // GC_JUDGEMENTS bounds the judgements of a group that ended. - it('reads a group that shows only zombies, also frozen, ended after ten judgements', async () => { + // Two frozen judgements that read gone stay inconclusive, so gc judges + // the group again, and reads it ended only after the last judgement. + it('reads a group that shows only zombies, frozen twice in each of ten judgements, ended', async () => { const directory = await recordedSession(); try { procShowsTokenGroup('Z'); @@ -1051,13 +1054,140 @@ describe('a program group with a token, as a faked /proc shows it', () => { expect(await provenProgramGroupRuns(directory)).toBe(false); expect(signals).toEqual( - Array.from({ length: 10 }, () => [0, 'SIGSTOP', 'SIGCONT']).flat(), + Array.from({ length: 10 }, () => [ + 0, + 'SIGSTOP', + 'SIGCONT', + 'SIGSTOP', + 'SIGCONT', + ]).flat(), ); } finally { await rm(directory, { recursive: true, force: true }); } }); + // A SIGCONT from another gc or a destroy before both frozen judgements + // lets the live member escape them. The next judgement still finds it. + it('keeps the session when a live member escapes both frozen judgements of one pass', async () => { + const directory = await recordedSession(); + try { + procShowsTokenGroup('Z'); + const signals: unknown[] = []; + let stops = 0; + vi.spyOn(process, 'kill').mockImplementation((_pid, signal) => { + signals.push(signal); + if (signal === 'SIGSTOP') { + stops += 1; + if (stops === 3) { + procShowsTokenGroup('Z', 'T'); + } + } + return true; + }); + + expect(await provenProgramGroupRuns(directory)).toBe(true); + expect(signals).toEqual([ + 0, + 'SIGSTOP', + 'SIGCONT', + 'SIGSTOP', + 'SIGCONT', + 0, + 'SIGSTOP', + 'SIGCONT', + ]); + } finally { + await rm(directory, { recursive: true, force: true }); + } + }); + + // A member of another session or autogroup that took the id is not the + // program's, and it gets its SIGCONT. + it.each([ + { + member: 'another autogroup', + frozen: () => { + procShowsTokenGroup('Z', 'T'); + const read = autogroupFile.read; + autogroupFile.read = (file) => + file === '/proc/101/autogroup' + ? '/autogroup-9 nice 0\n' + : (read?.(file) ?? null); + }, + }, + { + member: 'another session', + frozen: () => { + procShowsTokenGroup('Z'); + procHooks.stat?.set( + '101', + `101 (a) T 1 ${String(CHILD_PID)} 4242 ${STAT_TAIL}`, + ); + }, + }, + ])( + 'reads a frozen group whose live member is in $member ended, and resumes it', + async ({ frozen }) => { + const directory = await recordedSession(); + try { + procShowsTokenGroup('Z'); + const signals: unknown[] = []; + vi.spyOn(process, 'kill').mockImplementation((_pid, signal) => { + signals.push(signal); + if (signal === 'SIGSTOP') { + frozen(); + } + return true; + }); + + expect(await provenProgramGroupRuns(directory)).toBe(false); + expect(signals).toEqual([0, 'SIGSTOP', 'SIGCONT']); + } finally { + await rm(directory, { recursive: true, force: true }); + } + }, + ); + + // A /proc that names another pid than this process's belongs to another + // pid namespace, so the group reads unshared and gc sends no signal. + it('sends no signal when /proc/self names another pid', async () => { + const directory = await recordedSession(); + try { + procShowsTokenGroup('Z'); + procHooks.self = '1'; + const kill = vi.spyOn(process, 'kill').mockReturnValue(true); + + expect(await provenProgramGroupRuns(directory)).toBe(false); + expect(kill).not.toHaveBeenCalled(); + } finally { + await rm(directory, { recursive: true, force: true }); + } + }); + + // sharesHostPids read /proc/self as this process's pid a moment before, + // so only a /proc that changed since, such as one mounted over it, + // reaches the guard of the freeze. The probe changes it here. + it('sends no SIGSTOP when /proc/self names another pid at the freeze', async () => { + const directory = await recordedSession(); + try { + procShowsTokenGroup('Z'); + const signals: unknown[] = []; + vi.spyOn(process, 'kill').mockImplementation((_pid, signal) => { + signals.push(signal); + if (signal === 0) { + procHooks.self = '1'; + } + return true; + }); + + expect(await provenProgramGroupRuns(directory)).toBe(false); + expect(signals).toEqual([0]); + } finally { + await rm(directory, { recursive: true, force: true }); + } + }); + it('gives a frozen group SIGCONT when its judgement throws', async () => { const directory = await recordedSession(); try { @@ -1655,6 +1785,23 @@ describe.runIf(platform === 'linux')('a program record with a token', () => { }); }); + // gc names destroy --force for a failed reconcile only after this check. + it('skips the group for destroy --force only when its first read fails for good', async () => { + recordHostIn(readlinkSync('/proc/self/ns/pid')); + expect(await forceSkipsGroup(directory, 4242)).toBe(false); + + procHooks.listError = errno('EMFILE'); + expect(await forceSkipsGroup(directory, 4242)).toBe(false); + + procHooks.listError = errno('EIO'); + expect(await forceSkipsGroup(directory, 4242)).toBe(true); + + procHooks.listError = undefined; + await rm(programRecordPath(directory)); + await mkdir(programRecordPath(directory)); + expect(await forceSkipsGroup(directory, 4242)).toBe(true); + }); + // Only an agent-tty version between program.json and host.json wrote a // token without host.json, and nothing names its pid space. it('reads alive and gets no kill without a host record', async () => { @@ -1687,3 +1834,48 @@ describe.runIf(platform === 'linux')('a program record with a token', () => { expect(kill).not.toHaveBeenCalled(); }); }); + +// destroy --force ends a session without its group only after such a read. +describe('isUnreadableGroupError', () => { + const refused = (code: string) => + makeCliError(ERROR_CODES.STORAGE_READ_ERROR, { cause: errno(code) }); + it.each([ + ['a program.json that the read refuses', refused('EACCES'), true], + [ + 'a program.json behind a file where a folder was', + refused('ENOTDIR'), + true, + ], + ['a /proc scan that fails with EIO', errno('EIO'), true], + ['a /proc read that fails with EACCES', errno('EACCES'), true], + ['a read that EPERM refuses', errno('EPERM'), true], + ['a path that loops', errno('ELOOP'), true], + ['a program.json that is a folder', refused('EISDIR'), true], + ['a name too long', errno('ENAMETOOLONG'), true], + [ + 'a program.json read that ran out of file descriptors', + refused('EMFILE'), + false, + ], + ['EMFILE', errno('EMFILE'), false], + ['ENFILE', errno('ENFILE'), false], + ['ENOMEM', errno('ENOMEM'), false], + ['EAGAIN', errno('EAGAIN'), false], + ['EINTR', errno('EINTR'), false], + [ + 'a STORAGE_READ_ERROR without a cause', + makeCliError(ERROR_CODES.STORAGE_READ_ERROR), + false, + ], + ['HOST_TIMEOUT', makeCliError(ERROR_CODES.HOST_TIMEOUT), false], + [ + 'an assertion', + Object.assign(new Error('x'), { code: 'ERR_ASSERTION' }), + false, + ], + ['an error without a code', new Error('EIO'), false], + ['a value that is no error', { code: 'EIO' }, false], + ])('reads %s as unreadable: %s', (_name, error, unreadable) => { + expect(isUnreadableGroupError(error)).toBe(unreadable); + }); +});