From 35bce9d87d7699e03e2cdbd1965c373d629d15cd Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 06:46:05 +0000 Subject: [PATCH 01/34] test: a destroy marker makes a terminal session read destroyed --- test/unit/host/lifecycle.test.ts | 53 +++++++++++++++++++++++++++++ test/unit/storage/homeScope.test.ts | 14 +++++++- 2 files changed, 66 insertions(+), 1 deletion(-) diff --git a/test/unit/host/lifecycle.test.ts b/test/unit/host/lifecycle.test.ts index f638e223..ce3ee7ed 100644 --- a/test/unit/host/lifecycle.test.ts +++ b/test/unit/host/lifecycle.test.ts @@ -358,6 +358,59 @@ describe('reconcileSession', () => { expect(manifest.failureReason).toBeUndefined(); }); + it('records destroyed for a failed session whose reconcile died before it repaired a destroy', async () => { + const directory = await seedSession( + makeRecord({ + status: 'failed', + failureOrigin: 'host-death', + failureReason: 'host process died unexpectedly', + hostPid: null, + childPid: null, + }), + ); + writeFileSync(join(directory, 'destroyed'), ''); + + await reconcileSession(directory); + + const manifest = await readManifest(manifestPath(directory)); + expect(manifest).toMatchObject({ status: 'destroyed' }); + expect(manifest.failureOrigin).toBeUndefined(); + expect(manifest.failureReason).toBeUndefined(); + }); + + it('records destroyed for an exited session whose destroy failed after the marker', async () => { + const directory = await seedSession( + makeRecord({ + status: 'exited', + exitCode: 3, + hostPid: null, + childPid: null, + }), + ); + writeFileSync(join(directory, 'destroyed'), ''); + + await reconcileSession(directory); + + expect(await readManifest(manifestPath(directory))).toMatchObject({ + status: 'destroyed', + exitCode: 3, + }); + }); + + it('leaves an exited session without the marker as it is', async () => { + const exited = makeRecord({ + status: 'exited', + exitCode: 0, + hostPid: null, + childPid: null, + }); + const directory = await seedSession(exited); + + await reconcileSession(directory); + + expect(await readManifest(manifestPath(directory))).toEqual(exited); + }); + it('writes nothing while the program group survives its kill', async () => { const record = makeRecord(); const directory = await seedSession(record); diff --git a/test/unit/storage/homeScope.test.ts b/test/unit/storage/homeScope.test.ts index a5a657df..0b3fa268 100644 --- a/test/unit/storage/homeScope.test.ts +++ b/test/unit/storage/homeScope.test.ts @@ -1,4 +1,4 @@ -import { mkdir, mkdtemp, realpath, rm } from 'node:fs/promises'; +import { mkdir, mkdtemp, realpath, rm, writeFile } from 'node:fs/promises'; import { tmpdir } from 'node:os'; import { join } from 'node:path'; @@ -73,6 +73,18 @@ describe('scanHome (read-only Session counts)', () => { }); }); + // A reconcile that wrote failed over a destroy and has not yet written + // destroyed again, or was killed before it could. + it('skips a failed Session whose folder holds the destroy marker', async () => { + await seedSession({ sessionId: 'failed-1', status: 'failed' }); + await writeFile(join(sessionDir(home, 'failed-1'), 'destroyed'), ''); + + expect(await scanHome(home)).toEqual({ + activeSessions: 0, + totalSessions: 0, + }); + }); + it('treats a missing Home as having no Sessions', async () => { expect(await scanHome(join(home, 'does-not-exist'))).toEqual({ activeSessions: 0, From 135296374fd13113c966b70c860b3b9fe2b30054 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 06:48:16 +0000 Subject: [PATCH 02/34] fix(host): read a terminal session next to the destroy marker as destroyed --- src/host/lifecycle.ts | 36 ++++++++++++++++++++++++++++++++++++ src/storage/homeScope.ts | 9 +++++++-- 2 files changed, 43 insertions(+), 2 deletions(-) diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index b911801e..f2870070 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -976,12 +976,48 @@ export async function listSessions( return summaries; } +// Only a destroy writes the marker, after it stopped the session and right +// before its destroyed write, so a terminal record next to the marker is one +// that replaced that write or that the write never replaced. +async function writeMarkedDestroyed( + manifestFile: string, + manifest: SessionRecord, +): Promise { + const { failureReason: _reason, failureOrigin: _origin, ...rest } = manifest; + try { + await writeManifest(manifestFile, { + ...rest, + status: 'destroyed', + updatedAt: new Date().toISOString(), + hostPid: null, + childPid: null, + }); + } catch (error) { + if ( + error instanceof CliError && + error.code === ERROR_CODES.SESSION_NOT_FOUND + ) { + return; + } + throw error; + } +} + export async function reconcileSession( sessionDirectory: string, ): Promise { const manifestFile = manifestPath(sessionDirectory); const manifest = await readManifestIfExists(manifestFile); + if ( + manifest !== null && + isTerminalSessionStatus(manifest.status) && + !isDestroyedSessionStatus(manifest.status) && + existsSync(destroyMarkerPath(sessionDirectory)) + ) { + await writeMarkedDestroyed(manifestFile, manifest); + return; + } if (manifest === null || isTerminalSessionStatus(manifest.status)) { return; } diff --git a/src/storage/homeScope.ts b/src/storage/homeScope.ts index ebe9a3cf..3b994ecd 100644 --- a/src/storage/homeScope.ts +++ b/src/storage/homeScope.ts @@ -1,3 +1,4 @@ +import { existsSync } from 'node:fs'; import { readdir } from 'node:fs/promises'; import { resolve } from 'node:path'; @@ -8,7 +9,7 @@ import { import type { SessionRecord } from '../protocol/schemas.js'; import { createHomeRegistry, type HomeRegistry } from './homeRegistry.js'; import { readManifestIfExists } from './manifests.js'; -import { manifestPath, sessionDir } from './sessionPaths.js'; +import { destroyMarkerPath, manifestPath, sessionDir } from './sessionPaths.js'; /** * Active/all scope for listing Homes. Structurally identical to the dashboard's @@ -84,7 +85,11 @@ export async function scanHome( continue; } - if (manifest === null || isDestroyedSessionStatus(manifest.status)) { + if ( + manifest === null || + isDestroyedSessionStatus(manifest.status) || + existsSync(destroyMarkerPath(sessionDir(home, entry))) + ) { continue; } From 519ea8ad1ba7ed190f1053bc2612f2778d971a3c Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 06:48:16 +0000 Subject: [PATCH 03/34] fix(skills): model the repair of a marked terminal session at the reconcile read --- .../model/SessionLifecycle.tla | 30 +++++++++++++++---- .../verify-session-lifecycle/scripts/check.sh | 5 ++-- .../scripts/facts.mjs | 20 +++++++++++++ 3 files changed, 47 insertions(+), 8 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index 3c81122d..3f5872bc 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -90,6 +90,9 @@ CONSTANTS \* destroy marker before destroyed, and a \* reconcile that finds it after its own write \* writes destroyed again + ReconcileRepairsMarked, \* lifecycle.ts: a reconcile that reads a + \* terminal manifest other than destroyed next + \* to the destroy marker writes destroyed CreateStopsOnGiveUp, \* create.ts: a create that gives up on its \* host sends it SIGTERM, so the host stops \* its program and ends the session @@ -121,7 +124,8 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, ReconcileSkipsTerminal, InsideCheckReadsEnv, RecordsProgramSync, ProvesGroupOwnership, DestroyStopsLeftovers, FallbackNeedsFolder, CreateStopsOnGiveUp, - ReconcileRepairsDestroyed, TokenNamesProgram, + ReconcileRepairsDestroyed, ReconcileRepairsMarked, + TokenNamesProgram, ReusedIdReadsGone, ProvesHostPid} : b \in BOOLEAN Readers == {"gc", "list"} \* the two processes that run reconcileSession @@ -768,18 +772,28 @@ AfterReconcile(p) == IF p = "gc" THEN "readafter" ELSE "idle" \* isProcessAlive(manifest.hostPid). A null hostPid reads as a dead host. SkipsHost(read) == ReconcileSkipsLiveHost /\ read.pid /\ hostAlive -\* readManifestIfExists; return when it is null or terminal. +\* readManifestIfExists. With ReconcileRepairsMarked, a terminal manifest +\* other than destroyed next to the destroy marker gets destroyed from this +\* copy (writeMarkedDestroyed), with hostPid and childPid null and the exit +\* code kept, and reconcile returns. Otherwise it returns when the manifest +\* is null or terminal. ReconcileReads(p) == /\ pc[p] = "r_read" - /\ IF mst = "none" \/ (ReconcileSkipsTerminal /\ mst \in Terminal) - THEN /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)] + /\ IF ReconcileRepairsMarked /\ dmark /\ mst \in Terminal + /\ mst # "destroyed" + THEN /\ Write("destroyed", FALSE, "none", mcode, FALSE) + /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)] /\ UNCHANGED rd + ELSE IF mst = "none" \/ (ReconcileSkipsTerminal /\ mst \in Terminal) + THEN /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)] + /\ UNCHANGED <> ELSE /\ pc' = [pc EXCEPT ![p] = "r_check"] /\ rd' = [rd EXCEPT ![p] = [st |-> mst, pid |-> mpid, code |-> mcode, child |-> mchild, grp |-> "none"]] - /\ UNCHANGED <> + /\ UNCHANGED diskVars + /\ UNCHANGED <> \* After its group kill, reconcileSession waits for the group, or, without \* ReconcileWaitsForGroup, writes at once. @@ -1392,6 +1406,10 @@ NoUnrelatedHostKilled == ~hitUnrelatedHost WitnessGcRemovesSession == gres # "removed" WitnessReconcileRepairs == ~(dmark /\ mst = "failed" /\ \E p \in Readers : pc[p] = "r_repair") +\* A reader's first read already wrote destroyed over the failed that the +\* other reader wrote and has yet to repair. +WitnessMarkedRepaired == + ~(dmark /\ mst = "destroyed" /\ \E p \in Readers : pc[p] = "r_repair") 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 a1b3f3a5..e5a641ce 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 ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid" +GUARDS="GcSkipsNonCollectable GcFinalCheck ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed ReconcileRepairsMarked CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid" # 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; @@ -136,7 +136,7 @@ NO_TOKEN_RULES="NoLiveSessionDeleted HostDeathOnlyWhenDead TerminalIsFinal Recor # R15 and R16 are what the token adds, so only the runs with Token check them. RULES="$NO_TOKEN_RULES NoUnrelatedGroupKilled DestroyedSessionStopped" NO_TOKEN_WITNESSES="WitnessCreateGivesUp WitnessCrashReconciled WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessReconcileRepairs" -WITNESSES="WitnessGcRemovesSession WitnessCreateGivesUp WitnessSessionServes WitnessResizeLands WitnessCleanExitRecorded WitnessCrashReconciled WitnessDestroyCompletes WitnessSigtermRecorded WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessLeftoverMeetsDestroy WitnessReusedIdMeetsKill WitnessRecordNamesProgram WitnessUnrecordedProgramOutlives WitnessReconcileRepairs WitnessWaitPassesReusedId WitnessReusedHostMeetsKill WitnessUnrecordedHostMeetsKill" +WITNESSES="WitnessGcRemovesSession WitnessCreateGivesUp WitnessSessionServes WitnessResizeLands WitnessCleanExitRecorded WitnessCrashReconciled WitnessDestroyCompletes WitnessSigtermRecorded WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessLeftoverMeetsDestroy WitnessReusedIdMeetsKill WitnessRecordNamesProgram WitnessUnrecordedProgramOutlives WitnessReconcileRepairs WitnessMarkedRepaired WitnessWaitPassesReusedId WitnessReusedHostMeetsKill WitnessUnrecordedHostMeetsKill" # --- runs ---------------------------------------------------------------- @@ -201,6 +201,7 @@ write_run mutant-CreateStopsOnGiveUp violated FailedCreateStopped "CreateStopsOn 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 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-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 66e0525d..4ca3b56c 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -464,12 +464,31 @@ function repairFacts() { 'src/storage/manifests.ts', 'writeDestroyMarker', ).getText(); + const reconcile = requireDeclaration(lifecycle, 'reconcileSession').body; + const marked = indexOfStatement( + reconcile, + /^if \(\s*manifest !== null &&\s*isTerminalSessionStatus\(manifest\.status\) &&\s*!isDestroyedSessionStatus\(manifest\.status\) &&\s*existsSync\(destroyMarkerPath\(sessionDirectory\)\)\s*\) \{\s*await writeMarkedDestroyed\(manifestFile, manifest\);\s*return;\s*\}$/, + ); + const terminal = guardIndex( + reconcile, + 'manifest === null || isTerminalSessionStatus(manifest.status)', + ts.SyntaxKind.ReturnStatement, + ); + const rewrite = normalize( + requireDeclaration(lifecycle, 'writeMarkedDestroyed').body.getText(), + ); return { ReconcileRepairsDestroyed: marks && repairs && marker.includes("await replaceFileAtomic(path, '')") && !marker.includes('mkdir'), + ReconcileRepairsMarked: + marked >= 0 && + marked < terminal && + rewrite.includes( + "await writeManifest(manifestFile, { ...rest, status: 'destroyed',", + ), }; } @@ -1218,6 +1237,7 @@ const COVERED = [ ['src/host/lifecycle.ts', 'stopSessionProcesses'], ['src/host/lifecycle.ts', 'recordDestroyed'], ['src/host/lifecycle.ts', 'destroySession'], + ['src/host/lifecycle.ts', 'writeMarkedDestroyed'], ['src/host/lifecycle.ts', 'reconcileSession'], ['src/host/hostMain.ts', 'waitForManifestFromCreate'], ['src/host/hostMain.ts', 'isSessionCommandable'], From ac2e5bf87de223eeebab27d5900dfd693e787270 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 06:53:33 +0000 Subject: [PATCH 04/34] docs: describe the repair of a marked terminal session and the home list count --- docs/USAGE.md | 4 ++-- src/host/README.md | 2 +- src/storage/README.md | 4 ++-- src/storage/homeScope.ts | 5 +++-- 4 files changed, 8 insertions(+), 7 deletions(-) diff --git a/docs/USAGE.md b/docs/USAGE.md index 2628fd68..305e1c41 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -309,8 +309,8 @@ A `destroy` that runs inside the session, such as one typed into the session's s The session's terminal is closed by then, so redirect stdout to keep the result, for example `agent-tty destroy "$AGENT_TTY_SESSION_ID" --json > destroy.json`. When `destroy` records `destroyed` itself, as with `--force`, for a session whose host died or for a session that has already ended, it first writes an empty internal file, `destroyed`, in the session folder. When the host records `destroyed`, as after a plain `destroy` of a live session, nobody writes that file. A reconcile that writes over the record at the same moment finds the file right after its own write and records `destroyed` again. -A `list`, `inspect` or `gc` that reads the session between those two writes sees `failed`. If the reconciling process is killed between them, the session stays `failed`. -If `destroy` fails after it wrote the file, for example because its manifest write fails, the file stays. For a session that had not ended yet, the next reconcile then records it as `destroyed`. A reconcile skips a session that has already ended, so for such a session run `destroy` again. +A `list`, `inspect` or `gc` that reads the session between those two writes sees `failed`, and `home list` and the dashboard count a session with that file as destroyed. If the reconciling process is killed between them, the next reconcile finds the file and records the session as `destroyed`. +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. When `create` cannot reach its new host within about 6 s, it fails with `HOST_UNREACHABLE` or `HOST_TIMEOUT` and tells the host to stop. 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. A host that has already died, or that gets the SIGTERM before it spawns the program, leaves the session to the reconcile above: the session reads `running` until the next reconcile records it `failed`, and no program runs. diff --git a/src/host/README.md b/src/host/README.md index fa0c5ff4..0fde33df 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -52,7 +52,7 @@ - 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, or when the session directory is gone at its `destroyed` write, and `SESSION_ALREADY_DESTROYED` for a destroyed session. When it records `destroyed` itself, `recordDestroyed` first writes the empty `/destroyed` marker with `writeDestroyMarker`. Before it records a terminal session as `destroyed`, it calls `stopProgramGroup` with the group from `readProvenProgramGroup`, so only a group with a token gets a signal, and it throws `HOST_TIMEOUT` while that group lives. A running session gets the `destroy` RPC. With `force` it gets `SIGKILL` for the program's group and, only when `hostMatches` proves the host, for the host: on Linux `judgeHost` must return `alive`, elsewhere `/bin/ps` must show `_host `, and on Windows the host gets no signal. It polls every 100 ms for at most 50 attempts and throws `HOST_TIMEOUT` if the status is still not terminal. [lifecycle.ts:destroySession] -- `reconcileSession` does nothing when the manifest is missing, the status is terminal or the host can be alive: `judgeHost` with the record from `host.json` does not return `dead`. A null `hostPid` counts as a dead host. `allocateSession` writes the host PID into the first manifest, so a new session already has a `hostPid`. After the liveness check, `reconcileSession` reads the manifest again and does nothing when it is now missing or terminal. Otherwise it maps the status it read again: `running` to `failed` (failure origin `host-death`), `exiting` to `exited`, `destroying` to `destroyed` and any other status to `failed` (origin `unknown`), and sets both PIDs to `null`. Right after that write, when its status was not `destroyed` and the destroy marker exists, it writes `destroyed` again from the same copy, with both PIDs `null` and no failure fields. When the session directory is gone at either write, it returns. [lifecycle.ts:reconcileSession] +- `reconcileSession` writes `destroyed` (both PIDs `null`, the exit code kept, no failure fields) over a terminal manifest other than `destroyed` when the destroy marker exists, and returns (`writeMarkedDestroyed`). Otherwise it does nothing when the manifest is missing, the status is terminal or the host can be alive: `judgeHost` with the record from `host.json` does not return `dead`. A null `hostPid` counts as a dead host. `allocateSession` writes the host PID into the first manifest, so a new session already has a `hostPid`. After the liveness check, `reconcileSession` reads the manifest again and does nothing when it is now missing or terminal. Otherwise it maps the status it read again: `running` to `failed` (failure origin `host-death`), `exiting` to `exited`, `destroying` to `destroyed` and any other status to `failed` (origin `unknown`), and sets both PIDs to `null`. Right after that write, when its status was not `destroyed` and the destroy marker exists, it writes `destroyed` again from the same copy, with both PIDs `null` and no failure fields. When the session directory is gone at any of these writes, it returns. [lifecycle.ts:reconcileSession] [lifecycle.ts:writeMarkedDestroyed] - Every kill of the program's process group goes through `stopProgramGroup`. For a record with a token, `judgeProgramGroup` returns `owned` only when a process that is not a zombie (a process whose main thread exited is not one while another of its threads runs) has the program's pid as its process group and session id, and the recorded autogroup on the recorded boot. A scan that finds no live member runs once more, because a member can fork and end after the scan listed `/proc`. `stopProgramGroup` reads that process again right before the kill. `gone` (no live member), `unproven` (another boot id, or only members with another session id or autogroup) and `unknown` kill nothing. `unknown` means that `/proc` refused the boot id, or showed a member with the program's session id but no autogroup, so `isProgramGroupAlive` reads it alive. A record without a token gets the kill of its `pid`. A `{ childPid, sessionDirectory }` group gets the kill of `childPid`, and reads alive, only while `sessionDirectory` exists, checked in the same synchronous block. [programGroup.ts:stopProgramGroup] [programGroup.ts:judgeProgramGroup] - `captureProgram` records a token only on Linux, for its own child that leads its own session and has an autogroup other than the host's, within 250 ms, and only when `/proc` shows the boot id. `runHost` calls it right after `createPty` and writes the record before its first manifest write, with no `await` in between. [programGroup.ts:captureProgram] [hostMain.ts:runHost] - `allocateSession` throws `INVALID_DIMENSIONS` for non-positive `cols` or `rows`, `STORAGE_READ_ERROR` when `cwd` is not a directory and `INVALID_INPUT` when the shell path is not a file. An empty `command` defaults to the shell path. It creates the session directory and calls `launch` only after these checks pass. [lifecycle.ts:allocateSession] diff --git a/src/storage/README.md b/src/storage/README.md index edac5352..28bd46d1 100644 --- a/src/storage/README.md +++ b/src/storage/README.md @@ -42,7 +42,7 @@ - `computeArtifactHealth` maps only `MANIFEST_VALIDATION_ERROR` to health `manifest-invalid` and rethrows other errors. It validates its result with `ArtifactHealthSummarySchema`. [artifactHealth.ts:computeArtifactHealth] - The registry read returns `[]` on a read error, invalid JSON or a schema failure. The read checks each `homes` entry on its own and drops an invalid entry, so the valid entries survive. `resolveHomeRegistryPath` ignores an empty or relative `XDG_STATE_HOME`. [homeRegistry.ts:createHomeRegistry] [homeRegistry.ts:resolveHomeRegistryPath] - `upsert` reads and then writes the registry with no lock. A code comment states that concurrent creates can race and drop an entry, which registers again on the next create. [homeRegistry.ts:createHomeRegistry] -- The `scanHome` doc comment states that it does not reconcile sessions, does not write manifests and does not throw. It skips destroyed sessions and unreadable manifests. [homeScope.ts:scanHome] +- The `scanHome` doc comment states that it does not reconcile sessions, does not write manifests and does not throw. It skips destroyed sessions, sessions whose folder holds the destroy marker, and unreadable manifests. [homeScope.ts:scanHome] - `listRegisteredHomes` leaves out Homes with no visible sessions, and the `active` scope also leaves out Homes with no active session. Its doc comment states that it does not rewrite the registry file. [homeScope.ts:listRegisteredHomes] ## Side Effects @@ -57,7 +57,7 @@ - `publishArtifactWithRollback` has the side effects of `publishArtifactFile` and `appendArtifactWithRollback`. It also removes the temp file with `rm({ force: true })` when an earlier failure in the queue stops its publish step from running. [artifactManifest.ts:publishArtifactWithRollback] - `computeArtifactHealth` calls `fs.promises.access` on each artifact file. [artifactHealth.ts:computeArtifactHealth] - `resolveHomeRegistryPath` reads `XDG_STATE_HOME` and calls `os.homedir()`. `upsertHome` and `forgetHome` read and write the real `homes.json`. `readHomeRegistry` only reads it. [homeRegistry.ts:resolveHomeRegistryPath] [homeRegistry.ts:upsertHome] [homeRegistry.ts:readHomeRegistry] -- `scanHome` and `listRegisteredHomes` only read: `readdir(/sessions)`, each `session.json` and the registry. [homeScope.ts:scanHome] [homeScope.ts:listRegisteredHomes] +- `scanHome` and `listRegisteredHomes` only read: `readdir(/sessions)`, each `session.json`, whether each `destroyed` marker exists, and the registry. [homeScope.ts:scanHome] [homeScope.ts:listRegisteredHomes] ## Verification diff --git a/src/storage/homeScope.ts b/src/storage/homeScope.ts index 3b994ecd..f561eab5 100644 --- a/src/storage/homeScope.ts +++ b/src/storage/homeScope.ts @@ -54,8 +54,9 @@ const defaultScanDependencies: ScanHomeDependencies = { * still shows `running` until something reconciles it); entering a Home in the * dashboard, or running `gc`, reconciles for real. * - * "Visible" excludes destroyed Sessions, mirroring the dashboard's `all` scope - * (a destroyed Session's Event Log may already be collected). It never throws: + * "Visible" excludes destroyed Sessions and Sessions whose folder holds the + * destroy marker, mirroring the dashboard's `all` scope (a destroyed Session's + * Event Log may already be collected). It never throws: * a missing/unreadable sessions tree, or a corrupt individual manifest, counts * as zero/skip so a single bad Session can't break discovery. */ From 7ddc041e0dc3554491ff683cca680c6c869d8815 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 06:54:53 +0000 Subject: [PATCH 05/34] test: list shows destroyed for a failed session next to the destroy marker --- test/unit/host/lifecycle.test.ts | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/test/unit/host/lifecycle.test.ts b/test/unit/host/lifecycle.test.ts index ce3ee7ed..a75bf981 100644 --- a/test/unit/host/lifecycle.test.ts +++ b/test/unit/host/lifecycle.test.ts @@ -135,6 +135,7 @@ import type * as TimersPromises from 'node:timers/promises'; import { allocateSession, destroySession, + listSessions, cliRunsInsideProgramSession, reconcileSession, removeSocketDirectoryBestEffort, @@ -397,6 +398,25 @@ describe('reconcileSession', () => { }); }); + it('list shows destroyed for a failed session next to the destroy marker', async () => { + const directory = await seedSession( + makeRecord({ + status: 'failed', + failureOrigin: 'host-death', + hostPid: null, + childPid: null, + }), + ); + writeFileSync(join(directory, 'destroyed'), ''); + + const [summary] = await listSessions(home, true); + + expect(summary).toMatchObject({ + sessionId: 'session-01', + status: 'destroyed', + }); + }); + it('leaves an exited session without the marker as it is', async () => { const exited = makeRecord({ status: 'exited', From 963e45c7f1b3a81073e6422a5f693ba8ec75196f Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 06:55:06 +0000 Subject: [PATCH 06/34] fix(host): let list reconcile a terminal session next to the destroy marker --- src/host/lifecycle.ts | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index f2870070..2ba0c3a7 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -946,7 +946,11 @@ export async function listSessions( continue; } - if (isActiveSessionStatus(manifest.status)) { + if ( + isActiveSessionStatus(manifest.status) || + (!isDestroyedSessionStatus(manifest.status) && + existsSync(destroyMarkerPath(sessionDirectory))) + ) { try { await reconcileSession(sessionDirectory); manifest = await readManifestIfExists(manifestFile); From e274c6aa55c1def37312ca191926430b29758aa4 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 07:27:22 +0000 Subject: [PATCH 07/34] chore(skills): sync the lifecycle coverage record after the marked repair --- .../skills/verify-session-lifecycle/SKILL.md | 53 +++++++++++++------ .../verify-session-lifecycle/coverage.json | 12 +++-- 2 files changed, 43 insertions(+), 22 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index a51307a0..f2b91c4c 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -62,13 +62,13 @@ From the repo root: .agents/skills/verify-session-lifecycle/scripts/check.sh ``` -It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. On this repo it takes about eleven minutes with the default `CHECK_JOBS` of 4. Six runs explore the whole model, so `CHECK_JOBS=64` starts every run at once and takes about as long as the longest run. `JAVA=/path/to/java` picks another Java. `TLA2TOOLS_JAR=/path/to/tla2tools.jar` uses a jar you already have, which must be the same 1.7.4 build. `CHECK_OUT=` keeps the results in that folder (default: a new temp folder, printed at the end). +It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. On this repo it takes about eleven minutes with the default `CHECK_JOBS` of 4. Six runs explore the whole model, so `CHECK_JOBS=66` 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 twenty-eight guards that the rules depend on and the status sets of the policy table, and it hashes each covered function with comments and layout removed. +1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the twenty-nine guards that the rules depend on and the status sets of the policy table, and it hashes each covered function with comments and layout removed. 2. It writes one TLC config per run, with those facts as constants. A guard that is not in the code, in the expected place and order, reads FALSE, and the model then runs without it. -3. It runs TLC 64 times and prints one line per run. +3. It runs TLC 66 times and prints one line per run. 4. It compares the hashes and call sites with `coverage.json`. Exit codes: 0 means every run gave the expected result and the covered code matches the sync record. 1 means at least one run gave an unexpected result; the line says `UNEXPECTED`. 3 means every result was as expected, but covered code changed since the sync commit; that is not a pass, so follow "When you change covered code on purpose". 2 means a tool could not run. When both 1 and 3 apply, the exit code is 1. @@ -77,18 +77,19 @@ Exit codes: 0 means every run gave the expected result and the covered code matc At the sync commit, the expected results are: -| Runs | Expected | Why | -| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -| `current`, the code as it is with the program's session token, every rule | pass | No order of the modelled steps breaks a rule. This is the run that catches a new bug. | -| `current-no-token`, the code as it is without a token, R1 to R14 and R17 to R19 | pass | The same for a session whose `program.json` holds no token: on macOS, on a kernel without autogroups, when the capture read none, and for a session that an older agent-tty created. Every kill then falls back to the id that a manifest or the host's own record names. R15 and R16 are what the token adds, so this run leaves them out (see Scope). | -| `witness-*` without a suffix | violated | Each witness is a state that must be reachable: a `create` that gave up recorded the session destroyed, gc removes a session, a session serves, a resize lands, a clean exit is recorded, a crash is reconciled, a plain destroy completes, a SIGTERM shutdown is recorded, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` (which ends with `HOST_TIMEOUT` and leaves the session destroying) and `destroy --force` (which ends with `HOST_TIMEOUT` too), a process that the program left meets the kill of `destroy`, an unrelated group has the program's group id when `destroy --force` kills, `destroy --force` stops a program that only `program.json` names, a program whose host died before `program.json` named it outlives `destroy`, a wait of `destroy` through `program.json` reads the group gone while an unrelated group holds its id, a reconcile writes destroyed again over the failed that it wrote, `destroy --force` reaches its kill while a process that took the ended host's pid runs, and `destroy --force` reaches its kill while a live host has not written `host.json` yet. A witness that passes means the model can no longer reach that state, and the passing rules prove nothing. | -| `witness-*-no-token` | violated | Eight of those states without a token: a `create` that gave up recorded the session destroyed, a crash is reconciled, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` and `destroy --force`, and a reconcile writes destroyed again over the failed that it wrote. They show that `current-no-token` reaches the fallback kill and the EPERM probe. | -| `mutant-CreateRecordsHostPid`, `mutant-HostWaitsForManifest`, `mutant-ReconcileRereads`, `mutant-HostSerializesWrites`, `mutant-ReconcileSkipsLiveHost`, `mutant-HostStopsAfterTerminalWrite`, `mutant-DestroyRecordsDestroyed`, `mutant-DestroyKeepsExitCode`, `mutant-ManifestWriteNeedsFolder`, `mutant-KillsProgramGroup`, `mutant-HostWaitsForGroup`, `mutant-ReconcileWaitsForGroup`, `mutant-ReRunsInNewSession`, `mutant-InsideCheckReadsEnv`, `mutant-RecordsProgramSync`, `mutant-ProvesGroupOwnership`, `mutant-DestroyStopsLeftovers`, `mutant-FallbackNeedsFolder`, `mutant-ReconcileRepairsDestroyed`, `mutant-CreateStopsOnGiveUp`, `mutant-TokenNamesProgram`, `mutant-ProvesHostPid`, `mutant-GcBothChecks`, `mutant-ShutdownBothChecks` | violated | Each run removes a guard from the model and checks only the rule that the guard protects. That rule must break, which shows the check can fail. | -| `mutant-ProbeCountsDeniedGroup-no-token`, `mutant-KillsProgramGroup-no-token`, `mutant-HostWaitsForGroup-no-token`, `mutant-ReconcileWaitsForGroup-no-token` | violated | The same without a token. The fallback depends on these guards as the code before `program.json` did. With a token, the token check reads a process of another user in view, so only this path checks `ProbeCountsDeniedGroup`. | -| `mutant-ReusedIdReadsGone` | pass | Without the guard, a group that took the program's id reads alive, so no wait of `destroy` passes while it runs, and `WitnessWaitPassesReusedId` is never reached. The model has no rule for a wait that never ends, so this run checks that witness instead of a rule. | -| `mutant-ReconcileSkipsTerminal` | pass | The re-read in `reconcileSession` also returns on a terminal manifest, so the first terminal return alone is redundant. | -| `mutant-GcSkipsNonCollectable`, `mutant-GcFinalCheck` | pass | gc checks "collectable" twice. One check alone still keeps R1, so removing one is safe. Removing both is not. | -| `mutant-ShutdownChecksCommandable` | pass | `initiateShutdown` requests destroy only while the session is commandable, and the writer writes nothing after a terminal record. Either one alone keeps R3. Removing both is not safe. | +| Runs | Expected | Why | +| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | +| `current`, the code as it is with the program's session token, every rule | pass | No order of the modelled steps breaks a rule. This is the run that catches a new bug. | +| `current-no-token`, the code as it is without a token, R1 to R14 and R17 to R19 | pass | The same for a session whose `program.json` holds no token: on macOS, on a kernel without autogroups, when the capture read none, and for a session that an older agent-tty created. Every kill then falls back to the id that a manifest or the host's own record names. R15 and R16 are what the token adds, so this run leaves them out (see Scope). | +| `witness-*` without a suffix | violated | Each witness is a state that must be reachable: a `create` that gave up recorded the session destroyed, gc removes a session, a session serves, a resize lands, a clean exit is recorded, a crash is reconciled, a plain destroy completes, a SIGTERM shutdown is recorded, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` (which ends with `HOST_TIMEOUT` and leaves the session destroying) and `destroy --force` (which ends with `HOST_TIMEOUT` too), a process that the program left meets the kill of `destroy`, an unrelated group has the program's group id when `destroy --force` kills, `destroy --force` stops a program that only `program.json` names, a program whose host died before `program.json` named it outlives `destroy`, a wait of `destroy` through `program.json` reads the group gone while an unrelated group holds its id, a reconcile writes destroyed again over the failed that it wrote, the first read of another reconcile writes destroyed over that failed first, `destroy --force` reaches its kill while a process that took the ended host's pid runs, and `destroy --force` reaches its kill while a live host has not written `host.json` yet. A witness that passes means the model can no longer reach that state, and the passing rules prove nothing. | +| `witness-*-no-token` | violated | Eight of those states without a token: a `create` that gave up recorded the session destroyed, a crash is reconciled, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` and `destroy --force`, and a reconcile writes destroyed again over the failed that it wrote. They show that `current-no-token` reaches the fallback kill and the EPERM probe. | +| `mutant-CreateRecordsHostPid`, `mutant-HostWaitsForManifest`, `mutant-ReconcileRereads`, `mutant-HostSerializesWrites`, `mutant-ReconcileSkipsLiveHost`, `mutant-HostStopsAfterTerminalWrite`, `mutant-DestroyRecordsDestroyed`, `mutant-DestroyKeepsExitCode`, `mutant-ManifestWriteNeedsFolder`, `mutant-KillsProgramGroup`, `mutant-HostWaitsForGroup`, `mutant-ReconcileWaitsForGroup`, `mutant-ReRunsInNewSession`, `mutant-InsideCheckReadsEnv`, `mutant-RecordsProgramSync`, `mutant-ProvesGroupOwnership`, `mutant-DestroyStopsLeftovers`, `mutant-FallbackNeedsFolder`, `mutant-ReconcileRepairsDestroyed`, `mutant-CreateStopsOnGiveUp`, `mutant-TokenNamesProgram`, `mutant-ProvesHostPid`, `mutant-GcBothChecks`, `mutant-ShutdownBothChecks` | violated | Each run removes a guard from the model and checks only the rule that the guard protects. That rule must break, which shows the check can fail. | +| `mutant-ProbeCountsDeniedGroup-no-token`, `mutant-KillsProgramGroup-no-token`, `mutant-HostWaitsForGroup-no-token`, `mutant-ReconcileWaitsForGroup-no-token` | violated | The same without a token. The fallback depends on these guards as the code before `program.json` did. With a token, the token check reads a process of another user in view, so only this path checks `ProbeCountsDeniedGroup`. | +| `mutant-ReusedIdReadsGone` | pass | Without the guard, a group that took the program's id reads alive, so no wait of `destroy` passes while it runs, and `WitnessWaitPassesReusedId` is never reached. The model has no rule for a wait that never ends, so this run checks that witness instead of a rule. | +| `mutant-ReconcileRepairsMarked` | pass | Without the guard, a reconcile skips a marked `failed` as it skips any terminal manifest. The reconcile that wrote that `failed` always repairs it in the model, because the model has no crash of a reconciling process, so no rule breaks. The unit tests in `test/unit/host/lifecycle.test.ts` cover the crash. | +| `mutant-ReconcileSkipsTerminal` | pass | The re-read in `reconcileSession` also returns on a terminal manifest, so the first terminal return alone is redundant. | +| `mutant-GcSkipsNonCollectable`, `mutant-GcFinalCheck` | pass | gc checks "collectable" twice. One check alone still keeps R1, so removing one is safe. Removing both is not. | +| `mutant-ShutdownChecksCommandable` | pass | `initiateShutdown` requests destroy only while the session is commandable, and the writer writes nothing after a terminal record. Either one alone keeps R3. Removing both is not safe. | 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`. @@ -412,6 +413,24 @@ wait node -e 'console.log(require(process.argv[1]).status)' "$AGENT_TTY_HOME/sessions/$id/session.json" # destroyed ``` +### `ReconcileRepairsMarked`: a marked session that a killed reconcile left `failed` + +`ReconcileRepairsDestroyed` repairs a destroyed record in the reconcile that replaced it, right after its own write. A reconcile process that was killed between that write and the repair left `failed`, after `destroy` had printed `destroyed: true`, and every later reconcile skipped the terminal manifest (coder/agent-tty#265). A `destroy` of an ended session that failed after its marker write left the marker next to `exited` or `failed` the same way. + +Now `reconcileSession` first checks a terminal manifest other than destroyed for the marker. When the marker is there, `writeMarkedDestroyed` writes destroyed from that copy, with `hostPid` and `childPid` null, the exit code kept and no failure fields, and the reconcile returns. Only a `destroy` writes the marker, after it stopped the session and right before its destroyed write, so the marker means that `destroy` chose destroyed. `scanHome` skips a session with the marker, so `home list` and the dashboard picker do not count it while its manifest reads `failed`. The replay holds the repair write of the reconcile in `list` and kills that process: + +```sh +id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'exec cat' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))') +kill -KILL "$(node -e 'console.log(require(process.argv[1]).hostPid)' "$AGENT_TTY_HOME/sessions/$id/session.json")" +LOG=$(mktemp) +REPLAY_LOG=$LOG REPLAY_HOLD='list:rename:/session.json:1:4000,list:rename:/session.json:2:60000' NODE_OPTIONS="$HOLD" node --import tsx src/cli/main.ts list --json >/dev/null & +until grep -q 'hold rename' "$LOG"; do sleep 0.1; done +node --import tsx src/cli/main.ts destroy "$id" --force --json # ok: true, destroyed: true +until [ "$(grep -c 'hold rename' "$LOG")" -ge 2 ]; do sleep 0.1; done +kill -KILL $! # the reconcile dies before its repair +node --import tsx src/cli/main.ts list --all --json # the session reads destroyed +``` + ### `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. @@ -454,7 +473,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 22,897,048 distinct states, and without one 22,308,620. 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 23,017,012 distinct states, and without one 22,429,940. The check prints both counts. It assumes: @@ -470,7 +489,7 @@ 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`, because every later reconcile skips a terminal manifest. The model has no crash of a reconciling process. +- 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. - 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 stops its host only once the manifest names the program, and the next reconcile records `failed` and ends the program. Before that write, `create` leaves the host alone. `CreateStopsOnGiveUp` checks the stop for Linux and macOS. - 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. diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 94118b6c..675ac4aa 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -29,7 +29,8 @@ "src/host/lifecycle.ts#stopSessionProcesses": "74794e19bc382784", "src/host/lifecycle.ts#recordDestroyed": "d968f32f58d3920a", "src/host/lifecycle.ts#destroySession": "873354edcae17792", - "src/host/lifecycle.ts#reconcileSession": "c2904456d54b87c8", + "src/host/lifecycle.ts#writeMarkedDestroyed": "197e7ca08045e384", + "src/host/lifecycle.ts#reconcileSession": "74e867ca0d35d1d1", "src/host/hostMain.ts#waitForManifestFromCreate": "fd500651f83683eb", "src/host/hostMain.ts#isSessionCommandable": "260060f07b068ec1", "src/host/hostMain.ts#SHUTDOWN_KILL_GRACE_MS": "51171d9c5aa6c510", @@ -79,16 +80,17 @@ "src/host/hostMain.ts#runHost(final try)": "16789dd4e2534bc7", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "c3e13b1bab88e18f", - "skill:scripts/facts.mjs": "ae186f3448932144", - "skill:scripts/check.sh": "27da959697f6af33" + "skill:model/SessionLifecycle.tla": "87fd01745ef6d2d5", + "skill:scripts/facts.mjs": "d49d18dba7311993", + "skill:scripts/check.sh": "a7840ba3b1d5c554" }, "callSites": { "writeManifest": [ "src/host/lifecycle.ts#allocateSession", "src/host/lifecycle.ts#reconcileSession", "src/host/lifecycle.ts#reconcileSession", - "src/host/lifecycle.ts#recordDestroyed" + "src/host/lifecycle.ts#recordDestroyed", + "src/host/lifecycle.ts#writeMarkedDestroyed" ], "persistManifest": [ "src/host/hostMain.ts#runHost", From 64b1092deba5a1658a78a078d9d79a206a8aa0fc Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 07:28:10 +0000 Subject: [PATCH 08/34] chore: trim comments in the marked repair --- src/host/lifecycle.ts | 3 --- test/unit/storage/homeScope.test.ts | 2 -- 2 files changed, 5 deletions(-) diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index 2ba0c3a7..f4a32506 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -980,9 +980,6 @@ export async function listSessions( return summaries; } -// Only a destroy writes the marker, after it stopped the session and right -// before its destroyed write, so a terminal record next to the marker is one -// that replaced that write or that the write never replaced. async function writeMarkedDestroyed( manifestFile: string, manifest: SessionRecord, diff --git a/test/unit/storage/homeScope.test.ts b/test/unit/storage/homeScope.test.ts index 0b3fa268..923fbcd3 100644 --- a/test/unit/storage/homeScope.test.ts +++ b/test/unit/storage/homeScope.test.ts @@ -73,8 +73,6 @@ describe('scanHome (read-only Session counts)', () => { }); }); - // A reconcile that wrote failed over a destroy and has not yet written - // destroyed again, or was killed before it could. it('skips a failed Session whose folder holds the destroy marker', async () => { await seedSession({ sessionId: 'failed-1', status: 'failed' }); await writeFile(join(sessionDir(home, 'failed-1'), 'destroyed'), ''); From cd9af9c0fc152b5dc67d9dae923ecb68fbf9cfef Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 07:29:07 +0000 Subject: [PATCH 09/34] refactor(host): name the marked terminal check isMarkedDestroyed --- .../scripts/facts.mjs | 8 ++++++- src/host/lifecycle.ts | 21 ++++++++++++------- 2 files changed, 20 insertions(+), 9 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 4ca3b56c..8fa7c1e7 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -467,7 +467,10 @@ function repairFacts() { const reconcile = requireDeclaration(lifecycle, 'reconcileSession').body; const marked = indexOfStatement( reconcile, - /^if \(\s*manifest !== null &&\s*isTerminalSessionStatus\(manifest\.status\) &&\s*!isDestroyedSessionStatus\(manifest\.status\) &&\s*existsSync\(destroyMarkerPath\(sessionDirectory\)\)\s*\) \{\s*await writeMarkedDestroyed\(manifestFile, manifest\);\s*return;\s*\}$/, + /^if \(manifest !== null && isMarkedDestroyed\(sessionDirectory, manifest\)\) \{\s*await writeMarkedDestroyed\(manifestFile, manifest\);\s*return;\s*\}$/, + ); + const markedCheck = normalize( + requireDeclaration(lifecycle, 'isMarkedDestroyed').body.getText(), ); const terminal = guardIndex( reconcile, @@ -486,6 +489,8 @@ function repairFacts() { ReconcileRepairsMarked: marked >= 0 && marked < terminal && + markedCheck === + '{ return ( isTerminalSessionStatus(manifest.status) && !isDestroyedSessionStatus(manifest.status) && existsSync(destroyMarkerPath(sessionDirectory)) ); }' && rewrite.includes( "await writeManifest(manifestFile, { ...rest, status: 'destroyed',", ), @@ -1237,6 +1242,7 @@ const COVERED = [ ['src/host/lifecycle.ts', 'stopSessionProcesses'], ['src/host/lifecycle.ts', 'recordDestroyed'], ['src/host/lifecycle.ts', 'destroySession'], + ['src/host/lifecycle.ts', 'isMarkedDestroyed'], ['src/host/lifecycle.ts', 'writeMarkedDestroyed'], ['src/host/lifecycle.ts', 'reconcileSession'], ['src/host/hostMain.ts', 'waitForManifestFromCreate'], diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index f4a32506..e2a0967e 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -948,8 +948,7 @@ export async function listSessions( if ( isActiveSessionStatus(manifest.status) || - (!isDestroyedSessionStatus(manifest.status) && - existsSync(destroyMarkerPath(sessionDirectory))) + isMarkedDestroyed(sessionDirectory, manifest) ) { try { await reconcileSession(sessionDirectory); @@ -980,6 +979,17 @@ export async function listSessions( return summaries; } +function isMarkedDestroyed( + sessionDirectory: string, + manifest: SessionRecord, +): boolean { + return ( + isTerminalSessionStatus(manifest.status) && + !isDestroyedSessionStatus(manifest.status) && + existsSync(destroyMarkerPath(sessionDirectory)) + ); +} + async function writeMarkedDestroyed( manifestFile: string, manifest: SessionRecord, @@ -1010,12 +1020,7 @@ export async function reconcileSession( const manifestFile = manifestPath(sessionDirectory); const manifest = await readManifestIfExists(manifestFile); - if ( - manifest !== null && - isTerminalSessionStatus(manifest.status) && - !isDestroyedSessionStatus(manifest.status) && - existsSync(destroyMarkerPath(sessionDirectory)) - ) { + if (manifest !== null && isMarkedDestroyed(sessionDirectory, manifest)) { await writeMarkedDestroyed(manifestFile, manifest); return; } From 7f3765d201c574e730c1e19cea1e08f4049a73b5 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 07:31:27 +0000 Subject: [PATCH 10/34] fix(skills): witness the repair at the reconcile read with a ghost --- .../skills/verify-session-lifecycle/SKILL.md | 2 +- .../model/SessionLifecycle.tla | 21 ++++++++++--------- 2 files changed, 12 insertions(+), 11 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index f2b91c4c..29900066 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -81,7 +81,7 @@ At the sync commit, the expected results are: | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | | `current`, the code as it is with the program's session token, every rule | pass | No order of the modelled steps breaks a rule. This is the run that catches a new bug. | | `current-no-token`, the code as it is without a token, R1 to R14 and R17 to R19 | pass | The same for a session whose `program.json` holds no token: on macOS, on a kernel without autogroups, when the capture read none, and for a session that an older agent-tty created. Every kill then falls back to the id that a manifest or the host's own record names. R15 and R16 are what the token adds, so this run leaves them out (see Scope). | -| `witness-*` without a suffix | violated | Each witness is a state that must be reachable: a `create` that gave up recorded the session destroyed, gc removes a session, a session serves, a resize lands, a clean exit is recorded, a crash is reconciled, a plain destroy completes, a SIGTERM shutdown is recorded, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` (which ends with `HOST_TIMEOUT` and leaves the session destroying) and `destroy --force` (which ends with `HOST_TIMEOUT` too), a process that the program left meets the kill of `destroy`, an unrelated group has the program's group id when `destroy --force` kills, `destroy --force` stops a program that only `program.json` names, a program whose host died before `program.json` named it outlives `destroy`, a wait of `destroy` through `program.json` reads the group gone while an unrelated group holds its id, a reconcile writes destroyed again over the failed that it wrote, the first read of another reconcile writes destroyed over that failed first, `destroy --force` reaches its kill while a process that took the ended host's pid runs, and `destroy --force` reaches its kill while a live host has not written `host.json` yet. A witness that passes means the model can no longer reach that state, and the passing rules prove nothing. | +| `witness-*` without a suffix | violated | Each witness is a state that must be reachable: a `create` that gave up recorded the session destroyed, gc removes a session, a session serves, a resize lands, a clean exit is recorded, a crash is reconciled, a plain destroy completes, a SIGTERM shutdown is recorded, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` (which ends with `HOST_TIMEOUT` and leaves the session destroying) and `destroy --force` (which ends with `HOST_TIMEOUT` too), a process that the program left meets the kill of `destroy`, an unrelated group has the program's group id when `destroy --force` kills, `destroy --force` stops a program that only `program.json` names, a program whose host died before `program.json` named it outlives `destroy`, a wait of `destroy` through `program.json` reads the group gone while an unrelated group holds its id, a reconcile writes destroyed again over the failed that it wrote, a reconcile's first read writes destroyed over a marked terminal manifest, `destroy --force` reaches its kill while a process that took the ended host's pid runs, and `destroy --force` reaches its kill while a live host has not written `host.json` yet. A witness that passes means the model can no longer reach that state, and the passing rules prove nothing. | | `witness-*-no-token` | violated | Eight of those states without a token: a `create` that gave up recorded the session destroyed, a crash is reconciled, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` and `destroy --force`, and a reconcile writes destroyed again over the failed that it wrote. They show that `current-no-token` reaches the fallback kill and the EPERM probe. | | `mutant-CreateRecordsHostPid`, `mutant-HostWaitsForManifest`, `mutant-ReconcileRereads`, `mutant-HostSerializesWrites`, `mutant-ReconcileSkipsLiveHost`, `mutant-HostStopsAfterTerminalWrite`, `mutant-DestroyRecordsDestroyed`, `mutant-DestroyKeepsExitCode`, `mutant-ManifestWriteNeedsFolder`, `mutant-KillsProgramGroup`, `mutant-HostWaitsForGroup`, `mutant-ReconcileWaitsForGroup`, `mutant-ReRunsInNewSession`, `mutant-InsideCheckReadsEnv`, `mutant-RecordsProgramSync`, `mutant-ProvesGroupOwnership`, `mutant-DestroyStopsLeftovers`, `mutant-FallbackNeedsFolder`, `mutant-ReconcileRepairsDestroyed`, `mutant-CreateStopsOnGiveUp`, `mutant-TokenNamesProgram`, `mutant-ProvesHostPid`, `mutant-GcBothChecks`, `mutant-ShutdownBothChecks` | violated | Each run removes a guard from the model and checks only the rule that the guard protects. That rule must break, which shows the check can fail. | | `mutant-ProbeCountsDeniedGroup-no-token`, `mutant-KillsProgramGroup-no-token`, `mutant-HostWaitsForGroup-no-token`, `mutant-ReconcileWaitsForGroup-no-token` | violated | The same without a token. The fallback depends on these guards as the code before `program.json` did. With a token, the token check reads a process of another user in view, so only this path checks `ProbeCountsDeniedGroup`. | diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index 3f5872bc..7a5ddbef 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -149,6 +149,8 @@ VARIABLES dmark, \* the destroy marker file exists in the session directory rec, \* program.json names the program with its token startFailed, \* ghost: the host died because its files were missing + readRepaired, \* ghost: a reconcile's first read wrote destroyed next to + \* the destroy marker sock, \* the RPC socket file exists (it is outside the directory) cpc, \* create: "alloc", "write", "launch", "done", "failed" \* (it gave up on its host) @@ -211,7 +213,7 @@ VARIABLES diskVars == <> -ghostVars == <> +ghostVars == <> hostVars == <> groupVars == <> @@ -226,7 +228,7 @@ Init == /\ mcode = FALSE /\ mchild = FALSE /\ wasTerminal = FALSE /\ wasExited = FALSE /\ wasNamed = FALSE /\ dmark = FALSE - /\ rec = FALSE /\ startFailed = FALSE + /\ rec = FALSE /\ startFailed = FALSE /\ readRepaired = FALSE /\ sock = FALSE /\ cpc = "alloc" /\ hostAlive = FALSE /\ hpc = "none" /\ hex = "none" /\ rsz = "none" @@ -351,6 +353,7 @@ GroupSeen(kind) == \* The host fails to start because its files are missing or were rewritten. HostFailsToStart == /\ startFailed' = TRUE + /\ readRepaired' = readRepaired /\ hostAlive' = FALSE /\ hpc' = "dead" /\ hex' = IF hex = "none" THEN "none" ELSE "gone" @@ -783,16 +786,17 @@ ReconcileReads(p) == /\ mst # "destroyed" THEN /\ Write("destroyed", FALSE, "none", mcode, FALSE) /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)] + /\ readRepaired' = TRUE /\ UNCHANGED rd ELSE IF mst = "none" \/ (ReconcileSkipsTerminal /\ mst \in Terminal) THEN /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)] - /\ UNCHANGED <> + /\ UNCHANGED <> ELSE /\ pc' = [pc EXCEPT ![p] = "r_check"] /\ rd' = [rd EXCEPT ![p] = [st |-> mst, pid |-> mpid, code |-> mcode, child |-> mchild, grp |-> "none"]] - /\ UNCHANGED diskVars - /\ UNCHANGED <> + /\ UNCHANGED <> \* After its group kill, reconcileSession waits for the group, or, without @@ -1275,7 +1279,7 @@ Spec == Init /\ [][Next]_vars TypeOK == /\ dmark => dir /\ {dir, mpid, mchild, wasTerminal, wasExited, wasNamed, dmark, startFailed, - sock, + readRepaired, sock, hostAlive, prog, foreign, sig, dforce, dinside, dsaw, dkill, rec, left, reused, hitUnrelated, diedUnrecorded, passedReused, hrec, hreused, hitUnrelatedHost} @@ -1406,10 +1410,7 @@ NoUnrelatedHostKilled == ~hitUnrelatedHost WitnessGcRemovesSession == gres # "removed" WitnessReconcileRepairs == ~(dmark /\ mst = "failed" /\ \E p \in Readers : pc[p] = "r_repair") -\* A reader's first read already wrote destroyed over the failed that the -\* other reader wrote and has yet to repair. -WitnessMarkedRepaired == - ~(dmark /\ mst = "destroyed" /\ \E p \in Readers : pc[p] = "r_repair") +WitnessMarkedRepaired == ~readRepaired WitnessCreateGivesUp == ~(cpc = "failed" /\ sig /\ mst = "destroyed" /\ ~hostAlive) WitnessSessionServes == ~(hpc = "serving" /\ sock /\ mst = "running" /\ mpid) From aea5277ed1768a1183e463d0a5be6a63f5302de7 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 08:17:28 +0000 Subject: [PATCH 11/34] chore(skills): sync the lifecycle coverage record after the repair witness --- .../skills/verify-session-lifecycle/SKILL.md | 26 +++++++++---------- .../verify-session-lifecycle/coverage.json | 7 ++--- 2 files changed, 17 insertions(+), 16 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 29900066..806566c4 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -77,19 +77,19 @@ Exit codes: 0 means every run gave the expected result and the covered code matc At the sync commit, the expected results are: -| Runs | Expected | Why | -| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | -| `current`, the code as it is with the program's session token, every rule | pass | No order of the modelled steps breaks a rule. This is the run that catches a new bug. | -| `current-no-token`, the code as it is without a token, R1 to R14 and R17 to R19 | pass | The same for a session whose `program.json` holds no token: on macOS, on a kernel without autogroups, when the capture read none, and for a session that an older agent-tty created. Every kill then falls back to the id that a manifest or the host's own record names. R15 and R16 are what the token adds, so this run leaves them out (see Scope). | +| Runs | Expected | Why | +| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `current`, the code as it is with the program's session token, every rule | pass | No order of the modelled steps breaks a rule. This is the run that catches a new bug. | +| `current-no-token`, the code as it is without a token, R1 to R14 and R17 to R19 | pass | The same for a session whose `program.json` holds no token: on macOS, on a kernel without autogroups, when the capture read none, and for a session that an older agent-tty created. Every kill then falls back to the id that a manifest or the host's own record names. R15 and R16 are what the token adds, so this run leaves them out (see Scope). | | `witness-*` without a suffix | violated | Each witness is a state that must be reachable: a `create` that gave up recorded the session destroyed, gc removes a session, a session serves, a resize lands, a clean exit is recorded, a crash is reconciled, a plain destroy completes, a SIGTERM shutdown is recorded, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` (which ends with `HOST_TIMEOUT` and leaves the session destroying) and `destroy --force` (which ends with `HOST_TIMEOUT` too), a process that the program left meets the kill of `destroy`, an unrelated group has the program's group id when `destroy --force` kills, `destroy --force` stops a program that only `program.json` names, a program whose host died before `program.json` named it outlives `destroy`, a wait of `destroy` through `program.json` reads the group gone while an unrelated group holds its id, a reconcile writes destroyed again over the failed that it wrote, a reconcile's first read writes destroyed over a marked terminal manifest, `destroy --force` reaches its kill while a process that took the ended host's pid runs, and `destroy --force` reaches its kill while a live host has not written `host.json` yet. A witness that passes means the model can no longer reach that state, and the passing rules prove nothing. | -| `witness-*-no-token` | violated | Eight of those states without a token: a `create` that gave up recorded the session destroyed, a crash is reconciled, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` and `destroy --force`, and a reconcile writes destroyed again over the failed that it wrote. They show that `current-no-token` reaches the fallback kill and the EPERM probe. | -| `mutant-CreateRecordsHostPid`, `mutant-HostWaitsForManifest`, `mutant-ReconcileRereads`, `mutant-HostSerializesWrites`, `mutant-ReconcileSkipsLiveHost`, `mutant-HostStopsAfterTerminalWrite`, `mutant-DestroyRecordsDestroyed`, `mutant-DestroyKeepsExitCode`, `mutant-ManifestWriteNeedsFolder`, `mutant-KillsProgramGroup`, `mutant-HostWaitsForGroup`, `mutant-ReconcileWaitsForGroup`, `mutant-ReRunsInNewSession`, `mutant-InsideCheckReadsEnv`, `mutant-RecordsProgramSync`, `mutant-ProvesGroupOwnership`, `mutant-DestroyStopsLeftovers`, `mutant-FallbackNeedsFolder`, `mutant-ReconcileRepairsDestroyed`, `mutant-CreateStopsOnGiveUp`, `mutant-TokenNamesProgram`, `mutant-ProvesHostPid`, `mutant-GcBothChecks`, `mutant-ShutdownBothChecks` | violated | Each run removes a guard from the model and checks only the rule that the guard protects. That rule must break, which shows the check can fail. | -| `mutant-ProbeCountsDeniedGroup-no-token`, `mutant-KillsProgramGroup-no-token`, `mutant-HostWaitsForGroup-no-token`, `mutant-ReconcileWaitsForGroup-no-token` | violated | The same without a token. The fallback depends on these guards as the code before `program.json` did. With a token, the token check reads a process of another user in view, so only this path checks `ProbeCountsDeniedGroup`. | -| `mutant-ReusedIdReadsGone` | pass | Without the guard, a group that took the program's id reads alive, so no wait of `destroy` passes while it runs, and `WitnessWaitPassesReusedId` is never reached. The model has no rule for a wait that never ends, so this run checks that witness instead of a rule. | -| `mutant-ReconcileRepairsMarked` | pass | Without the guard, a reconcile skips a marked `failed` as it skips any terminal manifest. The reconcile that wrote that `failed` always repairs it in the model, because the model has no crash of a reconciling process, so no rule breaks. The unit tests in `test/unit/host/lifecycle.test.ts` cover the crash. | -| `mutant-ReconcileSkipsTerminal` | pass | The re-read in `reconcileSession` also returns on a terminal manifest, so the first terminal return alone is redundant. | -| `mutant-GcSkipsNonCollectable`, `mutant-GcFinalCheck` | pass | gc checks "collectable" twice. One check alone still keeps R1, so removing one is safe. Removing both is not. | -| `mutant-ShutdownChecksCommandable` | pass | `initiateShutdown` requests destroy only while the session is commandable, and the writer writes nothing after a terminal record. Either one alone keeps R3. Removing both is not safe. | +| `witness-*-no-token` | violated | Eight of those states without a token: a `create` that gave up recorded the session destroyed, a crash is reconciled, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` and `destroy --force`, and a reconcile writes destroyed again over the failed that it wrote. They show that `current-no-token` reaches the fallback kill and the EPERM probe. | +| `mutant-CreateRecordsHostPid`, `mutant-HostWaitsForManifest`, `mutant-ReconcileRereads`, `mutant-HostSerializesWrites`, `mutant-ReconcileSkipsLiveHost`, `mutant-HostStopsAfterTerminalWrite`, `mutant-DestroyRecordsDestroyed`, `mutant-DestroyKeepsExitCode`, `mutant-ManifestWriteNeedsFolder`, `mutant-KillsProgramGroup`, `mutant-HostWaitsForGroup`, `mutant-ReconcileWaitsForGroup`, `mutant-ReRunsInNewSession`, `mutant-InsideCheckReadsEnv`, `mutant-RecordsProgramSync`, `mutant-ProvesGroupOwnership`, `mutant-DestroyStopsLeftovers`, `mutant-FallbackNeedsFolder`, `mutant-ReconcileRepairsDestroyed`, `mutant-CreateStopsOnGiveUp`, `mutant-TokenNamesProgram`, `mutant-ProvesHostPid`, `mutant-GcBothChecks`, `mutant-ShutdownBothChecks` | violated | Each run removes a guard from the model and checks only the rule that the guard protects. That rule must break, which shows the check can fail. | +| `mutant-ProbeCountsDeniedGroup-no-token`, `mutant-KillsProgramGroup-no-token`, `mutant-HostWaitsForGroup-no-token`, `mutant-ReconcileWaitsForGroup-no-token` | violated | The same without a token. The fallback depends on these guards as the code before `program.json` did. With a token, the token check reads a process of another user in view, so only this path checks `ProbeCountsDeniedGroup`. | +| `mutant-ReusedIdReadsGone` | pass | Without the guard, a group that took the program's id reads alive, so no wait of `destroy` passes while it runs, and `WitnessWaitPassesReusedId` is never reached. The model has no rule for a wait that never ends, so this run checks that witness instead of a rule. | +| `mutant-ReconcileRepairsMarked` | pass | Without the guard, a reconcile skips a marked `failed` as it skips any terminal manifest. The reconcile that wrote that `failed` always repairs it in the model, because the model has no crash of a reconciling process, so no rule breaks. The unit tests in `test/unit/host/lifecycle.test.ts` cover the crash. | +| `mutant-ReconcileSkipsTerminal` | pass | The re-read in `reconcileSession` also returns on a terminal manifest, so the first terminal return alone is redundant. | +| `mutant-GcSkipsNonCollectable`, `mutant-GcFinalCheck` | pass | gc checks "collectable" twice. One check alone still keeps R1, so removing one is safe. Removing both is not. | +| `mutant-ShutdownChecksCommandable` | pass | `initiateShutdown` requests destroy only while the session is commandable, and the writer writes nothing after a terminal record. Either one alone keeps R3. Removing both is not safe. | 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`. @@ -473,7 +473,7 @@ To bring the check back in line after changes that skipped it, use `/maintain-fo ## Scope -The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 23,017,012 distinct states, and without one 22,429,940. 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 23,720,236 distinct states, and without one 23,004,100. The check prints both counts. It assumes: diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 675ac4aa..7d3c0062 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -29,8 +29,9 @@ "src/host/lifecycle.ts#stopSessionProcesses": "74794e19bc382784", "src/host/lifecycle.ts#recordDestroyed": "d968f32f58d3920a", "src/host/lifecycle.ts#destroySession": "873354edcae17792", + "src/host/lifecycle.ts#isMarkedDestroyed": "c1d455f730e8e309", "src/host/lifecycle.ts#writeMarkedDestroyed": "197e7ca08045e384", - "src/host/lifecycle.ts#reconcileSession": "74e867ca0d35d1d1", + "src/host/lifecycle.ts#reconcileSession": "b0a7a94d191e13e4", "src/host/hostMain.ts#waitForManifestFromCreate": "fd500651f83683eb", "src/host/hostMain.ts#isSessionCommandable": "260060f07b068ec1", "src/host/hostMain.ts#SHUTDOWN_KILL_GRACE_MS": "51171d9c5aa6c510", @@ -80,8 +81,8 @@ "src/host/hostMain.ts#runHost(final try)": "16789dd4e2534bc7", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "87fd01745ef6d2d5", - "skill:scripts/facts.mjs": "d49d18dba7311993", + "skill:model/SessionLifecycle.tla": "5275ece860ba092a", + "skill:scripts/facts.mjs": "a5be3b297d608302", "skill:scripts/check.sh": "a7840ba3b1d5c554" }, "callSites": { From 2c47894e02d4aec405f1a5a968a9f8b9743751a6 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 09:32:44 +0000 Subject: [PATCH 12/34] test: a marked repair removes the dead host's socket, and list keeps the session when the repair fails --- test/unit/host/lifecycle.test.ts | 59 ++++++++++++++++++++++++++++++-- 1 file changed, 56 insertions(+), 3 deletions(-) diff --git a/test/unit/host/lifecycle.test.ts b/test/unit/host/lifecycle.test.ts index a75bf981..4ecebb5d 100644 --- a/test/unit/host/lifecycle.test.ts +++ b/test/unit/host/lifecycle.test.ts @@ -7,9 +7,9 @@ import { symlinkSync, writeFileSync, } from 'node:fs'; -import { mkdir, mkdtemp, realpath, rm } from 'node:fs/promises'; +import { chmod, mkdir, mkdtemp, realpath, rm } from 'node:fs/promises'; import { tmpdir } from 'node:os'; -import { join } from 'node:path'; +import { dirname, join } from 'node:path'; import process from 'node:process'; import { afterEach, beforeEach, describe, expect, it, vi } from 'vitest'; @@ -150,7 +150,11 @@ import { import { captureHost, writeHostRecord } from '../../../src/host/hostRecord.js'; import type { SessionRecord } from '../../../src/protocol/schemas.js'; import { readManifest, writeManifest } from '../../../src/storage/manifests.js'; -import { manifestPath, sessionDir } from '../../../src/storage/sessionPaths.js'; +import { + manifestPath, + sessionDir, + socketPath, +} from '../../../src/storage/sessionPaths.js'; import { capturesToken, killGroupIfAlive } from '../../helpers.js'; const HOST_PID = 2_147_483_646; @@ -417,6 +421,55 @@ describe('reconcileSession', () => { }); }); + it('removes the socket that a dead host left when it repairs a destroy', async () => { + const directory = await seedSession( + makeRecord({ + status: 'failed', + failureOrigin: 'host-death', + hostPid: null, + childPid: null, + }), + ); + writeFileSync(join(directory, 'destroyed'), ''); + const socketFile = socketPath(directory); + await mkdir(dirname(socketFile), { recursive: true, mode: 0o700 }); + writeFileSync(socketFile, ''); + + try { + await reconcileSession(directory); + + expect(existsSync(socketFile)).toBe(false); + expect(existsSync(dirname(socketFile))).toBe(false); + } finally { + await rm(dirname(socketFile), { recursive: true, force: true }); + } + }); + + // A root process can write into a folder of mode 0500. + it.skipIf(process.platform === 'win32' || process.getuid?.() === 0)( + 'list keeps a marked failed session when its repair write fails', + async () => { + const directory = await seedSession( + makeRecord({ + status: 'failed', + failureOrigin: 'host-death', + hostPid: null, + childPid: null, + }), + ); + writeFileSync(join(directory, 'destroyed'), ''); + await chmod(directory, 0o500); + + try { + expect(await listSessions(home, true)).toMatchObject([ + { sessionId: 'session-01', status: 'failed' }, + ]); + } finally { + await chmod(directory, 0o700); + } + }, + ); + it('leaves an exited session without the marker as it is', async () => { const exited = makeRecord({ status: 'exited', From 8a6695fdf2549bd00fb1c0f0a202c21ff2978ece Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 09:33:19 +0000 Subject: [PATCH 13/34] fix(host): unlink the socket after a marked repair, and list a marked session whose repair fails --- src/host/lifecycle.ts | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index e2a0967e..fec42291 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -950,11 +950,17 @@ export async function listSessions( isActiveSessionStatus(manifest.status) || isMarkedDestroyed(sessionDirectory, manifest) ) { + const read = manifest; try { await reconcileSession(sessionDirectory); manifest = await readManifestIfExists(manifestFile); } catch { - continue; + // A marked session that ended lists as it reads when its repair + // write fails. + if (isActiveSessionStatus(read.status)) { + continue; + } + manifest = read; } if (manifest === null) { @@ -990,10 +996,11 @@ function isMarkedDestroyed( ); } +// false when gc removed the session folder. async function writeMarkedDestroyed( manifestFile: string, manifest: SessionRecord, -): Promise { +): Promise { const { failureReason: _reason, failureOrigin: _origin, ...rest } = manifest; try { await writeManifest(manifestFile, { @@ -1003,12 +1010,13 @@ async function writeMarkedDestroyed( hostPid: null, childPid: null, }); + return true; } catch (error) { if ( error instanceof CliError && error.code === ERROR_CODES.SESSION_NOT_FOUND ) { - return; + return false; } throw error; } @@ -1021,7 +1029,11 @@ export async function reconcileSession( const manifest = await readManifestIfExists(manifestFile); if (manifest !== null && isMarkedDestroyed(sessionDirectory, manifest)) { - await writeMarkedDestroyed(manifestFile, manifest); + if (await writeMarkedDestroyed(manifestFile, manifest)) { + const socketFile = socketPath(sessionDirectory); + await unlinkIfPresent(socketFile); + await removeSocketDirectoryIfEmpty(socketFile); + } return; } if (manifest === null || isTerminalSessionStatus(manifest.status)) { From c5482b204be2ed68d63b001d74b614b83180b647 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 09:33:19 +0000 Subject: [PATCH 14/34] fix(skills): the marked repair goes on to the socket unlink --- .agents/skills/verify-session-lifecycle/SKILL.md | 2 +- .../verify-session-lifecycle/model/SessionLifecycle.tla | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 806566c4..4cd57bbe 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -417,7 +417,7 @@ node -e 'console.log(require(process.argv[1]).status)' "$AGENT_TTY_HOME/sessions `ReconcileRepairsDestroyed` repairs a destroyed record in the reconcile that replaced it, right after its own write. A reconcile process that was killed between that write and the repair left `failed`, after `destroy` had printed `destroyed: true`, and every later reconcile skipped the terminal manifest (coder/agent-tty#265). A `destroy` of an ended session that failed after its marker write left the marker next to `exited` or `failed` the same way. -Now `reconcileSession` first checks a terminal manifest other than destroyed for the marker. When the marker is there, `writeMarkedDestroyed` writes destroyed from that copy, with `hostPid` and `childPid` null, the exit code kept and no failure fields, and the reconcile returns. Only a `destroy` writes the marker, after it stopped the session and right before its destroyed write, so the marker means that `destroy` chose destroyed. `scanHome` skips a session with the marker, so `home list` and the dashboard picker do not count it while its manifest reads `failed`. The replay holds the repair write of the reconcile in `list` and kills that process: +Now `reconcileSession` first checks a terminal manifest other than destroyed for the marker. When the marker is there, `writeMarkedDestroyed` writes destroyed from that copy, with `hostPid` and `childPid` null, the exit code kept and no failure fields, and the reconcile unlinks the socket, which a `destroy` whose write failed left, and returns. Only a `destroy` writes the marker, after it stopped the session and right before its destroyed write, so the marker means that `destroy` chose destroyed. `scanHome` skips a session with the marker, so `home list` and the dashboard picker do not count it while its manifest reads `failed`. The replay holds the repair write of the reconcile in `list` and kills that process: ```sh id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'exec cat' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))') diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index 7a5ddbef..fe5e23a1 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -778,14 +778,14 @@ SkipsHost(read) == ReconcileSkipsLiveHost /\ read.pid /\ hostAlive \* readManifestIfExists. With ReconcileRepairsMarked, a terminal manifest \* other than destroyed next to the destroy marker gets destroyed from this \* copy (writeMarkedDestroyed), with hostPid and childPid null and the exit -\* code kept, and reconcile returns. Otherwise it returns when the manifest -\* is null or terminal. +\* code kept, and reconcile unlinks the socket and returns. Otherwise it +\* returns when the manifest is null or terminal. ReconcileReads(p) == /\ pc[p] = "r_read" /\ IF ReconcileRepairsMarked /\ dmark /\ mst \in Terminal /\ mst # "destroyed" THEN /\ Write("destroyed", FALSE, "none", mcode, FALSE) - /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)] + /\ pc' = [pc EXCEPT ![p] = "r_unlink"] /\ readRepaired' = TRUE /\ UNCHANGED rd ELSE IF mst = "none" \/ (ReconcileSkipsTerminal /\ mst \in Terminal) From d875e821d476465c592a2663f93cb6e266bcfc37 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 09:33:52 +0000 Subject: [PATCH 15/34] fix(skills): read the marked repair with its socket unlink --- .agents/skills/verify-session-lifecycle/scripts/facts.mjs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 8fa7c1e7..a38ca8e5 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -467,7 +467,7 @@ function repairFacts() { const reconcile = requireDeclaration(lifecycle, 'reconcileSession').body; const marked = indexOfStatement( reconcile, - /^if \(manifest !== null && isMarkedDestroyed\(sessionDirectory, manifest\)\) \{\s*await writeMarkedDestroyed\(manifestFile, manifest\);\s*return;\s*\}$/, + /^if \(manifest !== null && isMarkedDestroyed\(sessionDirectory, manifest\)\) \{\s*if \(await writeMarkedDestroyed\(manifestFile, manifest\)\) \{\s*const socketFile = socketPath\(sessionDirectory\);\s*await unlinkIfPresent\(socketFile\);\s*await removeSocketDirectoryIfEmpty\(socketFile\);\s*\}\s*return;\s*\}$/, ); const markedCheck = normalize( requireDeclaration(lifecycle, 'isMarkedDestroyed').body.getText(), From cb4b7f839c7fe5c328d5fa9ed8cb7b6c56a22a70 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 11:06:44 +0000 Subject: [PATCH 16/34] chore(skills): sync the lifecycle coverage record after the repair unlink --- .agents/skills/verify-session-lifecycle/SKILL.md | 2 +- .agents/skills/verify-session-lifecycle/coverage.json | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 4cd57bbe..fbdf8514 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -473,7 +473,7 @@ To bring the check back in line after changes that skipped it, use `/maintain-fo ## Scope -The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 23,720,236 distinct states, and without one 23,004,100. 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 24,208,708 distinct states, and without one 23,413,352. The check prints both counts. It assumes: diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 7d3c0062..ec75d1c4 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -30,8 +30,8 @@ "src/host/lifecycle.ts#recordDestroyed": "d968f32f58d3920a", "src/host/lifecycle.ts#destroySession": "873354edcae17792", "src/host/lifecycle.ts#isMarkedDestroyed": "c1d455f730e8e309", - "src/host/lifecycle.ts#writeMarkedDestroyed": "197e7ca08045e384", - "src/host/lifecycle.ts#reconcileSession": "b0a7a94d191e13e4", + "src/host/lifecycle.ts#writeMarkedDestroyed": "4863c35f70699757", + "src/host/lifecycle.ts#reconcileSession": "4e5dac8144a0d9fb", "src/host/hostMain.ts#waitForManifestFromCreate": "fd500651f83683eb", "src/host/hostMain.ts#isSessionCommandable": "260060f07b068ec1", "src/host/hostMain.ts#SHUTDOWN_KILL_GRACE_MS": "51171d9c5aa6c510", @@ -81,8 +81,8 @@ "src/host/hostMain.ts#runHost(final try)": "16789dd4e2534bc7", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "5275ece860ba092a", - "skill:scripts/facts.mjs": "a5be3b297d608302", + "skill:model/SessionLifecycle.tla": "e0bda9b1b76958e4", + "skill:scripts/facts.mjs": "a2b23bd2f95e4363", "skill:scripts/check.sh": "a7840ba3b1d5c554" }, "callSites": { From 749795da9b6fefa04c7b46c076f427d52769f92a Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 11:54:48 +0000 Subject: [PATCH 17/34] test: list shows destroyed when the socket cleanup fails after the repair write --- test/unit/host/lifecycle.test.ts | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/test/unit/host/lifecycle.test.ts b/test/unit/host/lifecycle.test.ts index 4ecebb5d..95176066 100644 --- a/test/unit/host/lifecycle.test.ts +++ b/test/unit/host/lifecycle.test.ts @@ -445,6 +445,29 @@ describe('reconcileSession', () => { } }); + it('list shows destroyed when the socket cleanup fails after the repair write', async () => { + const directory = await seedSession( + makeRecord({ + status: 'failed', + failureOrigin: 'host-death', + hostPid: null, + childPid: null, + }), + ); + writeFileSync(join(directory, 'destroyed'), ''); + // unlink of a directory fails with EISDIR (EPERM on macOS). + const socketFile = socketPath(directory); + await mkdir(socketFile, { recursive: true }); + + try { + expect(await listSessions(home, true)).toMatchObject([ + { sessionId: 'session-01', status: 'destroyed' }, + ]); + } finally { + await rm(dirname(socketFile), { recursive: true, force: true }); + } + }); + // A root process can write into a folder of mode 0500. it.skipIf(process.platform === 'win32' || process.getuid?.() === 0)( 'list keeps a marked failed session when its repair write fails', From e845dd71d0ee8e6690980c6e2584f550c3c96a07 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 11:55:42 +0000 Subject: [PATCH 18/34] fix(host): list re-reads the manifest when a marked repair throws after its write --- src/host/lifecycle.ts | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index fec42291..7ae307fb 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -955,12 +955,12 @@ export async function listSessions( await reconcileSession(sessionDirectory); manifest = await readManifestIfExists(manifestFile); } catch { - // A marked session that ended lists as it reads when its repair - // write fails. if (isActiveSessionStatus(read.status)) { continue; } - manifest = read; + // A marked session that ended lists as it reads when its repair + // fails. The repair write can have landed before a later step threw. + manifest = await readManifestIfExists(manifestFile).catch(() => read); } if (manifest === null) { From 35ae60d5fba1392553a2cbba52bd95c1a278f626 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 12:06:20 +0000 Subject: [PATCH 19/34] test: inspect repairs a marked session, and scanHome asks its dependencies for the marker --- test/unit/commands/inspect.test.ts | 25 +++++++++++++++++++++++++ test/unit/storage/homeScope.test.ts | 20 ++++++++++++++++++++ 2 files changed, 45 insertions(+) diff --git a/test/unit/commands/inspect.test.ts b/test/unit/commands/inspect.test.ts index 6e406ec0..d2c2b8a0 100644 --- a/test/unit/commands/inspect.test.ts +++ b/test/unit/commands/inspect.test.ts @@ -9,6 +9,7 @@ const mocks = vi.hoisted(() => ({ deriveTerminationCategory: vi.fn(), emitSuccess: vi.fn(), reconcileSession: vi.fn(), + isMarkedDestroyed: vi.fn(), sendRpc: vi.fn(), readManifest: vi.fn(), readManifestIfExists: vi.fn(), @@ -29,6 +30,7 @@ vi.mock('../../../src/host/eventLog.js', () => ({ vi.mock('../../../src/host/lifecycle.js', () => ({ reconcileSession: mocks.reconcileSession, + isMarkedDestroyed: mocks.isMarkedDestroyed, })); vi.mock('../../../src/host/rpcClient.js', () => ({ @@ -410,6 +412,29 @@ describe('inspect command', () => { ); }); + it('reconciles a failed session that a destroy marked and reports destroyed', async () => { + const failedSession = createSessionRecord('failed'); + mocks.readManifestIfExists.mockResolvedValueOnce(failedSession); + mocks.isMarkedDestroyed.mockReturnValueOnce(true); + mocks.readManifest.mockResolvedValueOnce({ + ...failedSession, + status: 'destroyed', + }); + mocks.countEventLogEntries.mockResolvedValueOnce(3); + + await runInspectCommand({ + context: TEST_CONTEXT, + json: true, + sessionId: 'session-01', + }); + + expect(mocks.reconcileSession).toHaveBeenCalledTimes(1); + const emitted = getLastEmitSuccessPayload() as { + result: { session: { status: string } }; + }; + expect(emitted.result.session.status).toBe('destroyed'); + }); + it('reports offline replay renderer runtime for exited sessions', async () => { const exitedSession = createSessionRecord('exited'); mocks.readManifestIfExists.mockResolvedValueOnce(exitedSession); diff --git a/test/unit/storage/homeScope.test.ts b/test/unit/storage/homeScope.test.ts index 923fbcd3..d61f2397 100644 --- a/test/unit/storage/homeScope.test.ts +++ b/test/unit/storage/homeScope.test.ts @@ -114,6 +114,25 @@ describe('scanHome (read-only Session counts)', () => { expect(after.status).toBe('running'); }); + it('asks its dependencies whether a Session folder holds the destroy marker', async () => { + const dependencies: ScanHomeDependencies = { + readdir: () => Promise.resolve(['marked', 'plain']), + readManifestIfExists: (path) => + Promise.resolve( + makeRecord({ + sessionId: path.includes('marked') ? 'marked' : 'plain', + status: 'failed', + }), + ), + pathExists: (path) => path === '/fake/home/sessions/marked/destroyed', + }; + + expect(await scanHome('/fake/home', dependencies)).toEqual({ + activeSessions: 0, + totalSessions: 1, + }); + }); + it('skips a Session whose manifest fails to read and counts the rest', async () => { // A single corrupt/unreadable manifest must not break discovery of the Home. const dependencies: ScanHomeDependencies = { @@ -124,6 +143,7 @@ describe('scanHome (read-only Session counts)', () => { : Promise.resolve( makeRecord({ sessionId: 'good', status: 'running' }), ), + pathExists: () => false, }; expect(await scanHome('/fake/home', dependencies)).toEqual({ From 18336a121316747ff05e5ca22d85292852c2dc10 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 12:07:19 +0000 Subject: [PATCH 20/34] fix(host): inspect repairs a marked session, and scanHome reads the marker through its dependencies --- src/cli/commands/inspect.ts | 9 ++++++++- src/host/lifecycle.ts | 2 +- src/storage/homeScope.ts | 4 +++- 3 files changed, 12 insertions(+), 3 deletions(-) diff --git a/src/cli/commands/inspect.ts b/src/cli/commands/inspect.ts index 70601277..b4ebcf9b 100644 --- a/src/cli/commands/inspect.ts +++ b/src/cli/commands/inspect.ts @@ -15,7 +15,7 @@ import { countEventLogEntries, statEventLogBytes, } from '../../host/eventLog.js'; -import { reconcileSession } from '../../host/lifecycle.js'; +import { isMarkedDestroyed, reconcileSession } from '../../host/lifecycle.js'; import { sendRpc } from '../../host/rpcClient.js'; import { isCommandableSessionStatus, @@ -208,6 +208,13 @@ export async function runInspectCommand( }); } + // A reconcile records destroyed for an ended session that a destroy marked + // but did not finish (see reconcileSession). + if (isMarkedDestroyed(sessionDirectory, session)) { + await reconcileSession(sessionDirectory); + session = await readManifest(manifestFile); + } + const isLiveHostEligible = isLiveHostEligibleSessionStatus(session.status); let hostInfo: HostInspectResult | undefined; if (isLiveHostEligible) { diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index 7ae307fb..5f918809 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -985,7 +985,7 @@ export async function listSessions( return summaries; } -function isMarkedDestroyed( +export function isMarkedDestroyed( sessionDirectory: string, manifest: SessionRecord, ): boolean { diff --git a/src/storage/homeScope.ts b/src/storage/homeScope.ts index f561eab5..c2b7f928 100644 --- a/src/storage/homeScope.ts +++ b/src/storage/homeScope.ts @@ -38,11 +38,13 @@ export interface HomeSessionCounts { export interface ScanHomeDependencies { readdir: (path: string) => Promise; readManifestIfExists: (path: string) => Promise; + pathExists: (path: string) => boolean; } const defaultScanDependencies: ScanHomeDependencies = { readdir, readManifestIfExists, + pathExists: existsSync, }; /** @@ -89,7 +91,7 @@ export async function scanHome( if ( manifest === null || isDestroyedSessionStatus(manifest.status) || - existsSync(destroyMarkerPath(sessionDir(home, entry))) + dependencies.pathExists(destroyMarkerPath(sessionDir(home, entry))) ) { continue; } From b8b8dbb4effd875220e0b263e0d46ae2ba758bcc Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 12:07:19 +0000 Subject: [PATCH 21/34] fix(skills): split the marked repair into its read and its write --- .../model/SessionLifecycle.tla | 37 +++++++++++++------ 1 file changed, 26 insertions(+), 11 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index fe5e23a1..53b42635 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -149,8 +149,8 @@ VARIABLES dmark, \* the destroy marker file exists in the session directory rec, \* program.json names the program with its token startFailed, \* ghost: the host died because its files were missing - readRepaired, \* ghost: a reconcile's first read wrote destroyed next to - \* the destroy marker + readRepaired, \* ghost: a reconcile wrote destroyed from its first read + \* next to the destroy marker sock, \* the RPC socket file exists (it is outside the directory) cpc, \* create: "alloc", "write", "launch", "done", "failed" \* (it gave up on its host) @@ -776,18 +776,18 @@ AfterReconcile(p) == IF p = "gc" THEN "readafter" ELSE "idle" SkipsHost(read) == ReconcileSkipsLiveHost /\ read.pid /\ hostAlive \* readManifestIfExists. With ReconcileRepairsMarked, a terminal manifest -\* other than destroyed next to the destroy marker gets destroyed from this -\* copy (writeMarkedDestroyed), with hostPid and childPid null and the exit -\* code kept, and reconcile unlinks the socket and returns. Otherwise it -\* returns when the manifest is null or terminal. +\* 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. ReconcileReads(p) == /\ pc[p] = "r_read" /\ IF ReconcileRepairsMarked /\ dmark /\ mst \in Terminal /\ mst # "destroyed" - THEN /\ Write("destroyed", FALSE, "none", mcode, FALSE) - /\ pc' = [pc EXCEPT ![p] = "r_unlink"] - /\ readRepaired' = TRUE - /\ UNCHANGED rd + THEN /\ pc' = [pc EXCEPT ![p] = "r_marked"] + /\ rd' = [rd EXCEPT ![p] = [st |-> mst, pid |-> mpid, + code |-> mcode, child |-> mchild, + grp |-> "none"]] + /\ UNCHANGED <> ELSE IF mst = "none" \/ (ReconcileSkipsTerminal /\ mst \in Terminal) THEN /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)] /\ UNCHANGED <> @@ -905,6 +905,21 @@ ReconcileRepairs(p) == /\ UNCHANGED <> +\* writeMarkedDestroyed: writeManifest destroyed from the copy that the read +\* took, with hostPid and childPid null and the exit code kept. When gc +\* removed the folder in the meantime, the write throws SESSION_NOT_FOUND, +\* and reconcile returns. Otherwise it unlinks the socket and returns. +ReconcileWritesMarked(p) == + /\ pc[p] = "r_marked" + /\ IF WriteLands + THEN /\ Write("destroyed", FALSE, "none", rd[p].code, FALSE) + /\ pc' = [pc EXCEPT ![p] = "r_unlink"] + /\ readRepaired' = TRUE + ELSE /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)] + /\ UNCHANGED <> + /\ UNCHANGED <> + \* unlinkIfPresent(socketPath(sessionDirectory)) ReconcileUnlinksSocket(p) == /\ pc[p] = "r_unlink" @@ -1259,7 +1274,7 @@ Next == \/ ReconcileRereadsManifest(p) \/ ReconcileReadsRecord(p) \/ ReconcilePollsGroup(p) \/ ReconcileWrites(p) \/ ReconcileRepairs(p) - \/ ReconcileUnlinksSocket(p) + \/ ReconcileWritesMarked(p) \/ ReconcileUnlinksSocket(p) \/ GcFindsDirectory \/ GcReadsManifest \/ GcReadsReconciled \/ GcFinalRead \/ GcRemoves \/ ListStartsReconcile From b23d12145af3011154d433ee6f55451eb7fad784 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 12:19:02 +0000 Subject: [PATCH 22/34] test: the marker repairs only an ended session, in reconcile and in scanHome --- test/unit/host/lifecycle.test.ts | 16 ++++++++++++++++ test/unit/storage/homeScope.test.ts | 14 ++++++++++++++ 2 files changed, 30 insertions(+) diff --git a/test/unit/host/lifecycle.test.ts b/test/unit/host/lifecycle.test.ts index 95176066..7a6c5807 100644 --- a/test/unit/host/lifecycle.test.ts +++ b/test/unit/host/lifecycle.test.ts @@ -445,6 +445,22 @@ describe('reconcileSession', () => { } }); + it('leaves a running session with a live host as it is next to the destroy marker', async () => { + const running = makeRecord({ hostPid: process.pid, childPid: null }); + const directory = await seedSession(running); + const own = captureHost(process.pid); + if (own !== null) { + writeHostRecord(directory, own); + } + writeFileSync(join(directory, 'destroyed'), ''); + + await reconcileSession(directory); + expect(await readManifest(manifestPath(directory))).toEqual(running); + expect(await listSessions(home, true)).toMatchObject([ + { sessionId: 'session-01', status: 'running' }, + ]); + }); + it('list shows destroyed when the socket cleanup fails after the repair write', async () => { const directory = await seedSession( makeRecord({ diff --git a/test/unit/storage/homeScope.test.ts b/test/unit/storage/homeScope.test.ts index d61f2397..773ac2dd 100644 --- a/test/unit/storage/homeScope.test.ts +++ b/test/unit/storage/homeScope.test.ts @@ -133,6 +133,20 @@ describe('scanHome (read-only Session counts)', () => { }); }); + it('counts an active Session that holds the destroy marker', async () => { + const dependencies: ScanHomeDependencies = { + readdir: () => Promise.resolve(['marked']), + readManifestIfExists: () => + Promise.resolve(makeRecord({ sessionId: 'marked', status: 'running' })), + pathExists: () => true, + }; + + expect(await scanHome('/fake/home', dependencies)).toEqual({ + activeSessions: 1, + totalSessions: 1, + }); + }); + it('skips a Session whose manifest fails to read and counts the rest', async () => { // A single corrupt/unreadable manifest must not break discovery of the Home. const dependencies: ScanHomeDependencies = { From 6e0a595c3632dc1df8d0019c740e2d738ea5efb9 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 12:19:53 +0000 Subject: [PATCH 23/34] fix(storage): scanHome skips the destroy marker only for an ended session --- src/storage/homeScope.ts | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/storage/homeScope.ts b/src/storage/homeScope.ts index c2b7f928..4525286e 100644 --- a/src/storage/homeScope.ts +++ b/src/storage/homeScope.ts @@ -5,6 +5,7 @@ import { resolve } from 'node:path'; import { isActiveSessionStatus, isDestroyedSessionStatus, + isTerminalSessionStatus, } from '../protocol/sessionStatusPolicy.js'; import type { SessionRecord } from '../protocol/schemas.js'; import { createHomeRegistry, type HomeRegistry } from './homeRegistry.js'; @@ -56,8 +57,8 @@ const defaultScanDependencies: ScanHomeDependencies = { * still shows `running` until something reconciles it); entering a Home in the * dashboard, or running `gc`, reconciles for real. * - * "Visible" excludes destroyed Sessions and Sessions whose folder holds the - * destroy marker, mirroring the dashboard's `all` scope (a destroyed Session's + * "Visible" excludes destroyed Sessions and ended Sessions whose folder holds + * the destroy marker, mirroring the dashboard's `all` scope (a destroyed Session's * Event Log may already be collected). It never throws: * a missing/unreadable sessions tree, or a corrupt individual manifest, counts * as zero/skip so a single bad Session can't break discovery. @@ -91,7 +92,8 @@ export async function scanHome( if ( manifest === null || isDestroyedSessionStatus(manifest.status) || - dependencies.pathExists(destroyMarkerPath(sessionDir(home, entry))) + (isTerminalSessionStatus(manifest.status) && + dependencies.pathExists(destroyMarkerPath(sessionDir(home, entry)))) ) { continue; } From b08dad39a9d80fbaec6b1b34f2ee100ae2eca6cd Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 12:19:54 +0000 Subject: [PATCH 24/34] docs: describe the reach of list, inspect and home list for a marked session --- docs/USAGE.md | 2 +- src/cli/commands/home/README.md | 2 +- src/dashboard/README.md | 2 +- src/host/README.md | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/USAGE.md b/docs/USAGE.md index 305e1c41..8d18a1a0 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -309,7 +309,7 @@ A `destroy` that runs inside the session, such as one typed into the session's s The session's terminal is closed by then, so redirect stdout to keep the result, for example `agent-tty destroy "$AGENT_TTY_SESSION_ID" --json > destroy.json`. When `destroy` records `destroyed` itself, as with `--force`, for a session whose host died or for a session that has already ended, it first writes an empty internal file, `destroyed`, in the session folder. When the host records `destroyed`, as after a plain `destroy` of a live session, nobody writes that file. A reconcile that writes over the record at the same moment finds the file right after its own write and records `destroyed` again. -A `list`, `inspect` or `gc` that reads the session between those two writes sees `failed`, and `home list` and the dashboard count a session with that file as destroyed. If the reconciling process is killed between them, the next reconcile finds the file and records the session as `destroyed`. +A `list`, `inspect` or `gc` that reads the session between those two writes sees `failed`, and `home list` and the dashboard count a session that has ended and has that file as destroyed. If the reconciling process is killed between them, the next reconcile finds the file and records the session as `destroyed`. 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. When `create` cannot reach its new host within about 6 s, it fails with `HOST_UNREACHABLE` or `HOST_TIMEOUT` and tells the host to stop. 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. diff --git a/src/cli/commands/home/README.md b/src/cli/commands/home/README.md index 85d7b4b7..6a1f1c3f 100644 --- a/src/cli/commands/home/README.md +++ b/src/cli/commands/home/README.md @@ -16,7 +16,7 @@ This directory holds the handlers for the `home list` and `home forget` CLI subc - The Home path must be a non-empty string. `normalizeHomePath` enforces this with `invariant` before the registry is called. [src/storage/homeRegistry.ts:normalizeHomePath] - `forget` returns `null` and writes nothing when no entry matches the path as written or its normalized form. [src/storage/homeRegistry.ts:createHomeRegistry] - The registry path must be absolute (`invariant`). A relative `XDG_STATE_HOME` is ignored. [src/storage/homeRegistry.ts:resolveHomeRegistryPath] -- `listRegisteredHomes` drops Homes with zero visible sessions. The count leaves out destroyed sessions and sessions whose manifest is missing or unreadable, so a Home whose sessions are all destroyed is dropped too. In `'active'` scope it also drops Homes with zero active sessions. It sorts the result by `lastSeenAt`, newest first. [src/storage/homeScope.ts:listRegisteredHomes] [src/storage/homeScope.ts:scanHome] +- `listRegisteredHomes` drops Homes with zero visible sessions. The count leaves out destroyed sessions, ended sessions whose folder holds the destroy marker, and sessions whose manifest is missing or unreadable, so a Home whose sessions are all destroyed is dropped too. In `'active'` scope it also drops Homes with zero active sessions. It sorts the result by `lastSeenAt`, newest first. [src/storage/homeScope.ts:listRegisteredHomes] [src/storage/homeScope.ts:scanHome] - With an empty list, human output is the single line `No registered Homes.`. [list.ts:buildHomeListLines] ## Side Effects diff --git a/src/dashboard/README.md b/src/dashboard/README.md index 59fdd4c4..8602828e 100644 --- a/src/dashboard/README.md +++ b/src/dashboard/README.md @@ -28,7 +28,7 @@ The Session Dashboard is an Ink/React terminal UI that lists the Sessions in a h ## Side Effects - `EventLogTailSource.poll()` reads the Event Log with `node:fs/promises` `stat` and `open`/`read`/`close`. [eventSource.ts:EventLogTailSource] -- `listDashboardSessions` reads manifests through `listSessions` (`src/host/lifecycle.ts`) and `readManifestIfExists` (`src/storage/manifests.ts`). `listSessions` calls `reconcileSession` for active Sessions, and that function can rewrite a manifest with `writeManifest` and remove the socket file. [sessionScope.ts:listDashboardSessions] +- `listDashboardSessions` reads manifests through `listSessions` (`src/host/lifecycle.ts`) and `readManifestIfExists` (`src/storage/manifests.ts`). `listSessions` calls `reconcileSession` for active Sessions and for ended Sessions other than destroyed whose folder holds the destroy marker, and that function can rewrite a manifest with `writeManifest` and remove the socket file. [sessionScope.ts:listDashboardSessions] - `runDashboardApp` renders to the terminal with Ink `render()` and waits for `waitUntilExit()`. `App` reads keys with `useInput`, and `q` or Ctrl-C calls `exit()`. [app.tsx:runDashboardApp] [app.tsx:App] - `useFollower` polls with `setInterval` every 33 ms (`FRAME_INTERVAL_MS`) and creates a `libghostty-vt` renderer backend with `createRendererBackend` and the `reference-dark` profile. Cleanup aborts, clears the interval and disposes the follower. [app.tsx:useFollower] - `App` refreshes the Session list with `setInterval` every 1500 ms (`LIST_REFRESH_MS`) and calls `listRegisteredHomes` (`src/storage/homeScope.ts`) for the home picker. [app.tsx:App] diff --git a/src/host/README.md b/src/host/README.md index 0fde33df..e4d66b06 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -18,7 +18,7 @@ - `listenInSocketDirectory(socketFile, listen)` runs `mkdir`, `chmod 0o700` and `listen` up to 5 times when the socket directory vanished before the `chmod` or the bind, because a teardown in the same Home removed it. libuv reports such a bind as `EACCES`. The host and `doctor`'s socket check use it. [lifecycle.ts:listenInSocketDirectory] - `isProcessAlive(pid)` returns `false` for `null` and for a PID that `process.kill(pid, 0)` reports as `ESRCH`, and `true` when the probe succeeds. It asserts a positive integer PID and rethrows other errors, such as `EPERM`. [lifecycle.ts:isProcessAlive] - `destroySession(sessionId, force?, options?)` destroys a session and waits until its manifest shows a terminal status. `DestroySessionOptions` has an optional `AbortSignal`. [lifecycle.ts:destroySession] [lifecycle.ts:DestroySessionOptions] -- `listSessions(home, all?)` returns `SessionSummary[]`. It reconciles active sessions first and hides terminal sessions unless `all` is true. [lifecycle.ts:listSessions] [lifecycle.ts:SessionSummary] +- `listSessions(home, all?)` returns `SessionSummary[]`. It reconciles active sessions, and ended sessions other than destroyed whose folder holds the destroy marker, first. It hides terminal sessions unless `all` is true. [lifecycle.ts:listSessions] [lifecycle.ts:SessionSummary] - `reconcileSession(sessionDirectory)` moves a non-terminal session to a terminal status when its host process is gone. [lifecycle.ts:reconcileSession] - `captureProgram(pid)` returns a `ProgramRecord` (`version`, `pid`, `bootId`, `autogroup`) for the program that the host just spawned, and `writeProgramRecord(sessionDirectory, record)` writes it to `program.json`. `bootId` is a string and `autogroup` a number, or both are `null`. [programGroup.ts:captureProgram] [programGroup.ts:writeProgramRecord] - `readProvenProgramGroup(sessionDirectory)` returns the `program.json` record when it has a token, else `null`. `readProgramGroup(sessionDirectory, childPid)` returns that record, else `{ childPid, sessionDirectory }`, or `null` when `childPid` is `null` or, on Linux, when `host.json` names another pid namespace than the CLI's (`sharesHostPidNamespace`). A `program.json` that does not validate reads as `null` in both, so it gets no kill and no throw. [programGroup.ts:readProgramRecord] [programGroup.ts:readProvenProgramGroup] [programGroup.ts:readProgramGroup] [hostRecord.ts:sharesHostPidNamespace] From ad17bf61ebd06893b5531640f86c5a634a1d85e5 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 12:45:46 +0000 Subject: [PATCH 25/34] chore(skills): sync the lifecycle coverage record after the marked repair split --- .agents/skills/verify-session-lifecycle/SKILL.md | 2 +- .agents/skills/verify-session-lifecycle/coverage.json | 5 +++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index fbdf8514..4cc485aa 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -473,7 +473,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 24,208,708 distinct states, and without one 23,413,352. 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 24,866,000 distinct states, and without one 24,005,824. The check prints both counts. It assumes: diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index ec75d1c4..f078113c 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -29,7 +29,7 @@ "src/host/lifecycle.ts#stopSessionProcesses": "74794e19bc382784", "src/host/lifecycle.ts#recordDestroyed": "d968f32f58d3920a", "src/host/lifecycle.ts#destroySession": "873354edcae17792", - "src/host/lifecycle.ts#isMarkedDestroyed": "c1d455f730e8e309", + "src/host/lifecycle.ts#isMarkedDestroyed": "d178f4a63473915c", "src/host/lifecycle.ts#writeMarkedDestroyed": "4863c35f70699757", "src/host/lifecycle.ts#reconcileSession": "4e5dac8144a0d9fb", "src/host/hostMain.ts#waitForManifestFromCreate": "fd500651f83683eb", @@ -81,7 +81,7 @@ "src/host/hostMain.ts#runHost(final try)": "16789dd4e2534bc7", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "e0bda9b1b76958e4", + "skill:model/SessionLifecycle.tla": "b7d5fd88f74e673f", "skill:scripts/facts.mjs": "a2b23bd2f95e4363", "skill:scripts/check.sh": "a7840ba3b1d5c554" }, @@ -137,6 +137,7 @@ "reconcileSession": [ "src/cli/commands/gc.ts#gcSessions", "src/cli/commands/inspect.ts#runInspectCommand", + "src/cli/commands/inspect.ts#runInspectCommand", "src/host/lifecycle.ts#destroySession", "src/host/lifecycle.ts#destroySession", "src/host/lifecycle.ts#listSessions" From d22e3df44878bbdb622bd11ad54000e20bea16c0 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 15:07:04 +0000 Subject: [PATCH 26/34] test: inspect shows a marked session as it reads when its repair throws --- test/unit/commands/inspect.test.ts | 50 ++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) diff --git a/test/unit/commands/inspect.test.ts b/test/unit/commands/inspect.test.ts index d2c2b8a0..afc02b09 100644 --- a/test/unit/commands/inspect.test.ts +++ b/test/unit/commands/inspect.test.ts @@ -435,6 +435,56 @@ describe('inspect command', () => { expect(emitted.result.session.status).toBe('destroyed'); }); + it('shows the record it read when the repair of a marked session fails', async () => { + const failedSession = createSessionRecord('failed'); + mocks.readManifestIfExists + .mockResolvedValueOnce(failedSession) + .mockResolvedValueOnce(failedSession); + mocks.isMarkedDestroyed.mockReturnValueOnce(true); + mocks.reconcileSession.mockRejectedValueOnce( + makeCliError(ERROR_CODES.STORAGE_WRITE_ERROR, { + message: 'disk full', + }), + ); + mocks.countEventLogEntries.mockResolvedValueOnce(3); + + await runInspectCommand({ + context: TEST_CONTEXT, + json: true, + sessionId: 'session-01', + }); + + const emitted = getLastEmitSuccessPayload() as { + result: { session: { status: string } }; + }; + expect(emitted.result.session.status).toBe('failed'); + }); + + it('shows destroyed when the repair write of a marked session landed before a later step threw', async () => { + const failedSession = createSessionRecord('failed'); + mocks.readManifestIfExists + .mockResolvedValueOnce(failedSession) + .mockResolvedValueOnce({ ...failedSession, status: 'destroyed' }); + mocks.isMarkedDestroyed.mockReturnValueOnce(true); + mocks.reconcileSession.mockRejectedValueOnce( + Object.assign(new Error('EPERM: operation not permitted, unlink'), { + code: 'EPERM', + }), + ); + mocks.countEventLogEntries.mockResolvedValueOnce(3); + + await runInspectCommand({ + context: TEST_CONTEXT, + json: true, + sessionId: 'session-01', + }); + + const emitted = getLastEmitSuccessPayload() as { + result: { session: { status: string } }; + }; + expect(emitted.result.session.status).toBe('destroyed'); + }); + it('reports offline replay renderer runtime for exited sessions', async () => { const exitedSession = createSessionRecord('exited'); mocks.readManifestIfExists.mockResolvedValueOnce(exitedSession); From 61e81f1cdc1b996462650f993605ebcdf4ccd9da Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 15:07:58 +0000 Subject: [PATCH 27/34] fix(cli): inspect shows a marked session as it reads when its repair throws --- src/cli/commands/inspect.ts | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/src/cli/commands/inspect.ts b/src/cli/commands/inspect.ts index b4ebcf9b..4d94228d 100644 --- a/src/cli/commands/inspect.ts +++ b/src/cli/commands/inspect.ts @@ -211,8 +211,17 @@ export async function runInspectCommand( // A reconcile records destroyed for an ended session that a destroy marked // but did not finish (see reconcileSession). if (isMarkedDestroyed(sessionDirectory, session)) { - await reconcileSession(sessionDirectory); - session = await readManifest(manifestFile); + const read = session; + try { + await reconcileSession(sessionDirectory); + session = await readManifest(manifestFile); + } catch { + // A marked session that ended shows as it reads when its repair fails, + // as in list. The repair write can have landed before a later step + // threw. + session = + (await readManifestIfExists(manifestFile).catch(() => read)) ?? read; + } } const isLiveHostEligible = isLiveHostEligibleSessionStatus(session.status); From eaae86e0692cd06fd5e43d7d6e5d9b2795557985 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 15:07:58 +0000 Subject: [PATCH 28/34] docs: scanHome skips only an ended marked session, and inspect keeps its output when the repair fails --- docs/USAGE.md | 2 +- src/cli/commands/README.md | 2 +- src/storage/README.md | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/USAGE.md b/docs/USAGE.md index 8d18a1a0..0449fcc9 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -309,7 +309,7 @@ A `destroy` that runs inside the session, such as one typed into the session's s The session's terminal is closed by then, so redirect stdout to keep the result, for example `agent-tty destroy "$AGENT_TTY_SESSION_ID" --json > destroy.json`. When `destroy` records `destroyed` itself, as with `--force`, for a session whose host died or for a session that has already ended, it first writes an empty internal file, `destroyed`, in the session folder. When the host records `destroyed`, as after a plain `destroy` of a live session, nobody writes that file. A reconcile that writes over the record at the same moment finds the file right after its own write and records `destroyed` again. -A `list`, `inspect` or `gc` that reads the session between those two writes sees `failed`, and `home list` and the dashboard count a session that has ended and has that file as destroyed. If the reconciling process is killed between them, the next reconcile finds the file and records the session as `destroyed`. +A `list`, `inspect` or `gc` that reads the session between those two writes sees `failed`, and `home list` and the dashboard count a session that has ended and has that file as destroyed. If the reconciling process is killed between them, the next reconcile finds the file and records the session as `destroyed`. When that repair fails, for example on a full disk, `list` and `inspect` show the session as it reads. 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. When `create` cannot reach its new host within about 6 s, it fails with `HOST_UNREACHABLE` or `HOST_TIMEOUT` and tells the host to stop. 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. diff --git a/src/cli/commands/README.md b/src/cli/commands/README.md index 341cf2d6..4da44574 100644 --- a/src/cli/commands/README.md +++ b/src/cli/commands/README.md @@ -46,7 +46,7 @@ This directory holds one handler module per agent-tty CLI command. `src/cli/main - 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. A readiness-poll failure rethrows and leaves the session directory in place. It registers the Home through `upsertHome`. [create.ts:runCreateCommand] - `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. [inspect.ts:runInspectCommand] +- `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] - `snapshot`, `screenshot`, `wait` and `record diff` run offline replay through `withOfflineReplayRenderer` (`src/replay/offlineReplay.ts`). `record diff` sends no RPC. [wait.ts:runOfflineRenderWait] [record-diff.ts:runRecordDiffCommand] - Offline `snapshot` and `screenshot` write artifact files into the session artifacts directory and append artifact-manifest entries through `publishArtifactWithRollback` (`src/storage/artifactManifest.ts`). `snapshot` writes a temp JSON file through `writeTextFileAtomic`, and `screenshot` gets a temp PNG from the renderer. `publishArtifactWithRollback` links or copies the temp file into place without replacing an existing file. [src/snapshot/capture.ts:captureSnapshotResult] [src/snapshot/capture.ts:persistSnapshotArtifact] [src/screenshot/capture.ts:captureScreenshotResult] diff --git a/src/storage/README.md b/src/storage/README.md index 28bd46d1..93832219 100644 --- a/src/storage/README.md +++ b/src/storage/README.md @@ -42,7 +42,7 @@ - `computeArtifactHealth` maps only `MANIFEST_VALIDATION_ERROR` to health `manifest-invalid` and rethrows other errors. It validates its result with `ArtifactHealthSummarySchema`. [artifactHealth.ts:computeArtifactHealth] - The registry read returns `[]` on a read error, invalid JSON or a schema failure. The read checks each `homes` entry on its own and drops an invalid entry, so the valid entries survive. `resolveHomeRegistryPath` ignores an empty or relative `XDG_STATE_HOME`. [homeRegistry.ts:createHomeRegistry] [homeRegistry.ts:resolveHomeRegistryPath] - `upsert` reads and then writes the registry with no lock. A code comment states that concurrent creates can race and drop an entry, which registers again on the next create. [homeRegistry.ts:createHomeRegistry] -- The `scanHome` doc comment states that it does not reconcile sessions, does not write manifests and does not throw. It skips destroyed sessions, sessions whose folder holds the destroy marker, and unreadable manifests. [homeScope.ts:scanHome] +- The `scanHome` doc comment states that it does not reconcile sessions, does not write manifests and does not throw. It skips destroyed sessions, ended sessions whose folder holds the destroy marker, and unreadable manifests. [homeScope.ts:scanHome] - `listRegisteredHomes` leaves out Homes with no visible sessions, and the `active` scope also leaves out Homes with no active session. Its doc comment states that it does not rewrite the registry file. [homeScope.ts:listRegisteredHomes] ## Side Effects From 3868d3b05f4199a385c81791d4ad4673f539ccb8 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 16:26:19 +0000 Subject: [PATCH 29/34] docs(skills): count the 68 runs and thirty guards after the merge of main --- .agents/skills/verify-session-lifecycle/SKILL.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 3818aa25..31e793e8 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -62,13 +62,13 @@ From the repo root: .agents/skills/verify-session-lifecycle/scripts/check.sh ``` -It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. On this repo it takes about eleven minutes with the default `CHECK_JOBS` of 4. Seven runs explore the whole model, so `CHECK_JOBS=66` starts every run at once and takes about as long as the longest run. `JAVA=/path/to/java` picks another Java. `TLA2TOOLS_JAR=/path/to/tla2tools.jar` uses a jar you already have, which must be the same 1.7.4 build. `CHECK_OUT=` keeps the results in that folder (default: a new temp folder, printed at the end). +It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. On this repo it takes about eleven minutes with the default `CHECK_JOBS` of 4. Seven runs explore the whole model, so `CHECK_JOBS=68` 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 twenty-nine guards that the rules depend on and the status sets of the policy table, and it hashes each covered function with comments and layout removed. +1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the thirty guards that the rules depend on and the status sets of the policy table, and it hashes each covered function with comments and layout removed. 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 66 times and prints one line per run. +3. It runs TLC 68 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. From 7e259ab77d6d52af5906033fb65e5d6d883d8fcb Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 17:08:35 +0000 Subject: [PATCH 30/34] test: destroy keeps the old socket when the host check throws --- test/unit/host/lifecycle.test.ts | 60 ++++++++++++++++++++++++++++++++ 1 file changed, 60 insertions(+) diff --git a/test/unit/host/lifecycle.test.ts b/test/unit/host/lifecycle.test.ts index 25126006..e95f0ab4 100644 --- a/test/unit/host/lifecycle.test.ts +++ b/test/unit/host/lifecycle.test.ts @@ -9,6 +9,7 @@ import { writeFileSync, } from 'node:fs'; import { chmod, mkdir, mkdtemp, realpath, rm } from 'node:fs/promises'; +import { createServer, type Server } from 'node:net'; import { tmpdir } from 'node:os'; import { dirname, join } from 'node:path'; import process from 'node:process'; @@ -181,6 +182,7 @@ import { ensureSocketRoot } from '../../../src/host/socketRoot.js'; import type { SessionRecord } from '../../../src/protocol/schemas.js'; import { readManifest, writeManifest } from '../../../src/storage/manifests.js'; import { + legacySocketPath, manifestPath, sessionDir, socketPath, @@ -1535,6 +1537,64 @@ describe('removeSocketDirectoryBestEffort', () => { }); }); +// A host of an older version listens at the old path under /tmp/agent-tty. +describe.skipIf(process.platform === 'win32')( + 'the old socket of a destroyed session', + () => { + let oldSocketFile = ''; + let server: Server | undefined; + + beforeEach(async () => { + vi.stubEnv('AGENT_TTY_HOME', home); + const old = legacySocketPath(socketPath(sessionDir(home, 'session-01'))); + expect(old).not.toBeNull(); + oldSocketFile = old as string; + await mkdir(dirname(oldSocketFile), { recursive: true, mode: 0o700 }); + const listening = createServer(); + server = listening; + await new Promise((resolve) => { + listening.listen(oldSocketFile, resolve); + }); + }); + + afterEach(async () => { + await new Promise((resolve) => server?.close(resolve)); + server = undefined; + await rm(dirname(oldSocketFile), { recursive: true, force: true }); + }); + + it('destroy removes it when the host is dead', async () => { + await seedSession(makeRecord({ status: 'destroyed', childPid: null })); + killProbeReportsDead(); + + await expect(destroySession('session-01')).rejects.toMatchObject({ + code: 'SESSION_ALREADY_DESTROYED', + }); + expect(existsSync(oldSocketFile)).toBe(false); + }); + + it('destroy keeps it when the host check throws', async () => { + await seedSession(makeRecord({ status: 'destroyed', childPid: null })); + const failure = Object.assign(new Error('kill EINVAL'), { + code: 'EINVAL', + }); + vi.spyOn(process, 'kill').mockImplementation(() => { + throw failure; + }); + const debug = vi.spyOn(console, 'debug').mockImplementation(() => {}); + + await expect(destroySession('session-01')).rejects.toMatchObject({ + code: 'SESSION_ALREADY_DESTROYED', + }); + expect(existsSync(oldSocketFile)).toBe(true); + expect(debug).toHaveBeenCalledWith( + expect.stringContaining('could not judge the host'), + failure, + ); + }); + }, +); + describe.skipIf(process.platform === 'win32')( 'destroy of a destroyed session', () => { From 30c7173263a529de26d670dd80b7634d205856df Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 17:09:05 +0000 Subject: [PATCH 31/34] fix(host): keep both sockets when the host check of a dead-host socket throws --- src/host/lifecycle.ts | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index fc10b32d..3b723317 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -454,10 +454,18 @@ export async function removeDeadHostSocket( manifest: SessionRecord, ): Promise { const socketFile = socketPath(sessionDirectory); + let alive: boolean; + try { + alive = isHostAlive(await readSessionHost(sessionDirectory, manifest)); + } catch (error) { + // A host that the check cannot judge may still listen on either socket. + console.debug('could not judge the host of a socket:', error); + return; + } + if (alive) { + return; + } try { - if (isHostAlive(await readSessionHost(sessionDirectory, manifest))) { - return; - } await unlinkIfPresent(socketFile); await removeSocketDirectoryIfEmpty(socketFile); } catch (error) { From f452642de7d59cc5ac0653be1e3f2d5ac24d30aa Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 17:09:06 +0000 Subject: [PATCH 32/34] docs: name the umask 002 case of the old socket root, and the kept sockets when the host check throws --- docs/USAGE.md | 2 +- src/host/README.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/USAGE.md b/docs/USAGE.md index 5f4077b6..0db53d2f 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -376,7 +376,7 @@ Each session's RPC socket lies outside the Home, at `/tmp/agent-tty-/<8 hex Known limits: 1. Any user can create `/tmp/agent-tty-` before you do, because `/tmp` is shared. `create`, and every command that talks to a host that this version started, then fails as above until that user or an admin removes it. agent-tty never connects to a socket in such a folder. A host that an older version started stays reachable at the old path (limit 2). -2. A host that an older version started listens at `/tmp/agent-tty/<8 hex>/<12 hex>`. This version still reaches it there when that socket and its folder belong to your uid, no other user can write the folder, and `/tmp/agent-tty` belongs to you or to root and either no other user can write it or it has the sticky bit. `destroy` and `gc` remove that old socket. An older version cannot reach a host that this version started: destroy your sessions before you downgrade. +2. A host that an older version started listens at `/tmp/agent-tty/<8 hex>/<12 hex>`. This version still reaches it there when that socket and its folder belong to your uid, no other user can write the folder, and `/tmp/agent-tty` belongs to you or to root and either no other user can write it or it has the sticky bit. An older version created `/tmp/agent-tty` with your umask, so under umask `002` that folder has mode `0775`. Your group can then write it, and this version does not reach an old host there until you run `chmod g-w /tmp/agent-tty`. `destroy` and `gc` remove that old socket. An older version cannot reach a host that this version started: destroy your sessions before you downgrade. 3. The socket root belongs to the uid of the CLI. A CLI that runs as another uid, for example `sudo agent-tty ...` or `docker exec -u root`, looks under its own root and cannot reach a host that your uid started (`HOST_UNREACHABLE`). Run every command of a session as the uid that created it. For tests and automation, prefer an absolute temp directory: diff --git a/src/host/README.md b/src/host/README.md index 6c571e29..5dcc7aaa 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -18,7 +18,7 @@ - `ensureSocketRoot(root = socketRootDirectory())` creates the socket root with `mkdir` mode `0o700` and then `chmod 0o700` when it is missing. It throws `STORAGE_WRITE_ERROR`, with the path, the owner's uid and the mode in `details`, unless `lstat` shows a directory of the caller's uid with no group or other mode bit: a symlink, a file, a directory of another uid or a group or other bit fails. A private root without all owner bits, as another `create` shows it while umask took them and its `chmod` is pending, gets `chmod 0o700`. It does nothing where `process.getuid` is missing (Windows). `create` calls it before it allocates a session, because the host's errors reach nobody. [socketRoot.ts:ensureSocketRoot] - `socketRootExists(root = socketRootDirectory())` returns `false` for a missing root and `true` for a private one (a directory of the caller's uid with no group or other bit), after the same `chmod 0o700` of a private root without all owner bits. It throws the same `STORAGE_WRITE_ERROR` for any other root. [socketRoot.ts:socketRootExists] - `isOwnLegacySocket(socketFile)` is true when `lstat` shows a socket of the caller's uid, in a Home folder of that uid that no group or other user can write, under a root of that uid or of root that no group or other user can write or that has the sticky bit. No other user can then rename or replace a folder on the path before the connect. [socketRoot.ts:isOwnLegacySocket] -- `removeDeadHostSocket(sessionDirectory, manifest)` unlinks the session's socket and removes the Home's socket directory if it is empty, when the manifest names no host pid or `judgeHost` reads the host as dead. It also removes the socket at `legacySocketPath` when `isOwnLegacySocket` accepts it. It logs errors instead of throwing them. `gc` calls it before it removes a session folder, and `destroySession` calls it before it throws `SESSION_ALREADY_DESTROYED`. [lifecycle.ts:removeDeadHostSocket] +- `removeDeadHostSocket(sessionDirectory, manifest)` unlinks the session's socket and removes the Home's socket directory if it is empty, when the manifest names no host pid or `judgeHost` reads the host as dead. It also removes the socket at `legacySocketPath` when `isOwnLegacySocket` accepts it. When the host check throws, it removes neither socket. It logs errors instead of throwing them. `gc` calls it before it removes a session folder, and `destroySession` calls it before it throws `SESSION_ALREADY_DESTROYED`. [lifecycle.ts:removeDeadHostSocket] - `listenInSocketDirectory(socketFile, listen)` calls `ensureSocketRoot`, then runs `mkdir`, `chmod 0o700` and `listen` up to 5 times when the socket directory vanished before the `chmod` or the bind, because a teardown in the same Home removed it. libuv reports such a bind as `EACCES`. The host and `doctor`'s socket check use it. [lifecycle.ts:listenInSocketDirectory] - `isProcessAlive(pid)` returns `false` for `null` and for a PID that `process.kill(pid, 0)` reports as `ESRCH`, and `true` when the probe succeeds. It asserts a positive integer PID and rethrows other errors, such as `EPERM`. [lifecycle.ts:isProcessAlive] - `destroySession(sessionId, force?, options?)` destroys a session and waits until its manifest shows a terminal status. `DestroySessionOptions` has an optional `AbortSignal`. [lifecycle.ts:destroySession] [lifecycle.ts:DestroySessionOptions] From 90480ffae179452f7f6afbfeb32453defbdacb4e Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 17:48:36 +0000 Subject: [PATCH 33/34] chore(skills): sync the lifecycle coverage record after the merge of main and the socket check fix --- .agents/skills/verify-session-lifecycle/SKILL.md | 2 +- .../verify-session-lifecycle/coverage.json | 16 ++++++++++------ 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index f4c9d061..562eedcf 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -487,7 +487,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 24,866,000 distinct states, and without one 24,005,824. The check prints both counts. +The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 25,534,376 distinct states, and without one 24,675,744. The check prints both counts. It assumes: diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 1f758d60..82fc79f3 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -34,9 +34,11 @@ "src/host/lifecycle.ts#waitForProcessesToExit": "bdab1d674a6856b8", "src/host/lifecycle.ts#stopSessionProcesses": "b1db0094b0a47dba", "src/host/lifecycle.ts#recordDestroyed": "d3a74237a9c8459c", - "src/host/lifecycle.ts#removeDeadHostSocket": "e4044ea706544ff8", + "src/host/lifecycle.ts#removeDeadHostSocket": "34ce07ab7b7e8d7b", "src/host/lifecycle.ts#destroySession": "7eca5878718b1a16", - "src/host/lifecycle.ts#reconcileSession": "c2904456d54b87c8", + "src/host/lifecycle.ts#isMarkedDestroyed": "d178f4a63473915c", + "src/host/lifecycle.ts#writeMarkedDestroyed": "4863c35f70699757", + "src/host/lifecycle.ts#reconcileSession": "4e5dac8144a0d9fb", "src/host/hostMain.ts#waitForManifestFromCreate": "fd500651f83683eb", "src/host/hostMain.ts#isSessionCommandable": "260060f07b068ec1", "src/host/hostMain.ts#SHUTDOWN_KILL_GRACE_MS": "51171d9c5aa6c510", @@ -87,16 +89,17 @@ "src/host/hostMain.ts#runHost(final try)": "16789dd4e2534bc7", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "e6d79fb59b23b4e6", - "skill:scripts/facts.mjs": "c9104f32c0f98233", - "skill:scripts/check.sh": "2609b5abb529c8ee" + "skill:model/SessionLifecycle.tla": "b6f54c9f7169328e", + "skill:scripts/facts.mjs": "d345a22b9b247993", + "skill:scripts/check.sh": "804c565c5d1c68ce" }, "callSites": { "writeManifest": [ "src/host/lifecycle.ts#allocateSession", "src/host/lifecycle.ts#reconcileSession", "src/host/lifecycle.ts#reconcileSession", - "src/host/lifecycle.ts#recordDestroyed" + "src/host/lifecycle.ts#recordDestroyed", + "src/host/lifecycle.ts#writeMarkedDestroyed" ], "persistManifest": [ "src/host/hostMain.ts#runHost", @@ -142,6 +145,7 @@ "reconcileSession": [ "src/cli/commands/gc.ts#gcSessions", "src/cli/commands/inspect.ts#runInspectCommand", + "src/cli/commands/inspect.ts#runInspectCommand", "src/host/lifecycle.ts#destroySession", "src/host/lifecycle.ts#destroySession", "src/host/lifecycle.ts#listSessions" From 91d7f7440274587db33b34a1e24c8a69f1947130 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Tue, 3 Nov 2026 19:46:34 +0000 Subject: [PATCH 34/34] chore(skills): sync the lifecycle coverage record after the merge of main --- .../verify-session-lifecycle/coverage.json | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index c6b3ea55..2687578b 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -34,9 +34,11 @@ "src/host/lifecycle.ts#waitForProcessesToExit": "bdab1d674a6856b8", "src/host/lifecycle.ts#stopSessionProcesses": "d1abb608b1d2160a", "src/host/lifecycle.ts#recordDestroyed": "d3a74237a9c8459c", - "src/host/lifecycle.ts#removeDeadHostSocket": "e4044ea706544ff8", + "src/host/lifecycle.ts#removeDeadHostSocket": "34ce07ab7b7e8d7b", "src/host/lifecycle.ts#destroySession": "d840dd07a0e481f5", - "src/host/lifecycle.ts#reconcileSession": "c2904456d54b87c8", + "src/host/lifecycle.ts#isMarkedDestroyed": "d178f4a63473915c", + "src/host/lifecycle.ts#writeMarkedDestroyed": "4863c35f70699757", + "src/host/lifecycle.ts#reconcileSession": "4e5dac8144a0d9fb", "src/host/hostMain.ts#waitForManifestFromCreate": "fd500651f83683eb", "src/host/hostMain.ts#isSessionCommandable": "260060f07b068ec1", "src/host/hostMain.ts#SHUTDOWN_KILL_GRACE_MS": "51171d9c5aa6c510", @@ -87,16 +89,17 @@ "src/host/hostMain.ts#runHost(final try)": "16789dd4e2534bc7", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "25bc78980b0d67cd", - "skill:scripts/facts.mjs": "86ec94456c10cb37", - "skill:scripts/check.sh": "422878fda4460ac0" + "skill:model/SessionLifecycle.tla": "f7270faba013acff", + "skill:scripts/facts.mjs": "6ae4fd3279517f42", + "skill:scripts/check.sh": "3a47553300cb217a" }, "callSites": { "writeManifest": [ "src/host/lifecycle.ts#allocateSession", "src/host/lifecycle.ts#reconcileSession", "src/host/lifecycle.ts#reconcileSession", - "src/host/lifecycle.ts#recordDestroyed" + "src/host/lifecycle.ts#recordDestroyed", + "src/host/lifecycle.ts#writeMarkedDestroyed" ], "persistManifest": [ "src/host/hostMain.ts#runHost", @@ -142,6 +145,7 @@ "reconcileSession": [ "src/cli/commands/gc.ts#gcSessions", "src/cli/commands/inspect.ts#runInspectCommand", + "src/cli/commands/inspect.ts#runInspectCommand", "src/host/lifecycle.ts#destroySession", "src/host/lifecycle.ts#destroySession", "src/host/lifecycle.ts#listSessions"