diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 8cbc79ac..dd4c172b 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -13,17 +13,18 @@ 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. The host's write then fails, or brings the folder back with only `session.json`. | -| R8 `DestroyedOnlyWhenEnded` | The manifest says destroyed only after the program has ended. | `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`. | +| 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` | The manifest says destroyed only after the program has ended. | `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. | `TypeOK` also runs in every run. When it breaks, the model is wrong, not the code. @@ -36,9 +37,9 @@ Yes, when the diff changes any of these: - `src/host/manifestWriter.ts` `createSerialManifestWriter`. - `src/cli/commands/gc.ts` `gcSessions`, `src/cli/commands/create.ts` `runCreateCommand` and `src/cli/commands/destroy.ts` `runDestroyCommand`. - `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/storage/manifests.ts` `readValidatedJsonFile`, `writeTextFileAtomic`, `writeValidatedJsonFile`, `writeManifest`. +- `src/storage/manifests.ts` `readValidatedJsonFile`, `replaceFileAtomic`, `writeManifest`. - The `SESSION_STATUS_POLICIES` table in `src/protocol/sessionStatusPolicy.ts`. -- Any new or removed call to `writeManifest`, `persistManifest`, `writeValidatedJsonFile`, `writeTextFileAtomic`, `manifestPath` or `reconcileSession` (also through an import alias), or a recursive `rm` (one with `recursive: true`, whatever its argument is named), anywhere in `src/`. +- Any new or removed call to `writeManifest`, `persistManifest`, `replaceFileAtomic`, `writeValidatedJsonFile`, `writeTextFileAtomic`, `manifestPath` or `reconcileSession` (also through an import alias), or a recursive `rm` (one with `recursive: true`, whatever its argument is named), anywhere in `src/`. - This skill's `model/SessionLifecycle.tla`, `scripts/facts.mjs` and `scripts/check.sh`: an edit to them also needs a new confirmed `coverage.json`. You do not have to judge this by hand. The check prints `STALE` when any of these changed since the sync commit. @@ -55,9 +56,9 @@ It needs `node`, Java 11 or newer (`java -version`), and the network once: the f What it does: -1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the twelve 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 thirteen 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 24 times and prints one line per run. +3. It runs TLC 25 times and prints one line per run. 4. It compares the hashes and call sites with `coverage.json`. Exit codes: 0 means every run gave the expected result and the covered code matches the sync record. 1 means at least one run gave an unexpected result; the line says `UNEXPECTED`. 3 means every result was as expected, but covered code changed since the sync commit; that is not a pass, so follow "When you change covered code on purpose". 2 means a tool could not run. When both 1 and 3 apply, the exit code is 1. @@ -66,14 +67,14 @@ Exit codes: 0 means every run gave the expected result and the covered code matc At the sync commit, the expected results are: -| Runs | Expected | Why | -| ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | -------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -| `current`, the code as it is, every rule | pass | No order of the modelled steps breaks a rule. This is the run that catches a new bug. | -| `witness-*` | violated | Each witness is a state that must be reachable: gc removes a session, a session serves, a resize lands, a clean exit is recorded, a crash is reconciled, a plain destroy completes, a SIGTERM shutdown is recorded, an exited session is destroyed, and `destroy --force` records a live session as destroyed. A witness that passes means the model can no longer reach that state, and the passing rules prove nothing. | -| `mutant-CreateRecordsHostPid`, `mutant-HostWaitsForManifest`, `mutant-ReconcileRereads`, `mutant-HostSerializesWrites`, `mutant-ReconcileSkipsLiveHost`, `mutant-HostStopsAfterTerminalWrite`, `mutant-DestroyRecordsDestroyed`, `mutant-DestroyKeepsExitCode`, `mutant-GcBothChecks`, `mutant-ShutdownBothChecks` | violated | Each run removes a guard from the model and checks only the rule that the guard protects. That rule must break, which shows the check can fail. | -| `mutant-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. | +| Runs | Expected | Why | +| ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `current`, the code as it is, every rule | pass | No order of the modelled steps breaks a rule. This is the run that catches a new bug. | +| `witness-*` | violated | Each witness is a state that must be reachable: gc removes a session, a session serves, a resize lands, a clean exit is recorded, a crash is reconciled, a plain destroy completes, a SIGTERM shutdown is recorded, an exited session is destroyed, and `destroy --force` records a live session as destroyed. A witness that passes means the model can no longer reach that state, and the passing rules prove nothing. | +| `mutant-CreateRecordsHostPid`, `mutant-HostWaitsForManifest`, `mutant-ReconcileRereads`, `mutant-HostSerializesWrites`, `mutant-ReconcileSkipsLiveHost`, `mutant-HostStopsAfterTerminalWrite`, `mutant-DestroyRecordsDestroyed`, `mutant-DestroyKeepsExitCode`, `mutant-ManifestWriteNeedsFolder`, `mutant-GcBothChecks`, `mutant-ShutdownBothChecks` | violated | Each run removes a guard from the model and checks only the rule that the guard protects. That rule must break, which shows the check can fail. | +| `mutant-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. | 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`. @@ -172,6 +173,23 @@ node --import tsx src/cli/main.ts destroy "$id" --force --json # returns in ab node --import tsx src/cli/main.ts inspect "$id" --json # status: destroyed ``` +### `ManifestWriteNeedsFolder`: a late write brings a removed folder back (R10) + +Without the guard, `writeManifest` went through `writeTextFileAtomic`, which runs `mkdir` before every write. A manifest write that landed after gc removed the session folder created the folder again, holding only `session.json`. `destroy` and `reconcileSession` both did that, and `list --all` showed the stub session until the next gc. + +Now `writeManifest` writes the temp file and renames it with no `mkdir`, so a write into a removed folder fails with `SESSION_NOT_FOUND`. `reconcileSession` then returns. `destroy` reports `SESSION_NOT_FOUND`, as it does when its reads find no manifest. A host write fails too. A failed start-up or exit write ends the host, and a failed resize write fails only that RPC. + +```sh +id=$(node --import tsx src/cli/main.ts create --json -- sleep 300 | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))') +LOG=$(mktemp) +REPLAY_LOG=$LOG REPLAY_HOLD='destroy:readFile:/session.json:2:3000' NODE_OPTIONS="$HOLD" \ + node --import tsx src/cli/main.ts destroy "$id" --force --json & +until grep -q hold "$LOG"; do sleep 0.1; done # destroy holds its read after the kill +node --import tsx src/cli/main.ts gc --json # removes the session folder +wait # destroy prints SESSION_NOT_FOUND +ls "$AGENT_TTY_HOME/sessions" # empty: the folder stays removed +``` + ## When you change covered code on purpose 1. Read the diff of every item that `STALE` lists, and the commits that the check prints. For a change that is not committed yet, read `git diff`. @@ -186,20 +204,20 @@ 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`, 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`), one SIGTERM to the host, a program exit at any time, and a host crash at any time. The current model has 451,432 distinct states, and the check prints that count. +The model checks every order of these steps for one session: one `create`, 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`), one SIGTERM to the host, a program exit at any time, and a host crash at any time. The current model has 438,636 distinct states, and the check prints that count. It assumes: - A pid is not reused while the check looks at it, so `isProcessAlive(hostPid)` is true exactly while the host lives. -- A manifest write is atomic, because `writeTextFileAtomic` renames a temp file. A write that fails counts as a host crash or a failed command. +- A manifest write is atomic, because `writeManifest` renames a temp file. A write that fails counts as a host crash or a failed command. That covers a host write into a removed folder, which only a state that already breaks R1 reaches. - The host waits for its manifest while the `create` process lives, so it gives up only when `create` dies before that write. That counts as a host crash, which R6 does not cover. -- gc's `rm(sessionDirectory, { recursive: true })` is one step, though the real `rm` deletes file by file. R1 already forbids removing a session whose host can still write, so the order of the deleted files does not matter. +- gc's `rm(sessionDirectory, { recursive: true })` is one step, though the real `rm` deletes file by file. R1 already forbids removing a session whose host can still write, so for the host the order of the deleted files does not matter. R10 is different. A reconcile or `destroy` write that lands during the real `rm` makes it fail with `ENOTEMPTY` and leaves the folder with only `session.json`, until the next gc removes it (coder/agent-tty#202). - Steps that only lead to the same outcome are joined: gc's `readdir` and `stat` (both only skip), the host's `EventLog.open` and `createPty` (synchronous after the open), and `recordExit` with the `exit` event append (no other process sees them). - A program ends with its host: a host crash or the SIGKILL of `destroy --force` ends both. `reconcileSession` also kills a live child of a dead host, which the model leaves out. - The `destroy` RPC is one step: the host's handler does the work. `destroySession`'s own `reconcileSession` calls are the reconciles of the other command, so `destroy` itself only reads after them. A poll that reads an active status is either retried later or is the last of its 50 tries. - Only the "destroying" write of `initiateShutdown` can wait for its turn while the in-memory status changes, so only it keeps its snapshot in the model. The start-up, resize and exit writes carry a status that cannot change before their turn. -It leaves out: a second `destroy` or a second SIGTERM, a rule that a folder gc removed stays removed (the `mkdir` in `writeTextFileAtomic` lets `destroy` and `reconcileSession` bring it back, coder/agent-tty#196), a SIGTERM before the host registers its handler (a crash covers it), a `destroy` RPC that fails for a reason other than an unreachable host (it writes nothing), `gc --stale-only` and `--older-than` (they only skip more), `gc --dry-run` (the other command covers its reconcile), the `rm` in `create`'s error path and in `doctor`, the Home registry, the contents of the event log and of the renderer, the kill of a child process whose host died, and the socket liveness probe in `rpcServer.listen`. A pass covers the model, not the whole product. +It leaves out: a second `destroy` or a second SIGTERM, a SIGTERM before the host registers its handler (a crash covers it), a `destroy` RPC that fails for a reason other than an unreachable host (it writes nothing), `gc --stale-only` and `--older-than` (they only skip more), `gc --dry-run` (the other command covers its reconcile), the `rm` in `create`'s error path and in `doctor`, the Home registry, the artifact commands (`snapshot`, `screenshot`, `record export`, whose `ensureArtifactsDir` can still bring back a removed folder, coder/agent-tty#198), the contents of the event log and of the renderer, the kill of a child process whose host died, and the socket liveness probe in `rpcServer.listen`. A pass covers the model, not the whole product. ## Coverage record diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index f01de089..17778fba 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -13,7 +13,7 @@ "src/host/lifecycle.ts#stopSessionProcesses": "c2121dfa9d2c0d43", "src/host/lifecycle.ts#recordDestroyed": "6610e88a55a2aa0d", "src/host/lifecycle.ts#destroySession": "b2713e315822b08d", - "src/host/lifecycle.ts#reconcileSession": "32e17d1bc75bb636", + "src/host/lifecycle.ts#reconcileSession": "c506c699762d398f", "src/host/hostMain.ts#waitForManifestFromCreate": "fd500651f83683eb", "src/host/hostMain.ts#isSessionCommandable": "260060f07b068ec1", "src/host/manifestWriter.ts#createSerialManifestWriter": "94a2decf4fedb2e2", @@ -26,16 +26,16 @@ "src/host/rpcServer.ts#RpcServer.listen": "aa62e1cd89eceaa4", "src/host/rpcServer.ts#RpcServer.close": "2d8092cceb4b8e13", "src/storage/manifests.ts#readValidatedJsonFile": "6287eb627b09bf80", - "src/storage/manifests.ts#writeTextFileAtomic": "87f4e3ecc13dbe59", - "src/storage/manifests.ts#writeManifest": "97c755b27788a6e5", + "src/storage/manifests.ts#replaceFileAtomic": "20532509b3dcaade", + "src/storage/manifests.ts#writeManifest": "1bcc99f09acfc577", "src/protocol/sessionStatusPolicy.ts#SESSION_STATUS_POLICIES": "83827f9f7f6b8e1d", "src/host/hostMain.ts#runHost(parts)": "d2cd124b6e820920", "src/host/hostMain.ts#runHost(final try)": "ad91fa180ff36ffb", "src/host/hostMain.ts#runHost>handlers.resize": "30dd1da32879d478", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "10ba06448b1bd6ff", - "skill:scripts/facts.mjs": "553e1cac7b74042a", - "skill:scripts/check.sh": "8059eab056acc01b" + "skill:model/SessionLifecycle.tla": "0b52bbddfeae290c", + "skill:scripts/facts.mjs": "82268d59fc07d657", + "skill:scripts/check.sh": "8ce08f1c1196895f" }, "callSites": { "writeManifest": [ @@ -49,9 +49,12 @@ "src/host/hostMain.ts#runHost>initiateShutdown", "src/host/hostMain.ts#runHost>resize" ], + "replaceFileAtomic": [ + "src/storage/manifests.ts#writeManifest", + "src/storage/manifests.ts#writeTextFileAtomic" + ], "writeValidatedJsonFile": [ "src/storage/artifactManifest.ts#writeArtifactManifest", - "src/storage/manifests.ts#writeManifest", "src/tools/canonicalBundleArtifacts.ts#writeCanonicalBundleManifest" ], "writeTextFileAtomic": [ diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index 446600e4..b947dc8f 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -47,6 +47,7 @@ CONSTANTS \* records destroyed through recordDestroyed DestroyKeepsExitCode, \* lifecycle.ts: recordDestroyed writes \* { ...manifest, status, updatedAt } only + ManifestWriteNeedsFolder, \* manifests.ts: writeManifest runs no mkdir MaxListReconciles \* how many times the "list" process reconciles ASSUME MaxListReconciles \in 1..3 @@ -55,7 +56,8 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, ReconcileSkipsTerminal, HostWaitsForManifest, ReconcileRereads, HostSerializesWrites, HostStopsAfterTerminalWrite, ShutdownChecksCommandable, - DestroyRecordsDestroyed, DestroyKeepsExitCode} : b \in BOOLEAN + DestroyRecordsDestroyed, DestroyKeepsExitCode, + ManifestWriteNeedsFolder} : b \in BOOLEAN Readers == {"gc", "list"} \* the two processes that run reconcileSession NoRead == [pid |-> FALSE, origin |-> "none", code |-> FALSE] @@ -124,9 +126,13 @@ Init == /\ dpc = "read" /\ dforce \in BOOLEAN /\ drd = NoRead /\ dres = "pending" /\ dsaw = FALSE /\ dkill = FALSE -\* writeManifest -> writeTextFileAtomic in src/storage/manifests.ts: mkdir -p -\* the session directory, write a temp file, rename it over session.json. -\* The rename is the visible step. The mkdir brings back a removed directory. +\* writeManifest in src/storage/manifests.ts: write a temp file in the session +\* directory and rename it over session.json. The rename is the visible step. +\* WriteLands: with ManifestWriteNeedsFolder there is no mkdir, so a write into +\* a removed directory throws SESSION_NOT_FOUND and creates nothing. Without +\* it, the write runs mkdir first and brings the directory back. +WriteLands == dir \/ ~ManifestWriteNeedsFolder + Write(s, pid, origin, code) == /\ dir' = TRUE /\ mst' = s @@ -168,7 +174,9 @@ CreateMakesDirectory == ghostVars, sock, hostVars, shutVars, readerVars, destroyVars>> -\* allocateSession: writeManifest with status "running". +\* allocateSession: writeManifest with status "running". gc skips a directory +\* without a manifest, so this write always finds its directory (TypeOK +\* checks that). CreateWritesManifest == /\ cpc = "write" /\ Write("running", CreateRecordsHostPid, "none", FALSE) @@ -205,10 +213,12 @@ WriterStopped == HostSerializesWrites /\ HostStopsAfterTerminalWrite /\ hwt \* A host write lands, or writes nothing once the writer has stopped. The \* record carries the exit code once recordExit or recordDestroyed ran. +\* WriteLands is false here only in a state that already breaks R1. HostWrite(s, code) == IF WriterStopped THEN UNCHANGED <> - ELSE /\ Write(s, TRUE, "none", code) + ELSE /\ WriteLands + /\ Write(s, TRUE, "none", code) /\ hwt' = (hwt \/ s \in Terminal) \* A write lands. When the queued "destroying" write is next, its turn starts @@ -427,14 +437,19 @@ ReconcileRereadsManifest(p) == \* writeManifest(reconciledManifest): "running" becomes failed/host-death, \* "destroying" becomes destroyed, any other status that gets here becomes \* failed/unknown (the default branch). hostPid and childPid become null. +\* When the directory is gone, the write throws SESSION_NOT_FOUND and +\* reconcileSession returns. ReconcileWrites(p) == /\ pc[p] = "r_write" - /\ CASE rd[p].st = "running" -> - Write("failed", FALSE, "host-death", rd[p].code) - [] rd[p].st = "destroying" -> - Write("destroyed", FALSE, "none", rd[p].code) - [] OTHER -> Write("failed", FALSE, "unknown", rd[p].code) - /\ pc' = [pc EXCEPT ![p] = "r_unlink"] + /\ IF WriteLands + THEN /\ CASE rd[p].st = "running" -> + Write("failed", FALSE, "host-death", rd[p].code) + [] rd[p].st = "destroying" -> + Write("destroyed", FALSE, "none", rd[p].code) + [] OTHER -> Write("failed", FALSE, "unknown", rd[p].code) + /\ pc' = [pc EXCEPT ![p] = "r_unlink"] + ELSE /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)] + /\ UNCHANGED diskVars /\ UNCHANGED <> @@ -554,14 +569,19 @@ DestroyReads == readerVars, dforce, dkill>> \* recordDestroyed: writeManifest({ ...manifest, status: 'destroyed' }) from -\* the copy that destroy read. Its mkdir brings back a folder that gc -\* removed in the meantime (coder/agent-tty#196). +\* the copy that destroy read. When gc removed the directory in the meantime, +\* the write throws SESSION_NOT_FOUND, and destroy reports that error. DestroyWritesDestroyed == /\ dpc = "twrite" - /\ Write("destroyed", drd.pid, drd.origin, DestroyKeepsExitCode /\ drd.code) - /\ dpc' = "tunlink" /\ drd' = NoRead /\ dsaw' = TRUE + /\ IF WriteLands + THEN /\ Write("destroyed", drd.pid, drd.origin, + DestroyKeepsExitCode /\ drd.code) + /\ dpc' = "tunlink" /\ drd' = NoRead /\ dsaw' = TRUE + /\ UNCHANGED dres + ELSE /\ DestroyEnds("error") + /\ UNCHANGED diskVars /\ UNCHANGED <> + dforce, dkill>> \* recordDestroyed: unlinkIfPresent(socketFile). destroy reports success. DestroyUnlinksSocket == @@ -683,6 +703,7 @@ TypeOK == /\ dsnap \in {"none", "destroying", "destroyed"} /\ (mst # "none") => dir /\ (dir /\ mst = "none") => cpc # "done" + /\ (cpc = "write") => dir /\ gres \in {"pending", "skipped", "removed"} /\ lruns \in 0..MaxListReconciles /\ dres \in {"pending", "ok", "error"} @@ -740,6 +761,9 @@ DestroyedOnlyWhenEnded == \* R9: destroy reports success only after it wrote destroyed or read it. DestroyEndsDestroyed == dres = "ok" => dsaw +\* R10: once gc removed the session directory, no write brings it back. +RemovedFolderStaysRemoved == gres = "removed" => ~dir + \* Witnesses. check.sh expects TLC to report each one VIOLATED, which shows \* that the model reaches the state: the rules above are not true only \* because the model can never get there. diff --git a/.agents/skills/verify-session-lifecycle/model/statechart-view.mjs b/.agents/skills/verify-session-lifecycle/model/statechart-view.mjs index 94f0c53c..f586b5f6 100644 --- a/.agents/skills/verify-session-lifecycle/model/statechart-view.mjs +++ b/.agents/skills/verify-session-lifecycle/model/statechart-view.mjs @@ -4,6 +4,8 @@ const reader = (from, to) => from.pc.gc === to.pc.gc ? 'another command' : 'gc'; const reconciles = (from, to) => `${reader(from, to)} reconciles:`; +const back = (from, to) => + !from.dir && to.dir ? ' and brings back the session folder' : ''; export const title = 'One agent-tty session while gc, destroy and another command run'; @@ -89,7 +91,9 @@ export const step = (action, from, to) => { case 'ReconcileRereadsManifest': return `${reconciles(from, to)} reads the manifest again`; case 'ReconcileWrites': - return `${reconciles(from, to)} writes "${to.mst}"`; + return to.dir + ? `${reconciles(from, to)} writes "${to.mst}"${back(from, to)}` + : `${reconciles(from, to)} finds the folder gone and returns`; case 'ReconcileUnlinksSocket': return `${reconciles(from, to)} unlinks the socket file`; case 'GcFindsDirectory': @@ -109,7 +113,9 @@ export const step = (action, from, to) => { ? 'destroy reads the manifest and fails' : 'destroy reads the manifest'; case 'DestroyWritesDestroyed': - return 'destroy writes "destroyed"'; + return to.dir + ? `destroy writes "destroyed"${back(from, to)}` + : 'destroy finds the folder gone and fails'; case 'DestroyUnlinksSocket': return 'destroy unlinks the socket file and succeeds'; case 'DestroyKills': diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index 18144f8e..c03d090d 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/check.sh +++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh @@ -122,7 +122,7 @@ TERMINAL=$(node -e ' const c = JSON.parse(require("node:fs").readFileSync(process.argv[1], "utf8")).constants; console.log("{" + c.Terminal.map((s) => JSON.stringify(s)).join(", ") + "}"); ' "$OUT/facts.json") -GUARDS="GcSkipsNonCollectable GcFinalCheck ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode" +GUARDS="GcSkipsNonCollectable GcFinalCheck ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder" # 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; @@ -132,7 +132,7 @@ FACTS_LINE=$(node -e ' }).join(" ")); ' "$OUT/facts.json" $GUARDS) || die "facts.json lacks a guard fact" -RULES="NoLiveSessionDeleted HostDeathOnlyWhenDead TerminalIsFinal RecordedExitKept RunningSessionReachable HostStartsWhenCreated TerminalIsLastWrite DestroyedOnlyWhenEnded DestroyEndsDestroyed" +RULES="NoLiveSessionDeleted HostDeathOnlyWhenDead TerminalIsFinal RecordedExitKept RunningSessionReachable HostStartsWhenCreated TerminalIsLastWrite DestroyedOnlyWhenEnded DestroyEndsDestroyed RemovedFolderStaysRemoved" WITNESSES="WitnessGcRemovesSession WitnessSessionServes WitnessResizeLands WitnessCleanExitRecorded WitnessCrashReconciled WitnessDestroyCompletes WitnessSigtermRecorded WitnessDestroyExitedSession WitnessForceDestroyRecorded" # --- runs ---------------------------------------------------------------- @@ -180,6 +180,7 @@ write_run mutant-ReconcileSkipsLiveHost violated HostDeathOnlyWhenDead "Reconcil write_run mutant-HostStopsAfterTerminalWrite violated TerminalIsLastWrite "HostStopsAfterTerminalWrite=FALSE" "without the stop, the exit write follows a destroyed record" TerminalIsLastWrite write_run mutant-DestroyRecordsDestroyed violated DestroyEndsDestroyed "DestroyRecordsDestroyed=FALSE" "without recordDestroyed, destroy succeeds on a session that is not destroyed" DestroyEndsDestroyed write_run mutant-DestroyKeepsExitCode violated RecordedExitKept "DestroyKeepsExitCode=FALSE" "without it, destroy writes destroyed without the exit code" RecordedExitKept +write_run mutant-ManifestWriteNeedsFolder violated RemovedFolderStaysRemoved "ManifestWriteNeedsFolder=FALSE" "without it, a write after gc's rm brings the folder back" RemovedFolderStaysRemoved 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" diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 6019303a..303b02cd 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -135,7 +135,7 @@ function reconcileFacts() { 'manifest.hostPid !== null && hostAlive', ts.SyntaxKind.ReturnStatement, ); - const write = indexOfStatement(body, /^await writeManifest\(/); + const write = indexOfStatement(body, /^(?:try \{\s*)?await writeManifest\(/); // The re-read after the host is found dead, its guard, and a reconciled // record built from that copy, all before the write. const reread = indexOfStatement( @@ -418,6 +418,38 @@ function destroyFacts() { }; } +function manifestWriteFacts() { + const file = 'src/storage/manifests.ts'; + const visited = new Set(); + let renames = 0; + let mkdirs = 0; + const visit = (fn) => { + walk(fn.body, (node) => { + if (!ts.isCallExpression(node) || !ts.isIdentifier(node.expression)) { + return; + } + const name = node.expression.text; + if (name === 'rename') { + renames += 1; + } + if (name === 'mkdir' || name === 'mkdirSync') { + mkdirs += 1; + } + const local = findDeclaration(file, name); + if ( + local !== undefined && + ts.isFunctionDeclaration(local) && + !visited.has(name) + ) { + visited.add(name); + visit(local); + } + }); + }; + visit(requireDeclaration(file, 'writeManifest')); + return { ManifestWriteNeedsFolder: renames > 0 && mkdirs === 0 }; +} + function gcFacts() { const fn = requireDeclaration('src/cli/commands/gc.ts', 'gcSessions'); let loop; @@ -515,7 +547,7 @@ const COVERED = [ ['src/host/rpcServer.ts', 'RpcServer.listen'], ['src/host/rpcServer.ts', 'RpcServer.close'], ['src/storage/manifests.ts', 'readValidatedJsonFile'], - ['src/storage/manifests.ts', 'writeTextFileAtomic'], + ['src/storage/manifests.ts', 'replaceFileAtomic'], ['src/storage/manifests.ts', 'writeManifest'], ['src/protocol/sessionStatusPolicy.ts', 'SESSION_STATUS_POLICIES'], ]; @@ -657,6 +689,7 @@ function hasRecursiveOption(call) { const TRACKED_CALLS = [ 'writeManifest', 'persistManifest', + 'replaceFileAtomic', 'writeValidatedJsonFile', 'writeTextFileAtomic', 'manifestPath', @@ -729,6 +762,7 @@ const constants = { ...createFacts(), ...hostFacts(), ...destroyFacts(), + ...manifestWriteFacts(), ...policyFacts(), }; console.log( diff --git a/src/host/README.md b/src/host/README.md index 9bc45cf3..07d0eb22 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -41,8 +41,8 @@ - The `signal` handler accepts only `SIGTERM`, `SIGINT`, `SIGKILL`, `SIGHUP`, `SIGUSR1` and `SIGUSR2`, and throws `INVALID_SIGNAL` for others. [hostMain.ts:runHost] - The `run` handler waits 30,000 ms by default. The `wait` handler needs exactly one of `exit` or `idleMs`, else it throws `INVALID_DURATION`. `waitForRender` polls every 200 ms. [hostMain.ts:runHost] - `runHost` handles PTY exit once. If the status is `destroying` it records `destroyed`, else `exited`. Shutdown runs once. [hostMain.ts:runHost] -- `destroySession` throws `SESSION_NOT_FOUND` when there is no manifest and `SESSION_ALREADY_DESTROYED` for a destroyed session. A terminal session moves to `destroyed` without a signal. A running session gets the `destroy` RPC, or `SIGKILL` with `force`. It polls every 100 ms for at most 50 attempts and throws `HOST_TIMEOUT` if the status is still not terminal. [lifecycle.ts:destroySession] -- `reconcileSession` does nothing when the manifest is missing, the status is terminal or the host PID is alive. A null `hostPid` counts as a dead host. `allocateSession` writes the host PID into the first manifest, so a new session already has a `hostPid`. After the liveness check, `reconcileSession` reads the manifest again and does nothing when it is now missing or terminal. Otherwise it maps the status it read again: `running` to `failed` (failure origin `host-death`), `exiting` to `exited`, `destroying` to `destroyed` and any other status to `failed` (origin `unknown`), and sets both PIDs to `null`. [lifecycle.ts:reconcileSession] +- `destroySession` throws `SESSION_NOT_FOUND` when there is no manifest, or when the session directory is gone at its `destroyed` write, and `SESSION_ALREADY_DESTROYED` for a destroyed session. A terminal session moves to `destroyed` without a signal. A running session gets the `destroy` RPC, or `SIGKILL` with `force`. It polls every 100 ms for at most 50 attempts and throws `HOST_TIMEOUT` if the status is still not terminal. [lifecycle.ts:destroySession] +- `reconcileSession` does nothing when the manifest is missing, the status is terminal or the host PID is alive. A null `hostPid` counts as a dead host. `allocateSession` writes the host PID into the first manifest, so a new session already has a `hostPid`. After the liveness check, `reconcileSession` reads the manifest again and does nothing when it is now missing or terminal. Otherwise it maps the status it read again: `running` to `failed` (failure origin `host-death`), `exiting` to `exited`, `destroying` to `destroyed` and any other status to `failed` (origin `unknown`), and sets both PIDs to `null`. When the session directory is gone at that write, it returns. [lifecycle.ts:reconcileSession] - `allocateSession` throws `INVALID_DIMENSIONS` for non-positive `cols` or `rows`, `STORAGE_READ_ERROR` when `cwd` is not a directory and `INVALID_INPUT` when the shell path is not a file. An empty `command` defaults to the shell path. It creates the session directory and calls `launch` only after these checks pass. [lifecycle.ts:allocateSession] - `buildReplayInput` validates the manifest with `SessionRecordSchema` and requires its `sessionId` to match. It validates the events with `validateEventRecords` unless `trustValidated` is set. `targetSeq` is -1 for no events, else from 0 to the last `seq`. [replay.ts:buildReplayInput] - `RpcServer.listen` removes a stale socket file (no answer within 1,000 ms, `ECONNREFUSED` or `ENOENT`) and throws when another server is listening. It asserts a socket path of at most 104 characters. [rpcServer.ts:RpcServer] diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index 7e33b67f..6b482160 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -742,6 +742,16 @@ export async function reconcileSession( ...(failureOrigin !== undefined ? { failureOrigin } : {}), }; - await writeManifest(manifestFile, reconciledManifest); + try { + await writeManifest(manifestFile, reconciledManifest); + } catch (error) { + if ( + error instanceof CliError && + error.code === ERROR_CODES.SESSION_NOT_FOUND + ) { + return; + } + throw error; + } await unlinkIfPresent(socketPath(sessionDirectory)); } diff --git a/src/storage/README.md b/src/storage/README.md index 08c3a96b..0e51b5bf 100644 --- a/src/storage/README.md +++ b/src/storage/README.md @@ -31,7 +31,7 @@ - `artifactPath` rejects a file name that is empty or has `/` or `\`, and asserts that the result is directly inside `/artifacts`. File-name builders replace unsafe characters in the profile name with `-` and require a non-negative integer `seq`. [artifactPaths.ts:artifactPath] [artifactPaths.ts:screenshotFilename] - `assertEventLogSize` requires an integer from 0 to `MAX_EVENT_LOG_SIZE`. `readEventLogRecords` checks the size with `stat` before it reads the file. [eventLogCodec.ts:assertEventLogSize] [eventLogCodec.ts:readEventLogRecords] - `parseEventLogContent` and `validateEventRecords` require each record to match `EventRecordSchema`, the first `seq` to be 0, and each next `seq` to be the previous one plus 1. Blank lines are skipped. [eventLogCodec.ts:parseEventLogContent] [eventLogCodec.ts:validateEventRecords] -- Read and write paths in `manifests.ts` must be non-empty and absolute. Invalid JSON and schema failures throw `MANIFEST_VALIDATION_ERROR`. Other read errors throw `STORAGE_READ_ERROR`. Write failures throw `STORAGE_WRITE_ERROR`. [manifests.ts:readValidatedJsonFile] [manifests.ts:writeTextFileAtomic] [manifests.ts:writeManifest] +- Read and write paths in `manifests.ts` must be non-empty and absolute. Invalid JSON and schema failures throw `MANIFEST_VALIDATION_ERROR`. Other read errors throw `STORAGE_READ_ERROR`. Write failures throw `STORAGE_WRITE_ERROR`, except that `writeManifest` throws `SESSION_NOT_FOUND` when the session directory is gone. [manifests.ts:readValidatedJsonFile] [manifests.ts:writeTextFileAtomic] [manifests.ts:writeManifest] - `ArtifactEntrySchema` and `ArtifactManifestSchema` are `.strict()`. `kind` is `screenshot`, `snapshot`, `recording` or `video`. `capturedAtSeq` is a non-negative integer. The manifest `version` is the literal `1`. The manifest and entry `sessionId` must equal the session directory name. [artifactManifest.ts:ArtifactEntrySchema] [artifactManifest.ts:ArtifactManifestSchema] - `appendArtifactWithRollback` serializes appends per session directory with an in-process `KeyedSerializer` (from `src/util/keyedSerializer.ts`). Appends from two processes are not serialized. [artifactManifest.ts:appendArtifactWithRollback] - `computeArtifactHealth` maps only `MANIFEST_VALIDATION_ERROR` to health `manifest-invalid` and rethrows other errors. It validates its result with `ArtifactHealthSummarySchema`. [artifactHealth.ts:computeArtifactHealth] @@ -44,7 +44,7 @@ - `resolveHome` reads `process.env.AGENT_TTY_HOME` and calls `os.homedir()` and `realpathSync`. [home.ts:resolveHome] - `ensureHome` calls `mkdir(home, { recursive: true })`. It runs `chmod(home, 0o700)` only when `mkdir` created the directory. [home.ts:ensureHome] -- `writeTextFileAtomic` creates the parent directory, writes `.tmp-` with mode `0o600`, then renames it to ``. On failure it removes the temp file. It does not call `fsync`. `writeManifest`, `writeValidatedJsonFile`, `writeArtifactManifest` and the registry writes all go through it. [manifests.ts:writeTextFileAtomic] +- `writeTextFileAtomic` creates the parent directory, writes `.tmp-` with mode `0o600`, then renames it to ``. On failure it removes the temp file. It does not call `fsync`. `writeValidatedJsonFile`, `writeArtifactManifest` and the registry writes all go through it. `writeManifest` writes and renames the temp file the same way but creates no directory, so it cannot bring back a session directory that `gc` removed. [manifests.ts:writeTextFileAtomic] [manifests.ts:writeManifest] - `readValidatedJsonFile` and `readEventLogRecords` read files with `fs.promises.readFile`. `readEventLogRecords` also calls `stat`. [manifests.ts:readValidatedJsonFile] [eventLogCodec.ts:readEventLogRecords] - `ensureArtifactsDir` runs `mkdir(/artifacts, { recursive: true })`. The other path functions are pure, and `socketPath` only hashes strings with `crypto`. [artifactPaths.ts:ensureArtifactsDir] [sessionPaths.ts:socketPath] - `appendArtifactWithRollback` reads, changes and writes the artifact manifest. On failure it calls `rm(rollbackArtifactPath, { force: true })`. [artifactManifest.ts:appendArtifactWithRollback] diff --git a/src/storage/manifests.ts b/src/storage/manifests.ts index 8e167790..1a087a95 100644 --- a/src/storage/manifests.ts +++ b/src/storage/manifests.ts @@ -97,23 +97,30 @@ export async function readValidatedJsonFile( ); } +async function replaceFileAtomic( + path: string, + contents: string, +): Promise { + const temporaryPath = `${path}.tmp-${randomUUID()}`; + + try { + await writeFile(temporaryPath, contents, { encoding: 'utf8', mode: 0o600 }); + await rename(temporaryPath, path); + } catch (error) { + await rm(temporaryPath, { force: true }).catch(() => undefined); + throw error; + } +} + export async function writeTextFileAtomic( options: WriteTextFileAtomicOptions, ): Promise { assertAbsoluteStoragePath(options.path, options.pathLabel); - const outputDirectory = dirname(options.path); - const temporaryPath = `${options.path}.tmp-${randomUUID()}`; - try { - await mkdir(outputDirectory, { recursive: true }); - await writeFile(temporaryPath, options.contents, { - encoding: 'utf8', - mode: 0o600, - }); - await rename(temporaryPath, options.path); + await mkdir(dirname(options.path), { recursive: true }); + await replaceFileAtomic(options.path, options.contents); } catch (error) { - await rm(temporaryPath, { force: true }).catch(() => undefined); throw makeCliError(ERROR_CODES.STORAGE_WRITE_ERROR, { message: options.writeErrorMessage, details: { path: options.path }, @@ -183,11 +190,24 @@ export async function writeManifest( path: string, record: SessionRecord, ): Promise { - await writeValidatedJsonFile({ - path, - pathLabel: 'manifest path', - data: record, - writeErrorMessage: `Failed to write session manifest at ${path}.`, - validate: validateManifestData, - }); + assertAbsoluteStoragePath(path, 'manifest path'); + const manifest = validateManifestData(path, record); + + try { + await replaceFileAtomic(path, `${JSON.stringify(manifest, null, 2)}\n`); + } catch (error) { + if (isEnoentError(error)) { + throw makeCliError(ERROR_CODES.SESSION_NOT_FOUND, { + message: `Session "${manifest.sessionId}" was not found: its folder ${dirname(path)} no longer exists.`, + details: { sessionId: manifest.sessionId, manifestPath: path }, + cause: error, + }); + } + + throw makeCliError(ERROR_CODES.STORAGE_WRITE_ERROR, { + message: `Failed to write session manifest at ${path}.`, + details: { path }, + cause: error, + }); + } } diff --git a/test/unit/cli/commandTarget.test.ts b/test/unit/cli/commandTarget.test.ts index d4f22345..360eff6f 100644 --- a/test/unit/cli/commandTarget.test.ts +++ b/test/unit/cli/commandTarget.test.ts @@ -1,4 +1,4 @@ -import { mkdtemp, rm } from 'node:fs/promises'; +import { mkdir, mkdtemp, rm } from 'node:fs/promises'; import { tmpdir } from 'node:os'; import { join } from 'node:path'; @@ -44,7 +44,9 @@ async function writeSessionManifest( childPid: status === 'running' ? 456 : null, exitCode: status === 'exited' ? 0 : null, }); - await writeManifest(manifestPath(sessionDir(home, sessionId)), manifest); + const directory = sessionDir(home, sessionId); + await mkdir(directory, { recursive: true }); + await writeManifest(manifestPath(directory), manifest); return manifest; } diff --git a/test/unit/host/lifecycle.test.ts b/test/unit/host/lifecycle.test.ts index fc07fb24..190035aa 100644 --- a/test/unit/host/lifecycle.test.ts +++ b/test/unit/host/lifecycle.test.ts @@ -6,8 +6,29 @@ import process from 'node:process'; import { afterEach, beforeEach, describe, expect, it, vi } from 'vitest'; +const fsHooks = vi.hoisted(() => ({ + afterReadFile: undefined as ((path: string) => Promise) | undefined, +})); + +vi.mock('node:fs/promises', async () => { + const actual = await vi.importActual('node:fs/promises'); + const readFile = async ( + ...args: Parameters + ): Promise => { + const contents = await actual.readFile(...args); + if (typeof args[0] === 'string') { + await fsHooks.afterReadFile?.(args[0]); + } + return contents; + }; + return { ...actual, readFile }; +}); + +import type * as FsPromises from 'node:fs/promises'; + import { allocateSession, + destroySession, reconcileSession, type AllocateConfig, } from '../../../src/host/lifecycle.js'; @@ -26,9 +47,41 @@ beforeEach(async () => { afterEach(async () => { vi.restoreAllMocks(); + vi.unstubAllEnvs(); + fsHooks.afterReadFile = undefined; await rm(home, { recursive: true, force: true }); }); +function gcRemovesFolderAfterRead(directory: string, nth: number): void { + let reads = 0; + fsHooks.afterReadFile = async (path) => { + if (path === manifestPath(directory)) { + reads += 1; + if (reads === nth) { + await rm(directory, { recursive: true, force: true }); + } + } + }; +} + +async function seedSession(record: SessionRecord): Promise { + const directory = sessionDir(home, record.sessionId); + await mkdir(directory, { recursive: true }); + await writeManifest(manifestPath(directory), record); + return directory; +} + +function killProbeReportsDead( + beforeHostReportsDead: () => void = () => undefined, +) { + vi.spyOn(process, 'kill').mockImplementation((pid, signal) => { + if (pid === HOST_PID && signal === 0) { + beforeHostReportsDead(); + } + throw Object.assign(new Error('kill ESRCH'), { code: 'ESRCH' }); + }); +} + function makeRecord(overrides: Partial = {}): SessionRecord { return { version: 1, @@ -110,24 +163,6 @@ describe('allocateSession', () => { }); describe('reconcileSession', () => { - async function seedSession(record: SessionRecord): Promise { - const directory = sessionDir(home, record.sessionId); - await mkdir(directory, { recursive: true }); - await writeManifest(manifestPath(directory), record); - return directory; - } - - function killProbeReportsDead( - beforeHostReportsDead: () => void = () => undefined, - ) { - vi.spyOn(process, 'kill').mockImplementation((pid, signal) => { - if (pid === HOST_PID && signal === 0) { - beforeHostReportsDead(); - } - throw Object.assign(new Error('kill ESRCH'), { code: 'ESRCH' }); - }); - } - it('keeps an exit that the host records after the read and before the liveness check', async () => { const directory = await seedSession(makeRecord()); const exited = makeRecord({ status: 'exited', exitCode: 0 }); @@ -154,4 +189,29 @@ describe('reconcileSession', () => { childPid: null, }); }); + + it('leaves a folder that gc removed after the re-read removed', async () => { + const directory = await seedSession(makeRecord()); + killProbeReportsDead(); + gcRemovesFolderAfterRead(directory, 2); + + await reconcileSession(directory); + + expect(existsSync(directory)).toBe(false); + }); +}); + +describe('destroySession', () => { + it('fails with SESSION_NOT_FOUND and leaves the folder removed when gc removes it before the destroyed write', async () => { + vi.stubEnv('AGENT_TTY_HOME', home); + const directory = await seedSession(makeRecord()); + killProbeReportsDead(); + gcRemovesFolderAfterRead(directory, 2); + + await expect(destroySession('session-01', true)).rejects.toMatchObject({ + code: 'SESSION_NOT_FOUND', + }); + + expect(existsSync(directory)).toBe(false); + }); }); diff --git a/test/unit/storage/sessionPaths.test.ts b/test/unit/storage/sessionPaths.test.ts index 4c8ad996..9e726234 100644 --- a/test/unit/storage/sessionPaths.test.ts +++ b/test/unit/storage/sessionPaths.test.ts @@ -1,5 +1,12 @@ import crypto from 'node:crypto'; -import { mkdtemp, realpath, rm, writeFile } from 'node:fs/promises'; +import { + mkdir, + mkdtemp, + realpath, + rm, + stat, + writeFile, +} from 'node:fs/promises'; import { tmpdir } from 'node:os'; import { join } from 'node:path'; @@ -87,9 +94,11 @@ describe('manifest storage', () => { // oxfmt-ignore const home = await realpath(await mkdtemp(join(tmpdir(), 'agent-tty-home-'))); temporaryDirectories.push(home); - const path = manifestPath(sessionDir(home, 'session-01')); + const directory = sessionDir(home, 'session-01'); + const path = manifestPath(directory); const record = createSessionRecord(); + await mkdir(directory, { recursive: true }); await writeManifest(path, record); const roundTripped = await readManifest(path); @@ -97,6 +106,18 @@ describe('manifest storage', () => { expect(roundTripped).toEqual(record); }); + it('fails with SESSION_NOT_FOUND and creates nothing when the session folder is gone', async () => { + // oxfmt-ignore + const home = await realpath(await mkdtemp(join(tmpdir(), 'agent-tty-home-'))); + temporaryDirectories.push(home); + const directory = sessionDir(home, 'session-01'); + + await expect( + writeManifest(manifestPath(directory), createSessionRecord()), + ).rejects.toMatchObject({ code: 'SESSION_NOT_FOUND' }); + await expect(stat(directory)).rejects.toMatchObject({ code: 'ENOENT' }); + }); + it('returns null when a manifest does not exist', async () => { // oxfmt-ignore const home = await realpath(await mkdtemp(join(tmpdir(), 'agent-tty-home-'))); @@ -110,8 +131,10 @@ describe('manifest storage', () => { // oxfmt-ignore const home = await realpath(await mkdtemp(join(tmpdir(), 'agent-tty-home-'))); temporaryDirectories.push(home); - const path = manifestPath(sessionDir(home, 'session-01')); + const directory = sessionDir(home, 'session-01'); + const path = manifestPath(directory); + await mkdir(directory, { recursive: true }); await writeManifest(path, createSessionRecord()); await writeFile( path,