diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 6c2cac10..fc3d465d 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -13,27 +13,27 @@ The tool is TLC, the TLA+ model checker, pinned to release 1.7.4 by sha256. The ## The rules -| Rule | What must hold | Harm when it breaks | -| ------------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | -| R1 `NoLiveSessionDeleted` | gc never removes the folder of a session whose host can still write to it. | A running or starting session loses its manifest and event log. | -| R2 `HostDeathOnlyWhenDead` | The manifest says "failed, host died" only when the host process is dead. | `list` and `inspect` show a live session as failed. Commands refuse it. | -| R3 `TerminalIsFinal` | Once the manifest shows exited, failed or destroyed, it never shows running again. | A finished session looks running, and the next reconcile marks it failed. | -| R4 `RecordedExitKept` | Once the manifest records that the program exited, only `destroy` changes it, to destroyed, and keeps the exit code. | A program that exited 0 is reported as failed, with its exit code lost. | -| R5 `RunningSessionReachable` | While the host serves a running program, the socket file exists. | The session runs, but no command can reach it. | -| R6 `HostStartsWhenCreated` | A host never fails to start because another process removed or rewrote its files. | `create` fails with `HOST_UNREACHABLE` for a session nobody touched. | -| R7 `TerminalIsLastWrite` | Once the manifest shows exited, failed or destroyed, the host has no write left to make. | gc removes the folder while the host still writes to it, and the host's write then fails. | -| R8 `DestroyedOnlyWhenEnded` | While the host lives, the manifest says destroyed only after the host saw the program end. | `list` hides a program that still runs, and gc removes its folder. | -| R9 `DestroyEndsDestroyed` | `destroy` reports success only after it wrote destroyed or read it. | `destroy` says `destroyed: true`, but the session reads failed, "host process died unexpectedly", until a second `destroy`. | -| R10 `RemovedFolderStaysRemoved` | Once gc removed the session folder, no write brings it back. | A late write creates the folder again with only `session.json`. `list --all` shows that stub session until the next gc removes it. | -| R11 `DestroyedProgramStopped` | When the manifest says destroyed, no process of the program's process group runs, unless the program exited on its own first or no manifest named its pid. | A process of the session keeps running, `list` hides it, and nothing stops it later. | -| R13 `LiveGroupStaysNamed` | While a process of the program's process group runs, a manifest that named the program still names it. | The session reads failed or destroyed without `childPid`, so no later `destroy` or reconcile can stop the process that still runs. | -| R14 `DestroyOutlivesProgram` | `destroy` is never killed before it reports, also when it runs inside the program's session. | `destroy` prints nothing. With `--force` it kills its own group, and the session reads exited, not destroyed. | -| R15 `NoUnrelatedGroupKilled` | No kill reaches a process group that took the program's group id after the program's group ended. | `destroy`, `destroy --force`, a reconcile or the host's shutdown sends SIGKILL to an unrelated group, such as the program of another session. | -| R16 `DestroyedSessionStopped` | When the manifest says destroyed, no process of the program's group runs, also none that the program left when it exited on its own, unless the host died before `program.json` named the program. | `destroy` reports `destroyed: true` while a process of the session runs, `list` hides it, and nothing stops it later. | -| R17 `FailedCreateStopped` | Once `create` gave up on its host, the host keeps the session `running` only while `create`'s SIGTERM is on its way to it, or while the host has yet to check for the create-failed marker. | `create` fails with `HOST_UNREACHABLE`, but the session runs, and `list --all` shows it running. | -| R18 `DestroyedStaysDestroyed` | Once `destroy` reported success, the manifest says destroyed while the session folder exists, except while a reconcile that wrote over it has yet to write destroyed again. | `destroy` reports `destroyed: true`, and the session then reads `failed`. | -| R19 `NoUnrelatedHostKilled` | No kill of `destroy --force` reaches a process that took the host's pid after the host ended. | `destroy --force` sends SIGKILL to an unrelated process that got the crashed host's pid. | -| R20 `RemovedSessionStopped` | gc in the host's pid space removes a session folder, and with it `program.json`, only once no process of the program's group runs, also none that the program left when it exited on its own. | A process of the session keeps running, and nothing can prove or stop it later. | +| Rule | What must hold | Harm when it breaks | +| ------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | +| R1 `NoLiveSessionDeleted` | gc never removes the folder of a session whose host can still write to it. | A running or starting session loses its manifest and event log. | +| R2 `HostDeathOnlyWhenDead` | The manifest says "failed, host died" only when the host process is dead. | `list` and `inspect` show a live session as failed. Commands refuse it. | +| R3 `TerminalIsFinal` | Once the manifest shows exited, failed or destroyed, it never shows running again. | A finished session looks running, and the next reconcile marks it failed. | +| R4 `RecordedExitKept` | Once the manifest records that the program exited, only `destroy` changes it, to destroyed, and keeps the exit code. | A program that exited 0 is reported as failed, with its exit code lost. | +| R5 `RunningSessionReachable` | While the host serves a running program, the socket file exists. | The session runs, but no command can reach it. | +| R6 `HostStartsWhenCreated` | A host never fails to start because another process removed or rewrote its files. | `create` fails with `HOST_UNREACHABLE` for a session nobody touched. | +| R7 `TerminalIsLastWrite` | Once the manifest shows exited, failed or destroyed, the host has no write left to make. | gc removes the folder while the host still writes to it, and the host's write then fails. | +| R8 `DestroyedOnlyWhenEnded` | While the host lives, the manifest says destroyed only after the host saw the program end. | `list` hides a program that still runs, and gc removes its folder. | +| R9 `DestroyEndsDestroyed` | `destroy` reports success only after it wrote destroyed or read it. | `destroy` says `destroyed: true`, but the session reads failed, "host process died unexpectedly", until a second `destroy`. | +| R10 `RemovedFolderStaysRemoved` | Once gc removed the session folder, no write brings it back. | A late write creates the folder again with only `session.json`. `list --all` shows that stub session until the next gc removes it. | +| R11 `DestroyedProgramStopped` | When the manifest says destroyed, no process of the program's process group runs, unless the program exited on its own first 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. | `TypeOK` also runs in every run. When it breaks, the model is wrong, not the code. @@ -43,9 +43,9 @@ 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/hostMain.ts`: `waitForManifestFromCreate`, `isSessionCommandable`, and in `runHost` the start-up statements (the manifest wait, the `hostPid === process.pid` check, the `host.json` write with `captureHost` and `writeHostRecord`, `createSerialManifestWriter`, `EventLog.open`, the create-failed marker check, `createPty`, `setChildPid`, `captureProgram`), `hangUpProgram` with its kill timer and the `SHUTDOWN_KILL_GRACE_MS` constant, `startIdlePolling` (the idle time-out), `initiateShutdown`, `startShutdown`, `handlePtyExit` with its wait for the program's group, `pty.onExit`, the `SIGTERM` handler, the `resize` and `destroy` handlers, and the last `try` block (the `program.json` write, the start-up manifest write and `rpcServer.listen`). +- `src/host/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`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`. +- `src/cli/commands/gc.ts` `gcSessions` and `defaultDependencies`, `src/cli/commands/create.ts` `runCreateCommand` with `waitForReadyHost`, `writeMarkerOrLog` and `hostRuns`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`. - `src/host/sessionState.ts` `setDimensions`, `requestDestroy`, `recordDestroyed` and `recordExit`, `src/host/eventLog.ts` `EventLog.open`, `src/host/rpcServer.ts` `listen` and `close`, `src/host/rpcClient.ts` `toTransportCliError` (which socket errors read as `HOST_UNREACHABLE`). - `src/host/hostRecord.ts`: `captureHost`, `writeHostRecord`, `readHostRecord`, `pidExists`, `judgeHost`, `inPidNamespace`, `readTimeNamespace`, `inTimeNamespace`, `readMachineId`, `inHostPidSpace` and `sharesHostPids`. - `src/storage/manifests.ts` `readValidatedJsonFile`, `replaceFileAtomic`, `replaceFileAtomicSync`, `writeValidatedJsonFileSync`, `writeManifest`, `writeDestroyMarker` and `writeCreateFailedMarker` with `writeEmptyMarker`. @@ -65,13 +65,13 @@ From the repo root: .agents/skills/verify-session-lifecycle/scripts/check.sh ``` -It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. On a CI runner with 4 vCPUs and the default `CHECK_JOBS` of 4 it takes about an hour, so CI runs it in four shares. Ten runs explore more than 20 million distinct states each, so `CHECK_JOBS=79` starts every run at once and takes about as long as the longest run. `JAVA=/path/to/java` picks another Java. `TLA2TOOLS_JAR=/path/to/tla2tools.jar` uses a jar you already have, which must be the same 1.7.4 build. `CHECK_OUT=` keeps the results in that folder (default: a new temp folder, printed at the end). +It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. On a CI runner with 4 vCPUs and the default `CHECK_JOBS` of 4 it takes about an hour, so CI runs it in four shares. 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). What it does: -1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the thirty-six guards that the rules depend on and the status sets of the policy table, and it hashes each covered function with comments and layout removed. +1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the thirty-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. 2. It writes one TLC config per run, with those facts as constants. A guard that is not in the code, in the expected place and order, reads FALSE, and the model then runs without it. -3. It runs TLC 79 times and prints one line per run. +3. It runs TLC 85 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. @@ -92,7 +92,7 @@ At the sync commit, the expected results are: | `mutant-FreezesUnseenGroup-unseen`, `mutant-GcProbesUnseenGroup-unseen` | violated | Without the freeze, the kill through the token finds no member in view, the wait reads the group gone, and `destroy` records destroyed while the fork chain runs (R11). | | `mutant-GcFreezesUnseenGroup-unseen-zombies` | violated | `ZombiesInView`: under a PID 1 that never reaps, the fork chain also leaves zombies in view. Without the freeze, gc reads the group ended and removes `program.json` while the chain runs (R20). With every guard, `ZombiesInView` changes nothing, so `current-unseen` covers the pass run. | | `mutant-ReusedIdReadsGone` | pass | Without the guard, a group that took the program's id reads alive, so no wait of `destroy` passes while it runs, and `WitnessWaitPassesReusedId` is never reached. The model has no rule for a wait that never ends, so this run checks that witness instead of a rule. | -| `mutant-ReconcileRepairsMarked` | pass | Without the guard, a reconcile skips a marked `failed` as it skips any terminal manifest. The reconcile that wrote that `failed` always repairs it in the model, because the model has no crash of a reconciling process, so no rule breaks. The unit tests in `test/unit/host/lifecycle.test.ts` cover the crash. | +| `mutant-ReconcileRepairsMarked` | violated | R18: without the guard, a `list` that died between its write and its repair leaves `failed`, and the next reconcile skips it as it skips any terminal manifest. | | `mutant-ReconcileSkipsTerminal` | pass | The re-read in `reconcileSession` also returns on a terminal manifest, so the first terminal return alone is redundant. | | `mutant-GcSkipsNonCollectable`, `mutant-GcFinalCheck` | pass | gc checks "collectable" twice. One check alone still keeps R1, so removing one is safe. Removing both is not. | | `mutant-ShutdownChecksCommandable` | pass | `initiateShutdown` requests destroy only while the session is commandable, and the writer writes nothing after a terminal record. Either one alone keeps R3. Removing both is not safe. | @@ -103,6 +103,10 @@ At the sync commit, the expected results are: | `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. | +| `mutant-HostPollsCreateFailed` | pass | Redundant off Windows: the SIGTERM of a `create` that gave up stops the host without a manifest read. | +| `mutant-HostPollsCreateFailed-win32` | violated | R17: without the watch, a host that checked for the marker before `create` wrote it keeps serving when `create` cannot read the manifest. | +| `mutant-CreateRetriesMarker-win32` | violated | R17: without the retries, a marker write that fails once leaves a host that the manifest does not name yet serving after `create` gave up. | +| `witness-WitnessMarkerRetried-win32` | violated | The model reaches a `create` on Windows that writes the marker again. | Read `current` first. The witness and mutant runs use the same facts from the code, so a code change that breaks `current` can also turn them `UNEXPECTED`. @@ -394,6 +398,18 @@ On Windows, SIGTERM ends the host at once, so the host cannot stop its program. Now the catch of the readiness wait first writes an empty marker, `/create-failed`, with `writeCreateFailedMarker`, and only then reads the manifest for the platform rule. `runHost` checks for the marker right before its SIGTERM check, before the spawn, and returns without a program when it finds it. It checks again right after its start-up write lands, before it listens, and then calls `initiateShutdown`, which stops the program and records `destroyed`. The host's write comes before its check, and `create`'s marker write comes before its read, so either the host finds the marker or `create` reads the program's pid and sends the SIGTERM. `create` writes the marker on every platform, and off Windows the SIGTERM also stops the host, so `mutant-HostChecksCreateFailed` passes and only `mutant-HostChecksCreateFailed-win32` breaks R17. In the model, `CreateGivesUp` writes the marker, and with `Win32` `CreateStopsHostOnWindows` reads the manifest and ends a named host as a crash. `HostOpensLogAndSpawns` and `HostChecksMarker` are the two checks. The integration test `a create that gives up on Windows, where SIGTERM ends the host at once` runs the Windows path on Linux: a preload makes `create` read `win32` and turns its SIGTERM into a SIGKILL. +### `HostPollsCreateFailed`: on Windows, a host serves a failed create when create cannot read the manifest (R17) + +The order of the marker write and the manifest read closes the race only while that read works. When the host's start-up write and its marker check came before `create` gave up, the host listens without the marker, and `create` reads the manifest to send the SIGTERM. When that read fails, for example on an unreadable file, `create` on Windows takes the manifest as naming no program and sends nothing, and the host serves the failed session. + +Now `runHost` starts `watchCreateFailed` right after its start-up check. Every 100 ms it checks whether its creator still runs and then whether the marker exists. On the marker it calls `startShutdown`, as for a SIGTERM. Once a check after the creator's exit found no marker, it stops: `create` writes the marker before it exits, so no marker comes later. A liveness probe that throws, such as EPERM from a process of another user that took the creator's pid, counts as an exited creator, so no error leaves the timer and ends the host. So does a zombie creator, which `kill(pid, 0)` still finds until its parent reaps it: `readProcStat` shows it as `Z` on Linux. In the model, `CreateStopsHostOnWindows` reads the manifest or fails to read it, and `HostPollsMarker` is the watch from `"sockdir"` on. `mutant-HostPollsCreateFailed-win32` breaks R17, and `mutant-HostPollsCreateFailed` passes, because off Windows the SIGTERM does not need the read. The integration test `a create on Windows whose manifest read fails after it gave up` holds the host's socket-directory `mkdir` until `create` has exited and makes `create`'s manifest reads fail once the marker exists. + +### `CreateRetriesMarker`: on Windows, a failed marker write leaves a host serving a failed create (R17) + +The marker closes the race only when its write lands. On Windows, a `create` whose marker write failed, for example on an antivirus lock of the temp file, and whose manifest read named no program sent nothing. A host that started late then found no marker and served the failed session. + +Now the catch of the readiness wait writes the marker through `writeMarkerOrLog`, which logs a failed write and reports whether it landed. On Windows, while the write fails, the manifest names no program and `hostRuns(host.pid)` holds, the catch waits 100 ms, writes the marker again and reads the manifest after the write, up to 50 times. The stop after the loop then ends a host that the last read names. `hostRuns` counts a probe that throws, such as EPERM from a process of another user that took the host's pid, as an exited host, so the catch still reports its own error. A write that lands reaches the host by its start-up check or its watch, because `create` still runs. In the model, the marker write in `CreateGivesUp` can fail on every platform, and off Windows the SIGTERM then still stops the host. On Windows `CreateStopsHostOnWindows` goes on to `"retry"`, and `CreateRewritesMarker` is one more write and read, or the last one (`"exhausted"`). `mutant-CreateRetriesMarker-win32` breaks R17, and `witness-WitnessMarkerRetried-win32` shows the retry. The give-up integration case `on Windows, when its first marker write fails` fails the first marker write with EIO. + ### `FallbackNeedsFolder`: a childPid that gc's removal left stale gets the kill (R15) The model found this race. Without a token, `readProgramGroup` falls back to the childPid of the manifest copy that the caller read before it, as before `program.json` existed. When gc removed the session folder between that read and the `program.json` read, the record read missing too, and the kill used a childPid whose group could have ended and whose id could name an unrelated group by then. @@ -450,6 +466,8 @@ kill -KILL $! # the reconcil node --import tsx src/cli/main.ts list --all --json # the session reads destroyed ``` +In the model, `ListDiesBeforeRepair` kills the `list` process between its write and its repair. The ghost `lostRepair` then holds until the next reconcile reads the manifest, and R18 allows `failed` only until that read. With the guard, that read goes to the repair write (`r_marked`). Without it, the read skips the terminal manifest and R18 breaks. `WitnessDeadRepairRepaired` shows that a session reads destroyed again after such a death. + ### `TokenNamesProgram`: a token that no member of the group carries (R16) node-pty returns before the program calls `setsid()`, so the first reads of the program often show the host's own session and autogroup. Without the guard, `captureToken` could keep an autogroup that it read before the program's `setsid()`, while its next read of the program's stat already showed the new session. The record then held the host's autogroup. No member of the program's group carries that id, so every kill through the record killed nothing and every wait through it read the group gone. `destroy` then recorded destroyed while a process of the program's group ran. @@ -539,7 +557,7 @@ To bring the check back in line after changes that skipped it, use `/maintain-fo ## Scope -The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 29,309,460 distinct states, and without one 29,186,546. The check prints both counts. +The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 64,052,288 distinct states, and without one 63,127,914. The check prints both counts. It assumes: @@ -557,9 +575,9 @@ It assumes: - A program can outlive its host: the PTY closes with the host and sends the program SIGHUP, which a program can ignore. The model keeps such a program running until a kill of its group ends it, the worst case for R11. A SIGKILL of the group ends every process of our user in it at once. - A process of another user can run in the program's group, such as the root child of `sudo cmd &`. Our SIGKILL does not reach it, and once only such processes are left, `kill(-pgid)` fails with EPERM. `isProcessGroupAlive` reads EPERM as alive unless `/proc` shows only zombies of the group, and `killProcessGroupBestEffort` ignores it. While such a process runs, three things take about 5 seconds, the length of `waitForProcessesToExit`. The host waits that long after the program's exit, then leaves the manifest destroying and ends. `destroy` and `destroy --force` end with `HOST_TIMEOUT`. Every reconcile of the session (`list`, `inspect`, `gc`, the dashboard) waits that long and writes nothing. The model lets each wait give up at any poll that reads the group alive. With a token, the model lets such a process carry the token in view. Where `/proc` hides or refuses it, the token check reads it through `isProcessGroupAlive`, which reads it alive in the same states while `ProbeCountsDeniedGroup` holds. - A killed process stays a zombie until its parent, or init once its parent has died, reaps it, and `kill(-pgid, 0)` still finds a zombie. On Linux, `isProcessGroupAlive` then reads `/proc//stat` of every process and reads the group gone when two scans in a row each show processes of it and only zombies, because a process can fork and end while one scan runs. When a scan shows no process of the group, the probe decides: EPERM reads alive and a found group reads gone. So a group whose last processes are never reaped, as under a container's PID 1 without an init, reads gone. A process whose main thread called `pthread_exit` while another thread runs also shows Z there, so `readProcStat` reads `/proc//task` of every process that shows Z and gives it the state of a thread that is not a zombie. Such a process counts as live in the scan and in the token check, where it can carry the token. On macOS it does not scan, so a zombie still reads alive until launchd reaps it. The model has no zombies: a killed process ends at once. A process that `/proc` refuses to show, as `hidepid=1` (EPERM) or a security module (EACCES) does for other users, reads alive. With `hidepid=2` or `hidepid=4` (`invisible` and `ptraceable` on newer kernels), `/proc` can leave such a process out of its listing, so the probe reads the last `/proc` line of `/proc/self/mountinfo`, skips the scan and reads a group with a zombie alive, as on macOS. With a token, neither a zombie nor a process that `/proc` refuses to show witnesses the token. When no live member is in view, `isProgramGroupAlive` reads the group as `isProcessGroupAlive` does, with the zombie scan, the refused reads and the same `hidepid` check. So under any of those `hidepid` modes, a group that a process of another user took after the program's group ended reads alive, and `destroy` ends with `HOST_TIMEOUT` until that process ends. -- A destroy that lands between reconcile's last read and its write is still overwritten with failed, for the time until that reconcile finds the destroy marker and writes destroyed again (`ReconcileRepairsDestroyed`). A `list` or `gc` that reads in that time sees `failed`, a terminal status, so gc can remove the folder as it would remove a destroyed one. A reconcile whose process dies in that time leaves `failed` until the next reconcile reads it: that read finds the marker and writes destroyed (`ReconcileRepairsMarked`). `home list` and the dashboard count a session with the marker as destroyed, also in that time. The model has no crash of a reconciling process, so it checks that the repair at the read breaks no rule, not that it heals the crash. +- A destroy that lands between reconcile's last read and its write is still overwritten with failed, for the time until that reconcile finds the destroy marker and writes destroyed again (`ReconcileRepairsDestroyed`). A `list` or `gc` that reads in that time sees `failed`, a terminal status, so gc can remove the folder as it would remove a destroyed one. A reconcile whose process dies in that time leaves `failed` until the next reconcile reads it: that read finds the marker and writes destroyed (`ReconcileRepairsMarked`). `home list` and the dashboard count a session with the marker as destroyed, also in that time. The model kills the `list` process in that time (`ListDiesBeforeRepair`), so it checks that the repair at the read heals the death. A `gc` that dies there leaves the same record, and the model leaves it out. - The idle time-out calls the same `hangUpProgram` as `initiateShutdown`: SIGHUP, then the group kill after `SHUTDOWN_KILL_GRACE_MS`. When the program exits on that SIGHUP, `handlePtyExit` kills the group too, so a process that ignores SIGHUP does not outlive the idle time-out. An idle time-out still ends exited. When the check cannot run (`unknown`), the idle kill sends nothing, and the session ends exited with that process running, as after a program that exits on its own and leaves a process (coder/agent-tty#222). The model leaves both group kills out: they go through `stopProgramGroup` like every kill, and a process that outlives them is one that the program left, which the model keeps after a normal exit anyway. -- Windows has no process groups, so there `processGroupTarget` gives the program's pid, and every kill reaches only that process. `destroy` never re-runs on Windows. There SIGTERM ends the host at once, so a `create` that gives up sends it only once the manifest names the program, and the next reconcile records `failed` and ends the program. Before that write, the host finds the create-failed marker (`HostChecksCreateFailed`). `current-win32` checks this with a SIGTERM that is a host crash and without a token, and keeps the process groups of Linux. A marker write that fails, for example on a full disk, leaves a host that the manifest does not name yet serving on Windows. The model has no such failure. +- Windows has no process groups, so there `processGroupTarget` gives the program's pid, and every kill reaches only that process. `destroy` never re-runs on Windows. There SIGTERM ends the host at once, so a `create` that gives up sends it only once the manifest names the program, and the next reconcile records `failed` and ends the program. Before that write, the host finds the create-failed marker (`HostChecksCreateFailed`), and after it the host's watch finds it when `create`'s manifest read fails (`HostPollsCreateFailed`). `current-win32` checks this with a SIGTERM that is a host crash and without a token, and keeps the process groups of Linux. When the marker write fails on Windows, `create` writes it again every 100 ms, up to 50 times, while the manifest names no program and the host runs (`CreateRetriesMarker`). When every write fails, for example on a full disk, a host that the manifest does not name yet serves the session. The model ends such a `create` as `"exhausted"`, which R17 does not cover. - A host stopped with SIGSTOP, or with a blocked event loop, takes the SIGTERM of a `create` that gave up only when it runs again. Until then its program runs and the session reads `running`, which R17 allows because the SIGTERM is still on its way. A plain `destroy` fails because the host does not answer, and only `destroy --force` ends such a session sooner. - A destroy that the program runs, or that someone types into the program's interactive shell, runs inside the program's session, and `rerunInNewSession` runs it again in a new session. The model lets such a destroy start while the program's leader runs, and assumes that it kept `AGENT_TTY_SESSION_ID`, which every process of the program inherits at spawn. A destroy whose environment lost the variable, or whose `create --env` overrode it, is seen through the id comparison only. On Linux that compares the CLI's session id with `childPid`, so it misses such a destroy only before the host's start-up write. Other POSIX systems compare the process group and the controlling terminal, through `/bin/ps`. A terminal is the controlling terminal of one session and of every process in it, so that also finds a job of an interactive shell, which runs in a group of its own. A process without a controlling terminal is seen only through the group. - The program's processes stay in its process group. A process that leaves the group (`setsid`, or the job control of an interactive shell) is out of reach of the group kill, and it is no witness for the token either. That is case 4 of coder/agent-tty#203, a documented limit with no code change. diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index cafb794e..94b58db2 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -12,6 +12,8 @@ "CreateRecordsHost": true, "CreateStopsOnGiveUp": true, "HostChecksCreateFailed": true, + "HostPollsCreateFailed": true, + "CreateRetriesMarker": true, "HostWaitsForManifest": true, "HostSerializesWrites": true, "HostStopsAfterTerminalWrite": true, @@ -40,8 +42,10 @@ "Terminal": ["destroyed", "exited", "failed"] }, "fingerprints": { - "src/cli/commands/create.ts#runCreateCommand": "131d2707818ea283", + "src/cli/commands/create.ts#runCreateCommand": "bb4fa596cc1e4af7", "src/cli/commands/create.ts#waitForReadyHost": "a7fd2ba345b6bfd6", + "src/cli/commands/create.ts#writeMarkerOrLog": "abf293bd80df1c3d", + "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", @@ -135,13 +139,13 @@ "src/storage/manifests.ts#writeCreateFailedMarker": "587c8047e563db4e", "src/storage/manifests.ts#writeEmptyMarker": "143325689100f36c", "src/protocol/sessionStatusPolicy.ts#SESSION_STATUS_POLICIES": "83827f9f7f6b8e1d", - "src/host/hostMain.ts#runHost(parts)": "1d75544221b3c6c1", - "src/host/hostMain.ts#runHost(final try)": "251f1e68a4ec17cc", + "src/host/hostMain.ts#runHost(parts)": "7bd4c6553a831b9d", + "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": "77ec28d60359f635", - "skill:scripts/facts.mjs": "eded6c52629e3523", - "skill:scripts/check.sh": "e33db0960de216fe" + "skill:model/SessionLifecycle.tla": "7f1c6dd7943968c3", + "skill:scripts/facts.mjs": "6ee4da3ef9b6bac3", + "skill:scripts/check.sh": "b48bc5fd343aefb5" }, "callSites": { "writeManifest": [ diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index ae65e610..5bc325c5 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -111,6 +111,15 @@ CONSTANTS \* it reads the manifest, and the host checks \* for it before the spawn and right after its \* start-up write, and then ends the session + HostPollsCreateFailed, \* hostMain.ts: from its start-up check on, the + \* host checks for the create-failed marker + \* while its creator runs and once after, and + \* then ends the session + CreateRetriesMarker, \* create.ts: on Windows, while the marker write + \* fails and the manifest names no program, + \* create writes the marker again and reads + \* the manifest after each write, up to 50 + \* times, while the host runs TokenNamesProgram, \* programGroup.ts: captureToken records an \* autogroup only once the program leads its \* own session in an autogroup other than the @@ -170,7 +179,8 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, GcKeepsLiveGroup, InsideCheckReadsEnv, RecordsProgramSync, ProvesGroupOwnership, DestroyStopsLeftovers, FallbackNeedsFolder, CreateStopsOnGiveUp, - HostChecksCreateFailed, + HostChecksCreateFailed, HostPollsCreateFailed, + CreateRetriesMarker, ReconcileRepairsDestroyed, ReconcileRepairsMarked, TokenNamesProgram, ReusedIdReadsGone, ProvesHostPid, CreateRecordsHost, @@ -199,11 +209,20 @@ VARIABLES rec, \* program.json names the program with its token startFailed, \* ghost: the host died because its files were missing readRepaired, \* ghost: a reconcile wrote destroyed from its first read + lostRepair, \* ghost: a reconcile died between its write and its + \* repair while the marker existed, and no reconcile has + \* read the manifest since + diedBeforeRepair, \* ghost: such a death happened + polled, \* ghost: the host's watch found the create-failed marker \* next to the destroy marker sock, \* the RPC socket file exists (it is outside the directory) cpc, \* create: "alloc", "write", "launch", "done", "giveup" \* (Windows: the marker is written, the manifest read - \* is next), "failed" (it gave up on its host) + \* is next), "retry" (Windows: the marker write failed + \* and the manifest named no program, so the next + \* write is due), "failed" (it gave up on its host), + \* "exhausted" (Windows: it gave up after its last + \* marker write failed too, see R17) hostAlive, \* the detached host process is alive hpc, \* host start-up path: "none", "boot", "open", "record" \* (the program runs, program.json is not written yet), @@ -265,7 +284,8 @@ VARIABLES diskVars == <> -ghostVars == <> +ghostVars == <> hostVars == <> groupVars == <> @@ -281,6 +301,7 @@ Init == /\ wasTerminal = FALSE /\ wasExited = FALSE /\ wasNamed = FALSE /\ dmark = FALSE /\ cmark = FALSE /\ rec = FALSE /\ startFailed = FALSE /\ readRepaired = FALSE + /\ lostRepair = FALSE /\ diedBeforeRepair = FALSE /\ polled = FALSE /\ sock = FALSE /\ cpc = "alloc" /\ hostAlive = FALSE /\ hpc = "none" /\ hex = "none" /\ rsz = "none" @@ -431,6 +452,8 @@ CliKillThrough(named) == IF OtherPidSpace THEN NoKill ELSE KillThrough(named) HostFailsToStart == /\ startFailed' = TRUE /\ readRepaired' = readRepaired + /\ lostRepair' = lostRepair /\ diedBeforeRepair' = diedBeforeRepair + /\ polled' = polled /\ hostAlive' = FALSE /\ hpc' = "dead" /\ hex' = IF hex = "none" THEN "none" ELSE "gone" @@ -499,30 +522,64 @@ CreateLaunchesHost == \* the program. create writes nothing else: without a token only the host \* knows which group is the program's. Without the guard, create only \* reports the error. On Linux and macOS the manifest read changes nothing, -\* so the model joins the marker write, the read and the SIGTERM. +\* so the model joins the marker write, the read and the SIGTERM. The +\* marker write can also fail for a reason of its own, such as an antivirus +\* lock on its temp file. Off Windows the SIGTERM then still stops the host. CreateGivesUp == /\ cpc = "done" - /\ cmark' = (cmark \/ (HostChecksCreateFailed /\ dir)) + /\ \E written \in BOOLEAN : + cmark' = (cmark \/ (HostChecksCreateFailed /\ dir /\ written)) /\ cpc' = IF Win32 THEN "giveup" ELSE "failed" /\ UNCHANGED <> +\* On Windows, create's SIGTERM to a host that the manifest names. +CreateStopsNamedHost(readOk) == + IF CreateStopsOnGiveUp /\ readOk /\ mchild /\ hostAlive + THEN /\ HostDies + /\ UNCHANGED <> + ELSE UNCHANGED <> + \* On Windows the SIGTERM ends the host at once, without its handlers, so \* create sends it only when the manifest that it reads after the marker \* write names the program. The next reconcile then records failed and ends -\* the program. +\* the program. That read can fail, for example when the file is not +\* readable, and then create sends nothing. With CreateRetriesMarker, a +\* create whose marker write failed and whose read named no program writes +\* the marker again while the host runs. CreateStopsHostOnWindows == /\ cpc = "giveup" - /\ cpc' = "failed" - /\ IF CreateStopsOnGiveUp /\ mchild /\ hostAlive - THEN /\ HostDies - /\ UNCHANGED <> - ELSE UNCHANGED <> + /\ \E readOk \in BOOLEAN : + IF CreateRetriesMarker /\ HostChecksCreateFailed /\ ~cmark + /\ ~(readOk /\ mchild) /\ hostAlive + THEN /\ cpc' = "retry" + /\ UNCHANGED <> + ELSE /\ cpc' = "failed" + /\ CreateStopsNamedHost(readOk) /\ UNCHANGED <> +\* One more marker write, 100 ms after the last one, then a manifest read. +\* create goes on while the write fails, the read names no program and the +\* host runs. The model has no clock, so after any write that failed it can +\* also stop as if its 50th write had failed ("exhausted"). Then the host +\* that the manifest does not name yet sees no marker and serves the +\* session. The SKILL.md Scope section states this residual. +CreateRewritesMarker == + /\ cpc = "retry" + /\ \E written \in BOOLEAN, readOk \in BOOLEAN, more \in BOOLEAN : + /\ cmark' = (cmark \/ (dir /\ written)) + /\ IF ~(dir /\ written) /\ ~(readOk /\ mchild) /\ hostAlive + THEN /\ cpc' = IF more THEN "retry" ELSE "exhausted" + /\ UNCHANGED <> + ELSE /\ cpc' = "failed" + /\ CreateStopsNamedHost(readOk) + /\ UNCHANGED <> + \* ------------------------------------------------------------------------- \* The host's serial manifest writer (createSerialManifestWriter). Each write \* takes its snapshot of the in-memory state when its turn starts, which is @@ -716,6 +773,21 @@ HostGetsSigterm == /\ UNCHANGED <> +\* watchCreateFailed: from right after the start-up check on, the host +\* checks for the create-failed marker every 100 ms while its creator runs, +\* and once after the creator exited. create writes the marker before it +\* exits, so the watch finds every marker. On the marker it calls +\* startShutdown, as for a SIGTERM. +HostPollsMarker == + /\ HostPollsCreateFailed + /\ hostAlive /\ cmark /\ hsd = "none" + /\ hpc \in {"sockdir", "serving"} + /\ polled' = TRUE + /\ StartShutdown(WriteQueued) + /\ UNCHANGED <> + \* initiateShutdown's `await persistManifest()` lands, then its finally block \* starts. HostWritesDestroying == @@ -907,9 +979,13 @@ SkipsHost(read) == ReconcileSkipsLiveHost /\ read.pid /\ CliHostAlive \* readManifestIfExists. With ReconcileRepairsMarked, a terminal manifest \* other than destroyed next to the destroy marker (isMarkedDestroyed) goes \* to the repair write from this copy ("r_marked"). Otherwise it returns when -\* the manifest is null or terminal. +\* the manifest is null or terminal. A reconcile that died before its +\* repair left its failed record, and this read is the next chance to +\* repair it. ReconcileReads(p) == /\ pc[p] = "r_read" + /\ lostRepair' = FALSE /\ diedBeforeRepair' = diedBeforeRepair + /\ polled' = polled /\ IF ReconcileRepairsMarked /\ dmark /\ mst \in Terminal /\ mst # "destroyed" THEN /\ pc' = [pc EXCEPT ![p] = "r_marked"] @@ -1046,8 +1122,9 @@ ReconcileWritesMarked(p) == /\ readRepaired' = TRUE ELSE /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)] /\ UNCHANGED <> - /\ UNCHANGED <> + /\ UNCHANGED <> \* unlinkIfPresent(socketPath(sessionDirectory)) ReconcileUnlinksSocket(p) == @@ -1057,6 +1134,20 @@ ReconcileUnlinksSocket(p) == /\ UNCHANGED <> +\* The list process is killed between its write and its repair, for +\* example by a Ctrl-C. Its write may have replaced the destroyed record +\* of a destroy that already reported success. gc's death in the same +\* place leaves the same record, so only list dies in the model. A later +\* list starts a new reconcile. +ListDiesBeforeRepair == + /\ pc["list"] = "r_repair" + /\ pc' = [pc EXCEPT !["list"] = "idle"] + /\ lostRepair' = (lostRepair \/ (dmark /\ mst # "destroyed")) + /\ diedBeforeRepair' = (diedBeforeRepair \/ (dmark /\ mst # "destroyed")) + /\ UNCHANGED <> + \* ------------------------------------------------------------------------- \* gc @@ -1423,16 +1514,17 @@ DestroyFinalRead == \* 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. AllFinished == - /\ cpc \in {"done", "failed"} /\ ~hostAlive /\ pc["gc"] = "done" + /\ cpc \in {"done", "failed", "exhausted"} /\ ~hostAlive + /\ pc["gc"] = "done" /\ pc["list"] = "idle" /\ lruns = MaxListReconciles /\ dpc = "done" /\ UNCHANGED vars Next == \/ CreateMakesDirectory \/ CreateWritesManifest \/ CreateLaunchesHost - \/ CreateGivesUp \/ CreateStopsHostOnWindows + \/ CreateGivesUp \/ CreateStopsHostOnWindows \/ CreateRewritesMarker \/ HostReadsManifest \/ HostOpensLogAndSpawns \/ HostRecordsProgram - \/ HostWritesPids \/ HostChecksMarker + \/ HostWritesPids \/ HostChecksMarker \/ HostPollsMarker \/ HostListens \/ HostStartsResize \/ HostResizeWriteLands \/ HostGetsSigterm \/ HostWritesDestroying \/ HostClosesSocket \/ HostKillsProgram \/ ProgramExits \/ HostPollsGroup \/ HostWritesExit @@ -1445,6 +1537,7 @@ Next == \/ ReconcilePollsGroup(p) \/ ReconcileWrites(p) \/ ReconcileRepairs(p) \/ ReconcileWritesMarked(p) \/ ReconcileUnlinksSocket(p) + \/ ListDiesBeforeRepair \/ GcFindsDirectory \/ GcReadsManifest \/ GcReadsReconciled \/ GcChecksGroup \/ GcFinalRead \/ GcRemoves \/ ListStartsReconcile @@ -1466,7 +1559,7 @@ TypeOK == /\ cmark => dir /\ {dir, mpid, mchild, wasTerminal, wasExited, wasNamed, dmark, cmark, startFailed, - readRepaired, sock, + readRepaired, lostRepair, diedBeforeRepair, polled, sock, hostAlive, prog, foreign, sig, dforce, dinside, dsaw, dkill, rec, left, reused, hitUnrelated, diedUnrecorded, passedReused, hrec, hreused, hitUnrelatedHost} @@ -1480,7 +1573,8 @@ TypeOK == /\ hsd \in {"none", "write", "wait", "closed"} /\ dsnap \in {"none", "destroying", "destroyed"} /\ (mst # "none") => dir - /\ (dir /\ mst = "none") => cpc \notin {"done", "giveup", "failed"} + /\ (dir /\ mst = "none") => + cpc \notin {"done", "giveup", "retry", "failed", "exhausted"} /\ (cpc = "write") => dir /\ gres \in {"pending", "skipped", "removed"} /\ lruns \in 0..MaxListReconciles @@ -1576,19 +1670,25 @@ DestroyedSessionStopped == \* 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 -\* yet to check for the create-failed marker. +\* yet to check for the create-failed marker. A create that gave up after +\* all its marker writes failed ends as "exhausted", which R17 does not +\* cover (see the Scope section of SKILL.md). FailedCreateStopped == (cpc = "failed" /\ hostAlive /\ hst = "running") => \/ CreateStopsOnGiveUp /\ ~Win32 /\ ~sig \/ HostChecksCreateFailed /\ cmark /\ hpc \in {"boot", "open", "record", "pidwrite", "markcheck"} + \/ HostPollsCreateFailed /\ cmark /\ hpc \in {"sockdir", "serving"} \* R18: once destroy reported success, the manifest says destroyed while the \* directory exists, except while a reconcile that wrote over it has yet to -\* write destroyed again. +\* write destroyed again, or, after that reconcile died, until the next +\* reconcile reads the manifest and writes destroyed. DestroyedStaysDestroyed == (dres = "ok" /\ dir) => - (mst = "destroyed" \/ \E p \in Readers : pc[p] = "r_repair") + \/ mst = "destroyed" + \/ \E p \in Readers : pc[p] \in {"r_repair", "r_marked"} + \/ lostRepair \* R19: no kill of destroy --force reaches a process that took the host's \* pid after the host ended. @@ -1611,6 +1711,10 @@ WitnessGcRemovesSession == gres # "removed" WitnessReconcileRepairs == ~(dmark /\ mst = "failed" /\ \E p \in Readers : pc[p] = "r_repair") WitnessMarkedRepaired == ~readRepaired +WitnessMarkerPolled == ~polled +WitnessMarkerRetried == cpc # "retry" +WitnessDeadRepairRepaired == + ~(diedBeforeRepair /\ ~lostRepair /\ mst = "destroyed" /\ dir) WitnessCreateGivesUp == ~(cpc = "failed" /\ sig /\ mst = "destroyed" /\ ~hostAlive) WitnessSessionServes == ~(hpc = "serving" /\ sock /\ mst = "running" /\ mpid) diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index 0d500c93..061e278c 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/check.sh +++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh @@ -166,7 +166,7 @@ TERMINAL=$(node -e ' const c = JSON.parse(require("node:fs").readFileSync(process.argv[1], "utf8")).constants; console.log("{" + c.Terminal.map((s) => JSON.stringify(s)).join(", ") + "}"); ' "$OUT/facts.json") -GUARDS="GcSkipsNonCollectable GcFinalCheck GcKeepsLiveGroup GcProbesUnseenGroup GcFreezesUnseenGroup ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed ReconcileRepairsMarked CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid CreateRecordsHost FreezesUnseenGroup UnsharedGroupReadsUnknown HostChecksCreateFailed" +GUARDS="GcSkipsNonCollectable GcFinalCheck GcKeepsLiveGroup GcProbesUnseenGroup GcFreezesUnseenGroup ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed ReconcileRepairsMarked CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid CreateRecordsHost FreezesUnseenGroup UnsharedGroupReadsUnknown HostChecksCreateFailed HostPollsCreateFailed CreateRetriesMarker" # 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; @@ -181,7 +181,7 @@ NO_TOKEN_RULES="NoLiveSessionDeleted HostDeathOnlyWhenDead TerminalIsFinal Recor # check them. RULES="$NO_TOKEN_RULES NoUnrelatedGroupKilled DestroyedSessionStopped RemovedSessionStopped" NO_TOKEN_WITNESSES="WitnessCreateGivesUp WitnessCrashReconciled WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessReconcileRepairs" -WITNESSES="WitnessGcRemovesSession WitnessCreateGivesUp WitnessSessionServes WitnessResizeLands WitnessCleanExitRecorded WitnessCrashReconciled WitnessDestroyCompletes WitnessSigtermRecorded WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessLeftoverMeetsDestroy WitnessReusedIdMeetsKill WitnessRecordNamesProgram WitnessUnrecordedProgramOutlives WitnessReconcileRepairs WitnessMarkedRepaired WitnessWaitPassesReusedId WitnessReusedHostMeetsKill" +WITNESSES="WitnessGcRemovesSession WitnessCreateGivesUp WitnessSessionServes WitnessResizeLands WitnessCleanExitRecorded WitnessCrashReconciled WitnessDestroyCompletes WitnessSigtermRecorded WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessLeftoverMeetsDestroy WitnessReusedIdMeetsKill WitnessRecordNamesProgram WitnessUnrecordedProgramOutlives WitnessReconcileRepairs WitnessMarkedRepaired WitnessDeadRepairRepaired WitnessWaitPassesReusedId WitnessReusedHostMeetsKill WitnessMarkerPolled" # --- runs ---------------------------------------------------------------- @@ -257,11 +257,12 @@ write_run mutant-FallbackNeedsFolder violated NoUnrelatedGroupKilled "FallbackNe write_run mutant-ReconcileRepairsDestroyed violated DestroyedStaysDestroyed "ReconcileRepairsDestroyed=FALSE" "without the marker, a reconcile writes failed over the destroyed that destroy reported" DestroyedStaysDestroyed write_run mutant-CreateStopsOnGiveUp violated FailedCreateStopped "CreateStopsOnGiveUp=FALSE" "without the SIGTERM, a create that gave up leaves its host serving the session" FailedCreateStopped write_run mutant-HostChecksCreateFailed pass FailedCreateStopped "HostChecksCreateFailed=FALSE" "redundant off Windows: the SIGTERM stops the host" +write_run mutant-HostPollsCreateFailed pass FailedCreateStopped "HostPollsCreateFailed=FALSE" "redundant off Windows: the SIGTERM stops the host" write_run mutant-TokenNamesProgram violated DestroyedSessionStopped "TokenNamesProgram=FALSE" "with the host's autogroup as the token, no member carries it, and destroy records destroyed while the program's group runs" DestroyedSessionStopped write_run mutant-ReusedIdReadsGone pass WitnessWaitPassesReusedId "ReusedIdReadsGone=FALSE" "with a group that took the id read alive, no wait of destroy passes while that group runs" write_run mutant-ProvesHostPid violated NoUnrelatedHostKilled "ProvesHostPid=FALSE" "without the start-up record, destroy --force kills a process that took the host's pid" NoUnrelatedHostKilled write_run witness-WitnessUnrecordedHostMeetsKill violated WitnessUnrecordedHostMeetsKill "CreateRecordsHost=FALSE" "without a record from create, as when its capture fails, a kill meets a host that host.json does not name yet" -write_run mutant-ReconcileRepairsMarked pass DestroyedStaysDestroyed "ReconcileRepairsMarked=FALSE" "redundant in the model: it has no crash of a reconciling process, so the repair after the reconcile's own write always runs" +write_run mutant-ReconcileRepairsMarked violated DestroyedStaysDestroyed "ReconcileRepairsMarked=FALSE" "without the repair at the first read, a list that died between its write and its repair leaves failed, and the next reconcile skips it" DestroyedStaysDestroyed write_run mutant-ReconcileSkipsTerminal pass RecordedExitKept "ReconcileSkipsTerminal=FALSE" "redundant: the re-read returns on a terminal manifest" write_run mutant-GcSkipsNonCollectable pass NoLiveSessionDeleted "GcSkipsNonCollectable=FALSE" "redundant: the final check still skips" write_run mutant-GcFinalCheck pass NoLiveSessionDeleted "GcFinalCheck=FALSE" "redundant: the first check still skips" @@ -311,6 +312,9 @@ write_run mutant-ReconcileWaitsForGroup-no-token violated LiveGroupStaysNamed "R WIN32=TRUE write_run current-win32 pass "$NO_TOKEN_RULES" "" "the code on Windows: R1 to R14 and R17 to R19 hold" write_run mutant-HostChecksCreateFailed-win32 violated FailedCreateStopped "HostChecksCreateFailed=FALSE" "without the marker, a host that the manifest does not name yet keeps serving after create gave up" FailedCreateStopped +write_run mutant-HostPollsCreateFailed-win32 violated FailedCreateStopped "HostPollsCreateFailed=FALSE" "without the watch, a host that checked for the marker before create wrote it keeps serving when create cannot read the manifest" FailedCreateStopped +write_run mutant-CreateRetriesMarker-win32 violated FailedCreateStopped "CreateRetriesMarker=FALSE" "without the retries, a marker write that fails once leaves a host that the manifest does not name yet serving after create gave up" FailedCreateStopped +write_run witness-WitnessMarkerRetried-win32 violated WitnessMarkerRetried "" "the model reaches this state on Windows" WIN32=FALSE # A run that expects pass explores the whole model and takes minutes, and a diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 05e181ee..525f9858 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -257,6 +257,8 @@ function createFacts() { CreateRecordsHost: recordsHost, CreateStopsOnGiveUp: stopsOnGiveUp(create.body), HostChecksCreateFailed: checksCreateFailed(create.body), + HostPollsCreateFailed: pollsCreateFailed(), + CreateRetriesMarker: retriesMarker(create.body), }; } @@ -281,7 +283,13 @@ function giveUpCatch(body) { tried[0] === 'result = await waitForReadyHost(socketFile, sessionDirectory, sessionId);' ) { - return s.catchClause.block.statements.map((t) => normalize(t.getText())); + // The text-mode line that names the session changes no process or + // file, so the facts skip it. + return s.catchClause.block.statements + .map((t) => normalize(t.getText())) + .filter( + (t) => !t.startsWith('if (!options.json) { writeHumanErrorLines('), + ); } } return null; @@ -289,14 +297,11 @@ function giveUpCatch(body) { function stopsOnGiveUp(body) { const st = giveUpCatch(body) ?? []; + // No statement before the stop leaves the catch. const stops = st.length >= 4 && st[0].startsWith('invariant(host !== undefined,') && - st - .at(-3) - .startsWith( - 'const manifest = await readManifestIfExists( manifestPath(sessionDirectory), )', - ) && + st.slice(1, -2).every((t) => !/\b(return|throw|break)\b/.test(t)) && st.at(-2) === "if (process.platform !== 'win32' || manifest?.childPid != null) { host.stop(); }" && st.at(-1) === 'throw withSessionId(error, sessionId);'; @@ -330,11 +335,14 @@ function stopsOnGiveUp(body) { function checksCreateFailed(body) { const st = giveUpCatch(body) ?? []; const marks = - st.length === 5 && - st[1].startsWith( - 'await writeCreateFailedMarker( createFailedMarkerPath(sessionDirectory), sessionId, ).catch(', - ) && - st[2].startsWith('const manifest = await readManifestIfExists('); + st.length >= 8 && + st[1] === 'const markerFile = createFailedMarkerPath(sessionDirectory);' && + st[2] === 'const manifestFile = manifestPath(sessionDirectory);' && + st[4] === + 'let marked = await writeMarkerOrLog(markerFile, sessionId, logger);' && + st[5] === + 'let manifest = await readManifestIfExists(manifestFile).catch(() => null);' && + writesMarker(); const run = requireDeclaration('src/host/hostMain.ts', 'runHost').body; const check = indexOfStatement( run, @@ -364,6 +372,72 @@ function checksCreateFailed(body) { ); } +// writeMarkerOrLog writes the create-failed marker and reports whether the +// write landed. +function writesMarker() { + const helper = normalize( + requireDeclaration( + 'src/cli/commands/create.ts', + 'writeMarkerOrLog', + ).body.getText(), + ); + return helper.startsWith( + '{ return writeCreateFailedMarker(path, sessionId).then( () => true, (error: unknown) => {', + ); +} + +// On Windows, while the marker write fails and the manifest names no +// program, the give-up catch writes the marker again and reads the manifest +// after each write, a bounded number of times while the host runs, before +// its stop. So a host that the manifest does not name yet gets the marker, +// or the last read names its program and create stops it. +function retriesMarker(body) { + const st = giveUpCatch(body) ?? []; + const loop = + 'for ( let attempt = 1; ' + + "process.platform === 'win32' && !marked && manifest?.childPid == null && " + + 'attempt <= MARKER_RETRY_MAX_ATTEMPTS && hostRuns(host.pid); ' + + 'attempt += 1 ) { ' + + 'await delay(MARKER_RETRY_INTERVAL_MS); ' + + 'marked = await writeMarkerOrLog(markerFile, sessionId, logger); ' + + 'manifest = await readManifestIfExists(manifestFile).catch(() => null); }'; + // A probe that throws counts as an exited host. + const probe = normalize( + requireDeclaration('src/cli/commands/create.ts', 'hostRuns').body.getText(), + ); + return ( + st.length === 9 && + st[6] === loop && + probe === + '{ try { return isProcessAlive(pid); } catch { return false; } }' && + checksCreateFailed(body) + ); +} + +// runHost's watchCreateFailed checks, every CREATE_FAILED_POLL_INTERVAL_MS, +// whether the creator still runs and then whether the create-failed marker +// exists. A probe that throws, and a zombie creator, count as an exited +// creator, so no error leaves the timer. On the marker it calls startShutdown, and it stops once a check +// after the creator's exit found none. The start-up try calls it right after +// the check that follows the start-up write. +function pollsCreateFailed() { + const run = requireDeclaration('src/host/hostMain.ts', 'runHost').body; + const watch = indexOfStatement(run, /^const watchCreateFailed = /); + const watches = + watch >= 0 && + normalize(run.statements[watch].getText().replace(/\/\/[^\n]*/g, '')) === + "const watchCreateFailed = (): void => { const timer = setInterval(() => { let creatorGone = true; try { creatorGone = !isProcessAlive(creatorPid) || readProcStat(creatorPid)?.state === 'Z'; } catch { } if (existsSync(createFailedMarkerPath(sessDir))) { clearInterval(timer); startShutdown(); } else if (creatorGone) { clearInterval(timer); } }, CREATE_FAILED_POLL_INTERVAL_MS); timer.unref(); };"; + const last = run.statements.at(-1); + const tried = + last !== undefined && ts.isTryStatement(last) + ? last.tryBlock.statements.map((t) => normalize(t.getText())) + : []; + const check = tried.indexOf( + 'if (existsSync(createFailedMarkerPath(sessDir))) { await initiateShutdown(); return; }', + ); + return watches && check >= 0 && tried[check + 1] === 'watchCreateFailed();'; +} + // runHost waits for create's manifest, and every host write of session.json // goes through one createSerialManifestWriter. function hostFacts() { @@ -1516,6 +1590,8 @@ function policyFacts() { const COVERED = [ ['src/cli/commands/create.ts', 'runCreateCommand'], ['src/cli/commands/create.ts', 'waitForReadyHost'], + ['src/cli/commands/create.ts', 'writeMarkerOrLog'], + ['src/cli/commands/create.ts', 'hostRuns'], ['src/cli/commands/destroy.ts', 'runDestroyCommand'], ['src/cli/commands/destroy.ts', 'rerunInNewSession'], ['src/cli/commands/gc.ts', 'gcSessions'], @@ -1628,6 +1704,7 @@ const RUN_HOST_PARTS = [ /^process\.on\('SIGTERM'/, /^let onSigterm = /, /^if \(existsSync\(createFailedMarkerPath\(sessDir\)\)\) \{/, + /^const watchCreateFailed = /, /^if \(sigterm\.received\) \{/, /^invariant\(!sigterm\.received/, /^onSigterm = startShutdown;/, diff --git a/docs/USAGE.md b/docs/USAGE.md index a0b70efa..9ec4760b 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -326,7 +326,7 @@ A `list`, `inspect` or `gc` that reads the session between those two writes sees If `destroy` fails after it wrote the file, for example because its manifest write fails, the file stays, and the next reconcile records the session as `destroyed`, also when the session had already ended. Nothing deletes the file before `gc` removes the session folder, because a reconcile that read before the destroy can still write after it. A host that died after it recorded the session as ended leaves its socket. `gc`, and a `destroy` of a `destroyed` session, remove that socket when the manifest names no host pid or the host check below reads the host as ended. When `create` cannot reach its new host, it fails and tells the host to stop. It fails with `HOST_UNREACHABLE` (exit 6) after about 6 s when nothing listens on the socket, and with `HOST_TIMEOUT` (exit 5) after about 10 s when the host accepts the connection but does not answer. -`create` also tells the host to stop when it fails for another reason after it wrote the session's first manifest, for example when it cannot read that manifest again. Each such error names the session in `details.sessionId`. +`create` also tells the host to stop when it fails for another reason after it wrote the session's first manifest, for example when it cannot read that manifest again. Each such error names the session in `details.sessionId`, and in text mode `create` prints `Session failed to start.` before the error line. When that first manifest write fails, `create` removes the session folder. The host waits for the manifest only while `create` runs, so it then exits without starting the program. On Linux and macOS it sends the host SIGTERM, and the host stops the program the way `destroy` does and records the session as `destroyed` once the program's group has ended, also while its start-up is still slow. `create` exits before the host has ended the session, so a caller that checks at once can still read `running` or `destroying`. @@ -337,7 +337,7 @@ When the host cannot end the program's group, for example a process of another u A host stopped with SIGSTOP, or with a blocked event loop, handles the SIGTERM only when it runs again. Until then the program runs and the session reads `running`. A plain `destroy` fails because the host does not answer, and only `destroy --force` ends the session sooner. On Windows, SIGTERM ends the host at once, so the host cannot stop the program itself. There `create` sends it only once the manifest names the program: the session then reads `running` with a dead host until the next reconcile records it `failed` and ends the program. Before the host's start-up write, `create` sends nothing. For that case, on every platform, `create` first writes an empty internal file, `create-failed`, in the session folder, and then reads the manifest. The host checks for that file before it starts the program, and returns then, so no program runs and the next reconcile records the session `failed`. It checks again right after its start-up write, and then ends the session the way a SIGTERM does on Linux: it stops the program and records `destroyed`. -On Windows, a host whose start-up write lands before `create` reads the manifest is named by that read and gets the SIGTERM, and a host whose write lands after it finds the file. When the file write fails, for example on a full disk, a Windows host that starts late can still serve the session. This path is not tested on a real Windows host. +On Windows, a host whose start-up write lands before `create` reads the manifest is named by that read and gets the SIGTERM, and a host whose write lands after it finds the file. After its start-up write, the host also checks for the file every 100 ms while `create` runs, and once after `create` exits, so it ends the session also when `create` cannot read the manifest. When the file write fails, `create` writes it again every 100 ms, up to 50 times, while the host runs and the manifest names no program. When every write fails, for example on a full disk, a Windows host that starts late can still serve the session. This path is not tested on a real Windows host. On Linux, `destroy` and reconcile never kill a process group that they cannot prove is the session's. When the host starts the program, it records the program's pid, the boot id and the program's autogroup id in an internal file, `program.json`. diff --git a/src/cli/README.md b/src/cli/README.md index c85e9393..73993eeb 100644 --- a/src/cli/README.md +++ b/src/cli/README.md @@ -11,7 +11,7 @@ This directory is the agent-tty command-line front end. `main.ts` is the bin ent - Global options: `--home `, `--timeout-ms `, `--no-color`, `--log-level `, `--profile `, `--renderer `. Each command except `dashboard` (alias `d`) and the hidden `_host` registers its own `--json` option. [main.ts:main] - Commands: `version`, `doctor`, `create [command...]`, `list`, `inspect`, `destroy`, `gc`, `type`, `paste`, `run`, `batch`, `mark`, `send-keys`, `mouse`, `resize`, `signal`, `snapshot`, `screenshot`, `dashboard`, `wait`. Groups: `skills list|get|path`, `home list|forget`, `record diff|export`. A hidden `_host ` command imports `src/host/hostMain.ts` and runs `runHost(sessionId, Number(creatorPid))`. [main.ts:main] - `resolveCommandContext(options, env?, deps?)`, `getCommandContext`, `setCommandContext`, `parseTimeoutMsOption`, `resolveRendererDefault`, `resolveLogLevel`, `clearRendererDefaultProbeCacheForTests`, and the types `GlobalCliOptions` and `CommandContext`. [context.ts:resolveCommandContext] [context.ts:CommandContext] -- `emitSuccess`, `emitSuccessSync`, `emitFailure`, `emitCliError`, `argvHasFlag`, `exitAfterOutputFlush`, `formatSuccessOutput`, `writeJsonEnvelope`, `writeHumanLines`, `writeStdoutSync`, `setColorEnabled`. [output.ts:emitSuccess] [output.ts:emitFailure] [output.ts:writeStdoutSync] [output.ts:argvHasFlag] [output.ts:exitAfterOutputFlush] +- `emitSuccess`, `emitSuccessSync`, `emitFailure`, `emitCliError`, `argvHasFlag`, `exitAfterOutputFlush`, `formatSuccessOutput`, `writeJsonEnvelope`, `writeHumanLines`, `writeHumanErrorLines`, `writeStdoutSync`, `setColorEnabled`. [output.ts:emitSuccess] [output.ts:emitFailure] [output.ts:writeStdoutSync] [output.ts:argvHasFlag] [output.ts:exitAfterOutputFlush] - `resolveCommandTarget(options)` returns a `CommandTarget` (`sessionId`, `sessionDirectory`, `manifestPath`, `socketPath`, `manifest`). Also exports `ResolveCommandTargetOptions` and `CommandTargetManifest`. [commandTarget.ts:resolveCommandTarget] [commandTarget.ts:CommandTarget] - `assertSessionCommandable(manifest, sessionId)` and `checkedSessionDir(home, sessionId)`. [sessionGuards.ts:assertSessionCommandable] [sessionGuards.ts:checkedSessionDir] - `exitCodeForError(code)`. [exitCodes.ts:exitCodeForError] diff --git a/src/cli/commands/README.md b/src/cli/commands/README.md index 5c5a62b6..f2863672 100644 --- a/src/cli/commands/README.md +++ b/src/cli/commands/README.md @@ -44,7 +44,7 @@ This directory holds one handler module per agent-tty CLI command. `src/cli/main ## Side Effects - Session commands send RPCs over the session socket through `sendRpc`. The method names are `run`, `type`, `paste`, `sendKeys`, `mouse`, `mark`, `resize`, `signal`, `snapshot`, `screenshot`, `wait`, `waitForRender` and `inspect`. `create` also sends `inspect` while it polls. [run.ts:runRunCommand] [send-keys.ts:runSendKeysCommand] [wait.ts:runWaitCommand] [create.ts:runCreateCommand] -- `create` calls `allocateSession` (`src/host/lifecycle.ts`) with a `launch` callback that records the session ID and starts the host process through `launchHost`. If `launchHost` or a later step of `allocateSession` throws, `create` removes the session directory with `fs.rm`. A bad `cwd`, shell path or command segment fails before `allocateSession` creates the directory, so no session directory is left behind. A failure between `mkdir` and the callback, such as a failed `chmod`, leaves the empty session directory in place. Any failure after `allocateSession` returned, a failed readiness poll included, writes the empty `create-failed` marker with `writeCreateFailedMarker`, logs a failed marker write at debug level, then calls the host's `stop()` (on Windows only once the manifest names the program) and leaves the session directory in place. `create` rethrows the error with `details.sessionId` added, and an error that is not a `CliError` becomes `INTERNAL_ERROR`. It registers the Home through `upsertHome`. [create.ts:runCreateCommand] +- `create` calls `allocateSession` (`src/host/lifecycle.ts`) with a `launch` callback that records the session ID and starts the host process through `launchHost`. If `launchHost` or a later step of `allocateSession` throws, `create` removes the session directory with `fs.rm`. A bad `cwd`, shell path or command segment fails before `allocateSession` creates the directory, so no session directory is left behind. A failure between `mkdir` and the callback, such as a failed `chmod`, leaves the empty session directory in place. Any failure after `allocateSession` returned, a failed readiness poll included, writes the empty `create-failed` marker with `writeCreateFailedMarker` and logs a failed marker write at debug level (`writeMarkerOrLog`). On Windows, while that write fails, the manifest names no program and the host runs (`hostRuns`, where a probe that throws counts as an exited host), it writes the marker again every 100 ms, up to 50 times, and reads the manifest after each write. It then calls the host's `stop()` (on Windows only once the manifest names the program) and leaves the session directory in place. `create` rethrows the error with `details.sessionId` added, and an error that is not a `CliError` becomes `INTERNAL_ERROR`. In text mode it first writes `Session failed to start.` to stderr with `writeHumanErrorLines`. It registers the Home through `upsertHome`. [create.ts:runCreateCommand] [create.ts:writeMarkerOrLog] [create.ts:hostRuns] - `gc` reads session directories, calls `reconcileSession` (which can rewrite manifests), deletes collectable session directories with `fs.rm` outside dry-run mode, and deregisters Homes through `forgetHome`. [gc.ts:gcSessions] [gc.ts:runGcCommand] - `inspect` calls `reconcileSession` when the host is unreachable, and for an ended session other than destroyed whose folder holds the destroy marker. When that repair throws, it shows the manifest as it reads. [inspect.ts:runInspectCommand] - `destroy` and `list` call `destroySession` and `listSessions` from `src/host/lifecycle.ts`. [destroy.ts:runDestroyCommand] [list.ts:runListCommand] diff --git a/src/cli/commands/create.ts b/src/cli/commands/create.ts index fd9da566..544d55ff 100644 --- a/src/cli/commands/create.ts +++ b/src/cli/commands/create.ts @@ -4,10 +4,11 @@ import { setTimeout as delay } from 'node:timers/promises'; import { CliError } from '../errors.js'; import type { CommandContext } from '../context.js'; -import { emitSuccess } from '../output.js'; +import { emitSuccess, writeHumanErrorLines } from '../output.js'; import { DEFAULT_IDLE_TIMEOUT_MS } from '../../config/defaults.js'; import { allocateSession, + isProcessAlive, launchHost, type LaunchedHost, } from '../../host/lifecycle.js'; @@ -31,6 +32,8 @@ import { invariant } from '../../util/assert.js'; const READINESS_POLL_INTERVAL_MS = 100; const READINESS_MAX_ATTEMPTS = 50; const READINESS_RPC_TIMEOUT_MS = 100; +const MARKER_RETRY_INTERVAL_MS = 100; +const MARKER_RETRY_MAX_ATTEMPTS = 50; type SessionEnvironment = Record; @@ -177,6 +180,35 @@ function withSessionId(error: unknown, sessionId: string): CliError { }); } +// A probe that throws, such as EPERM from a process of another user that +// took the host's pid, counts as an exited host, so the create still reports +// its own error. +function hostRuns(pid: number): boolean { + try { + return isProcessAlive(pid); + } catch { + return false; + } +} + +// A failed write is logged, so the create still reports its own error. +function writeMarkerOrLog( + path: string, + sessionId: string, + logger: CommandContext['logger'], +): Promise { + return writeCreateFailedMarker(path, sessionId).then( + () => true, + (error: unknown) => { + logger.debug('failed to write the create-failed marker', { + sessionId, + error: error instanceof Error ? error.message : String(error), + }); + return false; + }, + ); +} + export async function runCreateCommand(options: CommandOptions): Promise { const environment = normalizeCreateEnvironment(options.envEntries); const idleTimeoutMs = @@ -274,24 +306,36 @@ export async function runCreateCommand(options: CommandOptions): Promise { // for it after its start-up write names the program: either the host // finds the marker, or the manifest read below finds the program. invariant(host !== undefined, 'a session that create polls has a host'); - await writeCreateFailedMarker( - createFailedMarkerPath(sessionDirectory), - sessionId, - ).catch((markerError: unknown) => { - options.context.logger.debug('failed to write the create-failed marker', { - sessionId, - error: - markerError instanceof Error - ? markerError.message - : String(markerError), - }); - }); - const manifest = await readManifestIfExists( - manifestPath(sessionDirectory), - ).catch(() => null); + const markerFile = createFailedMarkerPath(sessionDirectory); + const manifestFile = manifestPath(sessionDirectory); + const logger = options.context.logger; + let marked = await writeMarkerOrLog(markerFile, sessionId, logger); + let manifest = await readManifestIfExists(manifestFile).catch(() => null); + // On Windows a host that the manifest does not name yet sees only the + // marker. So while the marker write fails, create writes it again and + // reads the manifest after each write, until the marker lands, the + // manifest names the program, or the host has exited. + for ( + let attempt = 1; + process.platform === 'win32' && + !marked && + manifest?.childPid == null && + attempt <= MARKER_RETRY_MAX_ATTEMPTS && + hostRuns(host.pid); + attempt += 1 + ) { + await delay(MARKER_RETRY_INTERVAL_MS); + marked = await writeMarkerOrLog(markerFile, sessionId, logger); + manifest = await readManifestIfExists(manifestFile).catch(() => null); + } if (process.platform !== 'win32' || manifest?.childPid != null) { host.stop(); } + // JSON names the session in details.sessionId. Text mode prints only the + // error line, so name the session before it. + if (!options.json) { + writeHumanErrorLines([`Session ${sessionId} failed to start.`]); + } throw withSessionId(error, sessionId); } diff --git a/src/cli/output.ts b/src/cli/output.ts index 1ce1e6b1..7134581d 100644 --- a/src/cli/output.ts +++ b/src/cli/output.ts @@ -43,6 +43,10 @@ export function writeHumanLines(lines: readonly string[]): void { process.stdout.write(`${formatHumanText(lines.join('\n'))}\n`); } +export function writeHumanErrorLines(lines: readonly string[]): void { + process.stderr.write(`${formatHumanText(lines.join('\n'))}\n`); +} + interface SuccessOutputOptions { command: string; json: boolean; diff --git a/src/host/README.md b/src/host/README.md index 87bcc2f4..e52580d3 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -80,7 +80,7 @@ - `runHost` spawns the PTY with `createPty` (`src/pty/createPty.ts`), writes input to it, resizes it and kills it on idle timeout and shutdown. It writes `TerminalQueryResponder` replies to the PTY without logging them. [hostMain.ts:runHost] - `runHost` polls `session.json` with `readManifestIfExists` and probes the creator process with `isProcessAlive` until the manifest appears or the creator exits. It writes `session.json` through `createSerialManifestWriter`, creates the socket directory with mode `0o700` and listens with `RpcServer` through `listenInSocketDirectory` and writes snapshot and screenshot artifacts through `src/snapshot/capture.ts` and `src/screenshot/capture.ts`. [hostMain.ts:runHost] - `runHost` registers a `process.on('SIGTERM')` handler that starts shutdown, sends signals to the child with `process.kill` and starts `setInterval` timers for idle and wait polling. [hostMain.ts:runHost] -- `runHost` checks for the `create-failed` marker with `existsSync` before it spawns the program, and returns when it finds it. It checks again right after its start-up manifest write, before it listens, and then shuts down. [hostMain.ts:runHost] +- `runHost` checks for the `create-failed` marker with `existsSync` before it spawns the program, and returns when it finds it. It checks again right after its start-up manifest write, before it listens, and then shuts down. From there on, `watchCreateFailed` checks for the marker every `CREATE_FAILED_POLL_INTERVAL_MS` (100 ms) while the creator process lives and once after it exited (a liveness probe that throws, such as EPERM from a process of another user that took the pid, and a zombie creator that `readProcStat` shows as `Z` count as exited), and starts the shutdown when it finds the marker. [hostMain.ts:runHost] - `runHost` rethrows a PTY-ingestion, event-log append, exit-handling or shutdown error in `process.nextTick`. The uncaught exception crashes the host process. [hostMain.ts:rethrowAsync] - `resolveHostRendererName` reads `process.env.AGENT_TTY_HOST_RENDERER` and `process.env.AGENT_TTY_RENDERER`. [hostMain.ts:resolveHostRendererName] - `EventLog.open` opens the file in append mode and runs `chmod 0o600`. `append` writes with `fileHandle.appendFile`, one call at a time. `close` calls `fileHandle.sync()` and then closes the file. [eventLog.ts:EventLog] diff --git a/src/host/hostMain.ts b/src/host/hostMain.ts index 82673d85..f2ec81e9 100644 --- a/src/host/hostMain.ts +++ b/src/host/hostMain.ts @@ -20,6 +20,7 @@ import { createSerialManifestWriter } from './manifestWriter.js'; import { captureProgram, programWithoutToken, + readProcStat, stopProgramGroup, writeProgramRecord, } from './programGroup.js'; @@ -106,6 +107,7 @@ export const MAX_CONSECUTIVE_POLL_FAILURES = 10; // may exceed idleTimeoutMs by up to checkIntervalMs (bounded by this cap). const IDLE_CHECK_CAP_MS = 5_000; const MANIFEST_WAIT_INTERVAL_MS = 20; +const CREATE_FAILED_POLL_INTERVAL_MS = 100; // How long the host waits after SIGHUP before it kills the program's process // group. nvim takes about 1 s to exit on SIGHUP, and `destroy` waits about 5 s. const SHUTDOWN_KILL_GRACE_MS = 2_000; @@ -1272,6 +1274,33 @@ export async function runHost( invariant(!sigterm.received, 'SIGTERM is handled only after the spawn block'); onSigterm = startShutdown; + // A create that gives up after the check below may not stop the host: on + // Windows it sends nothing when its manifest read fails. It writes the + // create-failed marker before it exits, so the host watches for the marker + // while its creator runs, and once more after the creator has exited. + const watchCreateFailed = (): void => { + const timer = setInterval(() => { + // An error of the probe, such as EPERM from a process of another user + // that took the pid, means that the creator has exited. So does a + // zombie, which kill(pid, 0) still finds until its parent reaps it. + let creatorGone = true; + try { + creatorGone = + !isProcessAlive(creatorPid) || + readProcStat(creatorPid)?.state === 'Z'; + } catch { + // creatorGone stays true. + } + if (existsSync(createFailedMarkerPath(sessDir))) { + clearInterval(timer); + startShutdown(); + } else if (creatorGone) { + clearInterval(timer); + } + }, CREATE_FAILED_POLL_INTERVAL_MS); + timer.unref(); + }; + try { writeProgramRecord(sessDir, program); await persistManifest(); @@ -1283,6 +1312,7 @@ export async function runHost( await initiateShutdown(); return; } + watchCreateFailed(); if (!isSessionCommandable(state)) { await initiateShutdown(); diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index 1ffc620a..5f7a184a 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -437,7 +437,8 @@ export async function removeSocketDirectoryBestEffort( } // Removes the socket at the old path of the same session, which a host of an -// older version listens at. Remove this after one minor release. +// older version listens at. Hosts of 0.5.0 and earlier listen there, and +// 0.6.0 is the first release with the per-uid root, so remove this in 0.7.0. async function removeLegacySocketBestEffort(socketFile: string): Promise { const oldSocketFile = legacySocketPath(socketFile); if (oldSocketFile === null || !(await isOwnLegacySocket(oldSocketFile))) { @@ -1131,6 +1132,10 @@ export async function reconcileSession( const manifestFile = manifestPath(sessionDirectory); const manifest = await readManifestIfExists(manifestFile); + // Only recordDestroyed writes the marker, and only for a terminal manifest + // or once the host and the program's group are dead. So the host has + // ended or is ending, and the repair removes both sockets without a + // liveness check. if (manifest !== null && isMarkedDestroyed(sessionDirectory, manifest)) { if (await writeMarkedDestroyed(manifestFile, manifest)) { const socketFile = socketPath(sessionDirectory); diff --git a/src/host/rpcClient.ts b/src/host/rpcClient.ts index 29d16a00..58c291f8 100644 --- a/src/host/rpcClient.ts +++ b/src/host/rpcClient.ts @@ -119,8 +119,8 @@ export async function sendRpc( signal?: AbortSignal, ): Promise { throwIfAborted(signal); - // A host that an older version started listens at the old path. Remove - // this fallback after one minor release. + // A host that an older version started listens at the old path. Hosts of + // 0.5.0 and earlier listen there, so remove this fallback in 0.7.0. const oldSocketPath = legacySocketPath(socketPath); if (oldSocketPath === null) { return await sendRpcAt(socketPath, method, params, timeoutMs, signal); diff --git a/src/host/socketRoot.ts b/src/host/socketRoot.ts index 6d15d21f..9150598d 100644 --- a/src/host/socketRoot.ts +++ b/src/host/socketRoot.ts @@ -97,7 +97,8 @@ export async function socketRootExists( // listens. No other user may be able to rename or replace a folder on its // path before the connect: the Home's folder is this uid's and not writable // by others, and the root is this uid's or root's, either not writable by -// others or sticky. Remove this after one minor release. +// others or sticky. Hosts of 0.5.0 and earlier listen there, and 0.6.0 is +// the first release with the per-uid root, so remove this in 0.7.0. export async function isOwnLegacySocket(socketFile: string): Promise { const uid = process.getuid?.(); if (uid === undefined) { diff --git a/src/storage/sessionPaths.ts b/src/storage/sessionPaths.ts index c007591b..90c5bf07 100644 --- a/src/storage/sessionPaths.ts +++ b/src/storage/sessionPaths.ts @@ -179,8 +179,8 @@ export function socketPath(sessionDirectory: string): string { return socketFile; } -// A host that an older version started listens under the shared root. Remove -// this after one minor release. +// A host that an older version started listens under the shared root. Hosts +// of 0.5.0 and earlier listen there, so remove this in 0.7.0. export function legacySocketPath(socketFile: string): string | null { const root = socketRootDirectory(); const socketDirectory = dirname(socketFile); diff --git a/test/fixtures/fail-first-marker-write.ts b/test/fixtures/fail-first-marker-write.ts new file mode 100644 index 00000000..988b31c6 --- /dev/null +++ b/test/fixtures/fail-first-marker-write.ts @@ -0,0 +1,28 @@ +// Preload (`--import`) for a `create` process: the first write of the +// create-failed marker's temp file fails with EIO, as a write that an +// antivirus lock blocks once does. The host inherits NODE_OPTIONS and skips +// this. +import fsp from 'node:fs/promises'; +import { syncBuiltinESMExports } from 'node:module'; +import { basename } from 'node:path'; +import process from 'node:process'; + +if (process.argv.includes('create') && !process.argv.includes('_host')) { + const writeFile = fsp.writeFile as (...args: unknown[]) => Promise; + let failed = false; + fsp.writeFile = ((path: unknown, ...rest: unknown[]) => { + const file = path instanceof URL ? path.pathname : String(path); + if (!failed && basename(file).startsWith('create-failed.tmp-')) { + failed = true; + return Promise.reject( + Object.assign(new Error(`EIO: i/o error, open '${file}'`), { + code: 'EIO', + syscall: 'open', + path: file, + }), + ); + } + return writeFile(path, ...rest); + }) as typeof fsp.writeFile; + syncBuiltinESMExports(); +} diff --git a/test/fixtures/fail-manifest-read-after-marker.ts b/test/fixtures/fail-manifest-read-after-marker.ts new file mode 100644 index 00000000..71037a47 --- /dev/null +++ b/test/fixtures/fail-manifest-read-after-marker.ts @@ -0,0 +1,29 @@ +// Preload (`--import`) for a `create` process: once the create-failed marker +// exists, every read of the session's session.json fails with EACCES, as an +// unreadable manifest does. The host inherits NODE_OPTIONS and skips this. +import { existsSync } from 'node:fs'; +import fsp from 'node:fs/promises'; +import { syncBuiltinESMExports } from 'node:module'; +import { basename, dirname } from 'node:path'; +import process from 'node:process'; + +if (process.argv.includes('create') && !process.argv.includes('_host')) { + const readFile = fsp.readFile as (...args: unknown[]) => Promise; + fsp.readFile = ((path: unknown, ...rest: unknown[]) => { + const file = path instanceof URL ? path.pathname : String(path); + if ( + basename(file) === 'session.json' && + existsSync(`${dirname(file)}/create-failed`) + ) { + return Promise.reject( + Object.assign(new Error(`EACCES: permission denied, open '${file}'`), { + code: 'EACCES', + syscall: 'open', + path: file, + }), + ); + } + return readFile(path, ...rest); + }) as typeof fsp.readFile; + syncBuiltinESMExports(); +} diff --git a/test/integration/lifecycle.test.ts b/test/integration/lifecycle.test.ts index 06046646..868284fe 100644 --- a/test/integration/lifecycle.test.ts +++ b/test/integration/lifecycle.test.ts @@ -13,7 +13,7 @@ import { writeFile, } from 'node:fs/promises'; import { tmpdir } from 'node:os'; -import { join, resolve } from 'node:path'; +import { basename, dirname, join, resolve } from 'node:path'; import { pathToFileURL } from 'node:url'; import { afterEach, beforeEach, describe, expect, it, vi } from 'vitest'; @@ -1869,6 +1869,15 @@ describe('lifecycle integration', { timeout: 60_000 }, () => { `--import=${pathToFileURL(resolve('test/fixtures/fake-win32-create.ts')).href}`, ], ], + // create retries the marker write while the manifest names no program. + [ + 'on Windows, when its first marker write fails', + [ + `--import=${pathToFileURL(resolve('test/fixtures/denied-autogroup.ts')).href}`, + `--import=${pathToFileURL(resolve('test/fixtures/fake-win32-create.ts')).href}`, + `--import=${pathToFileURL(resolve('test/fixtures/fail-first-marker-write.ts')).href}`, + ], + ], ])('a create that gives up %s', (_name, preloads) => { let pgid = 0; @@ -2034,6 +2043,103 @@ describe('lifecycle integration', { timeout: 60_000 }, () => { expect(inspectSession(testHome, sessionId as string).status).toBe('failed'); }, 60_000); + // On Windows, create stops a host only when its manifest read names the + // program. Here the host's start-up write and its marker check come before + // create gives up, its listen is held past create's exit, and create's + // manifest read after the marker write fails. Only the host can see the + // marker then. + describe('a create on Windows whose manifest read fails after it gave up', () => { + let pgid = 0; + + afterEach(() => { + if (pgid > 1) { + killGroupIfAlive(pgid); + } + pgid = 0; + }); + + it('lets its host find the marker, stop the program and record destroyed', async () => { + const holdLog = join(testHome, 'hold.log'); + const release = join(testHome, 'release'); + const socketDirectory = basename( + dirname(socketPath(sessionDir(testHome, 'probe'))), + ); + const creator = spawn( + process.execPath, + [ + '--import', + 'tsx', + './src/cli/main.ts', + 'create', + '--json', + '--', + '/bin/sh', + '-c', + 'trap "" HUP; sleep 300 & wait', + ], + { + stdio: ['ignore', 'pipe', 'ignore'], + env: { + ...process.env, + AGENT_TTY_HOME: testHome, + REPLAY_LOG: holdLog, + REPLAY_RELEASE: release, + REPLAY_HOLD: `_host:mkdir:/${socketDirectory}:1:60000`, + NODE_OPTIONS: [ + process.env.NODE_OPTIONS ?? '', + `--import=${pathToFileURL(resolve('.agents/skills/verify-session-lifecycle/scripts/replay-hold.mjs')).href}`, + `--import=${pathToFileURL(resolve('test/fixtures/denied-autogroup.ts')).href}`, + `--import=${pathToFileURL(resolve('test/fixtures/fake-win32-create.ts')).href}`, + `--import=${pathToFileURL(resolve('test/fixtures/fail-manifest-read-after-marker.ts')).href}`, + ].join(' '), + }, + }, + ); + let stdout = ''; + creator.stdout.on('data', (chunk: Buffer) => { + stdout += chunk.toString('utf8'); + }); + const creatorExit = once(creator, 'exit'); + const deadline = Date.now() + 15_000; + while ( + !(await readFile(holdLog, 'utf8').then( + (log) => log.includes('hold mkdir'), + () => false, + )) + ) { + expect(Date.now()).toBeLessThan(deadline); + await sleep(50); + } + const [sessionId] = await readdir(join(testHome, 'sessions')); + const directory = sessionDir(testHome, sessionId as string); + const manifest = SessionRecordSchema.parse( + JSON.parse(await readFile(manifestPath(directory), 'utf8')), + ); + expect(manifest.childPid).not.toBeNull(); + const hostPid = manifest.hostPid as number; + pgid = manifest.childPid as number; + expect(isGroupAlive(pgid)).toBe(true); + + const [code] = (await creatorExit) as [number | null]; + expect(code).toBe(6); + expect(JSON.parse(stdout)).toMatchObject({ + ok: false, + error: { code: 'HOST_UNREACHABLE', details: { sessionId } }, + }); + expect(existsSync(join(directory, 'create-failed'))).toBe(true); + await writeFile(release, ''); + + const stopDeadline = Date.now() + 20_000; + while (isGroupAlive(pgid) || isProcessAlive(hostPid)) { + expect(Date.now()).toBeLessThan(stopDeadline); + await sleep(100); + } + expect(inspectSession(testHome, sessionId as string).status).toBe( + 'destroyed', + ); + }, 60_000); + }); + // A SIGTERM that the default action would turn into a host death between // the spawn and program.json leaves a program that no file names. describe('a host that gets SIGTERM right after it spawns the program', () => { diff --git a/test/unit/cli/output.test.ts b/test/unit/cli/output.test.ts index b6f10e48..22ce719f 100644 --- a/test/unit/cli/output.test.ts +++ b/test/unit/cli/output.test.ts @@ -94,6 +94,25 @@ describe('emitCliError', () => { }); }); +describe('writeHumanErrorLines', () => { + it('writes the lines to stderr, without color when color is off', () => { + const stderr = vi.spyOn(process.stderr, 'write').mockReturnValue(true); + const stdout = vi.spyOn(process.stdout, 'write').mockReturnValue(true); + output.setColorEnabled(false); + output.writeHumanErrorLines([ + '\u001b[31mSession s-1\u001b[0m failed.', + 'next', + ]); + const stderrCalls = stderr.mock.calls.map(([chunk]) => String(chunk)); + const stdoutCalls = stdout.mock.calls.length; + stderr.mockRestore(); + stdout.mockRestore(); + + expect(stderrCalls).toEqual(['Session s-1 failed.\nnext\n']); + expect(stdoutCalls).toBe(0); + }); +}); + describe('argvHasFlag', () => { afterEach(() => { process.argv = originalArgv; diff --git a/test/unit/commands/create.test.ts b/test/unit/commands/create.test.ts index c1f5087a..17a04f44 100644 --- a/test/unit/commands/create.test.ts +++ b/test/unit/commands/create.test.ts @@ -10,9 +10,11 @@ import type { SessionRecord } from '../../../src/protocol/schemas.js'; const mocks = vi.hoisted(() => ({ emitSuccess: vi.fn(), + writeHumanErrorLines: vi.fn(), allocateSession: vi.fn(), ensureSocketRoot: vi.fn(), launchHost: vi.fn(), + isProcessAlive: vi.fn(), stopHost: vi.fn(), sendRpc: vi.fn(), readManifestIfExists: vi.fn(), @@ -26,10 +28,12 @@ const mocks = vi.hoisted(() => ({ vi.mock('../../../src/cli/output.js', () => ({ emitSuccess: mocks.emitSuccess, + writeHumanErrorLines: mocks.writeHumanErrorLines, })); vi.mock('../../../src/host/lifecycle.js', () => ({ allocateSession: mocks.allocateSession, + isProcessAlive: mocks.isProcessAlive, launchHost: mocks.launchHost, })); @@ -124,6 +128,7 @@ describe('create command', () => { }, ); mocks.launchHost.mockReturnValue({ pid: 12345, stop: mocks.stopHost }); + mocks.isProcessAlive.mockReturnValue(true); mocks.sendRpc.mockResolvedValue({ session: { sessionId: 'session-01' } }); mocks.readManifestIfExists.mockResolvedValue(makeManifest()); mocks.sessionDir.mockImplementation( @@ -366,6 +371,34 @@ describe('create command', () => { expect(mocks.writeCreateFailedMarker).not.toHaveBeenCalled(); }); + it('names the session in text mode when the host never answers', async () => { + mocks.sendRpc.mockRejectedValue( + makeCliError(ERROR_CODES.HOST_UNREACHABLE, { + message: 'host unreachable', + }), + ); + + await expect( + runCreateCommand({ ...baseOptions, json: false, context }), + ).rejects.toMatchObject({ code: 'HOST_UNREACHABLE' }); + expect(mocks.writeHumanErrorLines).toHaveBeenCalledWith([ + 'Session session-01 failed to start.', + ]); + }); + + it('leaves the session line out of JSON mode, where details.sessionId names it', async () => { + mocks.sendRpc.mockRejectedValue( + makeCliError(ERROR_CODES.HOST_UNREACHABLE, { + message: 'host unreachable', + }), + ); + + await expect( + runCreateCommand({ ...baseOptions, context }), + ).rejects.toMatchObject({ details: { sessionId: 'session-01' } }); + expect(mocks.writeHumanErrorLines).not.toHaveBeenCalled(); + }); + it('keeps the details of the last error and adds the session id', async () => { mocks.sendRpc.mockRejectedValue( makeCliError(ERROR_CODES.HOST_TIMEOUT, { @@ -492,6 +525,109 @@ describe('create command', () => { expect(mocks.stopHost).toHaveBeenCalledOnce(); }); + describe('on Windows, when the marker write fails while the manifest names no program', () => { + const diskError = makeCliError(ERROR_CODES.STORAGE_WRITE_ERROR, { + message: 'i/o error', + }); + + beforeEach(() => { + const platform = process.platform; + Object.defineProperty(process, 'platform', { value: 'win32' }); + onTestFinished(() => { + Object.defineProperty(process, 'platform', { value: platform }); + }); + mocks.sendRpc.mockRejectedValue( + makeCliError(ERROR_CODES.HOST_UNREACHABLE, { + message: 'host unreachable', + }), + ); + }); + + it('retries the marker write, and reads the manifest after each write', async () => { + mocks.writeCreateFailedMarker + .mockRejectedValueOnce(diskError) + .mockResolvedValue(undefined); + + await expect( + runCreateCommand({ ...baseOptions, context }), + ).rejects.toMatchObject({ + code: 'HOST_UNREACHABLE', + details: { sessionId: 'session-01' }, + }); + + expect(mocks.writeCreateFailedMarker).toHaveBeenCalledTimes(2); + const lastWrite = Math.max( + ...mocks.writeCreateFailedMarker.mock.invocationCallOrder, + ); + const lastRead = Math.max( + ...mocks.readManifestIfExists.mock.invocationCallOrder, + ); + expect(lastWrite).toBeLessThan(lastRead); + expect(mocks.stopHost).not.toHaveBeenCalled(); + }); + + it('stops the host once the manifest names the program', async () => { + mocks.writeCreateFailedMarker.mockRejectedValue(diskError); + // The read after the third write finds the program. + mocks.readManifestIfExists.mockImplementation(() => + Promise.resolve( + mocks.writeCreateFailedMarker.mock.calls.length >= 3 + ? makeManifest({ childPid: 4321 }) + : makeManifest(), + ), + ); + + await expect( + runCreateCommand({ ...baseOptions, context }), + ).rejects.toMatchObject({ code: 'HOST_UNREACHABLE' }); + + expect(mocks.writeCreateFailedMarker).toHaveBeenCalledTimes(3); + expect(mocks.stopHost).toHaveBeenCalledOnce(); + }); + + it('gives up after 50 more writes', async () => { + mocks.writeCreateFailedMarker.mockRejectedValue(diskError); + + await expect( + runCreateCommand({ ...baseOptions, context }), + ).rejects.toMatchObject({ code: 'HOST_UNREACHABLE' }); + + expect(mocks.writeCreateFailedMarker).toHaveBeenCalledTimes(51); + expect(mocks.stopHost).not.toHaveBeenCalled(); + }); + + it('counts a host probe that throws as an exited host and keeps the error', async () => { + mocks.writeCreateFailedMarker.mockRejectedValue(diskError); + // A process of another user that took the host's pid answers EPERM. + mocks.isProcessAlive.mockImplementation(() => { + throw Object.assign(new Error('kill EPERM'), { code: 'EPERM' }); + }); + + await expect( + runCreateCommand({ ...baseOptions, context }), + ).rejects.toMatchObject({ + code: 'HOST_UNREACHABLE', + details: { sessionId: 'session-01' }, + }); + + expect(mocks.writeCreateFailedMarker).toHaveBeenCalledOnce(); + expect(mocks.stopHost).not.toHaveBeenCalled(); + }); + + it('stops retrying once the host has exited', async () => { + mocks.writeCreateFailedMarker.mockRejectedValue(diskError); + mocks.isProcessAlive.mockReturnValueOnce(true).mockReturnValue(false); + + await expect( + runCreateCommand({ ...baseOptions, context }), + ).rejects.toMatchObject({ code: 'HOST_UNREACHABLE' }); + + expect(mocks.isProcessAlive).toHaveBeenCalledWith(12345); + expect(mocks.writeCreateFailedMarker).toHaveBeenCalledTimes(2); + expect(mocks.stopHost).not.toHaveBeenCalled(); + }); + }); + it('leaves a host that answers alone', async () => { await runCreateCommand({ ...baseOptions, context }); diff --git a/test/unit/host/hostMarker.test.ts b/test/unit/host/hostMarker.test.ts index 43a90b74..228bccbb 100644 --- a/test/unit/host/hostMarker.test.ts +++ b/test/unit/host/hostMarker.test.ts @@ -1,13 +1,24 @@ +import { spawn } from 'node:child_process'; +import { once } from 'node:events'; import { existsSync, readFileSync, writeFileSync } from 'node:fs'; -import { mkdir, mkdtemp, rm } from 'node:fs/promises'; +import { mkdir, mkdtemp, realpath, rm } from 'node:fs/promises'; import { tmpdir } from 'node:os'; import { join } from 'node:path'; import process from 'node:process'; import { setTimeout as delay } from 'node:timers/promises'; -import { afterEach, beforeEach, describe, expect, it, vi } from 'vitest'; +import { + afterEach, + beforeEach, + describe, + expect, + it, + onTestFinished, + vi, +} from 'vitest'; import { runHost } from '../../../src/host/hostMain.js'; +import { readProcStat } from '../../../src/host/programGroup.js'; import type * as ProgramGroupModule from '../../../src/host/programGroup.js'; import type { SessionRecord } from '../../../src/protocol/schemas.js'; import { @@ -55,8 +66,59 @@ function readProgramGroup(): number { return pid; } +// The host records destroyed, its program's group is gone and its socket is +// removed. +async function expectHostStopped(group: number): Promise { + const deadline = Date.now() + 10_000; + let manifest = await readManifest(manifestPath(directory)); + while ( + manifest.status !== 'destroyed' || + isGroupAlive(group) || + existsSync(socketPath(directory)) + ) { + expect(Date.now()).toBeLessThan(deadline); + await delay(50); + manifest = await readManifest(manifestPath(directory)); + } +} + +// Spies on the timers before runHost starts. The returned function waits +// until the host's marker watch, its only 100 ms interval, has stopped. A +// stopped watch never checks for the marker again. +function trackMarkerWatch(): () => Promise { + const setSpy = vi.spyOn(globalThis, 'setInterval'); + const clearSpy = vi.spyOn(globalThis, 'clearInterval'); + return async () => { + const deadline = Date.now() + 10_000; + for (;;) { + const watches = setSpy.mock.calls.flatMap((call, index) => + call[1] === 100 ? [setSpy.mock.results[index]?.value as unknown] : [], + ); + expect(watches).toHaveLength(1); + if (clearSpy.mock.calls.some(([timer]) => timer === watches[0])) { + return; + } + expect(Date.now()).toBeLessThan(deadline); + await delay(20); + } + }; +} + +// Stops the host as a SIGTERM would. +function sendSigterm(): void { + for (const listener of process.rawListeners('SIGTERM')) { + if (!sigtermListeners.has(listener)) { + (listener as () => void)(); + } + } +} + beforeEach(async () => { - home = await mkdtemp(join(tmpdir(), 'agent-tty-host-marker-')); + // The host resolves its Home to the real path, and the socket path is + // derived from that path, as on macOS, where tmpdir() is a symlink. + home = await realpath( + await mkdtemp(join(tmpdir(), 'agent-tty-host-marker-')), + ); vi.stubEnv('AGENT_TTY_HOME', home); directory = sessionDir(home, SESSION_ID); await mkdir(directory, { recursive: true, mode: 0o700 }); @@ -80,6 +142,7 @@ beforeEach(async () => { }); afterEach(async () => { + vi.restoreAllMocks(); hooks.afterProgramRecord = () => {}; // runHost adds a SIGTERM listener that would outlive the test. for (const listener of process.rawListeners('SIGTERM')) { @@ -117,13 +180,137 @@ describe('runHost and the create-failed marker', () => { await runHost(SESSION_ID, process.pid); expect(existsSync(socketPath(directory))).toBe(false); - const group = readProgramGroup(); - const deadline = Date.now() + 10_000; - let manifest = await readManifest(manifestPath(directory)); - while (manifest.status !== 'destroyed' || isGroupAlive(group)) { - expect(Date.now()).toBeLessThan(deadline); - await delay(50); - manifest = await readManifest(manifestPath(directory)); - } + await expectHostStopped(readProgramGroup()); + }); + + it('stops a serving host when the marker appears while its creator runs', async () => { + await runHost(SESSION_ID, process.pid); + expect(existsSync(socketPath(directory))).toBe(true); + + await writeCreateFailedMarker( + createFailedMarkerPath(directory), + SESSION_ID, + ); + + await expectHostStopped(readProgramGroup()); }); + + it('keeps serving when the marker appears after its creator has exited', async () => { + const creator = spawn('sleep', ['30'], { stdio: 'ignore' }); + expect(creator.pid).toBeGreaterThan(0); + const watchStopped = trackMarkerWatch(); + await runHost(SESSION_ID, creator.pid as number); + expect(existsSync(socketPath(directory))).toBe(true); + creator.kill('SIGKILL'); + await once(creator, 'exit'); + await watchStopped(); + + await writeCreateFailedMarker( + createFailedMarkerPath(directory), + SESSION_ID, + ); + + expect((await readManifest(manifestPath(directory))).status).toBe( + 'running', + ); + expect(existsSync(socketPath(directory))).toBe(true); + sendSigterm(); + await expectHostStopped(readProgramGroup()); + }, 15_000); + + it('keeps serving when a process of another user takes the pid of its creator', async () => { + const creator = spawn('sleep', ['30'], { stdio: 'ignore' }); + onTestFinished(() => { + creator.kill('SIGKILL'); + }); + const creatorPid = creator.pid as number; + expect(creatorPid).toBeGreaterThan(0); + const watchStopped = trackMarkerWatch(); + await runHost(SESSION_ID, creatorPid); + expect(existsSync(socketPath(directory))).toBe(true); + // From here on, the probe of the creator's pid answers EPERM. + const kill = process.kill.bind(process); + vi.spyOn(process, 'kill').mockImplementation((pid, signal) => { + if (pid === creatorPid && signal === 0) { + throw Object.assign(new Error('kill EPERM'), { code: 'EPERM' }); + } + return kill(pid, signal); + }); + await watchStopped(); + + await writeCreateFailedMarker( + createFailedMarkerPath(directory), + SESSION_ID, + ); + + expect((await readManifest(manifestPath(directory))).status).toBe( + 'running', + ); + expect(existsSync(socketPath(directory))).toBe(true); + vi.restoreAllMocks(); + sendSigterm(); + await expectHostStopped(readProgramGroup()); + }, 15_000); + + it('stops when the creator writes the marker and exits between its probe and its check', async () => { + const creator = spawn('sleep', ['30'], { stdio: 'ignore' }); + onTestFinished(() => { + creator.kill('SIGKILL'); + }); + const creatorPid = creator.pid as number; + expect(creatorPid).toBeGreaterThan(0); + await runHost(SESSION_ID, creatorPid); + expect(existsSync(socketPath(directory))).toBe(true); + // The next probe finds the creator gone, and it wrote the marker first. + const kill = process.kill.bind(process); + vi.spyOn(process, 'kill').mockImplementation((pid, signal) => { + if (pid === creatorPid && signal === 0) { + writeFileSync(createFailedMarkerPath(directory), ''); + throw Object.assign(new Error('kill ESRCH'), { code: 'ESRCH' }); + } + return kill(pid, signal); + }); + + await expectHostStopped(readProgramGroup()); + }, 15_000); + + // kill(pid, 0) succeeds for a zombie, so only /proc shows that the creator + // has exited while its parent has yet to reap it. + it.runIf(process.platform === 'linux')( + 'stops the watch when its creator is a zombie', + async () => { + const parent = spawn( + '/bin/sh', + ['-c', 'sleep 0 & echo $!; exec sleep 30'], + { stdio: ['ignore', 'pipe', 'ignore'] }, + ); + onTestFinished(() => { + parent.kill('SIGKILL'); + }); + const [line] = (await once(parent.stdout, 'data')) as [Buffer]; + const zombie = Number(line.toString('utf8').trim()); + expect(zombie).toBeGreaterThan(1); + const deadline = Date.now() + 10_000; + while (readProcStat(zombie)?.state !== 'Z') { + expect(Date.now()).toBeLessThan(deadline); + await delay(20); + } + const watchStopped = trackMarkerWatch(); + await runHost(SESSION_ID, zombie); + expect(existsSync(socketPath(directory))).toBe(true); + await watchStopped(); + + await writeCreateFailedMarker( + createFailedMarkerPath(directory), + SESSION_ID, + ); + + expect((await readManifest(manifestPath(directory))).status).toBe( + 'running', + ); + sendSigterm(); + await expectHostStopped(readProgramGroup()); + }, + 20_000, + ); });