From 31bcad69508facfed2128f824fb4c1730aeb94ea Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 01:05:31 +0000 Subject: [PATCH 01/28] fix(skills): let a reconciling list die before its repair, so the repair at the first read must heal it --- .../skills/verify-session-lifecycle/SKILL.md | 46 ++++++++++--------- .../model/SessionLifecycle.tla | 43 ++++++++++++++--- .../verify-session-lifecycle/scripts/check.sh | 4 +- 3 files changed, 62 insertions(+), 31 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 01a783c3..653160e7 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -13,26 +13,26 @@ The tool is TLC, the TLA+ model checker, pinned to release 1.7.4 by sha256. The ## The rules -| Rule | What must hold | Harm when it breaks | -| ------------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | -| R1 `NoLiveSessionDeleted` | gc never removes the folder of a session whose host can still write to it. | A running or starting session loses its manifest and event log. | -| R2 `HostDeathOnlyWhenDead` | The manifest says "failed, host died" only when the host process is dead. | `list` and `inspect` show a live session as failed. Commands refuse it. | -| R3 `TerminalIsFinal` | Once the manifest shows exited, failed or destroyed, it never shows running again. | A finished session looks running, and the next reconcile marks it failed. | -| R4 `RecordedExitKept` | Once the manifest records that the program exited, only `destroy` changes it, to destroyed, and keeps the exit code. | A program that exited 0 is reported as failed, with its exit code lost. | -| R5 `RunningSessionReachable` | While the host serves a running program, the socket file exists. | The session runs, but no command can reach it. | -| R6 `HostStartsWhenCreated` | A host never fails to start because another process removed or rewrote its files. | `create` fails with `HOST_UNREACHABLE` for a session nobody touched. | -| R7 `TerminalIsLastWrite` | Once the manifest shows exited, failed or destroyed, the host has no write left to make. | gc removes the folder while the host still writes to it, and the host's write then fails. | -| R8 `DestroyedOnlyWhenEnded` | While the host lives, the manifest says destroyed only after the host saw the program end. | `list` hides a program that still runs, and gc removes its folder. | -| R9 `DestroyEndsDestroyed` | `destroy` reports success only after it wrote destroyed or read it. | `destroy` says `destroyed: true`, but the session reads failed, "host process died unexpectedly", until a second `destroy`. | -| R10 `RemovedFolderStaysRemoved` | Once gc removed the session folder, no write brings it back. | A late write creates the folder again with only `session.json`. `list --all` shows that stub session until the next gc removes it. | -| R11 `DestroyedProgramStopped` | When the manifest says destroyed, no process of the program's process group runs, unless the program exited on its own first or no manifest named its pid. | A process of the session keeps running, `list` hides it, and nothing stops it later. | -| R13 `LiveGroupStaysNamed` | While a process of the program's process group runs, a manifest that named the program still names it. | The session reads failed or destroyed without `childPid`, so no later `destroy` or reconcile can stop the process that still runs. | -| R14 `DestroyOutlivesProgram` | `destroy` is never killed before it reports, also when it runs inside the program's session. | `destroy` prints nothing. With `--force` it kills its own group, and the session reads exited, not destroyed. | -| R15 `NoUnrelatedGroupKilled` | No kill reaches a process group that took the program's group id after the program's group ended. | `destroy`, `destroy --force`, a reconcile or the host's shutdown sends SIGKILL to an unrelated group, such as the program of another session. | -| R16 `DestroyedSessionStopped` | When the manifest says destroyed, no process of the program's group runs, also none that the program left when it exited on its own, unless the host died before `program.json` named the program. | `destroy` reports `destroyed: true` while a process of the session runs, `list` hides it, and nothing stops it later. | -| R17 `FailedCreateStopped` | Once `create` gave up on its host, the host keeps the session `running` only while `create`'s SIGTERM is on its way to it, or while the host has yet to check for the create-failed marker. | `create` fails with `HOST_UNREACHABLE`, but the session runs, and `list --all` shows it running. | -| R18 `DestroyedStaysDestroyed` | Once `destroy` reported success, the manifest says destroyed while the session folder exists, except while a reconcile that wrote over it has yet to write destroyed again. | `destroy` reports `destroyed: true`, and the session then reads `failed`. | -| R19 `NoUnrelatedHostKilled` | No kill of `destroy --force` reaches a process that took the host's pid after the host ended. | `destroy --force` sends SIGKILL to an unrelated process that got the crashed host's pid. | +| Rule | What must hold | Harm when it breaks | +| ------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | +| R1 `NoLiveSessionDeleted` | gc never removes the folder of a session whose host can still write to it. | A running or starting session loses its manifest and event log. | +| R2 `HostDeathOnlyWhenDead` | The manifest says "failed, host died" only when the host process is dead. | `list` and `inspect` show a live session as failed. Commands refuse it. | +| R3 `TerminalIsFinal` | Once the manifest shows exited, failed or destroyed, it never shows running again. | A finished session looks running, and the next reconcile marks it failed. | +| R4 `RecordedExitKept` | Once the manifest records that the program exited, only `destroy` changes it, to destroyed, and keeps the exit code. | A program that exited 0 is reported as failed, with its exit code lost. | +| R5 `RunningSessionReachable` | While the host serves a running program, the socket file exists. | The session runs, but no command can reach it. | +| R6 `HostStartsWhenCreated` | A host never fails to start because another process removed or rewrote its files. | `create` fails with `HOST_UNREACHABLE` for a session nobody touched. | +| R7 `TerminalIsLastWrite` | Once the manifest shows exited, failed or destroyed, the host has no write left to make. | gc removes the folder while the host still writes to it, and the host's write then fails. | +| R8 `DestroyedOnlyWhenEnded` | While the host lives, the manifest says destroyed only after the host saw the program end. | `list` hides a program that still runs, and gc removes its folder. | +| R9 `DestroyEndsDestroyed` | `destroy` reports success only after it wrote destroyed or read it. | `destroy` says `destroyed: true`, but the session reads failed, "host process died unexpectedly", until a second `destroy`. | +| R10 `RemovedFolderStaysRemoved` | Once gc removed the session folder, no write brings it back. | A late write creates the folder again with only `session.json`. `list --all` shows that stub session until the next gc removes it. | +| R11 `DestroyedProgramStopped` | When the manifest says destroyed, no process of the program's process group runs, unless the program exited on its own first or no manifest named its pid. | A process of the session keeps running, `list` hides it, and nothing stops it later. | +| R13 `LiveGroupStaysNamed` | While a process of the program's process group runs, a manifest that named the program still names it. | The session reads failed or destroyed without `childPid`, so no later `destroy` or reconcile can stop the process that still runs. | +| R14 `DestroyOutlivesProgram` | `destroy` is never killed before it reports, also when it runs inside the program's session. | `destroy` prints nothing. With `--force` it kills its own group, and the session reads exited, not destroyed. | +| R15 `NoUnrelatedGroupKilled` | No kill reaches a process group that took the program's group id after the program's group ended. | `destroy`, `destroy --force`, a reconcile or the host's shutdown sends SIGKILL to an unrelated group, such as the program of another session. | +| R16 `DestroyedSessionStopped` | When the manifest says destroyed, no process of the program's group runs, also none that the program left when it exited on its own, unless the host died before `program.json` named the program. | `destroy` reports `destroyed: true` while a process of the session runs, `list` hides it, and nothing stops it later. | +| R17 `FailedCreateStopped` | Once `create` gave up on its host, the host keeps the session `running` only while `create`'s SIGTERM is on its way to it, or while the host has yet to check for the create-failed marker. | `create` fails with `HOST_UNREACHABLE`, but the session runs, and `list --all` shows it running. | +| R18 `DestroyedStaysDestroyed` | Once `destroy` reported success, the manifest says destroyed while the session folder exists, except while a reconcile that wrote over it has yet to write destroyed again, or, after that reconcile died, until the next reconcile reads the manifest. | `destroy` reports `destroyed: true`, and the session then reads `failed`. | +| R19 `NoUnrelatedHostKilled` | No kill of `destroy --force` reaches a process that took the host's pid after the host ended. | `destroy --force` sends SIGKILL to an unrelated process that got the crashed host's pid. | `TypeOK` also runs in every run. When it breaks, the model is wrong, not the code. @@ -88,7 +88,7 @@ At the sync commit, the expected results are: | `mutant-ProbeCountsDeniedGroup-no-token`, `mutant-KillsProgramGroup-no-token`, `mutant-HostWaitsForGroup-no-token`, `mutant-ReconcileWaitsForGroup-no-token` | violated | The same without a token. The fallback depends on these guards as the code before `program.json` did. With a token, the token check reads a process of another user in view, so only this path checks `ProbeCountsDeniedGroup`. | | `mutant-FreezesUnseenGroup-unseen` | violated | Without the freeze, the kill through the token finds no member in view, the wait reads the group gone, and `destroy` records destroyed while the fork chain runs (R11). | | `mutant-ReusedIdReadsGone` | pass | Without the guard, a group that took the program's id reads alive, so no wait of `destroy` passes while it runs, and `WitnessWaitPassesReusedId` is never reached. The model has no rule for a wait that never ends, so this run checks that witness instead of a rule. | -| `mutant-ReconcileRepairsMarked` | pass | Without the guard, a reconcile skips a marked `failed` as it skips any terminal manifest. The reconcile that wrote that `failed` always repairs it in the model, because the model has no crash of a reconciling process, so no rule breaks. The unit tests in `test/unit/host/lifecycle.test.ts` cover the crash. | +| `mutant-ReconcileRepairsMarked` | violated | R18: without the guard, a `list` that died between its write and its repair leaves `failed`, and the next reconcile skips it as it skips any terminal manifest. | | `mutant-ReconcileSkipsTerminal` | pass | The re-read in `reconcileSession` also returns on a terminal manifest, so the first terminal return alone is redundant. | | `mutant-GcSkipsNonCollectable`, `mutant-GcFinalCheck` | pass | gc checks "collectable" twice. One check alone still keeps R1, so removing one is safe. Removing both is not. | | `mutant-ShutdownChecksCommandable` | pass | `initiateShutdown` requests destroy only while the session is commandable, and the writer writes nothing after a terminal record. Either one alone keeps R3. Removing both is not safe. | @@ -445,6 +445,8 @@ kill -KILL $! # the reconcil node --import tsx src/cli/main.ts list --all --json # the session reads destroyed ``` +In the model, `ListDiesBeforeRepair` kills the `list` process between its write and its repair. The ghost `lostRepair` then holds until the next reconcile reads the manifest, and R18 allows `failed` only until that read. With the guard, that read goes to the repair write (`r_marked`). Without it, the read skips the terminal manifest and R18 breaks. `WitnessDeadRepairRepaired` shows that a session reads destroyed again after such a death. + ### `TokenNamesProgram`: a token that no member of the group carries (R16) node-pty returns before the program calls `setsid()`, so the first reads of the program often show the host's own session and autogroup. Without the guard, `captureToken` could keep an autogroup that it read before the program's `setsid()`, while its next read of the program's stat already showed the new session. The record then held the host's autogroup. No member of the program's group carries that id, so every kill through the record killed nothing and every wait through it read the group gone. `destroy` then recorded destroyed while a process of the program's group ran. @@ -537,7 +539,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` until the next reconcile reads it: that read finds the marker and writes destroyed (`ReconcileRepairsMarked`). `home list` and the dashboard count a session with the marker as destroyed, also in that time. The model has no crash of a reconciling process, so it checks that the repair at the read breaks no rule, not that it heals the crash. +- A destroy that lands between reconcile's last read and its write is still overwritten with failed, for the time until that reconcile finds the destroy marker and writes destroyed again (`ReconcileRepairsDestroyed`). A `list` or `gc` that reads in that time sees `failed`, a terminal status, so gc can remove the folder as it would remove a destroyed one. A reconcile whose process dies in that time leaves `failed` until the next reconcile reads it: that read finds the marker and writes destroyed (`ReconcileRepairsMarked`). `home list` and the dashboard count a session with the marker as destroyed, also in that time. The model kills the `list` process in that time (`ListDiesBeforeRepair`), so it checks that the repair at the read heals the death. A `gc` that dies there leaves the same record, and the model leaves it out. - The idle time-out calls the same `hangUpProgram` as `initiateShutdown`: SIGHUP, then the group kill after `SHUTDOWN_KILL_GRACE_MS`. When the program exits on that SIGHUP, `handlePtyExit` kills the group too, so a process that ignores SIGHUP does not outlive the idle time-out. An idle time-out still ends exited. When the check cannot run (`unknown`), the idle kill sends nothing, and the session ends exited with that process running, as after a program that exits on its own and leaves a process (coder/agent-tty#222). The model leaves both group kills out: they go through `stopProgramGroup` like every kill, and a process that outlives them is one that the program left, which the model keeps after a normal exit anyway. - Windows has no process groups, so there `processGroupTarget` gives the program's pid, and every kill reaches only that process. `destroy` never re-runs on Windows. There SIGTERM ends the host at once, so a `create` that gives up sends it only once the manifest names the program, and the next reconcile records `failed` and ends the program. Before that write, the host finds the create-failed marker (`HostChecksCreateFailed`). `current-win32` checks this with a SIGTERM that is a host crash and without a token, and keeps the process groups of Linux. A marker write that fails, for example on a full disk, leaves a host that the manifest does not name yet serving on Windows. The model has no such failure. - A host stopped with SIGSTOP, or with a blocked event loop, takes the SIGTERM of a `create` that gave up only when it runs again. Until then its program runs and the session reads `running`, which R17 allows because the SIGTERM is still on its way. A plain `destroy` fails because the host does not answer, and only `destroy --force` ends such a session sooner. diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index 76a11572..1ead4ba7 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -183,6 +183,10 @@ VARIABLES rec, \* program.json names the program with its token startFailed, \* ghost: the host died because its files were missing readRepaired, \* ghost: a reconcile wrote destroyed from its first read + lostRepair, \* ghost: a reconcile died between its write and its + \* repair while the marker existed, and no reconcile has + \* read the manifest since + diedBeforeRepair, \* ghost: such a death happened \* next to the destroy marker sock, \* the RPC socket file exists (it is outside the directory) cpc, \* create: "alloc", "write", "launch", "done", "giveup" @@ -249,7 +253,7 @@ VARIABLES diskVars == <> -ghostVars == <> +ghostVars == <> hostVars == <> groupVars == <> @@ -265,6 +269,7 @@ Init == /\ wasTerminal = FALSE /\ wasExited = FALSE /\ wasNamed = FALSE /\ dmark = FALSE /\ cmark = FALSE /\ rec = FALSE /\ startFailed = FALSE /\ readRepaired = FALSE + /\ lostRepair = FALSE /\ diedBeforeRepair = FALSE /\ sock = FALSE /\ cpc = "alloc" /\ hostAlive = FALSE /\ hpc = "none" /\ hex = "none" /\ rsz = "none" @@ -415,6 +420,7 @@ CliKillThrough(named) == IF OtherPidSpace THEN NoKill ELSE KillThrough(named) HostFailsToStart == /\ startFailed' = TRUE /\ readRepaired' = readRepaired + /\ lostRepair' = lostRepair /\ diedBeforeRepair' = diedBeforeRepair /\ hostAlive' = FALSE /\ hpc' = "dead" /\ hex' = IF hex = "none" THEN "none" ELSE "gone" @@ -888,9 +894,12 @@ SkipsHost(read) == ReconcileSkipsLiveHost /\ read.pid /\ CliHostAlive \* readManifestIfExists. With ReconcileRepairsMarked, a terminal manifest \* other than destroyed next to the destroy marker (isMarkedDestroyed) goes \* to the repair write from this copy ("r_marked"). Otherwise it returns when -\* the manifest is null or terminal. +\* the manifest is null or terminal. A reconcile that died before its +\* repair left its failed record, and this read is the next chance to +\* repair it. ReconcileReads(p) == /\ pc[p] = "r_read" + /\ lostRepair' = FALSE /\ diedBeforeRepair' = diedBeforeRepair /\ IF ReconcileRepairsMarked /\ dmark /\ mst \in Terminal /\ mst # "destroyed" THEN /\ pc' = [pc EXCEPT ![p] = "r_marked"] @@ -1027,8 +1036,9 @@ ReconcileWritesMarked(p) == /\ readRepaired' = TRUE ELSE /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)] /\ UNCHANGED <> - /\ UNCHANGED <> + /\ UNCHANGED <> \* unlinkIfPresent(socketPath(sessionDirectory)) ReconcileUnlinksSocket(p) == @@ -1038,6 +1048,19 @@ ReconcileUnlinksSocket(p) == /\ UNCHANGED <> +\* The list process is killed between its write and its repair, for +\* example by a Ctrl-C. Its write may have replaced the destroyed record +\* of a destroy that already reported success. gc's death in the same +\* place leaves the same record, so only list dies in the model. A later +\* list starts a new reconcile. +ListDiesBeforeRepair == + /\ pc["list"] = "r_repair" + /\ pc' = [pc EXCEPT !["list"] = "idle"] + /\ lostRepair' = (lostRepair \/ (dmark /\ mst # "destroyed")) + /\ diedBeforeRepair' = (diedBeforeRepair \/ (dmark /\ mst # "destroyed")) + /\ UNCHANGED <> + \* ------------------------------------------------------------------------- \* gc @@ -1396,6 +1419,7 @@ Next == \/ ReconcilePollsGroup(p) \/ ReconcileWrites(p) \/ ReconcileRepairs(p) \/ ReconcileWritesMarked(p) \/ ReconcileUnlinksSocket(p) + \/ ListDiesBeforeRepair \/ GcFindsDirectory \/ GcReadsManifest \/ GcReadsReconciled \/ GcFinalRead \/ GcRemoves \/ ListStartsReconcile @@ -1417,7 +1441,7 @@ TypeOK == /\ cmark => dir /\ {dir, mpid, mchild, wasTerminal, wasExited, wasNamed, dmark, cmark, startFailed, - readRepaired, sock, + readRepaired, lostRepair, diedBeforeRepair, sock, hostAlive, prog, foreign, sig, dforce, dinside, dsaw, dkill, rec, left, reused, hitUnrelated, diedUnrecorded, passedReused, hrec, hreused, hitUnrelatedHost} @@ -1536,10 +1560,13 @@ FailedCreateStopped == \* R18: once destroy reported success, the manifest says destroyed while the \* directory exists, except while a reconcile that wrote over it has yet to -\* write destroyed again. +\* write destroyed again, or, after that reconcile died, until the next +\* reconcile reads the manifest and writes destroyed. DestroyedStaysDestroyed == (dres = "ok" /\ dir) => - (mst = "destroyed" \/ \E p \in Readers : pc[p] = "r_repair") + \/ mst = "destroyed" + \/ \E p \in Readers : pc[p] \in {"r_repair", "r_marked"} + \/ lostRepair \* R19: no kill of destroy --force reaches a process that took the host's \* pid after the host ended. @@ -1552,6 +1579,8 @@ WitnessGcRemovesSession == gres # "removed" WitnessReconcileRepairs == ~(dmark /\ mst = "failed" /\ \E p \in Readers : pc[p] = "r_repair") WitnessMarkedRepaired == ~readRepaired +WitnessDeadRepairRepaired == + ~(diedBeforeRepair /\ ~lostRepair /\ mst = "destroyed" /\ dir) WitnessCreateGivesUp == ~(cpc = "failed" /\ sig /\ mst = "destroyed" /\ ~hostAlive) WitnessSessionServes == ~(hpc = "serving" /\ sock /\ mst = "running" /\ mpid) diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index 399c57bb..cc061c6a 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/check.sh +++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh @@ -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 WitnessMarkedRepaired WitnessWaitPassesReusedId WitnessReusedHostMeetsKill" +WITNESSES="WitnessGcRemovesSession WitnessCreateGivesUp WitnessSessionServes WitnessResizeLands WitnessCleanExitRecorded WitnessCrashReconciled WitnessDestroyCompletes WitnessSigtermRecorded WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessLeftoverMeetsDestroy WitnessReusedIdMeetsKill WitnessRecordNamesProgram WitnessUnrecordedProgramOutlives WitnessReconcileRepairs WitnessMarkedRepaired WitnessDeadRepairRepaired WitnessWaitPassesReusedId WitnessReusedHostMeetsKill" # --- runs ---------------------------------------------------------------- @@ -212,7 +212,7 @@ write_run mutant-TokenNamesProgram violated DestroyedSessionStopped "TokenNamesP write_run mutant-ReusedIdReadsGone pass WitnessWaitPassesReusedId "ReusedIdReadsGone=FALSE" "with a group that took the id read alive, no wait of destroy passes while that group runs" write_run mutant-ProvesHostPid violated NoUnrelatedHostKilled "ProvesHostPid=FALSE" "without the start-up record, destroy --force kills a process that took the host's pid" NoUnrelatedHostKilled write_run witness-WitnessUnrecordedHostMeetsKill violated WitnessUnrecordedHostMeetsKill "CreateRecordsHost=FALSE" "without a record from create, as when its capture fails, a kill meets a host that host.json does not name yet" -write_run mutant-ReconcileRepairsMarked pass DestroyedStaysDestroyed "ReconcileRepairsMarked=FALSE" "redundant in the model: it has no crash of a reconciling process, so the repair after the reconcile's own write always runs" +write_run mutant-ReconcileRepairsMarked violated DestroyedStaysDestroyed "ReconcileRepairsMarked=FALSE" "without the repair at the first read, a list that died between its write and its repair leaves failed, and the next reconcile skips it" DestroyedStaysDestroyed write_run mutant-ReconcileSkipsTerminal pass RecordedExitKept "ReconcileSkipsTerminal=FALSE" "redundant: the re-read returns on a terminal manifest" write_run mutant-GcSkipsNonCollectable pass NoLiveSessionDeleted "GcSkipsNonCollectable=FALSE" "redundant: the final check still skips" write_run mutant-GcFinalCheck pass NoLiveSessionDeleted "GcFinalCheck=FALSE" "redundant: the first check still skips" From 71154cf2a0418b7058fa1d0ee06c83743a8e9f59 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 01:06:09 +0000 Subject: [PATCH 02/28] docs(host): name the release that drops the old socket path, and why the marked repair needs no liveness check --- src/host/lifecycle.ts | 6 +++++- src/host/rpcClient.ts | 4 ++-- src/host/socketRoot.ts | 3 ++- src/storage/sessionPaths.ts | 4 ++-- 4 files changed, 11 insertions(+), 6 deletions(-) diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index 1ffc620a..a3efad11 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -437,7 +437,8 @@ export async function removeSocketDirectoryBestEffort( } // Removes the socket at the old path of the same session, which a host of an -// older version listens at. Remove this after one minor release. +// older version listens at. Hosts of 0.5.0 and earlier listen there, and +// 0.6.0 is the first release with the per-uid root, so remove this in 0.7.0. async function removeLegacySocketBestEffort(socketFile: string): Promise { const oldSocketFile = legacySocketPath(socketFile); if (oldSocketFile === null || !(await isOwnLegacySocket(oldSocketFile))) { @@ -1131,6 +1132,9 @@ export async function reconcileSession( const manifestFile = manifestPath(sessionDirectory); const manifest = await readManifestIfExists(manifestFile); + // Only a destroy writes the marker, after it stopped the host, so no host + // listens on either socket, and the repair removes both without a liveness + // check. if (manifest !== null && isMarkedDestroyed(sessionDirectory, manifest)) { if (await writeMarkedDestroyed(manifestFile, manifest)) { const socketFile = socketPath(sessionDirectory); diff --git a/src/host/rpcClient.ts b/src/host/rpcClient.ts index 4322cb90..be7bcec5 100644 --- a/src/host/rpcClient.ts +++ b/src/host/rpcClient.ts @@ -119,8 +119,8 @@ export async function sendRpc( signal?: AbortSignal, ): Promise { throwIfAborted(signal); - // A host that an older version started listens at the old path. Remove - // this fallback after one minor release. + // A host that an older version started listens at the old path. Hosts of + // 0.5.0 and earlier listen there, so remove this fallback in 0.7.0. const oldSocketPath = legacySocketPath(socketPath); if (oldSocketPath === null) { return await sendRpcAt(socketPath, method, params, timeoutMs, signal); diff --git a/src/host/socketRoot.ts b/src/host/socketRoot.ts index 6d15d21f..9150598d 100644 --- a/src/host/socketRoot.ts +++ b/src/host/socketRoot.ts @@ -97,7 +97,8 @@ export async function socketRootExists( // listens. No other user may be able to rename or replace a folder on its // path before the connect: the Home's folder is this uid's and not writable // by others, and the root is this uid's or root's, either not writable by -// others or sticky. Remove this after one minor release. +// others or sticky. Hosts of 0.5.0 and earlier listen there, and 0.6.0 is +// the first release with the per-uid root, so remove this in 0.7.0. export async function isOwnLegacySocket(socketFile: string): Promise { const uid = process.getuid?.(); if (uid === undefined) { diff --git a/src/storage/sessionPaths.ts b/src/storage/sessionPaths.ts index c007591b..90c5bf07 100644 --- a/src/storage/sessionPaths.ts +++ b/src/storage/sessionPaths.ts @@ -179,8 +179,8 @@ export function socketPath(sessionDirectory: string): string { return socketFile; } -// A host that an older version started listens under the shared root. Remove -// this after one minor release. +// A host that an older version started listens under the shared root. Hosts +// of 0.5.0 and earlier listen there, so remove this in 0.7.0. export function legacySocketPath(socketFile: string): string | null { const root = socketRootDirectory(); const socketDirectory = dirname(socketFile); From 00b3d5ee72498bf37a5e84113d312cb3a4e767a0 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 01:07:12 +0000 Subject: [PATCH 03/28] test: a failed create names its session in text mode --- test/unit/cli/output.test.ts | 19 +++++++++++++++++++ test/unit/commands/create.test.ts | 30 ++++++++++++++++++++++++++++++ 2 files changed, 49 insertions(+) diff --git a/test/unit/cli/output.test.ts b/test/unit/cli/output.test.ts index b6f10e48..22ce719f 100644 --- a/test/unit/cli/output.test.ts +++ b/test/unit/cli/output.test.ts @@ -94,6 +94,25 @@ describe('emitCliError', () => { }); }); +describe('writeHumanErrorLines', () => { + it('writes the lines to stderr, without color when color is off', () => { + const stderr = vi.spyOn(process.stderr, 'write').mockReturnValue(true); + const stdout = vi.spyOn(process.stdout, 'write').mockReturnValue(true); + output.setColorEnabled(false); + output.writeHumanErrorLines([ + '\u001b[31mSession s-1\u001b[0m failed.', + 'next', + ]); + const stderrCalls = stderr.mock.calls.map(([chunk]) => String(chunk)); + const stdoutCalls = stdout.mock.calls.length; + stderr.mockRestore(); + stdout.mockRestore(); + + expect(stderrCalls).toEqual(['Session s-1 failed.\nnext\n']); + expect(stdoutCalls).toBe(0); + }); +}); + describe('argvHasFlag', () => { afterEach(() => { process.argv = originalArgv; diff --git a/test/unit/commands/create.test.ts b/test/unit/commands/create.test.ts index c1f5087a..f718fd46 100644 --- a/test/unit/commands/create.test.ts +++ b/test/unit/commands/create.test.ts @@ -10,6 +10,7 @@ import type { SessionRecord } from '../../../src/protocol/schemas.js'; const mocks = vi.hoisted(() => ({ emitSuccess: vi.fn(), + writeHumanErrorLines: vi.fn(), allocateSession: vi.fn(), ensureSocketRoot: vi.fn(), launchHost: vi.fn(), @@ -26,6 +27,7 @@ const mocks = vi.hoisted(() => ({ vi.mock('../../../src/cli/output.js', () => ({ emitSuccess: mocks.emitSuccess, + writeHumanErrorLines: mocks.writeHumanErrorLines, })); vi.mock('../../../src/host/lifecycle.js', () => ({ @@ -366,6 +368,34 @@ describe('create command', () => { expect(mocks.writeCreateFailedMarker).not.toHaveBeenCalled(); }); + it('names the session in text mode when the host never answers', async () => { + mocks.sendRpc.mockRejectedValue( + makeCliError(ERROR_CODES.HOST_UNREACHABLE, { + message: 'host unreachable', + }), + ); + + await expect( + runCreateCommand({ ...baseOptions, json: false, context }), + ).rejects.toMatchObject({ code: 'HOST_UNREACHABLE' }); + expect(mocks.writeHumanErrorLines).toHaveBeenCalledWith([ + 'Session session-01 failed to start.', + ]); + }); + + it('leaves the session line out of JSON mode, where details.sessionId names it', async () => { + mocks.sendRpc.mockRejectedValue( + makeCliError(ERROR_CODES.HOST_UNREACHABLE, { + message: 'host unreachable', + }), + ); + + await expect( + runCreateCommand({ ...baseOptions, context }), + ).rejects.toMatchObject({ details: { sessionId: 'session-01' } }); + expect(mocks.writeHumanErrorLines).not.toHaveBeenCalled(); + }); + it('keeps the details of the last error and adds the session id', async () => { mocks.sendRpc.mockRejectedValue( makeCliError(ERROR_CODES.HOST_TIMEOUT, { From 54fed21641c472251bb7faabe7ccb7d61f4ab8cc Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 01:07:12 +0000 Subject: [PATCH 04/28] fix(cli): a failed create names its session in text mode --- .agents/skills/verify-session-lifecycle/scripts/facts.mjs | 8 +++++++- src/cli/commands/create.ts | 7 ++++++- src/cli/output.ts | 4 ++++ 3 files changed, 17 insertions(+), 2 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 0bd9da5d..5d13f889 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -281,7 +281,13 @@ function giveUpCatch(body) { tried[0] === 'result = await waitForReadyHost(socketFile, sessionDirectory, sessionId);' ) { - return s.catchClause.block.statements.map((t) => normalize(t.getText())); + // The text-mode line that names the session changes no process or + // file, so the facts skip it. + return s.catchClause.block.statements + .map((t) => normalize(t.getText())) + .filter( + (t) => !t.startsWith('if (!options.json) { writeHumanErrorLines('), + ); } } return null; diff --git a/src/cli/commands/create.ts b/src/cli/commands/create.ts index fd9da566..f175afbc 100644 --- a/src/cli/commands/create.ts +++ b/src/cli/commands/create.ts @@ -4,7 +4,7 @@ import { setTimeout as delay } from 'node:timers/promises'; import { CliError } from '../errors.js'; import type { CommandContext } from '../context.js'; -import { emitSuccess } from '../output.js'; +import { emitSuccess, writeHumanErrorLines } from '../output.js'; import { DEFAULT_IDLE_TIMEOUT_MS } from '../../config/defaults.js'; import { allocateSession, @@ -292,6 +292,11 @@ export async function runCreateCommand(options: CommandOptions): Promise { if (process.platform !== 'win32' || manifest?.childPid != null) { host.stop(); } + // JSON names the session in details.sessionId. Text mode prints only the + // error line, so name the session before it. + if (!options.json) { + writeHumanErrorLines([`Session ${sessionId} failed to start.`]); + } throw withSessionId(error, sessionId); } diff --git a/src/cli/output.ts b/src/cli/output.ts index 1ce1e6b1..7134581d 100644 --- a/src/cli/output.ts +++ b/src/cli/output.ts @@ -43,6 +43,10 @@ export function writeHumanLines(lines: readonly string[]): void { process.stdout.write(`${formatHumanText(lines.join('\n'))}\n`); } +export function writeHumanErrorLines(lines: readonly string[]): void { + process.stderr.write(`${formatHumanText(lines.join('\n'))}\n`); +} + interface SuccessOutputOptions { command: string; json: boolean; From bfbf46646a585e772b6f89ee801bafa168469534 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 01:09:36 +0000 Subject: [PATCH 05/28] test: on Windows, a host keeps serving when create's manifest read fails after its marker write --- .../fail-manifest-read-after-marker.ts | 29 ++++++ test/integration/lifecycle.test.ts | 99 ++++++++++++++++++- 2 files changed, 127 insertions(+), 1 deletion(-) create mode 100644 test/fixtures/fail-manifest-read-after-marker.ts diff --git a/test/fixtures/fail-manifest-read-after-marker.ts b/test/fixtures/fail-manifest-read-after-marker.ts new file mode 100644 index 00000000..71037a47 --- /dev/null +++ b/test/fixtures/fail-manifest-read-after-marker.ts @@ -0,0 +1,29 @@ +// Preload (`--import`) for a `create` process: once the create-failed marker +// exists, every read of the session's session.json fails with EACCES, as an +// unreadable manifest does. The host inherits NODE_OPTIONS and skips this. +import { existsSync } from 'node:fs'; +import fsp from 'node:fs/promises'; +import { syncBuiltinESMExports } from 'node:module'; +import { basename, dirname } from 'node:path'; +import process from 'node:process'; + +if (process.argv.includes('create') && !process.argv.includes('_host')) { + const readFile = fsp.readFile as (...args: unknown[]) => Promise; + fsp.readFile = ((path: unknown, ...rest: unknown[]) => { + const file = path instanceof URL ? path.pathname : String(path); + if ( + basename(file) === 'session.json' && + existsSync(`${dirname(file)}/create-failed`) + ) { + return Promise.reject( + Object.assign(new Error(`EACCES: permission denied, open '${file}'`), { + code: 'EACCES', + syscall: 'open', + path: file, + }), + ); + } + return readFile(path, ...rest); + }) as typeof fsp.readFile; + syncBuiltinESMExports(); +} diff --git a/test/integration/lifecycle.test.ts b/test/integration/lifecycle.test.ts index 9395091a..d85fff24 100644 --- a/test/integration/lifecycle.test.ts +++ b/test/integration/lifecycle.test.ts @@ -13,7 +13,7 @@ import { writeFile, } from 'node:fs/promises'; import { tmpdir } from 'node:os'; -import { join, resolve } from 'node:path'; +import { basename, dirname, join, resolve } from 'node:path'; import { pathToFileURL } from 'node:url'; import { afterEach, beforeEach, describe, expect, it, vi } from 'vitest'; @@ -1890,6 +1890,103 @@ describe('lifecycle integration', { timeout: 60_000 }, () => { expect(inspectSession(testHome, sessionId as string).status).toBe('failed'); }, 60_000); + // On Windows, create stops a host only when its manifest read names the + // program. Here the host's start-up write and its marker check come before + // create gives up, its listen is held past create's exit, and create's + // manifest read after the marker write fails. Only the host can see the + // marker then. + describe('a create on Windows whose manifest read fails after it gave up', () => { + let pgid = 0; + + afterEach(() => { + if (pgid > 1) { + killGroupIfAlive(pgid); + } + pgid = 0; + }); + + it('lets its host find the marker, stop the program and record destroyed', async () => { + const holdLog = join(testHome, 'hold.log'); + const release = join(testHome, 'release'); + const socketDirectory = basename( + dirname(socketPath(sessionDir(testHome, 'probe'))), + ); + const creator = spawn( + process.execPath, + [ + '--import', + 'tsx', + './src/cli/main.ts', + 'create', + '--json', + '--', + '/bin/sh', + '-c', + 'trap "" HUP; sleep 300 & wait', + ], + { + stdio: ['ignore', 'pipe', 'ignore'], + env: { + ...process.env, + AGENT_TTY_HOME: testHome, + REPLAY_LOG: holdLog, + REPLAY_RELEASE: release, + REPLAY_HOLD: `_host:mkdir:/${socketDirectory}:1:60000`, + NODE_OPTIONS: [ + process.env.NODE_OPTIONS ?? '', + `--import=${pathToFileURL(resolve('.agents/skills/verify-session-lifecycle/scripts/replay-hold.mjs')).href}`, + `--import=${pathToFileURL(resolve('test/fixtures/denied-autogroup.ts')).href}`, + `--import=${pathToFileURL(resolve('test/fixtures/fake-win32-create.ts')).href}`, + `--import=${pathToFileURL(resolve('test/fixtures/fail-manifest-read-after-marker.ts')).href}`, + ].join(' '), + }, + }, + ); + let stdout = ''; + creator.stdout.on('data', (chunk: Buffer) => { + stdout += chunk.toString('utf8'); + }); + const creatorExit = once(creator, 'exit'); + const deadline = Date.now() + 15_000; + while ( + !(await readFile(holdLog, 'utf8').then( + (log) => log.includes('hold mkdir'), + () => false, + )) + ) { + expect(Date.now()).toBeLessThan(deadline); + await sleep(50); + } + const [sessionId] = await readdir(join(testHome, 'sessions')); + const directory = sessionDir(testHome, sessionId as string); + const manifest = SessionRecordSchema.parse( + JSON.parse(await readFile(manifestPath(directory), 'utf8')), + ); + expect(manifest.childPid).not.toBeNull(); + const hostPid = manifest.hostPid as number; + pgid = manifest.childPid as number; + expect(isGroupAlive(pgid)).toBe(true); + + const [code] = (await creatorExit) as [number | null]; + expect(code).toBe(6); + expect(JSON.parse(stdout)).toMatchObject({ + ok: false, + error: { code: 'HOST_UNREACHABLE', details: { sessionId } }, + }); + expect(existsSync(join(directory, 'create-failed'))).toBe(true); + await writeFile(release, ''); + + const stopDeadline = Date.now() + 20_000; + while (isGroupAlive(pgid) || isProcessAlive(hostPid)) { + expect(Date.now()).toBeLessThan(stopDeadline); + await sleep(100); + } + expect(inspectSession(testHome, sessionId as string).status).toBe( + 'destroyed', + ); + }, 60_000); + }); + // A SIGTERM that the default action would turn into a host death between // the spawn and program.json leaves a program that no file names. describe('a host that gets SIGTERM right after it spawns the program', () => { From 136b15e3bdf458b3848e10d92a3549014da52a99 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 01:12:35 +0000 Subject: [PATCH 06/28] fix(host): watch for the create-failed marker while the creator runs --- src/host/hostMain.ts | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/host/hostMain.ts b/src/host/hostMain.ts index 82673d85..3052f70c 100644 --- a/src/host/hostMain.ts +++ b/src/host/hostMain.ts @@ -106,6 +106,7 @@ export const MAX_CONSECUTIVE_POLL_FAILURES = 10; // may exceed idleTimeoutMs by up to checkIntervalMs (bounded by this cap). const IDLE_CHECK_CAP_MS = 5_000; const MANIFEST_WAIT_INTERVAL_MS = 20; +const CREATE_FAILED_POLL_INTERVAL_MS = 100; // How long the host waits after SIGHUP before it kills the program's process // group. nvim takes about 1 s to exit on SIGHUP, and `destroy` waits about 5 s. const SHUTDOWN_KILL_GRACE_MS = 2_000; @@ -1272,6 +1273,23 @@ export async function runHost( invariant(!sigterm.received, 'SIGTERM is handled only after the spawn block'); onSigterm = startShutdown; + // A create that gives up after the check below may not stop the host: on + // Windows it sends nothing when its manifest read fails. It writes the + // create-failed marker before it exits, so the host watches for the marker + // while its creator runs, and once more after the creator has exited. + const watchCreateFailed = (): void => { + const timer = setInterval(() => { + const creatorGone = !isProcessAlive(creatorPid); + if (existsSync(createFailedMarkerPath(sessDir))) { + clearInterval(timer); + startShutdown(); + } else if (creatorGone) { + clearInterval(timer); + } + }, CREATE_FAILED_POLL_INTERVAL_MS); + timer.unref(); + }; + try { writeProgramRecord(sessDir, program); await persistManifest(); @@ -1283,6 +1301,7 @@ export async function runHost( await initiateShutdown(); return; } + watchCreateFailed(); if (!isSessionCommandable(state)) { await initiateShutdown(); From c5c107cda55e3e229fe2724cda17f7bd3b7bebd6 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 01:12:35 +0000 Subject: [PATCH 07/28] fix(skills): model the host's marker watch and a Windows manifest read that fails --- .../model/SessionLifecycle.tla | 50 +++++++++++++++---- .../verify-session-lifecycle/scripts/check.sh | 6 ++- .../scripts/facts.mjs | 25 ++++++++++ 3 files changed, 68 insertions(+), 13 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index 1ead4ba7..8c5bc592 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -101,6 +101,10 @@ CONSTANTS \* it reads the manifest, and the host checks \* for it before the spawn and right after its \* start-up write, and then ends the session + HostPollsCreateFailed, \* hostMain.ts: from its start-up check on, the + \* host checks for the create-failed marker + \* while its creator runs and once after, and + \* then ends the session TokenNamesProgram, \* programGroup.ts: captureToken records an \* autogroup only once the program leads its \* own session in an autogroup other than the @@ -154,7 +158,7 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, ReconcileSkipsTerminal, InsideCheckReadsEnv, RecordsProgramSync, ProvesGroupOwnership, DestroyStopsLeftovers, FallbackNeedsFolder, CreateStopsOnGiveUp, - HostChecksCreateFailed, + HostChecksCreateFailed, HostPollsCreateFailed, ReconcileRepairsDestroyed, ReconcileRepairsMarked, TokenNamesProgram, ReusedIdReadsGone, ProvesHostPid, CreateRecordsHost, @@ -187,6 +191,7 @@ VARIABLES \* repair while the marker existed, and no reconcile has \* read the manifest since diedBeforeRepair, \* ghost: such a death happened + polled, \* ghost: the host's watch found the create-failed marker \* next to the destroy marker sock, \* the RPC socket file exists (it is outside the directory) cpc, \* create: "alloc", "write", "launch", "done", "giveup" @@ -253,7 +258,8 @@ VARIABLES diskVars == <> -ghostVars == <> +ghostVars == <> hostVars == <> groupVars == <> @@ -269,7 +275,7 @@ Init == /\ wasTerminal = FALSE /\ wasExited = FALSE /\ wasNamed = FALSE /\ dmark = FALSE /\ cmark = FALSE /\ rec = FALSE /\ startFailed = FALSE /\ readRepaired = FALSE - /\ lostRepair = FALSE /\ diedBeforeRepair = FALSE + /\ lostRepair = FALSE /\ diedBeforeRepair = FALSE /\ polled = FALSE /\ sock = FALSE /\ cpc = "alloc" /\ hostAlive = FALSE /\ hpc = "none" /\ hex = "none" /\ rsz = "none" @@ -421,6 +427,7 @@ HostFailsToStart == /\ startFailed' = TRUE /\ readRepaired' = readRepaired /\ lostRepair' = lostRepair /\ diedBeforeRepair' = diedBeforeRepair + /\ polled' = polled /\ hostAlive' = FALSE /\ hpc' = "dead" /\ hex' = IF hex = "none" THEN "none" ELSE "gone" @@ -501,11 +508,13 @@ CreateGivesUp == \* On Windows the SIGTERM ends the host at once, without its handlers, so \* create sends it only when the manifest that it reads after the marker \* write names the program. The next reconcile then records failed and ends -\* the program. +\* the program. That read can fail, for example when the file is not +\* readable, and then create sends nothing. CreateStopsHostOnWindows == /\ cpc = "giveup" /\ cpc' = "failed" - /\ IF CreateStopsOnGiveUp /\ mchild /\ hostAlive + /\ \E readOk \in BOOLEAN : + IF CreateStopsOnGiveUp /\ readOk /\ mchild /\ hostAlive THEN /\ HostDies /\ UNCHANGED <> @@ -703,6 +712,21 @@ HostGetsSigterm == /\ UNCHANGED <> +\* watchCreateFailed: from right after the start-up check on, the host +\* checks for the create-failed marker every 100 ms while its creator runs, +\* and once after the creator exited. create writes the marker before it +\* exits, so the watch finds every marker. On the marker it calls +\* startShutdown, as for a SIGTERM. +HostPollsMarker == + /\ HostPollsCreateFailed + /\ hostAlive /\ cmark /\ hsd = "none" + /\ hpc \in {"sockdir", "serving"} + /\ polled' = TRUE + /\ StartShutdown(WriteQueued) + /\ UNCHANGED <> + \* initiateShutdown's `await persistManifest()` lands, then its finally block \* starts. HostWritesDestroying == @@ -900,6 +924,7 @@ SkipsHost(read) == ReconcileSkipsLiveHost /\ read.pid /\ CliHostAlive ReconcileReads(p) == /\ pc[p] = "r_read" /\ lostRepair' = FALSE /\ diedBeforeRepair' = diedBeforeRepair + /\ polled' = polled /\ IF ReconcileRepairsMarked /\ dmark /\ mst \in Terminal /\ mst # "destroyed" THEN /\ pc' = [pc EXCEPT ![p] = "r_marked"] @@ -1036,8 +1061,8 @@ ReconcileWritesMarked(p) == /\ readRepaired' = TRUE ELSE /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)] /\ UNCHANGED <> - /\ UNCHANGED <> \* unlinkIfPresent(socketPath(sessionDirectory)) @@ -1058,8 +1083,9 @@ ListDiesBeforeRepair == /\ pc' = [pc EXCEPT !["list"] = "idle"] /\ lostRepair' = (lostRepair \/ (dmark /\ mst # "destroyed")) /\ diedBeforeRepair' = (diedBeforeRepair \/ (dmark /\ mst # "destroyed")) - /\ UNCHANGED <> + /\ UNCHANGED <> \* ------------------------------------------------------------------------- \* gc @@ -1406,7 +1432,7 @@ Next == \/ CreateMakesDirectory \/ CreateWritesManifest \/ CreateLaunchesHost \/ CreateGivesUp \/ CreateStopsHostOnWindows \/ HostReadsManifest \/ HostOpensLogAndSpawns \/ HostRecordsProgram - \/ HostWritesPids \/ HostChecksMarker + \/ HostWritesPids \/ HostChecksMarker \/ HostPollsMarker \/ HostListens \/ HostStartsResize \/ HostResizeWriteLands \/ HostGetsSigterm \/ HostWritesDestroying \/ HostClosesSocket \/ HostKillsProgram \/ ProgramExits \/ HostPollsGroup \/ HostWritesExit @@ -1441,7 +1467,7 @@ TypeOK == /\ cmark => dir /\ {dir, mpid, mchild, wasTerminal, wasExited, wasNamed, dmark, cmark, startFailed, - readRepaired, lostRepair, diedBeforeRepair, sock, + readRepaired, lostRepair, diedBeforeRepair, polled, sock, hostAlive, prog, foreign, sig, dforce, dinside, dsaw, dkill, rec, left, reused, hitUnrelated, diedUnrecorded, passedReused, hrec, hreused, hitUnrelatedHost} @@ -1557,6 +1583,7 @@ FailedCreateStopped == \/ CreateStopsOnGiveUp /\ ~Win32 /\ ~sig \/ HostChecksCreateFailed /\ cmark /\ hpc \in {"boot", "open", "record", "pidwrite", "markcheck"} + \/ HostPollsCreateFailed /\ cmark /\ hpc \in {"sockdir", "serving"} \* R18: once destroy reported success, the manifest says destroyed while the \* directory exists, except while a reconcile that wrote over it has yet to @@ -1579,6 +1606,7 @@ WitnessGcRemovesSession == gres # "removed" WitnessReconcileRepairs == ~(dmark /\ mst = "failed" /\ \E p \in Readers : pc[p] = "r_repair") WitnessMarkedRepaired == ~readRepaired +WitnessMarkerPolled == ~polled WitnessDeadRepairRepaired == ~(diedBeforeRepair /\ ~lostRepair /\ mst = "destroyed" /\ dir) WitnessCreateGivesUp == diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index cc061c6a..b597f65a 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 ReconcileRepairsMarked CreateStopsOnGiveUp HostChecksCreateFailed TokenNamesProgram ReusedIdReadsGone ProvesHostPid CreateRecordsHost FreezesUnseenGroup UnsharedGroupReadsUnknown" +GUARDS="GcSkipsNonCollectable GcFinalCheck ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed ReconcileRepairsMarked CreateStopsOnGiveUp HostChecksCreateFailed HostPollsCreateFailed TokenNamesProgram ReusedIdReadsGone ProvesHostPid CreateRecordsHost FreezesUnseenGroup UnsharedGroupReadsUnknown" # 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 WitnessMarkedRepaired WitnessDeadRepairRepaired WitnessWaitPassesReusedId WitnessReusedHostMeetsKill" +WITNESSES="WitnessGcRemovesSession WitnessCreateGivesUp WitnessSessionServes WitnessResizeLands WitnessCleanExitRecorded WitnessCrashReconciled WitnessDestroyCompletes WitnessSigtermRecorded WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessLeftoverMeetsDestroy WitnessReusedIdMeetsKill WitnessRecordNamesProgram WitnessUnrecordedProgramOutlives WitnessReconcileRepairs WitnessMarkedRepaired WitnessDeadRepairRepaired WitnessWaitPassesReusedId WitnessReusedHostMeetsKill WitnessMarkerPolled" # --- runs ---------------------------------------------------------------- @@ -208,6 +208,7 @@ write_run mutant-FallbackNeedsFolder violated NoUnrelatedGroupKilled "FallbackNe write_run mutant-ReconcileRepairsDestroyed violated DestroyedStaysDestroyed "ReconcileRepairsDestroyed=FALSE" "without the marker, a reconcile writes failed over the destroyed that destroy reported" DestroyedStaysDestroyed write_run mutant-CreateStopsOnGiveUp violated FailedCreateStopped "CreateStopsOnGiveUp=FALSE" "without the SIGTERM, a create that gave up leaves its host serving the session" FailedCreateStopped write_run mutant-HostChecksCreateFailed pass FailedCreateStopped "HostChecksCreateFailed=FALSE" "redundant off Windows: the SIGTERM stops the host" +write_run mutant-HostPollsCreateFailed pass FailedCreateStopped "HostPollsCreateFailed=FALSE" "redundant off Windows: the SIGTERM stops the host" write_run mutant-TokenNamesProgram violated DestroyedSessionStopped "TokenNamesProgram=FALSE" "with the host's autogroup as the token, no member carries it, and destroy records destroyed while the program's group runs" DestroyedSessionStopped write_run mutant-ReusedIdReadsGone pass WitnessWaitPassesReusedId "ReusedIdReadsGone=FALSE" "with a group that took the id read alive, no wait of destroy passes while that group runs" write_run mutant-ProvesHostPid violated NoUnrelatedHostKilled "ProvesHostPid=FALSE" "without the start-up record, destroy --force kills a process that took the host's pid" NoUnrelatedHostKilled @@ -254,6 +255,7 @@ write_run mutant-ReconcileWaitsForGroup-no-token violated LiveGroupStaysNamed "R WIN32=TRUE write_run current-win32 pass "$NO_TOKEN_RULES" "" "the code on Windows: R1 to R14 and R17 to R19 hold" write_run mutant-HostChecksCreateFailed-win32 violated FailedCreateStopped "HostChecksCreateFailed=FALSE" "without the marker, a host that the manifest does not name yet keeps serving after create gave up" FailedCreateStopped +write_run mutant-HostPollsCreateFailed-win32 violated FailedCreateStopped "HostPollsCreateFailed=FALSE" "without the watch, a host that checked for the marker before create wrote it keeps serving when create cannot read the manifest" FailedCreateStopped WIN32=FALSE run_tlc() { diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 5d13f889..093cabc2 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -257,6 +257,7 @@ function createFacts() { CreateRecordsHost: recordsHost, CreateStopsOnGiveUp: stopsOnGiveUp(create.body), HostChecksCreateFailed: checksCreateFailed(create.body), + HostPollsCreateFailed: pollsCreateFailed(), }; } @@ -370,6 +371,29 @@ function checksCreateFailed(body) { ); } +// runHost's watchCreateFailed checks, every CREATE_FAILED_POLL_INTERVAL_MS, +// whether the creator still runs and then whether the create-failed marker +// exists. On the marker it calls startShutdown, and it stops once a check +// after the creator's exit found none. The start-up try calls it right after +// the check that follows the start-up write. +function pollsCreateFailed() { + const run = requireDeclaration('src/host/hostMain.ts', 'runHost').body; + const watch = indexOfStatement(run, /^const watchCreateFailed = /); + const watches = + watch >= 0 && + normalize(run.statements[watch].getText()) === + 'const watchCreateFailed = (): void => { const timer = setInterval(() => { const creatorGone = !isProcessAlive(creatorPid); if (existsSync(createFailedMarkerPath(sessDir))) { clearInterval(timer); startShutdown(); } else if (creatorGone) { clearInterval(timer); } }, CREATE_FAILED_POLL_INTERVAL_MS); timer.unref(); };'; + const last = run.statements.at(-1); + const tried = + last !== undefined && ts.isTryStatement(last) + ? last.tryBlock.statements.map((t) => normalize(t.getText())) + : []; + const check = tried.indexOf( + 'if (existsSync(createFailedMarkerPath(sessDir))) { await initiateShutdown(); return; }', + ); + return watches && check >= 0 && tried[check + 1] === 'watchCreateFailed();'; +} + // runHost waits for create's manifest, and every host write of session.json // goes through one createSerialManifestWriter. function hostFacts() { @@ -1502,6 +1526,7 @@ const RUN_HOST_PARTS = [ /^process\.on\('SIGTERM'/, /^let onSigterm = /, /^if \(existsSync\(createFailedMarkerPath\(sessDir\)\)\) \{/, + /^const watchCreateFailed = /, /^if \(sigterm\.received\) \{/, /^invariant\(!sigterm\.received/, /^onSigterm = startShutdown;/, From 648aed63ebd295f86b978eede08b23f41a53a2d4 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 01:13:55 +0000 Subject: [PATCH 08/28] docs: describe the host's marker watch, the text-mode session line and a list that dies before its repair --- .../skills/verify-session-lifecycle/SKILL.md | 18 +++++++++++++----- docs/USAGE.md | 4 ++-- src/cli/README.md | 2 +- src/cli/commands/README.md | 2 +- src/host/README.md | 2 +- 5 files changed, 18 insertions(+), 10 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 653160e7..a81ff814 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -42,7 +42,7 @@ Yes, when the diff changes any of these: - `src/host/lifecycle.ts`: `allocateSession` (and the order of its `launch` call and first manifest write), `launchHost`, `isProcessAlive`, the host proof (`readSessionHost`, `psShowsSessionHost`, `isHostAlive`, `hostMatches`, `killHostBestEffort`), `cliRunsInsideProgramSession` with `ownLinuxSessionId`, `ownProcessGroupId`, `controllingTerminal` and `sharesControllingTerminal`, `reconcileSession`, and `destroySession` with its local `stopLeftoversThenRecordDestroyed` and its helpers `recordDestroyed`, `stopSessionProcesses`, `readSessionManifestOrThrow`, `waitForTerminalManifest`, `waitForProcessesToExit` and `killProcessBestEffort`, and `removeDeadHostSocket`, which `gc` and `destroySession` call. - `src/host/programGroup.ts`: the token capture (`captureProgram`, `captureToken`, `readAutogroup`, `parseAutogroup`, `parseProcStat`), the `/proc` reads (`readProcFileIfExists`, `readLiveThreadState`, `readProcStat`, `readShownProcStat`, `isRefusedRead`, `readBootId`), the record (`writeProgramRecord`, `readProgramRecord`, `readProvenProgramGroup`, `readProgramGroup`), `procShowsOwnPidSpace`, the verdict (`judgeProgramGroup`, `readGroupMembers`), and the kill and the probe (`stopProgramGroup`, `isProgramGroupAlive`, `processGroupTarget`, `isProcessGroupAlive` with `groupHasLiveProcess` and `procHidesOtherUsers`, `killProcessGroupBestEffort`, `signalProcessGroup`). -- `src/host/hostMain.ts`: `waitForManifestFromCreate`, `isSessionCommandable`, and in `runHost` the start-up statements (the manifest wait, the `hostPid === process.pid` check, the `host.json` write with `captureHost` and `writeHostRecord`, `createSerialManifestWriter`, `EventLog.open`, the create-failed marker check, `createPty`, `setChildPid`, `captureProgram`), `hangUpProgram` with its kill timer and the `SHUTDOWN_KILL_GRACE_MS` constant, `startIdlePolling` (the idle time-out), `initiateShutdown`, `startShutdown`, `handlePtyExit` with its wait for the program's group, `pty.onExit`, the `SIGTERM` handler, the `resize` and `destroy` handlers, and the last `try` block (the `program.json` write, the start-up manifest write and `rpcServer.listen`). +- `src/host/hostMain.ts`: `waitForManifestFromCreate`, `isSessionCommandable`, and in `runHost` the start-up statements (the manifest wait, the `hostPid === process.pid` check, the `host.json` write with `captureHost` and `writeHostRecord`, `createSerialManifestWriter`, `EventLog.open`, the create-failed marker check, `createPty`, `setChildPid`, `captureProgram`, `watchCreateFailed`), `hangUpProgram` with its kill timer and the `SHUTDOWN_KILL_GRACE_MS` constant, `startIdlePolling` (the idle time-out), `initiateShutdown`, `startShutdown`, `handlePtyExit` with its wait for the program's group, `pty.onExit`, the `SIGTERM` handler, the `resize` and `destroy` handlers, and the last `try` block (the `program.json` write, the start-up manifest write and `rpcServer.listen`). - `src/host/manifestWriter.ts` `createSerialManifestWriter`. - `src/cli/commands/gc.ts` `gcSessions`, `src/cli/commands/create.ts` `runCreateCommand` with `waitForReadyHost`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`. - `src/host/sessionState.ts` `setDimensions`, `requestDestroy`, `recordDestroyed` and `recordExit`, `src/host/eventLog.ts` `EventLog.open`, `src/host/rpcServer.ts` `listen` and `close`, `src/host/rpcClient.ts` `toTransportCliError` (which socket errors read as `HOST_UNREACHABLE`). @@ -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. Ten runs explore more than 20 million distinct states each, so `CHECK_JOBS=75` starts every run at once and takes about as long as the longest run. `JAVA=/path/to/java` picks another Java. `TLA2TOOLS_JAR=/path/to/tla2tools.jar` uses a jar you already have, which must be the same 1.7.4 build. `CHECK_OUT=` keeps the results in that folder (default: a new temp folder, printed at the end). +It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. On this repo it takes about eleven minutes with the default `CHECK_JOBS` of 4. Ten runs explore more than 20 million distinct states each, so `CHECK_JOBS=79` starts every run at once and takes about as long as the longest run. `JAVA=/path/to/java` picks another Java. `TLA2TOOLS_JAR=/path/to/tla2tools.jar` uses a jar you already have, which must be the same 1.7.4 build. `CHECK_OUT=` keeps the results in that folder (default: a new temp folder, printed at the end). What it does: -1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the thirty-three guards that the rules depend on and the status sets of the policy table, and it hashes each covered function with comments and layout removed. +1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the thirty-four guards that the rules depend on and the status sets of the policy table, and it hashes each covered function with comments and layout removed. 2. It writes one TLC config per run, with those facts as constants. A guard that is not in the code, in the expected place and order, reads FALSE, and the model then runs without it. -3. It runs TLC 75 times and prints one line per run. +3. It runs TLC 79 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. @@ -98,6 +98,8 @@ At the sync commit, the expected results are: | `mutant-HostChecksCreateFailed` | pass | Redundant off Windows: the SIGTERM of a `create` that gave up stops the host. | | `current-win32`, the code as it is on Windows, without a token and with a SIGTERM that ends the host at once, R1 to R14 and R17 to R19 | pass | `Win32`: `create` sends the SIGTERM only when the manifest names the program, and that SIGTERM is a host crash. | | `mutant-HostChecksCreateFailed-win32` | violated | R17: without the marker, a host that the manifest does not name yet keeps serving after `create` gave up. | +| `mutant-HostPollsCreateFailed` | pass | Redundant off Windows: the SIGTERM of a `create` that gave up stops the host without a manifest read. | +| `mutant-HostPollsCreateFailed-win32` | violated | R17: without the watch, a host that checked for the marker before `create` wrote it keeps serving when `create` cannot read the manifest. | 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`. @@ -389,6 +391,12 @@ On Windows, SIGTERM ends the host at once, so the host cannot stop its program. Now the catch of the readiness wait first writes an empty marker, `/create-failed`, with `writeCreateFailedMarker`, and only then reads the manifest for the platform rule. `runHost` checks for the marker right before its SIGTERM check, before the spawn, and returns without a program when it finds it. It checks again right after its start-up write lands, before it listens, and then calls `initiateShutdown`, which stops the program and records `destroyed`. The host's write comes before its check, and `create`'s marker write comes before its read, so either the host finds the marker or `create` reads the program's pid and sends the SIGTERM. `create` writes the marker on every platform, and off Windows the SIGTERM also stops the host, so `mutant-HostChecksCreateFailed` passes and only `mutant-HostChecksCreateFailed-win32` breaks R17. In the model, `CreateGivesUp` writes the marker, and with `Win32` `CreateStopsHostOnWindows` reads the manifest and ends a named host as a crash. `HostOpensLogAndSpawns` and `HostChecksMarker` are the two checks. The integration test `a create that gives up on Windows, where SIGTERM ends the host at once` runs the Windows path on Linux: a preload makes `create` read `win32` and turns its SIGTERM into a SIGKILL. +### `HostPollsCreateFailed`: on Windows, a host serves a failed create when create cannot read the manifest (R17) + +The order of the marker write and the manifest read closes the race only while that read works. When the host's start-up write and its marker check came before `create` gave up, the host listens without the marker, and `create` reads the manifest to send the SIGTERM. When that read fails, for example on an unreadable file, `create` on Windows takes the manifest as naming no program and sends nothing, and the host serves the failed session. + +Now `runHost` starts `watchCreateFailed` right after its start-up check. Every 100 ms it checks whether its creator still runs and then whether the marker exists. On the marker it calls `startShutdown`, as for a SIGTERM. Once a check after the creator's exit found no marker, it stops: `create` writes the marker before it exits, so no marker comes later. In the model, `CreateStopsHostOnWindows` reads the manifest or fails to read it, and `HostPollsMarker` is the watch from `"sockdir"` on. `mutant-HostPollsCreateFailed-win32` breaks R17, and `mutant-HostPollsCreateFailed` passes, because off Windows the SIGTERM does not need the read. The integration test `a create on Windows whose manifest read fails after it gave up` holds the host's socket-directory `mkdir` until `create` has exited and makes `create`'s manifest reads fail once the marker exists. + ### `FallbackNeedsFolder`: a childPid that gc's removal left stale gets the kill (R15) The model found this race. Without a token, `readProgramGroup` falls back to the childPid of the manifest copy that the caller read before it, as before `program.json` existed. When gc removed the session folder between that read and the `program.json` read, the record read missing too, and the kill used a childPid whose group could have ended and whose id could name an unrelated group by then. @@ -541,7 +549,7 @@ It assumes: - A killed process stays a zombie until its parent, or init once its parent has died, reaps it, and `kill(-pgid, 0)` still finds a zombie. On Linux, `isProcessGroupAlive` then reads `/proc//stat` of every process and reads the group gone when two scans in a row each show processes of it and only zombies, because a process can fork and end while one scan runs. When a scan shows no process of the group, the probe decides: EPERM reads alive and a found group reads gone. So a group whose last processes are never reaped, as under a container's PID 1 without an init, reads gone. A process whose main thread called `pthread_exit` while another thread runs also shows Z there, so `readProcStat` reads `/proc//task` of every process that shows Z and gives it the state of a thread that is not a zombie. Such a process counts as live in the scan and in the token check, where it can carry the token. On macOS it does not scan, so a zombie still reads alive until launchd reaps it. The model has no zombies: a killed process ends at once. A process that `/proc` refuses to show, as `hidepid=1` (EPERM) or a security module (EACCES) does for other users, reads alive. With `hidepid=2` or `hidepid=4` (`invisible` and `ptraceable` on newer kernels), `/proc` can leave such a process out of its listing, so the probe reads the last `/proc` line of `/proc/self/mountinfo`, skips the scan and reads a group with a zombie alive, as on macOS. With a token, neither a zombie nor a process that `/proc` refuses to show witnesses the token. When no live member is in view, `isProgramGroupAlive` reads the group as `isProcessGroupAlive` does, with the zombie scan, the refused reads and the same `hidepid` check. So under any of those `hidepid` modes, a group that a process of another user took after the program's group ended reads alive, and `destroy` ends with `HOST_TIMEOUT` until that process ends. - A destroy that lands between reconcile's last read and its write is still overwritten with failed, for the time until that reconcile finds the destroy marker and writes destroyed again (`ReconcileRepairsDestroyed`). A `list` or `gc` that reads in that time sees `failed`, a terminal status, so gc can remove the folder as it would remove a destroyed one. A reconcile whose process dies in that time leaves `failed` until the next reconcile reads it: that read finds the marker and writes destroyed (`ReconcileRepairsMarked`). `home list` and the dashboard count a session with the marker as destroyed, also in that time. The model kills the `list` process in that time (`ListDiesBeforeRepair`), so it checks that the repair at the read heals the death. A `gc` that dies there leaves the same record, and the model leaves it out. - The idle time-out calls the same `hangUpProgram` as `initiateShutdown`: SIGHUP, then the group kill after `SHUTDOWN_KILL_GRACE_MS`. When the program exits on that SIGHUP, `handlePtyExit` kills the group too, so a process that ignores SIGHUP does not outlive the idle time-out. An idle time-out still ends exited. When the check cannot run (`unknown`), the idle kill sends nothing, and the session ends exited with that process running, as after a program that exits on its own and leaves a process (coder/agent-tty#222). The model leaves both group kills out: they go through `stopProgramGroup` like every kill, and a process that outlives them is one that the program left, which the model keeps after a normal exit anyway. -- Windows has no process groups, so there `processGroupTarget` gives the program's pid, and every kill reaches only that process. `destroy` never re-runs on Windows. There SIGTERM ends the host at once, so a `create` that gives up sends it only once the manifest names the program, and the next reconcile records `failed` and ends the program. Before that write, the host finds the create-failed marker (`HostChecksCreateFailed`). `current-win32` checks this with a SIGTERM that is a host crash and without a token, and keeps the process groups of Linux. A marker write that fails, for example on a full disk, leaves a host that the manifest does not name yet serving on Windows. The model has no such failure. +- Windows has no process groups, so there `processGroupTarget` gives the program's pid, and every kill reaches only that process. `destroy` never re-runs on Windows. There SIGTERM ends the host at once, so a `create` that gives up sends it only once the manifest names the program, and the next reconcile records `failed` and ends the program. Before that write, the host finds the create-failed marker (`HostChecksCreateFailed`), and after it the host's watch finds it when `create`'s manifest read fails (`HostPollsCreateFailed`). `current-win32` checks this with a SIGTERM that is a host crash and without a token, and keeps the process groups of Linux. A marker write that fails, for example on a full disk, leaves a host that the manifest does not name yet serving on Windows. The model has no such failure. - A host stopped with SIGSTOP, or with a blocked event loop, takes the SIGTERM of a `create` that gave up only when it runs again. Until then its program runs and the session reads `running`, which R17 allows because the SIGTERM is still on its way. A plain `destroy` fails because the host does not answer, and only `destroy --force` ends such a session sooner. - A destroy that the program runs, or that someone types into the program's interactive shell, runs inside the program's session, and `rerunInNewSession` runs it again in a new session. The model lets such a destroy start while the program's leader runs, and assumes that it kept `AGENT_TTY_SESSION_ID`, which every process of the program inherits at spawn. A destroy whose environment lost the variable, or whose `create --env` overrode it, is seen through the id comparison only. On Linux that compares the CLI's session id with `childPid`, so it misses such a destroy only before the host's start-up write. Other POSIX systems compare the process group and the controlling terminal, through `/bin/ps`. A terminal is the controlling terminal of one session and of every process in it, so that also finds a job of an interactive shell, which runs in a group of its own. A process without a controlling terminal is seen only through the group. - The program's processes stay in its process group. A process that leaves the group (`setsid`, or the job control of an interactive shell) is out of reach of the group kill, and it is no witness for the token either. That is case 4 of coder/agent-tty#203, a documented limit with no code change. diff --git a/docs/USAGE.md b/docs/USAGE.md index bee6eb1c..209d06f4 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -326,7 +326,7 @@ A `list`, `inspect` or `gc` that reads the session between those two writes sees If `destroy` fails after it wrote the file, for example because its manifest write fails, the file stays, and the next reconcile records the session as `destroyed`, also when the session had already ended. Nothing deletes the file before `gc` removes the session folder, because a reconcile that read before the destroy can still write after it. A host that died after it recorded the session as ended leaves its socket. `gc`, and a `destroy` of a `destroyed` session, remove that socket when the manifest names no host pid or the host check below reads the host as ended. When `create` cannot reach its new host, it fails and tells the host to stop. It fails with `HOST_UNREACHABLE` (exit 6) after about 6 s when nothing listens on the socket, and with `HOST_TIMEOUT` (exit 5) after about 10 s when the host accepts the connection but does not answer. -`create` also tells the host to stop when it fails for another reason after it wrote the session's first manifest, for example when it cannot read that manifest again. Each such error names the session in `details.sessionId`. +`create` also tells the host to stop when it fails for another reason after it wrote the session's first manifest, for example when it cannot read that manifest again. Each such error names the session in `details.sessionId`, and in text mode `create` prints `Session failed to start.` before the error line. When that first manifest write fails, `create` removes the session folder. The host waits for the manifest only while `create` runs, so it then exits without starting the program. On Linux and macOS it sends the host SIGTERM, and the host stops the program the way `destroy` does and records the session as `destroyed` once the program's group has ended, also while its start-up is still slow. `create` exits before the host has ended the session, so a caller that checks at once can still read `running` or `destroying`. @@ -337,7 +337,7 @@ When the host cannot end the program's group, for example a process of another u A host stopped with SIGSTOP, or with a blocked event loop, handles the SIGTERM only when it runs again. Until then the program runs and the session reads `running`. A plain `destroy` fails because the host does not answer, and only `destroy --force` ends the session sooner. On Windows, SIGTERM ends the host at once, so the host cannot stop the program itself. There `create` sends it only once the manifest names the program: the session then reads `running` with a dead host until the next reconcile records it `failed` and ends the program. Before the host's start-up write, `create` sends nothing. For that case, on every platform, `create` first writes an empty internal file, `create-failed`, in the session folder, and then reads the manifest. The host checks for that file before it starts the program, and returns then, so no program runs and the next reconcile records the session `failed`. It checks again right after its start-up write, and then ends the session the way a SIGTERM does on Linux: it stops the program and records `destroyed`. -On Windows, a host whose start-up write lands before `create` reads the manifest is named by that read and gets the SIGTERM, and a host whose write lands after it finds the file. When the file write fails, for example on a full disk, a Windows host that starts late can still serve the session. This path is not tested on a real Windows host. +On Windows, a host whose start-up write lands before `create` reads the manifest is named by that read and gets the SIGTERM, and a host whose write lands after it finds the file. After its start-up write, the host also checks for the file every 100 ms while `create` runs, and once after `create` exits, so it ends the session also when `create` cannot read the manifest. When the file write fails, for example on a full disk, a Windows host that starts late can still serve the session. This path is not tested on a real Windows host. On Linux, `destroy` and reconcile never kill a process group that they cannot prove is the session's. When the host starts the program, it records the program's pid, the boot id and the program's autogroup id in an internal file, `program.json`. diff --git a/src/cli/README.md b/src/cli/README.md index c85e9393..73993eeb 100644 --- a/src/cli/README.md +++ b/src/cli/README.md @@ -11,7 +11,7 @@ This directory is the agent-tty command-line front end. `main.ts` is the bin ent - Global options: `--home `, `--timeout-ms `, `--no-color`, `--log-level `, `--profile `, `--renderer `. Each command except `dashboard` (alias `d`) and the hidden `_host` registers its own `--json` option. [main.ts:main] - Commands: `version`, `doctor`, `create [command...]`, `list`, `inspect`, `destroy`, `gc`, `type`, `paste`, `run`, `batch`, `mark`, `send-keys`, `mouse`, `resize`, `signal`, `snapshot`, `screenshot`, `dashboard`, `wait`. Groups: `skills list|get|path`, `home list|forget`, `record diff|export`. A hidden `_host ` command imports `src/host/hostMain.ts` and runs `runHost(sessionId, Number(creatorPid))`. [main.ts:main] - `resolveCommandContext(options, env?, deps?)`, `getCommandContext`, `setCommandContext`, `parseTimeoutMsOption`, `resolveRendererDefault`, `resolveLogLevel`, `clearRendererDefaultProbeCacheForTests`, and the types `GlobalCliOptions` and `CommandContext`. [context.ts:resolveCommandContext] [context.ts:CommandContext] -- `emitSuccess`, `emitSuccessSync`, `emitFailure`, `emitCliError`, `argvHasFlag`, `exitAfterOutputFlush`, `formatSuccessOutput`, `writeJsonEnvelope`, `writeHumanLines`, `writeStdoutSync`, `setColorEnabled`. [output.ts:emitSuccess] [output.ts:emitFailure] [output.ts:writeStdoutSync] [output.ts:argvHasFlag] [output.ts:exitAfterOutputFlush] +- `emitSuccess`, `emitSuccessSync`, `emitFailure`, `emitCliError`, `argvHasFlag`, `exitAfterOutputFlush`, `formatSuccessOutput`, `writeJsonEnvelope`, `writeHumanLines`, `writeHumanErrorLines`, `writeStdoutSync`, `setColorEnabled`. [output.ts:emitSuccess] [output.ts:emitFailure] [output.ts:writeStdoutSync] [output.ts:argvHasFlag] [output.ts:exitAfterOutputFlush] - `resolveCommandTarget(options)` returns a `CommandTarget` (`sessionId`, `sessionDirectory`, `manifestPath`, `socketPath`, `manifest`). Also exports `ResolveCommandTargetOptions` and `CommandTargetManifest`. [commandTarget.ts:resolveCommandTarget] [commandTarget.ts:CommandTarget] - `assertSessionCommandable(manifest, sessionId)` and `checkedSessionDir(home, sessionId)`. [sessionGuards.ts:assertSessionCommandable] [sessionGuards.ts:checkedSessionDir] - `exitCodeForError(code)`. [exitCodes.ts:exitCodeForError] diff --git a/src/cli/commands/README.md b/src/cli/commands/README.md index 5c5a62b6..f52bd695 100644 --- a/src/cli/commands/README.md +++ b/src/cli/commands/README.md @@ -44,7 +44,7 @@ This directory holds one handler module per agent-tty CLI command. `src/cli/main ## Side Effects - Session commands send RPCs over the session socket through `sendRpc`. The method names are `run`, `type`, `paste`, `sendKeys`, `mouse`, `mark`, `resize`, `signal`, `snapshot`, `screenshot`, `wait`, `waitForRender` and `inspect`. `create` also sends `inspect` while it polls. [run.ts:runRunCommand] [send-keys.ts:runSendKeysCommand] [wait.ts:runWaitCommand] [create.ts:runCreateCommand] -- `create` calls `allocateSession` (`src/host/lifecycle.ts`) with a `launch` callback that records the session ID and starts the host process through `launchHost`. If `launchHost` or a later step of `allocateSession` throws, `create` removes the session directory with `fs.rm`. A bad `cwd`, shell path or command segment fails before `allocateSession` creates the directory, so no session directory is left behind. A failure between `mkdir` and the callback, such as a failed `chmod`, leaves the empty session directory in place. Any failure after `allocateSession` returned, a failed readiness poll included, writes the empty `create-failed` marker with `writeCreateFailedMarker`, logs a failed marker write at debug level, then calls the host's `stop()` (on Windows only once the manifest names the program) and leaves the session directory in place. `create` rethrows the error with `details.sessionId` added, and an error that is not a `CliError` becomes `INTERNAL_ERROR`. It registers the Home through `upsertHome`. [create.ts:runCreateCommand] +- `create` calls `allocateSession` (`src/host/lifecycle.ts`) with a `launch` callback that records the session ID and starts the host process through `launchHost`. If `launchHost` or a later step of `allocateSession` throws, `create` removes the session directory with `fs.rm`. A bad `cwd`, shell path or command segment fails before `allocateSession` creates the directory, so no session directory is left behind. A failure between `mkdir` and the callback, such as a failed `chmod`, leaves the empty session directory in place. Any failure after `allocateSession` returned, a failed readiness poll included, writes the empty `create-failed` marker with `writeCreateFailedMarker`, logs a failed marker write at debug level, then calls the host's `stop()` (on Windows only once the manifest names the program) and leaves the session directory in place. `create` rethrows the error with `details.sessionId` added, and an error that is not a `CliError` becomes `INTERNAL_ERROR`. In text mode it first writes `Session failed to start.` to stderr with `writeHumanErrorLines`. 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, and for an ended session other than destroyed whose folder holds the destroy marker. When that repair throws, it shows the manifest as it reads. [inspect.ts:runInspectCommand] - `destroy` and `list` call `destroySession` and `listSessions` from `src/host/lifecycle.ts`. [destroy.ts:runDestroyCommand] [list.ts:runListCommand] diff --git a/src/host/README.md b/src/host/README.md index ba385416..0dad5bdb 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -80,7 +80,7 @@ - `runHost` spawns the PTY with `createPty` (`src/pty/createPty.ts`), writes input to it, resizes it and kills it on idle timeout and shutdown. It writes `TerminalQueryResponder` replies to the PTY without logging them. [hostMain.ts:runHost] - `runHost` polls `session.json` with `readManifestIfExists` and probes the creator process with `isProcessAlive` until the manifest appears or the creator exits. It writes `session.json` through `createSerialManifestWriter`, creates the socket directory with mode `0o700` and listens with `RpcServer` through `listenInSocketDirectory` and writes snapshot and screenshot artifacts through `src/snapshot/capture.ts` and `src/screenshot/capture.ts`. [hostMain.ts:runHost] - `runHost` registers a `process.on('SIGTERM')` handler that starts shutdown, sends signals to the child with `process.kill` and starts `setInterval` timers for idle and wait polling. [hostMain.ts:runHost] -- `runHost` checks for the `create-failed` marker with `existsSync` before it spawns the program, and returns when it finds it. It checks again right after its start-up manifest write, before it listens, and then shuts down. [hostMain.ts:runHost] +- `runHost` checks for the `create-failed` marker with `existsSync` before it spawns the program, and returns when it finds it. It checks again right after its start-up manifest write, before it listens, and then shuts down. From there on, `watchCreateFailed` checks for the marker every `CREATE_FAILED_POLL_INTERVAL_MS` (100 ms) while the creator process lives and once after it exited, and starts the shutdown when it finds the marker. [hostMain.ts:runHost] - `runHost` rethrows a PTY-ingestion, event-log append, exit-handling or shutdown error in `process.nextTick`. The uncaught exception crashes the host process. [hostMain.ts:rethrowAsync] - `resolveHostRendererName` reads `process.env.AGENT_TTY_HOST_RENDERER` and `process.env.AGENT_TTY_RENDERER`. [hostMain.ts:resolveHostRendererName] - `EventLog.open` opens the file in append mode and runs `chmod 0o600`. `append` writes with `fileHandle.appendFile`, one call at a time. `close` calls `fileHandle.sync()` and then closes the file. [eventLog.ts:EventLog] From fb460b5b5b64e071cebf97047b3b225f96cf8fc8 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 03:18:41 +0000 Subject: [PATCH 09/28] test: cover the host's marker watch in the test process A marker that appears while the creator runs stops a serving host. One that appears after the creator has exited does not: the watch has stopped. Each case fails without the code that it covers. --- test/unit/host/hostMarker.test.ts | 68 +++++++++++++++++++++++++++---- 1 file changed, 60 insertions(+), 8 deletions(-) diff --git a/test/unit/host/hostMarker.test.ts b/test/unit/host/hostMarker.test.ts index 43a90b74..2169ea6c 100644 --- a/test/unit/host/hostMarker.test.ts +++ b/test/unit/host/hostMarker.test.ts @@ -1,3 +1,5 @@ +import { spawn } from 'node:child_process'; +import { once } from 'node:events'; import { existsSync, readFileSync, writeFileSync } from 'node:fs'; import { mkdir, mkdtemp, rm } from 'node:fs/promises'; import { tmpdir } from 'node:os'; @@ -55,6 +57,22 @@ function readProgramGroup(): number { return pid; } +// The host records destroyed, its program's group is gone and its socket is +// removed. +async function expectHostStopped(group: number): Promise { + const deadline = Date.now() + 10_000; + let manifest = await readManifest(manifestPath(directory)); + while ( + manifest.status !== 'destroyed' || + isGroupAlive(group) || + existsSync(socketPath(directory)) + ) { + expect(Date.now()).toBeLessThan(deadline); + await delay(50); + manifest = await readManifest(manifestPath(directory)); + } +} + beforeEach(async () => { home = await mkdtemp(join(tmpdir(), 'agent-tty-host-marker-')); vi.stubEnv('AGENT_TTY_HOME', home); @@ -117,13 +135,47 @@ describe('runHost and the create-failed marker', () => { await runHost(SESSION_ID, process.pid); expect(existsSync(socketPath(directory))).toBe(false); - const group = readProgramGroup(); - const deadline = Date.now() + 10_000; - let manifest = await readManifest(manifestPath(directory)); - while (manifest.status !== 'destroyed' || isGroupAlive(group)) { - expect(Date.now()).toBeLessThan(deadline); - await delay(50); - manifest = await readManifest(manifestPath(directory)); - } + await expectHostStopped(readProgramGroup()); + }); + + it('stops a serving host when the marker appears while its creator runs', async () => { + await runHost(SESSION_ID, process.pid); + expect(existsSync(socketPath(directory))).toBe(true); + + await writeCreateFailedMarker( + createFailedMarkerPath(directory), + SESSION_ID, + ); + + await expectHostStopped(readProgramGroup()); }); + + it('keeps serving when the marker appears after its creator has exited', async () => { + const creator = spawn('sleep', ['30'], { stdio: 'ignore' }); + expect(creator.pid).toBeGreaterThan(0); + await runHost(SESSION_ID, creator.pid as number); + expect(existsSync(socketPath(directory))).toBe(true); + creator.kill('SIGKILL'); + await once(creator, 'exit'); + // Two polls see the creator gone and stop the watch. + await delay(300); + + await writeCreateFailedMarker( + createFailedMarkerPath(directory), + SESSION_ID, + ); + await delay(500); + + expect((await readManifest(manifestPath(directory))).status).toBe( + 'running', + ); + expect(existsSync(socketPath(directory))).toBe(true); + // Stop the host as a SIGTERM would. + for (const listener of process.rawListeners('SIGTERM')) { + if (!sigtermListeners.has(listener)) { + (listener as () => void)(); + } + } + await expectHostStopped(readProgramGroup()); + }, 15_000); }); From 6d2c217a2653f75984d90f5ce07236d61958e030 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 04:44:57 +0000 Subject: [PATCH 10/28] test: on Windows, a create whose marker write fails leaves a late host serving The new give-up case fails its first marker write with EIO. create then sees no program in the manifest, sends nothing, and the host that starts late finds no marker and serves. The unit cases ask create to retry the write, to stop the host once the manifest names the program, and to stop retrying after 50 writes or once the host has exited. --- test/fixtures/fail-first-marker-write.ts | 28 ++++++++ test/integration/lifecycle.test.ts | 9 +++ test/unit/commands/create.test.ts | 84 ++++++++++++++++++++++++ 3 files changed, 121 insertions(+) create mode 100644 test/fixtures/fail-first-marker-write.ts diff --git a/test/fixtures/fail-first-marker-write.ts b/test/fixtures/fail-first-marker-write.ts new file mode 100644 index 00000000..988b31c6 --- /dev/null +++ b/test/fixtures/fail-first-marker-write.ts @@ -0,0 +1,28 @@ +// Preload (`--import`) for a `create` process: the first write of the +// create-failed marker's temp file fails with EIO, as a write that an +// antivirus lock blocks once does. The host inherits NODE_OPTIONS and skips +// this. +import fsp from 'node:fs/promises'; +import { syncBuiltinESMExports } from 'node:module'; +import { basename } from 'node:path'; +import process from 'node:process'; + +if (process.argv.includes('create') && !process.argv.includes('_host')) { + const writeFile = fsp.writeFile as (...args: unknown[]) => Promise; + let failed = false; + fsp.writeFile = ((path: unknown, ...rest: unknown[]) => { + const file = path instanceof URL ? path.pathname : String(path); + if (!failed && basename(file).startsWith('create-failed.tmp-')) { + failed = true; + return Promise.reject( + Object.assign(new Error(`EIO: i/o error, open '${file}'`), { + code: 'EIO', + syscall: 'open', + path: file, + }), + ); + } + return writeFile(path, ...rest); + }) as typeof fsp.writeFile; + syncBuiltinESMExports(); +} diff --git a/test/integration/lifecycle.test.ts b/test/integration/lifecycle.test.ts index d85fff24..33e39b4f 100644 --- a/test/integration/lifecycle.test.ts +++ b/test/integration/lifecycle.test.ts @@ -1725,6 +1725,15 @@ describe('lifecycle integration', { timeout: 60_000 }, () => { `--import=${pathToFileURL(resolve('test/fixtures/fake-win32-create.ts')).href}`, ], ], + // create retries the marker write while the manifest names no program. + [ + 'on Windows, when its first marker write fails', + [ + `--import=${pathToFileURL(resolve('test/fixtures/denied-autogroup.ts')).href}`, + `--import=${pathToFileURL(resolve('test/fixtures/fake-win32-create.ts')).href}`, + `--import=${pathToFileURL(resolve('test/fixtures/fail-first-marker-write.ts')).href}`, + ], + ], ])('a create that gives up %s', (_name, preloads) => { let pgid = 0; diff --git a/test/unit/commands/create.test.ts b/test/unit/commands/create.test.ts index f718fd46..2694db70 100644 --- a/test/unit/commands/create.test.ts +++ b/test/unit/commands/create.test.ts @@ -14,6 +14,7 @@ const mocks = vi.hoisted(() => ({ allocateSession: vi.fn(), ensureSocketRoot: vi.fn(), launchHost: vi.fn(), + isProcessAlive: vi.fn(), stopHost: vi.fn(), sendRpc: vi.fn(), readManifestIfExists: vi.fn(), @@ -32,6 +33,7 @@ vi.mock('../../../src/cli/output.js', () => ({ vi.mock('../../../src/host/lifecycle.js', () => ({ allocateSession: mocks.allocateSession, + isProcessAlive: mocks.isProcessAlive, launchHost: mocks.launchHost, })); @@ -126,6 +128,7 @@ describe('create command', () => { }, ); mocks.launchHost.mockReturnValue({ pid: 12345, stop: mocks.stopHost }); + mocks.isProcessAlive.mockReturnValue(true); mocks.sendRpc.mockResolvedValue({ session: { sessionId: 'session-01' } }); mocks.readManifestIfExists.mockResolvedValue(makeManifest()); mocks.sessionDir.mockImplementation( @@ -522,6 +525,87 @@ describe('create command', () => { expect(mocks.stopHost).toHaveBeenCalledOnce(); }); + describe('on Windows, when the marker write fails while the manifest names no program', () => { + const diskError = makeCliError(ERROR_CODES.STORAGE_WRITE_ERROR, { + message: 'i/o error', + }); + + beforeEach(() => { + const platform = process.platform; + Object.defineProperty(process, 'platform', { value: 'win32' }); + onTestFinished(() => { + Object.defineProperty(process, 'platform', { value: platform }); + }); + mocks.sendRpc.mockRejectedValue( + makeCliError(ERROR_CODES.HOST_UNREACHABLE, { + message: 'host unreachable', + }), + ); + }); + + it('retries the marker write, and reads the manifest after each write', async () => { + mocks.writeCreateFailedMarker + .mockRejectedValueOnce(diskError) + .mockResolvedValue(undefined); + + await expect( + runCreateCommand({ ...baseOptions, context }), + ).rejects.toMatchObject({ + code: 'HOST_UNREACHABLE', + details: { sessionId: 'session-01' }, + }); + + expect(mocks.writeCreateFailedMarker).toHaveBeenCalledTimes(2); + const lastWrite = Math.max( + ...mocks.writeCreateFailedMarker.mock.invocationCallOrder, + ); + const lastRead = Math.max( + ...mocks.readManifestIfExists.mock.invocationCallOrder, + ); + expect(lastWrite).toBeLessThan(lastRead); + expect(mocks.stopHost).not.toHaveBeenCalled(); + }); + + it('stops the host once the manifest names the program', async () => { + mocks.writeCreateFailedMarker.mockRejectedValue(diskError); + mocks.readManifestIfExists + .mockResolvedValueOnce(makeManifest()) + .mockResolvedValueOnce(null) + .mockResolvedValue(makeManifest({ childPid: 4321 })); + + await expect( + runCreateCommand({ ...baseOptions, context }), + ).rejects.toMatchObject({ code: 'HOST_UNREACHABLE' }); + + expect(mocks.writeCreateFailedMarker).toHaveBeenCalledTimes(3); + expect(mocks.stopHost).toHaveBeenCalledOnce(); + }); + + it('gives up after 50 more writes', async () => { + mocks.writeCreateFailedMarker.mockRejectedValue(diskError); + + await expect( + runCreateCommand({ ...baseOptions, context }), + ).rejects.toMatchObject({ code: 'HOST_UNREACHABLE' }); + + expect(mocks.writeCreateFailedMarker).toHaveBeenCalledTimes(51); + expect(mocks.stopHost).not.toHaveBeenCalled(); + }); + + it('stops retrying once the host has exited', async () => { + mocks.writeCreateFailedMarker.mockRejectedValue(diskError); + mocks.isProcessAlive.mockReturnValueOnce(true).mockReturnValue(false); + + await expect( + runCreateCommand({ ...baseOptions, context }), + ).rejects.toMatchObject({ code: 'HOST_UNREACHABLE' }); + + expect(mocks.isProcessAlive).toHaveBeenCalledWith(12345); + expect(mocks.writeCreateFailedMarker).toHaveBeenCalledTimes(2); + expect(mocks.stopHost).not.toHaveBeenCalled(); + }); + }); + it('leaves a host that answers alone', async () => { await runCreateCommand({ ...baseOptions, context }); From e782437cd867552da17c48dab292cdc93c7dac50 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 04:48:08 +0000 Subject: [PATCH 11/28] fix(cli): on Windows, retry a failed marker write until the marker or the program record lands A create that gives up on Windows sends no SIGTERM while the manifest names no program, so only the marker can stop a host that starts late. When the marker write fails, create now writes it again every 100 ms, up to 50 times, and reads the manifest after each write. It stops when the marker lands, stops the host once the manifest names the program, and stops retrying once the host has exited. The unit case for the stop now finds the program by the number of marker writes, because the readiness loop also reads the manifest. --- src/cli/commands/create.ts | 58 +++++++++++++++++++++++-------- test/unit/commands/create.test.ts | 12 ++++--- 2 files changed, 51 insertions(+), 19 deletions(-) diff --git a/src/cli/commands/create.ts b/src/cli/commands/create.ts index f175afbc..34bded83 100644 --- a/src/cli/commands/create.ts +++ b/src/cli/commands/create.ts @@ -8,6 +8,7 @@ import { emitSuccess, writeHumanErrorLines } from '../output.js'; import { DEFAULT_IDLE_TIMEOUT_MS } from '../../config/defaults.js'; import { allocateSession, + isProcessAlive, launchHost, type LaunchedHost, } from '../../host/lifecycle.js'; @@ -31,6 +32,8 @@ import { invariant } from '../../util/assert.js'; const READINESS_POLL_INTERVAL_MS = 100; const READINESS_MAX_ATTEMPTS = 50; const READINESS_RPC_TIMEOUT_MS = 100; +const MARKER_RETRY_INTERVAL_MS = 100; +const MARKER_RETRY_MAX_ATTEMPTS = 50; type SessionEnvironment = Record; @@ -177,6 +180,24 @@ function withSessionId(error: unknown, sessionId: string): CliError { }); } +// A failed write is logged, so the create still reports its own error. +function writeMarkerOrLog( + path: string, + sessionId: string, + logger: CommandContext['logger'], +): Promise { + return writeCreateFailedMarker(path, sessionId).then( + () => true, + (error: unknown) => { + logger.debug('failed to write the create-failed marker', { + sessionId, + error: error instanceof Error ? error.message : String(error), + }); + return false; + }, + ); +} + export async function runCreateCommand(options: CommandOptions): Promise { const environment = normalizeCreateEnvironment(options.envEntries); const idleTimeoutMs = @@ -274,21 +295,28 @@ export async function runCreateCommand(options: CommandOptions): Promise { // for it after its start-up write names the program: either the host // finds the marker, or the manifest read below finds the program. invariant(host !== undefined, 'a session that create polls has a host'); - await writeCreateFailedMarker( - createFailedMarkerPath(sessionDirectory), - sessionId, - ).catch((markerError: unknown) => { - options.context.logger.debug('failed to write the create-failed marker', { - sessionId, - error: - markerError instanceof Error - ? markerError.message - : String(markerError), - }); - }); - const manifest = await readManifestIfExists( - manifestPath(sessionDirectory), - ).catch(() => null); + const markerFile = createFailedMarkerPath(sessionDirectory); + const manifestFile = manifestPath(sessionDirectory); + const logger = options.context.logger; + let marked = await writeMarkerOrLog(markerFile, sessionId, logger); + let manifest = await readManifestIfExists(manifestFile).catch(() => null); + // On Windows a host that the manifest does not name yet sees only the + // marker. So while the marker write fails, create writes it again and + // reads the manifest after each write, until the marker lands, the + // manifest names the program, or the host has exited. + for ( + let attempt = 1; + process.platform === 'win32' && + !marked && + manifest?.childPid == null && + attempt <= MARKER_RETRY_MAX_ATTEMPTS && + isProcessAlive(host.pid); + attempt += 1 + ) { + await delay(MARKER_RETRY_INTERVAL_MS); + marked = await writeMarkerOrLog(markerFile, sessionId, logger); + manifest = await readManifestIfExists(manifestFile).catch(() => null); + } if (process.platform !== 'win32' || manifest?.childPid != null) { host.stop(); } diff --git a/test/unit/commands/create.test.ts b/test/unit/commands/create.test.ts index 2694db70..7568eb45 100644 --- a/test/unit/commands/create.test.ts +++ b/test/unit/commands/create.test.ts @@ -568,10 +568,14 @@ describe('create command', () => { it('stops the host once the manifest names the program', async () => { mocks.writeCreateFailedMarker.mockRejectedValue(diskError); - mocks.readManifestIfExists - .mockResolvedValueOnce(makeManifest()) - .mockResolvedValueOnce(null) - .mockResolvedValue(makeManifest({ childPid: 4321 })); + // The read after the third write finds the program. + mocks.readManifestIfExists.mockImplementation(() => + Promise.resolve( + mocks.writeCreateFailedMarker.mock.calls.length >= 3 + ? makeManifest({ childPid: 4321 }) + : makeManifest(), + ), + ); await expect( runCreateCommand({ ...baseOptions, context }), From 5825ae1bf50c1714cdb377b7e99f4ae3ce38afd1 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 04:55:11 +0000 Subject: [PATCH 12/28] fix(skills): model the marker retries of a create on Windows On Windows the marker write in CreateGivesUp can now fail. With the new guard CreateRetriesMarker, which facts.mjs reads from the give-up catch, CreateStopsHostOnWindows goes on to "retry", and CreateRewritesMarker writes and reads again until the marker lands, the read names the program, or the host is gone. A create whose last write failed ends as "exhausted", which R17 does not cover. New runs: the win32 mutant breaks R17, and a win32 witness reaches the retry. Docs: SKILL.md, USAGE and the commands README. --- .../skills/verify-session-lifecycle/SKILL.md | 58 ++++++++------ .../model/SessionLifecycle.tla | 76 +++++++++++++++---- .../verify-session-lifecycle/scripts/check.sh | 4 +- .../scripts/facts.mjs | 54 ++++++++++--- docs/USAGE.md | 2 +- src/cli/commands/README.md | 2 +- 6 files changed, 144 insertions(+), 52 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index a81ff814..c410fc3f 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -13,26 +13,26 @@ The tool is TLC, the TLA+ model checker, pinned to release 1.7.4 by sha256. The ## The rules -| Rule | What must hold | Harm when it breaks | -| ------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | -| R1 `NoLiveSessionDeleted` | gc never removes the folder of a session whose host can still write to it. | A running or starting session loses its manifest and event log. | -| R2 `HostDeathOnlyWhenDead` | The manifest says "failed, host died" only when the host process is dead. | `list` and `inspect` show a live session as failed. Commands refuse it. | -| R3 `TerminalIsFinal` | Once the manifest shows exited, failed or destroyed, it never shows running again. | A finished session looks running, and the next reconcile marks it failed. | -| R4 `RecordedExitKept` | Once the manifest records that the program exited, only `destroy` changes it, to destroyed, and keeps the exit code. | A program that exited 0 is reported as failed, with its exit code lost. | -| R5 `RunningSessionReachable` | While the host serves a running program, the socket file exists. | The session runs, but no command can reach it. | -| R6 `HostStartsWhenCreated` | A host never fails to start because another process removed or rewrote its files. | `create` fails with `HOST_UNREACHABLE` for a session nobody touched. | -| R7 `TerminalIsLastWrite` | Once the manifest shows exited, failed or destroyed, the host has no write left to make. | gc removes the folder while the host still writes to it, and the host's write then fails. | -| R8 `DestroyedOnlyWhenEnded` | While the host lives, the manifest says destroyed only after the host saw the program end. | `list` hides a program that still runs, and gc removes its folder. | -| R9 `DestroyEndsDestroyed` | `destroy` reports success only after it wrote destroyed or read it. | `destroy` says `destroyed: true`, but the session reads failed, "host process died unexpectedly", until a second `destroy`. | -| R10 `RemovedFolderStaysRemoved` | Once gc removed the session folder, no write brings it back. | A late write creates the folder again with only `session.json`. `list --all` shows that stub session until the next gc removes it. | -| R11 `DestroyedProgramStopped` | When the manifest says destroyed, no process of the program's process group runs, unless the program exited on its own first or no manifest named its pid. | A process of the session keeps running, `list` hides it, and nothing stops it later. | -| R13 `LiveGroupStaysNamed` | While a process of the program's process group runs, a manifest that named the program still names it. | The session reads failed or destroyed without `childPid`, so no later `destroy` or reconcile can stop the process that still runs. | -| R14 `DestroyOutlivesProgram` | `destroy` is never killed before it reports, also when it runs inside the program's session. | `destroy` prints nothing. With `--force` it kills its own group, and the session reads exited, not destroyed. | -| R15 `NoUnrelatedGroupKilled` | No kill reaches a process group that took the program's group id after the program's group ended. | `destroy`, `destroy --force`, a reconcile or the host's shutdown sends SIGKILL to an unrelated group, such as the program of another session. | -| R16 `DestroyedSessionStopped` | When the manifest says destroyed, no process of the program's group runs, also none that the program left when it exited on its own, unless the host died before `program.json` named the program. | `destroy` reports `destroyed: true` while a process of the session runs, `list` hides it, and nothing stops it later. | -| R17 `FailedCreateStopped` | Once `create` gave up on its host, the host keeps the session `running` only while `create`'s SIGTERM is on its way to it, or while the host has yet to check for the create-failed marker. | `create` fails with `HOST_UNREACHABLE`, but the session runs, and `list --all` shows it running. | -| R18 `DestroyedStaysDestroyed` | Once `destroy` reported success, the manifest says destroyed while the session folder exists, except while a reconcile that wrote over it has yet to write destroyed again, or, after that reconcile died, until the next reconcile reads the manifest. | `destroy` reports `destroyed: true`, and the session then reads `failed`. | -| R19 `NoUnrelatedHostKilled` | No kill of `destroy --force` reaches a process that took the host's pid after the host ended. | `destroy --force` sends SIGKILL to an unrelated process that got the crashed host's pid. | +| Rule | What must hold | Harm when it breaks | +| ------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------- | +| R1 `NoLiveSessionDeleted` | gc never removes the folder of a session whose host can still write to it. | A running or starting session loses its manifest and event log. | +| R2 `HostDeathOnlyWhenDead` | The manifest says "failed, host died" only when the host process is dead. | `list` and `inspect` show a live session as failed. Commands refuse it. | +| R3 `TerminalIsFinal` | Once the manifest shows exited, failed or destroyed, it never shows running again. | A finished session looks running, and the next reconcile marks it failed. | +| R4 `RecordedExitKept` | Once the manifest records that the program exited, only `destroy` changes it, to destroyed, and keeps the exit code. | A program that exited 0 is reported as failed, with its exit code lost. | +| R5 `RunningSessionReachable` | While the host serves a running program, the socket file exists. | The session runs, but no command can reach it. | +| R6 `HostStartsWhenCreated` | A host never fails to start because another process removed or rewrote its files. | `create` fails with `HOST_UNREACHABLE` for a session nobody touched. | +| R7 `TerminalIsLastWrite` | Once the manifest shows exited, failed or destroyed, the host has no write left to make. | gc removes the folder while the host still writes to it, and the host's write then fails. | +| R8 `DestroyedOnlyWhenEnded` | While the host lives, the manifest says destroyed only after the host saw the program end. | `list` hides a program that still runs, and gc removes its folder. | +| R9 `DestroyEndsDestroyed` | `destroy` reports success only after it wrote destroyed or read it. | `destroy` says `destroyed: true`, but the session reads failed, "host process died unexpectedly", until a second `destroy`. | +| R10 `RemovedFolderStaysRemoved` | Once gc removed the session folder, no write brings it back. | A late write creates the folder again with only `session.json`. `list --all` shows that stub session until the next gc removes it. | +| R11 `DestroyedProgramStopped` | When the manifest says destroyed, no process of the program's process group runs, unless the program exited on its own first or no manifest named its pid. | A process of the session keeps running, `list` hides it, and nothing stops it later. | +| R13 `LiveGroupStaysNamed` | While a process of the program's process group runs, a manifest that named the program still names it. | The session reads failed or destroyed without `childPid`, so no later `destroy` or reconcile can stop the process that still runs. | +| R14 `DestroyOutlivesProgram` | `destroy` is never killed before it reports, also when it runs inside the program's session. | `destroy` prints nothing. With `--force` it kills its own group, and the session reads exited, not destroyed. | +| R15 `NoUnrelatedGroupKilled` | No kill reaches a process group that took the program's group id after the program's group ended. | `destroy`, `destroy --force`, a reconcile or the host's shutdown sends SIGKILL to an unrelated group, such as the program of another session. | +| R16 `DestroyedSessionStopped` | When the manifest says destroyed, no process of the program's group runs, also none that the program left when it exited on its own, unless the host died before `program.json` named the program. | `destroy` reports `destroyed: true` while a process of the session runs, `list` hides it, and nothing stops it later. | +| R17 `FailedCreateStopped` | Once `create` gave up on its host, the host keeps the session `running` only while `create`'s SIGTERM is on its way to it, or while the host has yet to check for the create-failed marker. A `create` on Windows whose marker writes all failed is outside R17 (see Scope). | `create` fails with `HOST_UNREACHABLE`, but the session runs, and `list --all` shows it running. | +| R18 `DestroyedStaysDestroyed` | Once `destroy` reported success, the manifest says destroyed while the session folder exists, except while a reconcile that wrote over it has yet to write destroyed again, or, after that reconcile died, until the next reconcile reads the manifest. | `destroy` reports `destroyed: true`, and the session then reads `failed`. | +| R19 `NoUnrelatedHostKilled` | No kill of `destroy --force` reaches a process that took the host's pid after the host ended. | `destroy --force` sends SIGKILL to an unrelated process that got the crashed host's pid. | `TypeOK` also runs in every run. When it breaks, the model is wrong, not the code. @@ -44,7 +44,7 @@ Yes, when the diff changes any of these: - `src/host/programGroup.ts`: the token capture (`captureProgram`, `captureToken`, `readAutogroup`, `parseAutogroup`, `parseProcStat`), the `/proc` reads (`readProcFileIfExists`, `readLiveThreadState`, `readProcStat`, `readShownProcStat`, `isRefusedRead`, `readBootId`), the record (`writeProgramRecord`, `readProgramRecord`, `readProvenProgramGroup`, `readProgramGroup`), `procShowsOwnPidSpace`, the verdict (`judgeProgramGroup`, `readGroupMembers`), and the kill and the probe (`stopProgramGroup`, `isProgramGroupAlive`, `processGroupTarget`, `isProcessGroupAlive` with `groupHasLiveProcess` and `procHidesOtherUsers`, `killProcessGroupBestEffort`, `signalProcessGroup`). - `src/host/hostMain.ts`: `waitForManifestFromCreate`, `isSessionCommandable`, and in `runHost` the start-up statements (the manifest wait, the `hostPid === process.pid` check, the `host.json` write with `captureHost` and `writeHostRecord`, `createSerialManifestWriter`, `EventLog.open`, the create-failed marker check, `createPty`, `setChildPid`, `captureProgram`, `watchCreateFailed`), `hangUpProgram` with its kill timer and the `SHUTDOWN_KILL_GRACE_MS` constant, `startIdlePolling` (the idle time-out), `initiateShutdown`, `startShutdown`, `handlePtyExit` with its wait for the program's group, `pty.onExit`, the `SIGTERM` handler, the `resize` and `destroy` handlers, and the last `try` block (the `program.json` write, the start-up manifest write and `rpcServer.listen`). - `src/host/manifestWriter.ts` `createSerialManifestWriter`. -- `src/cli/commands/gc.ts` `gcSessions`, `src/cli/commands/create.ts` `runCreateCommand` with `waitForReadyHost`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`. +- `src/cli/commands/gc.ts` `gcSessions`, `src/cli/commands/create.ts` `runCreateCommand` with `waitForReadyHost` and `writeMarkerOrLog`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`. - `src/host/sessionState.ts` `setDimensions`, `requestDestroy`, `recordDestroyed` and `recordExit`, `src/host/eventLog.ts` `EventLog.open`, `src/host/rpcServer.ts` `listen` and `close`, `src/host/rpcClient.ts` `toTransportCliError` (which socket errors read as `HOST_UNREACHABLE`). - `src/host/hostRecord.ts`: `captureHost`, `writeHostRecord`, `readHostRecord`, `pidExists`, `judgeHost`, `inPidNamespace`, `readTimeNamespace`, `inTimeNamespace`, `readMachineId`, `inHostPidSpace` and `sharesHostPids`. - `src/storage/manifests.ts` `readValidatedJsonFile`, `replaceFileAtomic`, `replaceFileAtomicSync`, `writeValidatedJsonFileSync`, `writeManifest`, `writeDestroyMarker` and `writeCreateFailedMarker` with `writeEmptyMarker`. @@ -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. Ten runs explore more than 20 million distinct states each, so `CHECK_JOBS=79` starts every run at once and takes about as long as the longest run. `JAVA=/path/to/java` picks another Java. `TLA2TOOLS_JAR=/path/to/tla2tools.jar` uses a jar you already have, which must be the same 1.7.4 build. `CHECK_OUT=` keeps the results in that folder (default: a new temp folder, printed at the end). +It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. On this repo it takes about eleven minutes with the default `CHECK_JOBS` of 4. Ten runs explore more than 20 million distinct states each, so `CHECK_JOBS=81` starts every run at once and takes about as long as the longest run. `JAVA=/path/to/java` picks another Java. `TLA2TOOLS_JAR=/path/to/tla2tools.jar` uses a jar you already have, which must be the same 1.7.4 build. `CHECK_OUT=` keeps the results in that folder (default: a new temp folder, printed at the end). What it does: -1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the thirty-four guards that the rules depend on and the status sets of the policy table, and it hashes each covered function with comments and layout removed. +1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the thirty-five guards that the rules depend on and the status sets of the policy table, and it hashes each covered function with comments and layout removed. 2. It writes one TLC config per run, with those facts as constants. A guard that is not in the code, in the expected place and order, reads FALSE, and the model then runs without it. -3. It runs TLC 79 times and prints one line per run. +3. It runs TLC 81 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. @@ -100,6 +100,8 @@ At the sync commit, the expected results are: | `mutant-HostChecksCreateFailed-win32` | violated | R17: without the marker, a host that the manifest does not name yet keeps serving after `create` gave up. | | `mutant-HostPollsCreateFailed` | pass | Redundant off Windows: the SIGTERM of a `create` that gave up stops the host without a manifest read. | | `mutant-HostPollsCreateFailed-win32` | violated | R17: without the watch, a host that checked for the marker before `create` wrote it keeps serving when `create` cannot read the manifest. | +| `mutant-CreateRetriesMarker-win32` | violated | R17: without the retries, a marker write that fails once leaves a host that the manifest does not name yet serving after `create` gave up. | +| `witness-WitnessMarkerRetried-win32` | violated | The model reaches a `create` on Windows that writes the marker again. | Read `current` first. The witness and mutant runs use the same facts from the code, so a code change that breaks `current` can also turn them `UNEXPECTED`. @@ -397,6 +399,12 @@ The order of the marker write and the manifest read closes the race only while t Now `runHost` starts `watchCreateFailed` right after its start-up check. Every 100 ms it checks whether its creator still runs and then whether the marker exists. On the marker it calls `startShutdown`, as for a SIGTERM. Once a check after the creator's exit found no marker, it stops: `create` writes the marker before it exits, so no marker comes later. In the model, `CreateStopsHostOnWindows` reads the manifest or fails to read it, and `HostPollsMarker` is the watch from `"sockdir"` on. `mutant-HostPollsCreateFailed-win32` breaks R17, and `mutant-HostPollsCreateFailed` passes, because off Windows the SIGTERM does not need the read. The integration test `a create on Windows whose manifest read fails after it gave up` holds the host's socket-directory `mkdir` until `create` has exited and makes `create`'s manifest reads fail once the marker exists. +### `CreateRetriesMarker`: on Windows, a failed marker write leaves a host serving a failed create (R17) + +The marker closes the race only when its write lands. On Windows, a `create` whose marker write failed, for example on an antivirus lock of the temp file, and whose manifest read named no program sent nothing. A host that started late then found no marker and served the failed session. + +Now the catch of the readiness wait writes the marker through `writeMarkerOrLog`, which logs a failed write and reports whether it landed. On Windows, while the write fails, the manifest names no program and `isProcessAlive(host.pid)` holds, the catch waits 100 ms, writes the marker again and reads the manifest after the write, up to 50 times. The stop after the loop then ends a host that the last read names. A write that lands reaches the host by its start-up check or its watch, because `create` still runs. In the model, `CreateGivesUp` can fail the marker write on Windows, `CreateStopsHostOnWindows` goes on to `"retry"`, and `CreateRewritesMarker` is one more write and read, or the last one (`"exhausted"`). `mutant-CreateRetriesMarker-win32` breaks R17, and `witness-WitnessMarkerRetried-win32` shows the retry. The give-up integration case `on Windows, when its first marker write fails` fails the first marker write with EIO. + ### `FallbackNeedsFolder`: a childPid that gc's removal left stale gets the kill (R15) The model found this race. Without a token, `readProgramGroup` falls back to the childPid of the manifest copy that the caller read before it, as before `program.json` existed. When gc removed the session folder between that read and the `program.json` read, the record read missing too, and the kill used a childPid whose group could have ended and whose id could name an unrelated group by then. @@ -549,7 +557,7 @@ It assumes: - A killed process stays a zombie until its parent, or init once its parent has died, reaps it, and `kill(-pgid, 0)` still finds a zombie. On Linux, `isProcessGroupAlive` then reads `/proc//stat` of every process and reads the group gone when two scans in a row each show processes of it and only zombies, because a process can fork and end while one scan runs. When a scan shows no process of the group, the probe decides: EPERM reads alive and a found group reads gone. So a group whose last processes are never reaped, as under a container's PID 1 without an init, reads gone. A process whose main thread called `pthread_exit` while another thread runs also shows Z there, so `readProcStat` reads `/proc//task` of every process that shows Z and gives it the state of a thread that is not a zombie. Such a process counts as live in the scan and in the token check, where it can carry the token. On macOS it does not scan, so a zombie still reads alive until launchd reaps it. The model has no zombies: a killed process ends at once. A process that `/proc` refuses to show, as `hidepid=1` (EPERM) or a security module (EACCES) does for other users, reads alive. With `hidepid=2` or `hidepid=4` (`invisible` and `ptraceable` on newer kernels), `/proc` can leave such a process out of its listing, so the probe reads the last `/proc` line of `/proc/self/mountinfo`, skips the scan and reads a group with a zombie alive, as on macOS. With a token, neither a zombie nor a process that `/proc` refuses to show witnesses the token. When no live member is in view, `isProgramGroupAlive` reads the group as `isProcessGroupAlive` does, with the zombie scan, the refused reads and the same `hidepid` check. So under any of those `hidepid` modes, a group that a process of another user took after the program's group ended reads alive, and `destroy` ends with `HOST_TIMEOUT` until that process ends. - A destroy that lands between reconcile's last read and its write is still overwritten with failed, for the time until that reconcile finds the destroy marker and writes destroyed again (`ReconcileRepairsDestroyed`). A `list` or `gc` that reads in that time sees `failed`, a terminal status, so gc can remove the folder as it would remove a destroyed one. A reconcile whose process dies in that time leaves `failed` until the next reconcile reads it: that read finds the marker and writes destroyed (`ReconcileRepairsMarked`). `home list` and the dashboard count a session with the marker as destroyed, also in that time. The model kills the `list` process in that time (`ListDiesBeforeRepair`), so it checks that the repair at the read heals the death. A `gc` that dies there leaves the same record, and the model leaves it out. - The idle time-out calls the same `hangUpProgram` as `initiateShutdown`: SIGHUP, then the group kill after `SHUTDOWN_KILL_GRACE_MS`. When the program exits on that SIGHUP, `handlePtyExit` kills the group too, so a process that ignores SIGHUP does not outlive the idle time-out. An idle time-out still ends exited. When the check cannot run (`unknown`), the idle kill sends nothing, and the session ends exited with that process running, as after a program that exits on its own and leaves a process (coder/agent-tty#222). The model leaves both group kills out: they go through `stopProgramGroup` like every kill, and a process that outlives them is one that the program left, which the model keeps after a normal exit anyway. -- Windows has no process groups, so there `processGroupTarget` gives the program's pid, and every kill reaches only that process. `destroy` never re-runs on Windows. There SIGTERM ends the host at once, so a `create` that gives up sends it only once the manifest names the program, and the next reconcile records `failed` and ends the program. Before that write, the host finds the create-failed marker (`HostChecksCreateFailed`), and after it the host's watch finds it when `create`'s manifest read fails (`HostPollsCreateFailed`). `current-win32` checks this with a SIGTERM that is a host crash and without a token, and keeps the process groups of Linux. A marker write that fails, for example on a full disk, leaves a host that the manifest does not name yet serving on Windows. The model has no such failure. +- Windows has no process groups, so there `processGroupTarget` gives the program's pid, and every kill reaches only that process. `destroy` never re-runs on Windows. There SIGTERM ends the host at once, so a `create` that gives up sends it only once the manifest names the program, and the next reconcile records `failed` and ends the program. Before that write, the host finds the create-failed marker (`HostChecksCreateFailed`), and after it the host's watch finds it when `create`'s manifest read fails (`HostPollsCreateFailed`). `current-win32` checks this with a SIGTERM that is a host crash and without a token, and keeps the process groups of Linux. When the marker write fails on Windows, `create` writes it again every 100 ms, up to 50 times, while the manifest names no program and the host runs (`CreateRetriesMarker`). When every write fails, for example on a full disk, a host that the manifest does not name yet serves the session. The model ends such a `create` as `"exhausted"`, which R17 does not cover. - A host stopped with SIGSTOP, or with a blocked event loop, takes the SIGTERM of a `create` that gave up only when it runs again. Until then its program runs and the session reads `running`, which R17 allows because the SIGTERM is still on its way. A plain `destroy` fails because the host does not answer, and only `destroy --force` ends such a session sooner. - A destroy that the program runs, or that someone types into the program's interactive shell, runs inside the program's session, and `rerunInNewSession` runs it again in a new session. The model lets such a destroy start while the program's leader runs, and assumes that it kept `AGENT_TTY_SESSION_ID`, which every process of the program inherits at spawn. A destroy whose environment lost the variable, or whose `create --env` overrode it, is seen through the id comparison only. On Linux that compares the CLI's session id with `childPid`, so it misses such a destroy only before the host's start-up write. Other POSIX systems compare the process group and the controlling terminal, through `/bin/ps`. A terminal is the controlling terminal of one session and of every process in it, so that also finds a job of an interactive shell, which runs in a group of its own. A process without a controlling terminal is seen only through the group. - The program's processes stay in its process group. A process that leaves the group (`setsid`, or the job control of an interactive shell) is out of reach of the group kill, and it is no witness for the token either. That is case 4 of coder/agent-tty#203, a documented limit with no code change. diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index 8c5bc592..c81a6c91 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -105,6 +105,11 @@ CONSTANTS \* host checks for the create-failed marker \* while its creator runs and once after, and \* then ends the session + CreateRetriesMarker, \* create.ts: on Windows, while the marker write + \* fails and the manifest names no program, + \* create writes the marker again and reads + \* the manifest after each write, up to 50 + \* times, while the host runs TokenNamesProgram, \* programGroup.ts: captureToken records an \* autogroup only once the program leads its \* own session in an autogroup other than the @@ -159,6 +164,7 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, ReconcileSkipsTerminal, ProvesGroupOwnership, DestroyStopsLeftovers, FallbackNeedsFolder, CreateStopsOnGiveUp, HostChecksCreateFailed, HostPollsCreateFailed, + CreateRetriesMarker, ReconcileRepairsDestroyed, ReconcileRepairsMarked, TokenNamesProgram, ReusedIdReadsGone, ProvesHostPid, CreateRecordsHost, @@ -196,7 +202,11 @@ VARIABLES sock, \* the RPC socket file exists (it is outside the directory) cpc, \* create: "alloc", "write", "launch", "done", "giveup" \* (Windows: the marker is written, the manifest read - \* is next), "failed" (it gave up on its host) + \* is next), "retry" (Windows: the marker write failed + \* and the manifest named no program, so the next + \* write is due), "failed" (it gave up on its host), + \* "exhausted" (Windows: it gave up after its last + \* marker write failed too, see R17) hostAlive, \* the detached host process is alive hpc, \* host start-up path: "none", "boot", "open", "record" \* (the program runs, program.json is not written yet), @@ -496,32 +506,65 @@ CreateLaunchesHost == \* the program. create writes nothing else: without a token only the host \* knows which group is the program's. Without the guard, create only \* reports the error. On Linux and macOS the manifest read changes nothing, -\* so the model joins the marker write, the read and the SIGTERM. +\* so the model joins the marker write, the read and the SIGTERM. On +\* Windows the marker write can also fail for a reason of its own, such as +\* an antivirus lock on its temp file. Off Windows such a failure changes +\* nothing, because the SIGTERM stops the host. CreateGivesUp == /\ cpc = "done" - /\ cmark' = (cmark \/ (HostChecksCreateFailed /\ dir)) + /\ \E written \in IF Win32 THEN BOOLEAN ELSE {TRUE} : + cmark' = (cmark \/ (HostChecksCreateFailed /\ dir /\ written)) /\ cpc' = IF Win32 THEN "giveup" ELSE "failed" /\ UNCHANGED <> +\* On Windows, create's SIGTERM to a host that the manifest names. +CreateStopsNamedHost(readOk) == + IF CreateStopsOnGiveUp /\ readOk /\ mchild /\ hostAlive + THEN /\ HostDies + /\ UNCHANGED <> + ELSE UNCHANGED <> + \* On Windows the SIGTERM ends the host at once, without its handlers, so \* create sends it only when the manifest that it reads after the marker \* write names the program. The next reconcile then records failed and ends \* the program. That read can fail, for example when the file is not -\* readable, and then create sends nothing. +\* readable, and then create sends nothing. With CreateRetriesMarker, a +\* create whose marker write failed and whose read named no program writes +\* the marker again while the host runs. CreateStopsHostOnWindows == /\ cpc = "giveup" - /\ cpc' = "failed" /\ \E readOk \in BOOLEAN : - IF CreateStopsOnGiveUp /\ readOk /\ mchild /\ hostAlive - THEN /\ HostDies - /\ UNCHANGED <> - ELSE UNCHANGED <> + IF CreateRetriesMarker /\ HostChecksCreateFailed /\ ~cmark + /\ ~(readOk /\ mchild) /\ hostAlive + THEN /\ cpc' = "retry" + /\ UNCHANGED <> + ELSE /\ cpc' = "failed" + /\ CreateStopsNamedHost(readOk) /\ UNCHANGED <> +\* One more marker write, 100 ms after the last one, then a manifest read. +\* create goes on while the write fails, the read names no program and the +\* host runs. The model has no clock, so after any write that failed it can +\* also stop as if its 50th write had failed ("exhausted"). Then the host +\* that the manifest does not name yet sees no marker and serves the +\* session. The SKILL.md Scope section states this residual. +CreateRewritesMarker == + /\ cpc = "retry" + /\ \E written \in BOOLEAN, readOk \in BOOLEAN, more \in BOOLEAN : + /\ cmark' = (cmark \/ (dir /\ written)) + /\ IF ~(dir /\ written) /\ ~(readOk /\ mchild) /\ hostAlive + THEN /\ cpc' = IF more THEN "retry" ELSE "exhausted" + /\ UNCHANGED <> + ELSE /\ cpc' = "failed" + /\ CreateStopsNamedHost(readOk) + /\ UNCHANGED <> + \* ------------------------------------------------------------------------- \* The host's serial manifest writer (createSerialManifestWriter). Each write \* takes its snapshot of the in-memory state when its turn starts, which is @@ -1423,14 +1466,15 @@ DestroyFinalRead == \* Every process is finished. This step keeps TLC from reporting the end \* states as deadlocks. Any other state without a step is a model error. AllFinished == - /\ cpc \in {"done", "failed"} /\ ~hostAlive /\ pc["gc"] = "done" + /\ cpc \in {"done", "failed", "exhausted"} /\ ~hostAlive + /\ pc["gc"] = "done" /\ pc["list"] = "idle" /\ lruns = MaxListReconciles /\ dpc = "done" /\ UNCHANGED vars Next == \/ CreateMakesDirectory \/ CreateWritesManifest \/ CreateLaunchesHost - \/ CreateGivesUp \/ CreateStopsHostOnWindows + \/ CreateGivesUp \/ CreateStopsHostOnWindows \/ CreateRewritesMarker \/ HostReadsManifest \/ HostOpensLogAndSpawns \/ HostRecordsProgram \/ HostWritesPids \/ HostChecksMarker \/ HostPollsMarker \/ HostListens \/ HostStartsResize \/ HostResizeWriteLands @@ -1481,7 +1525,8 @@ TypeOK == /\ hsd \in {"none", "write", "wait", "closed"} /\ dsnap \in {"none", "destroying", "destroyed"} /\ (mst # "none") => dir - /\ (dir /\ mst = "none") => cpc \notin {"done", "giveup", "failed"} + /\ (dir /\ mst = "none") => + cpc \notin {"done", "giveup", "retry", "failed", "exhausted"} /\ (cpc = "write") => dir /\ gres \in {"pending", "skipped", "removed"} /\ lruns \in 0..MaxListReconciles @@ -1577,7 +1622,9 @@ DestroyedSessionStopped == \* R17: once create gave up, its host keeps the session "running" only \* while create's SIGTERM is still on its way to it, or while the host has -\* yet to check for the create-failed marker. +\* yet to check for the create-failed marker. A create that gave up after +\* all its marker writes failed ends as "exhausted", which R17 does not +\* cover (see the Scope section of SKILL.md). FailedCreateStopped == (cpc = "failed" /\ hostAlive /\ hst = "running") => \/ CreateStopsOnGiveUp /\ ~Win32 /\ ~sig @@ -1607,6 +1654,7 @@ WitnessReconcileRepairs == ~(dmark /\ mst = "failed" /\ \E p \in Readers : pc[p] = "r_repair") WitnessMarkedRepaired == ~readRepaired WitnessMarkerPolled == ~polled +WitnessMarkerRetried == cpc # "retry" WitnessDeadRepairRepaired == ~(diedBeforeRepair /\ ~lostRepair /\ mst = "destroyed" /\ dir) WitnessCreateGivesUp == diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index b597f65a..ca2aafe2 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 ReconcileRepairsMarked CreateStopsOnGiveUp HostChecksCreateFailed HostPollsCreateFailed TokenNamesProgram ReusedIdReadsGone ProvesHostPid CreateRecordsHost FreezesUnseenGroup UnsharedGroupReadsUnknown" +GUARDS="GcSkipsNonCollectable GcFinalCheck ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed ReconcileRepairsMarked CreateStopsOnGiveUp HostChecksCreateFailed HostPollsCreateFailed CreateRetriesMarker TokenNamesProgram ReusedIdReadsGone ProvesHostPid CreateRecordsHost FreezesUnseenGroup UnsharedGroupReadsUnknown" # 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; @@ -256,6 +256,8 @@ WIN32=TRUE write_run current-win32 pass "$NO_TOKEN_RULES" "" "the code on Windows: R1 to R14 and R17 to R19 hold" write_run mutant-HostChecksCreateFailed-win32 violated FailedCreateStopped "HostChecksCreateFailed=FALSE" "without the marker, a host that the manifest does not name yet keeps serving after create gave up" FailedCreateStopped write_run mutant-HostPollsCreateFailed-win32 violated FailedCreateStopped "HostPollsCreateFailed=FALSE" "without the watch, a host that checked for the marker before create wrote it keeps serving when create cannot read the manifest" FailedCreateStopped +write_run mutant-CreateRetriesMarker-win32 violated FailedCreateStopped "CreateRetriesMarker=FALSE" "without the retries, a marker write that fails once leaves a host that the manifest does not name yet serving after create gave up" FailedCreateStopped +write_run witness-WitnessMarkerRetried-win32 violated WitnessMarkerRetried "" "the model reaches this state on Windows" WIN32=FALSE run_tlc() { diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 093cabc2..ae029e6f 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -258,6 +258,7 @@ function createFacts() { CreateStopsOnGiveUp: stopsOnGiveUp(create.body), HostChecksCreateFailed: checksCreateFailed(create.body), HostPollsCreateFailed: pollsCreateFailed(), + CreateRetriesMarker: retriesMarker(create.body), }; } @@ -296,14 +297,11 @@ function giveUpCatch(body) { function stopsOnGiveUp(body) { const st = giveUpCatch(body) ?? []; + // No statement before the stop leaves the catch. const stops = st.length >= 4 && st[0].startsWith('invariant(host !== undefined,') && - st - .at(-3) - .startsWith( - 'const manifest = await readManifestIfExists( manifestPath(sessionDirectory), )', - ) && + st.slice(1, -2).every((t) => !/\b(return|throw|break)\b/.test(t)) && st.at(-2) === "if (process.platform !== 'win32' || manifest?.childPid != null) { host.stop(); }" && st.at(-1) === 'throw withSessionId(error, sessionId);'; @@ -337,11 +335,14 @@ function stopsOnGiveUp(body) { function checksCreateFailed(body) { const st = giveUpCatch(body) ?? []; const marks = - st.length === 5 && - st[1].startsWith( - 'await writeCreateFailedMarker( createFailedMarkerPath(sessionDirectory), sessionId, ).catch(', - ) && - st[2].startsWith('const manifest = await readManifestIfExists('); + st.length >= 8 && + st[1] === 'const markerFile = createFailedMarkerPath(sessionDirectory);' && + st[2] === 'const manifestFile = manifestPath(sessionDirectory);' && + st[4] === + 'let marked = await writeMarkerOrLog(markerFile, sessionId, logger);' && + st[5] === + 'let manifest = await readManifestIfExists(manifestFile).catch(() => null);' && + writesMarker(); const run = requireDeclaration('src/host/hostMain.ts', 'runHost').body; const check = indexOfStatement( run, @@ -371,6 +372,38 @@ function checksCreateFailed(body) { ); } +// writeMarkerOrLog writes the create-failed marker and reports whether the +// write landed. +function writesMarker() { + const helper = normalize( + requireDeclaration( + 'src/cli/commands/create.ts', + 'writeMarkerOrLog', + ).body.getText(), + ); + return helper.startsWith( + '{ return writeCreateFailedMarker(path, sessionId).then( () => true, (error: unknown) => {', + ); +} + +// On Windows, while the marker write fails and the manifest names no +// program, the give-up catch writes the marker again and reads the manifest +// after each write, a bounded number of times while the host runs, before +// its stop. So a host that the manifest does not name yet gets the marker, +// or the last read names its program and create stops it. +function retriesMarker(body) { + const st = giveUpCatch(body) ?? []; + const loop = + 'for ( let attempt = 1; ' + + "process.platform === 'win32' && !marked && manifest?.childPid == null && " + + 'attempt <= MARKER_RETRY_MAX_ATTEMPTS && isProcessAlive(host.pid); ' + + 'attempt += 1 ) { ' + + 'await delay(MARKER_RETRY_INTERVAL_MS); ' + + 'marked = await writeMarkerOrLog(markerFile, sessionId, logger); ' + + 'manifest = await readManifestIfExists(manifestFile).catch(() => null); }'; + return st.length === 9 && st[6] === loop && checksCreateFailed(body); +} + // runHost's watchCreateFailed checks, every CREATE_FAILED_POLL_INTERVAL_MS, // whether the creator still runs and then whether the create-failed marker // exists. On the marker it calls startShutdown, and it stops once a check @@ -1420,6 +1453,7 @@ function policyFacts() { const COVERED = [ ['src/cli/commands/create.ts', 'runCreateCommand'], ['src/cli/commands/create.ts', 'waitForReadyHost'], + ['src/cli/commands/create.ts', 'writeMarkerOrLog'], ['src/cli/commands/destroy.ts', 'runDestroyCommand'], ['src/cli/commands/destroy.ts', 'rerunInNewSession'], ['src/cli/commands/gc.ts', 'gcSessions'], diff --git a/docs/USAGE.md b/docs/USAGE.md index 209d06f4..a18c33b8 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -337,7 +337,7 @@ When the host cannot end the program's group, for example a process of another u A host stopped with SIGSTOP, or with a blocked event loop, handles the SIGTERM only when it runs again. Until then the program runs and the session reads `running`. A plain `destroy` fails because the host does not answer, and only `destroy --force` ends the session sooner. On Windows, SIGTERM ends the host at once, so the host cannot stop the program itself. There `create` sends it only once the manifest names the program: the session then reads `running` with a dead host until the next reconcile records it `failed` and ends the program. Before the host's start-up write, `create` sends nothing. For that case, on every platform, `create` first writes an empty internal file, `create-failed`, in the session folder, and then reads the manifest. The host checks for that file before it starts the program, and returns then, so no program runs and the next reconcile records the session `failed`. It checks again right after its start-up write, and then ends the session the way a SIGTERM does on Linux: it stops the program and records `destroyed`. -On Windows, a host whose start-up write lands before `create` reads the manifest is named by that read and gets the SIGTERM, and a host whose write lands after it finds the file. After its start-up write, the host also checks for the file every 100 ms while `create` runs, and once after `create` exits, so it ends the session also when `create` cannot read the manifest. When the file write fails, for example on a full disk, a Windows host that starts late can still serve the session. This path is not tested on a real Windows host. +On Windows, a host whose start-up write lands before `create` reads the manifest is named by that read and gets the SIGTERM, and a host whose write lands after it finds the file. After its start-up write, the host also checks for the file every 100 ms while `create` runs, and once after `create` exits, so it ends the session also when `create` cannot read the manifest. When the file write fails, `create` writes it again every 100 ms, up to 50 times, while the host runs and the manifest names no program. When every write fails, for example on a full disk, a Windows host that starts late can still serve the session. This path is not tested on a real Windows host. On Linux, `destroy` and reconcile never kill a process group that they cannot prove is the session's. When the host starts the program, it records the program's pid, the boot id and the program's autogroup id in an internal file, `program.json`. diff --git a/src/cli/commands/README.md b/src/cli/commands/README.md index f52bd695..e92a5add 100644 --- a/src/cli/commands/README.md +++ b/src/cli/commands/README.md @@ -44,7 +44,7 @@ This directory holds one handler module per agent-tty CLI command. `src/cli/main ## Side Effects - Session commands send RPCs over the session socket through `sendRpc`. The method names are `run`, `type`, `paste`, `sendKeys`, `mouse`, `mark`, `resize`, `signal`, `snapshot`, `screenshot`, `wait`, `waitForRender` and `inspect`. `create` also sends `inspect` while it polls. [run.ts:runRunCommand] [send-keys.ts:runSendKeysCommand] [wait.ts:runWaitCommand] [create.ts:runCreateCommand] -- `create` calls `allocateSession` (`src/host/lifecycle.ts`) with a `launch` callback that records the session ID and starts the host process through `launchHost`. If `launchHost` or a later step of `allocateSession` throws, `create` removes the session directory with `fs.rm`. A bad `cwd`, shell path or command segment fails before `allocateSession` creates the directory, so no session directory is left behind. A failure between `mkdir` and the callback, such as a failed `chmod`, leaves the empty session directory in place. Any failure after `allocateSession` returned, a failed readiness poll included, writes the empty `create-failed` marker with `writeCreateFailedMarker`, logs a failed marker write at debug level, then calls the host's `stop()` (on Windows only once the manifest names the program) and leaves the session directory in place. `create` rethrows the error with `details.sessionId` added, and an error that is not a `CliError` becomes `INTERNAL_ERROR`. In text mode it first writes `Session failed to start.` to stderr with `writeHumanErrorLines`. It registers the Home through `upsertHome`. [create.ts:runCreateCommand] +- `create` calls `allocateSession` (`src/host/lifecycle.ts`) with a `launch` callback that records the session ID and starts the host process through `launchHost`. If `launchHost` or a later step of `allocateSession` throws, `create` removes the session directory with `fs.rm`. A bad `cwd`, shell path or command segment fails before `allocateSession` creates the directory, so no session directory is left behind. A failure between `mkdir` and the callback, such as a failed `chmod`, leaves the empty session directory in place. Any failure after `allocateSession` returned, a failed readiness poll included, writes the empty `create-failed` marker with `writeCreateFailedMarker` and logs a failed marker write at debug level (`writeMarkerOrLog`). On Windows, while that write fails, the manifest names no program and the host runs, it writes the marker again every 100 ms, up to 50 times, and reads the manifest after each write. It then calls the host's `stop()` (on Windows only once the manifest names the program) and leaves the session directory in place. `create` rethrows the error with `details.sessionId` added, and an error that is not a `CliError` becomes `INTERNAL_ERROR`. In text mode it first writes `Session failed to start.` to stderr with `writeHumanErrorLines`. It registers the Home through `upsertHome`. [create.ts:runCreateCommand] [create.ts:writeMarkerOrLog] - `gc` reads session directories, calls `reconcileSession` (which can rewrite manifests), deletes collectable session directories with `fs.rm` outside dry-run mode, and deregisters Homes through `forgetHome`. [gc.ts:gcSessions] [gc.ts:runGcCommand] - `inspect` calls `reconcileSession` when the host is unreachable, and for an ended session other than destroyed whose folder holds the destroy marker. When that repair throws, it shows the manifest as it reads. [inspect.ts:runInspectCommand] - `destroy` and `list` call `destroySession` and `listSessions` from `src/host/lifecycle.ts`. [destroy.ts:runDestroyCommand] [list.ts:runListCommand] From 9658e3d4e175eb3880d611e29f68df1715d32474 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 06:30:21 +0000 Subject: [PATCH 13/28] fix(skills): let the marker write fail on every platform With the host's watch, a marker that always landed off Windows made the SIGTERM redundant, so mutant-CreateStopsOnGiveUp passed. The write can fail on any platform, and off Windows the SIGTERM is then what stops the host: the mutant breaks R17 again. --- .agents/skills/verify-session-lifecycle/SKILL.md | 2 +- .../verify-session-lifecycle/model/SessionLifecycle.tla | 9 ++++----- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index c410fc3f..acb492f4 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -403,7 +403,7 @@ Now `runHost` starts `watchCreateFailed` right after its start-up check. Every 1 The marker closes the race only when its write lands. On Windows, a `create` whose marker write failed, for example on an antivirus lock of the temp file, and whose manifest read named no program sent nothing. A host that started late then found no marker and served the failed session. -Now the catch of the readiness wait writes the marker through `writeMarkerOrLog`, which logs a failed write and reports whether it landed. On Windows, while the write fails, the manifest names no program and `isProcessAlive(host.pid)` holds, the catch waits 100 ms, writes the marker again and reads the manifest after the write, up to 50 times. The stop after the loop then ends a host that the last read names. A write that lands reaches the host by its start-up check or its watch, because `create` still runs. In the model, `CreateGivesUp` can fail the marker write on Windows, `CreateStopsHostOnWindows` goes on to `"retry"`, and `CreateRewritesMarker` is one more write and read, or the last one (`"exhausted"`). `mutant-CreateRetriesMarker-win32` breaks R17, and `witness-WitnessMarkerRetried-win32` shows the retry. The give-up integration case `on Windows, when its first marker write fails` fails the first marker write with EIO. +Now the catch of the readiness wait writes the marker through `writeMarkerOrLog`, which logs a failed write and reports whether it landed. On Windows, while the write fails, the manifest names no program and `isProcessAlive(host.pid)` holds, the catch waits 100 ms, writes the marker again and reads the manifest after the write, up to 50 times. The stop after the loop then ends a host that the last read names. A write that lands reaches the host by its start-up check or its watch, because `create` still runs. In the model, the marker write in `CreateGivesUp` can fail on every platform, and off Windows the SIGTERM then still stops the host. On Windows `CreateStopsHostOnWindows` goes on to `"retry"`, and `CreateRewritesMarker` is one more write and read, or the last one (`"exhausted"`). `mutant-CreateRetriesMarker-win32` breaks R17, and `witness-WitnessMarkerRetried-win32` shows the retry. The give-up integration case `on Windows, when its first marker write fails` fails the first marker write with EIO. ### `FallbackNeedsFolder`: a childPid that gc's removal left stale gets the kill (R15) diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index c81a6c91..50d98862 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -506,13 +506,12 @@ CreateLaunchesHost == \* the program. create writes nothing else: without a token only the host \* knows which group is the program's. Without the guard, create only \* reports the error. On Linux and macOS the manifest read changes nothing, -\* so the model joins the marker write, the read and the SIGTERM. On -\* Windows the marker write can also fail for a reason of its own, such as -\* an antivirus lock on its temp file. Off Windows such a failure changes -\* nothing, because the SIGTERM stops the host. +\* so the model joins the marker write, the read and the SIGTERM. The +\* marker write can also fail for a reason of its own, such as an antivirus +\* lock on its temp file. Off Windows the SIGTERM then still stops the host. CreateGivesUp == /\ cpc = "done" - /\ \E written \in IF Win32 THEN BOOLEAN ELSE {TRUE} : + /\ \E written \in BOOLEAN : cmark' = (cmark \/ (HostChecksCreateFailed /\ dir /\ written)) /\ cpc' = IF Win32 THEN "giveup" ELSE "failed" /\ UNCHANGED < Date: Wed, 4 Nov 2026 07:52:20 +0000 Subject: [PATCH 14/28] chore(skills): sync the lifecycle coverage record and state counts --- .agents/skills/verify-session-lifecycle/SKILL.md | 4 ++-- .../skills/verify-session-lifecycle/coverage.json | 13 +++++++------ 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index acb492f4..63ae3cd2 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -62,7 +62,7 @@ From the repo root: .agents/skills/verify-session-lifecycle/scripts/check.sh ``` -It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. On this repo it takes about eleven minutes with the default `CHECK_JOBS` of 4. Ten runs explore more than 20 million distinct states each, so `CHECK_JOBS=81` 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. Eleven runs explore more than 20 million distinct states each, so `CHECK_JOBS=81` 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: @@ -537,7 +537,7 @@ To bring the check back in line after changes that skipped it, use `/maintain-fo ## Scope -The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 27,013,946 distinct states, and without one 26,822,518. The check prints both counts. +The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 58,644,364 distinct states, and without one 57,769,962. 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 9275b847..06fa1ce8 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -1,7 +1,8 @@ { "fingerprints": { - "src/cli/commands/create.ts#runCreateCommand": "131d2707818ea283", + "src/cli/commands/create.ts#runCreateCommand": "79bf6194263f5c99", "src/cli/commands/create.ts#waitForReadyHost": "a7fd2ba345b6bfd6", + "src/cli/commands/create.ts#writeMarkerOrLog": "abf293bd80df1c3d", "src/cli/commands/destroy.ts#runDestroyCommand": "ecaa8b1d572da7c6", "src/cli/commands/destroy.ts#rerunInNewSession": "cf32d7d082758522", "src/cli/commands/gc.ts#gcSessions": "667e4ebc3ca3029c", @@ -89,13 +90,13 @@ "src/storage/manifests.ts#writeCreateFailedMarker": "587c8047e563db4e", "src/storage/manifests.ts#writeEmptyMarker": "143325689100f36c", "src/protocol/sessionStatusPolicy.ts#SESSION_STATUS_POLICIES": "83827f9f7f6b8e1d", - "src/host/hostMain.ts#runHost(parts)": "1d75544221b3c6c1", - "src/host/hostMain.ts#runHost(final try)": "251f1e68a4ec17cc", + "src/host/hostMain.ts#runHost(parts)": "64190e53e002f80e", + "src/host/hostMain.ts#runHost(final try)": "e0615a9709fefb67", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "320f9c8a26340aeb", - "skill:scripts/facts.mjs": "0f4e240431fb0fcd", - "skill:scripts/check.sh": "606573a67217656e" + "skill:model/SessionLifecycle.tla": "92c2c7c68311a1cc", + "skill:scripts/facts.mjs": "fdea99c0724ce6a8", + "skill:scripts/check.sh": "169876a806f5e9cc" }, "callSites": { "writeManifest": [ From 1159cb73b746f295d25ab823779d53f15f1d6d88 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 08:22:03 +0000 Subject: [PATCH 15/28] test: give the host marker tests the real Home path The host resolves its Home to the real path and derives the socket path from it. On macOS tmpdir() is a symlink, so the tests looked for the socket at another path, and the two cases that need a serving host failed there. A TMPDIR that is a symlink reproduces it on Linux. --- test/unit/host/hostMarker.test.ts | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/test/unit/host/hostMarker.test.ts b/test/unit/host/hostMarker.test.ts index 2169ea6c..295276b2 100644 --- a/test/unit/host/hostMarker.test.ts +++ b/test/unit/host/hostMarker.test.ts @@ -1,7 +1,7 @@ import { spawn } from 'node:child_process'; import { once } from 'node:events'; import { existsSync, readFileSync, writeFileSync } from 'node:fs'; -import { mkdir, mkdtemp, rm } from 'node:fs/promises'; +import { mkdir, mkdtemp, realpath, rm } from 'node:fs/promises'; import { tmpdir } from 'node:os'; import { join } from 'node:path'; import process from 'node:process'; @@ -74,7 +74,11 @@ async function expectHostStopped(group: number): Promise { } beforeEach(async () => { - home = await mkdtemp(join(tmpdir(), 'agent-tty-host-marker-')); + // The host resolves its Home to the real path, and the socket path is + // derived from that path, as on macOS, where tmpdir() is a symlink. + home = await realpath( + await mkdtemp(join(tmpdir(), 'agent-tty-host-marker-')), + ); vi.stubEnv('AGENT_TTY_HOME', home); directory = sessionDir(home, SESSION_ID); await mkdir(directory, { recursive: true, mode: 0o700 }); From c449086852c42adb262129459e7616a1e6770016 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 08:28:33 +0000 Subject: [PATCH 16/28] test: a host whose creator's pid answers EPERM must not crash When a process of another user takes the creator's pid, the liveness probe of the marker watch throws EPERM inside its timer. In the host that is an uncaught exception, and here vitest reports it as unhandled errors, so the run fails. --- test/unit/host/hostMarker.test.ts | 48 ++++++++++++++++++++++++++++++- 1 file changed, 47 insertions(+), 1 deletion(-) diff --git a/test/unit/host/hostMarker.test.ts b/test/unit/host/hostMarker.test.ts index 295276b2..3e24fd7f 100644 --- a/test/unit/host/hostMarker.test.ts +++ b/test/unit/host/hostMarker.test.ts @@ -7,7 +7,15 @@ import { join } from 'node:path'; import process from 'node:process'; import { setTimeout as delay } from 'node:timers/promises'; -import { afterEach, beforeEach, describe, expect, it, vi } from 'vitest'; +import { + afterEach, + beforeEach, + describe, + expect, + it, + onTestFinished, + vi, +} from 'vitest'; import { runHost } from '../../../src/host/hostMain.js'; import type * as ProgramGroupModule from '../../../src/host/programGroup.js'; @@ -182,4 +190,42 @@ describe('runHost and the create-failed marker', () => { } await expectHostStopped(readProgramGroup()); }, 15_000); + + it('keeps serving when a process of another user takes the pid of its creator', async () => { + const creator = spawn('sleep', ['30'], { stdio: 'ignore' }); + onTestFinished(() => { + creator.kill('SIGKILL'); + }); + const creatorPid = creator.pid as number; + expect(creatorPid).toBeGreaterThan(0); + await runHost(SESSION_ID, creatorPid); + expect(existsSync(socketPath(directory))).toBe(true); + // From here on, the probe of the creator's pid answers EPERM. + const kill = process.kill.bind(process); + vi.spyOn(process, 'kill').mockImplementation((pid, signal) => { + if (pid === creatorPid && signal === 0) { + throw Object.assign(new Error('kill EPERM'), { code: 'EPERM' }); + } + return kill(pid, signal); + }); + await delay(300); + + await writeCreateFailedMarker( + createFailedMarkerPath(directory), + SESSION_ID, + ); + await delay(500); + + expect((await readManifest(manifestPath(directory))).status).toBe( + 'running', + ); + expect(existsSync(socketPath(directory))).toBe(true); + vi.restoreAllMocks(); + for (const listener of process.rawListeners('SIGTERM')) { + if (!sigtermListeners.has(listener)) { + (listener as () => void)(); + } + } + await expectHostStopped(readProgramGroup()); + }, 15_000); }); From e3b156226b9e17c8eb8fd33bd6f80f74c9691478 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 08:29:37 +0000 Subject: [PATCH 17/28] fix(host): count a creator probe that throws as an exited creator The marker watch probes the creator's pid inside its timer. A process of another user that took that pid answers EPERM, isProcessAlive throws it, and the uncaught error ended the host. The watch now counts any probe error as an exited creator, checks for the marker once more and stops. facts.mjs reads the new watch, and the docs say how it treats the error. --- .agents/skills/verify-session-lifecycle/SKILL.md | 2 +- .../skills/verify-session-lifecycle/scripts/facts.mjs | 7 ++++--- src/host/README.md | 2 +- src/host/hostMain.ts | 9 ++++++++- 4 files changed, 14 insertions(+), 6 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 63ae3cd2..53d9ddef 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -397,7 +397,7 @@ Now the catch of the readiness wait first writes an empty marker, `/cre The order of the marker write and the manifest read closes the race only while that read works. When the host's start-up write and its marker check came before `create` gave up, the host listens without the marker, and `create` reads the manifest to send the SIGTERM. When that read fails, for example on an unreadable file, `create` on Windows takes the manifest as naming no program and sends nothing, and the host serves the failed session. -Now `runHost` starts `watchCreateFailed` right after its start-up check. Every 100 ms it checks whether its creator still runs and then whether the marker exists. On the marker it calls `startShutdown`, as for a SIGTERM. Once a check after the creator's exit found no marker, it stops: `create` writes the marker before it exits, so no marker comes later. In the model, `CreateStopsHostOnWindows` reads the manifest or fails to read it, and `HostPollsMarker` is the watch from `"sockdir"` on. `mutant-HostPollsCreateFailed-win32` breaks R17, and `mutant-HostPollsCreateFailed` passes, because off Windows the SIGTERM does not need the read. The integration test `a create on Windows whose manifest read fails after it gave up` holds the host's socket-directory `mkdir` until `create` has exited and makes `create`'s manifest reads fail once the marker exists. +Now `runHost` starts `watchCreateFailed` right after its start-up check. Every 100 ms it checks whether its creator still runs and then whether the marker exists. On the marker it calls `startShutdown`, as for a SIGTERM. Once a check after the creator's exit found no marker, it stops: `create` writes the marker before it exits, so no marker comes later. A liveness probe that throws, such as EPERM from a process of another user that took the creator's pid, counts as an exited creator, so no error leaves the timer and ends the host. In the model, `CreateStopsHostOnWindows` reads the manifest or fails to read it, and `HostPollsMarker` is the watch from `"sockdir"` on. `mutant-HostPollsCreateFailed-win32` breaks R17, and `mutant-HostPollsCreateFailed` passes, because off Windows the SIGTERM does not need the read. The integration test `a create on Windows whose manifest read fails after it gave up` holds the host's socket-directory `mkdir` until `create` has exited and makes `create`'s manifest reads fail once the marker exists. ### `CreateRetriesMarker`: on Windows, a failed marker write leaves a host serving a failed create (R17) diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index ae029e6f..79aff58e 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -406,7 +406,8 @@ function retriesMarker(body) { // runHost's watchCreateFailed checks, every CREATE_FAILED_POLL_INTERVAL_MS, // whether the creator still runs and then whether the create-failed marker -// exists. On the marker it calls startShutdown, and it stops once a check +// exists. A probe that throws counts as an exited creator, so no error leaves +// the timer. On the marker it calls startShutdown, and it stops once a check // after the creator's exit found none. The start-up try calls it right after // the check that follows the start-up write. function pollsCreateFailed() { @@ -414,8 +415,8 @@ function pollsCreateFailed() { const watch = indexOfStatement(run, /^const watchCreateFailed = /); const watches = watch >= 0 && - normalize(run.statements[watch].getText()) === - 'const watchCreateFailed = (): void => { const timer = setInterval(() => { const creatorGone = !isProcessAlive(creatorPid); if (existsSync(createFailedMarkerPath(sessDir))) { clearInterval(timer); startShutdown(); } else if (creatorGone) { clearInterval(timer); } }, CREATE_FAILED_POLL_INTERVAL_MS); timer.unref(); };'; + normalize(run.statements[watch].getText().replace(/\/\/[^\n]*/g, '')) === + 'const watchCreateFailed = (): void => { const timer = setInterval(() => { let creatorGone = true; try { creatorGone = !isProcessAlive(creatorPid); } catch { } if (existsSync(createFailedMarkerPath(sessDir))) { clearInterval(timer); startShutdown(); } else if (creatorGone) { clearInterval(timer); } }, CREATE_FAILED_POLL_INTERVAL_MS); timer.unref(); };'; const last = run.statements.at(-1); const tried = last !== undefined && ts.isTryStatement(last) diff --git a/src/host/README.md b/src/host/README.md index 0dad5bdb..6b6f00b6 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -80,7 +80,7 @@ - `runHost` spawns the PTY with `createPty` (`src/pty/createPty.ts`), writes input to it, resizes it and kills it on idle timeout and shutdown. It writes `TerminalQueryResponder` replies to the PTY without logging them. [hostMain.ts:runHost] - `runHost` polls `session.json` with `readManifestIfExists` and probes the creator process with `isProcessAlive` until the manifest appears or the creator exits. It writes `session.json` through `createSerialManifestWriter`, creates the socket directory with mode `0o700` and listens with `RpcServer` through `listenInSocketDirectory` and writes snapshot and screenshot artifacts through `src/snapshot/capture.ts` and `src/screenshot/capture.ts`. [hostMain.ts:runHost] - `runHost` registers a `process.on('SIGTERM')` handler that starts shutdown, sends signals to the child with `process.kill` and starts `setInterval` timers for idle and wait polling. [hostMain.ts:runHost] -- `runHost` checks for the `create-failed` marker with `existsSync` before it spawns the program, and returns when it finds it. It checks again right after its start-up manifest write, before it listens, and then shuts down. From there on, `watchCreateFailed` checks for the marker every `CREATE_FAILED_POLL_INTERVAL_MS` (100 ms) while the creator process lives and once after it exited, and starts the shutdown when it finds the marker. [hostMain.ts:runHost] +- `runHost` checks for the `create-failed` marker with `existsSync` before it spawns the program, and returns when it finds it. It checks again right after its start-up manifest write, before it listens, and then shuts down. From there on, `watchCreateFailed` checks for the marker every `CREATE_FAILED_POLL_INTERVAL_MS` (100 ms) while the creator process lives and once after it exited (a liveness probe that throws, such as EPERM from a process of another user that took the pid, counts as exited), and starts the shutdown when it finds the marker. [hostMain.ts:runHost] - `runHost` rethrows a PTY-ingestion, event-log append, exit-handling or shutdown error in `process.nextTick`. The uncaught exception crashes the host process. [hostMain.ts:rethrowAsync] - `resolveHostRendererName` reads `process.env.AGENT_TTY_HOST_RENDERER` and `process.env.AGENT_TTY_RENDERER`. [hostMain.ts:resolveHostRendererName] - `EventLog.open` opens the file in append mode and runs `chmod 0o600`. `append` writes with `fileHandle.appendFile`, one call at a time. `close` calls `fileHandle.sync()` and then closes the file. [eventLog.ts:EventLog] diff --git a/src/host/hostMain.ts b/src/host/hostMain.ts index 3052f70c..192a7383 100644 --- a/src/host/hostMain.ts +++ b/src/host/hostMain.ts @@ -1279,7 +1279,14 @@ export async function runHost( // while its creator runs, and once more after the creator has exited. const watchCreateFailed = (): void => { const timer = setInterval(() => { - const creatorGone = !isProcessAlive(creatorPid); + // An error of the probe, such as EPERM from a process of another user + // that took the pid, means that the creator has exited. + let creatorGone = true; + try { + creatorGone = !isProcessAlive(creatorPid); + } catch { + // creatorGone stays true. + } if (existsSync(createFailedMarkerPath(sessDir))) { clearInterval(timer); startShutdown(); From cb5c98e0bc1035430916321f14b0ebdbfd777107 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 08:35:39 +0000 Subject: [PATCH 18/28] test: a create whose host probe throws EPERM keeps its error On Windows, a process of another user that took the host's pid makes isProcessAlive throw EPERM in the marker retries. The error then left the catch, and create reported it as INTERNAL_ERROR without the session id. --- test/unit/commands/create.test.ts | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/test/unit/commands/create.test.ts b/test/unit/commands/create.test.ts index 7568eb45..17a04f44 100644 --- a/test/unit/commands/create.test.ts +++ b/test/unit/commands/create.test.ts @@ -596,6 +596,24 @@ describe('create command', () => { expect(mocks.stopHost).not.toHaveBeenCalled(); }); + it('counts a host probe that throws as an exited host and keeps the error', async () => { + mocks.writeCreateFailedMarker.mockRejectedValue(diskError); + // A process of another user that took the host's pid answers EPERM. + mocks.isProcessAlive.mockImplementation(() => { + throw Object.assign(new Error('kill EPERM'), { code: 'EPERM' }); + }); + + await expect( + runCreateCommand({ ...baseOptions, context }), + ).rejects.toMatchObject({ + code: 'HOST_UNREACHABLE', + details: { sessionId: 'session-01' }, + }); + + expect(mocks.writeCreateFailedMarker).toHaveBeenCalledOnce(); + expect(mocks.stopHost).not.toHaveBeenCalled(); + }); + it('stops retrying once the host has exited', async () => { mocks.writeCreateFailedMarker.mockRejectedValue(diskError); mocks.isProcessAlive.mockReturnValueOnce(true).mockReturnValue(false); From af541001a92a1000fbd39b5fe095857a0356b113 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 08:36:02 +0000 Subject: [PATCH 19/28] fix(cli): count a host probe that throws as an exited host in the marker retries A process of another user that took the host's pid makes isProcessAlive throw EPERM. In the retry loop that error left the give-up catch, so create reported INTERNAL_ERROR without the session id. The new hostRuns counts any probe error as an exited host, and facts.mjs reads it. --- .agents/skills/verify-session-lifecycle/SKILL.md | 4 ++-- .../verify-session-lifecycle/scripts/facts.mjs | 15 +++++++++++++-- src/cli/commands/README.md | 2 +- src/cli/commands/create.ts | 13 ++++++++++++- 4 files changed, 28 insertions(+), 6 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 53d9ddef..79d31afb 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -44,7 +44,7 @@ Yes, when the diff changes any of these: - `src/host/programGroup.ts`: the token capture (`captureProgram`, `captureToken`, `readAutogroup`, `parseAutogroup`, `parseProcStat`), the `/proc` reads (`readProcFileIfExists`, `readLiveThreadState`, `readProcStat`, `readShownProcStat`, `isRefusedRead`, `readBootId`), the record (`writeProgramRecord`, `readProgramRecord`, `readProvenProgramGroup`, `readProgramGroup`), `procShowsOwnPidSpace`, the verdict (`judgeProgramGroup`, `readGroupMembers`), and the kill and the probe (`stopProgramGroup`, `isProgramGroupAlive`, `processGroupTarget`, `isProcessGroupAlive` with `groupHasLiveProcess` and `procHidesOtherUsers`, `killProcessGroupBestEffort`, `signalProcessGroup`). - `src/host/hostMain.ts`: `waitForManifestFromCreate`, `isSessionCommandable`, and in `runHost` the start-up statements (the manifest wait, the `hostPid === process.pid` check, the `host.json` write with `captureHost` and `writeHostRecord`, `createSerialManifestWriter`, `EventLog.open`, the create-failed marker check, `createPty`, `setChildPid`, `captureProgram`, `watchCreateFailed`), `hangUpProgram` with its kill timer and the `SHUTDOWN_KILL_GRACE_MS` constant, `startIdlePolling` (the idle time-out), `initiateShutdown`, `startShutdown`, `handlePtyExit` with its wait for the program's group, `pty.onExit`, the `SIGTERM` handler, the `resize` and `destroy` handlers, and the last `try` block (the `program.json` write, the start-up manifest write and `rpcServer.listen`). - `src/host/manifestWriter.ts` `createSerialManifestWriter`. -- `src/cli/commands/gc.ts` `gcSessions`, `src/cli/commands/create.ts` `runCreateCommand` with `waitForReadyHost` and `writeMarkerOrLog`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`. +- `src/cli/commands/gc.ts` `gcSessions`, `src/cli/commands/create.ts` `runCreateCommand` with `waitForReadyHost`, `writeMarkerOrLog` and `hostRuns`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`. - `src/host/sessionState.ts` `setDimensions`, `requestDestroy`, `recordDestroyed` and `recordExit`, `src/host/eventLog.ts` `EventLog.open`, `src/host/rpcServer.ts` `listen` and `close`, `src/host/rpcClient.ts` `toTransportCliError` (which socket errors read as `HOST_UNREACHABLE`). - `src/host/hostRecord.ts`: `captureHost`, `writeHostRecord`, `readHostRecord`, `pidExists`, `judgeHost`, `inPidNamespace`, `readTimeNamespace`, `inTimeNamespace`, `readMachineId`, `inHostPidSpace` and `sharesHostPids`. - `src/storage/manifests.ts` `readValidatedJsonFile`, `replaceFileAtomic`, `replaceFileAtomicSync`, `writeValidatedJsonFileSync`, `writeManifest`, `writeDestroyMarker` and `writeCreateFailedMarker` with `writeEmptyMarker`. @@ -403,7 +403,7 @@ Now `runHost` starts `watchCreateFailed` right after its start-up check. Every 1 The marker closes the race only when its write lands. On Windows, a `create` whose marker write failed, for example on an antivirus lock of the temp file, and whose manifest read named no program sent nothing. A host that started late then found no marker and served the failed session. -Now the catch of the readiness wait writes the marker through `writeMarkerOrLog`, which logs a failed write and reports whether it landed. On Windows, while the write fails, the manifest names no program and `isProcessAlive(host.pid)` holds, the catch waits 100 ms, writes the marker again and reads the manifest after the write, up to 50 times. The stop after the loop then ends a host that the last read names. A write that lands reaches the host by its start-up check or its watch, because `create` still runs. In the model, the marker write in `CreateGivesUp` can fail on every platform, and off Windows the SIGTERM then still stops the host. On Windows `CreateStopsHostOnWindows` goes on to `"retry"`, and `CreateRewritesMarker` is one more write and read, or the last one (`"exhausted"`). `mutant-CreateRetriesMarker-win32` breaks R17, and `witness-WitnessMarkerRetried-win32` shows the retry. The give-up integration case `on Windows, when its first marker write fails` fails the first marker write with EIO. +Now the catch of the readiness wait writes the marker through `writeMarkerOrLog`, which logs a failed write and reports whether it landed. On Windows, while the write fails, the manifest names no program and `hostRuns(host.pid)` holds, the catch waits 100 ms, writes the marker again and reads the manifest after the write, up to 50 times. The stop after the loop then ends a host that the last read names. `hostRuns` counts a probe that throws, such as EPERM from a process of another user that took the host's pid, as an exited host, so the catch still reports its own error. A write that lands reaches the host by its start-up check or its watch, because `create` still runs. In the model, the marker write in `CreateGivesUp` can fail on every platform, and off Windows the SIGTERM then still stops the host. On Windows `CreateStopsHostOnWindows` goes on to `"retry"`, and `CreateRewritesMarker` is one more write and read, or the last one (`"exhausted"`). `mutant-CreateRetriesMarker-win32` breaks R17, and `witness-WitnessMarkerRetried-win32` shows the retry. The give-up integration case `on Windows, when its first marker write fails` fails the first marker write with EIO. ### `FallbackNeedsFolder`: a childPid that gc's removal left stale gets the kill (R15) diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 79aff58e..4c3b742a 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -396,12 +396,22 @@ function retriesMarker(body) { const loop = 'for ( let attempt = 1; ' + "process.platform === 'win32' && !marked && manifest?.childPid == null && " + - 'attempt <= MARKER_RETRY_MAX_ATTEMPTS && isProcessAlive(host.pid); ' + + 'attempt <= MARKER_RETRY_MAX_ATTEMPTS && hostRuns(host.pid); ' + 'attempt += 1 ) { ' + 'await delay(MARKER_RETRY_INTERVAL_MS); ' + 'marked = await writeMarkerOrLog(markerFile, sessionId, logger); ' + 'manifest = await readManifestIfExists(manifestFile).catch(() => null); }'; - return st.length === 9 && st[6] === loop && checksCreateFailed(body); + // A probe that throws counts as an exited host. + const probe = normalize( + requireDeclaration('src/cli/commands/create.ts', 'hostRuns').body.getText(), + ); + return ( + st.length === 9 && + st[6] === loop && + probe === + '{ try { return isProcessAlive(pid); } catch { return false; } }' && + checksCreateFailed(body) + ); } // runHost's watchCreateFailed checks, every CREATE_FAILED_POLL_INTERVAL_MS, @@ -1455,6 +1465,7 @@ const COVERED = [ ['src/cli/commands/create.ts', 'runCreateCommand'], ['src/cli/commands/create.ts', 'waitForReadyHost'], ['src/cli/commands/create.ts', 'writeMarkerOrLog'], + ['src/cli/commands/create.ts', 'hostRuns'], ['src/cli/commands/destroy.ts', 'runDestroyCommand'], ['src/cli/commands/destroy.ts', 'rerunInNewSession'], ['src/cli/commands/gc.ts', 'gcSessions'], diff --git a/src/cli/commands/README.md b/src/cli/commands/README.md index e92a5add..f2863672 100644 --- a/src/cli/commands/README.md +++ b/src/cli/commands/README.md @@ -44,7 +44,7 @@ This directory holds one handler module per agent-tty CLI command. `src/cli/main ## Side Effects - Session commands send RPCs over the session socket through `sendRpc`. The method names are `run`, `type`, `paste`, `sendKeys`, `mouse`, `mark`, `resize`, `signal`, `snapshot`, `screenshot`, `wait`, `waitForRender` and `inspect`. `create` also sends `inspect` while it polls. [run.ts:runRunCommand] [send-keys.ts:runSendKeysCommand] [wait.ts:runWaitCommand] [create.ts:runCreateCommand] -- `create` calls `allocateSession` (`src/host/lifecycle.ts`) with a `launch` callback that records the session ID and starts the host process through `launchHost`. If `launchHost` or a later step of `allocateSession` throws, `create` removes the session directory with `fs.rm`. A bad `cwd`, shell path or command segment fails before `allocateSession` creates the directory, so no session directory is left behind. A failure between `mkdir` and the callback, such as a failed `chmod`, leaves the empty session directory in place. Any failure after `allocateSession` returned, a failed readiness poll included, writes the empty `create-failed` marker with `writeCreateFailedMarker` and logs a failed marker write at debug level (`writeMarkerOrLog`). On Windows, while that write fails, the manifest names no program and the host runs, it writes the marker again every 100 ms, up to 50 times, and reads the manifest after each write. It then calls the host's `stop()` (on Windows only once the manifest names the program) and leaves the session directory in place. `create` rethrows the error with `details.sessionId` added, and an error that is not a `CliError` becomes `INTERNAL_ERROR`. In text mode it first writes `Session failed to start.` to stderr with `writeHumanErrorLines`. It registers the Home through `upsertHome`. [create.ts:runCreateCommand] [create.ts:writeMarkerOrLog] +- `create` calls `allocateSession` (`src/host/lifecycle.ts`) with a `launch` callback that records the session ID and starts the host process through `launchHost`. If `launchHost` or a later step of `allocateSession` throws, `create` removes the session directory with `fs.rm`. A bad `cwd`, shell path or command segment fails before `allocateSession` creates the directory, so no session directory is left behind. A failure between `mkdir` and the callback, such as a failed `chmod`, leaves the empty session directory in place. Any failure after `allocateSession` returned, a failed readiness poll included, writes the empty `create-failed` marker with `writeCreateFailedMarker` and logs a failed marker write at debug level (`writeMarkerOrLog`). On Windows, while that write fails, the manifest names no program and the host runs (`hostRuns`, where a probe that throws counts as an exited host), it writes the marker again every 100 ms, up to 50 times, and reads the manifest after each write. It then calls the host's `stop()` (on Windows only once the manifest names the program) and leaves the session directory in place. `create` rethrows the error with `details.sessionId` added, and an error that is not a `CliError` becomes `INTERNAL_ERROR`. In text mode it first writes `Session failed to start.` to stderr with `writeHumanErrorLines`. It registers the Home through `upsertHome`. [create.ts:runCreateCommand] [create.ts:writeMarkerOrLog] [create.ts:hostRuns] - `gc` reads session directories, calls `reconcileSession` (which can rewrite manifests), deletes collectable session directories with `fs.rm` outside dry-run mode, and deregisters Homes through `forgetHome`. [gc.ts:gcSessions] [gc.ts:runGcCommand] - `inspect` calls `reconcileSession` when the host is unreachable, and for an ended session other than destroyed whose folder holds the destroy marker. When that repair throws, it shows the manifest as it reads. [inspect.ts:runInspectCommand] - `destroy` and `list` call `destroySession` and `listSessions` from `src/host/lifecycle.ts`. [destroy.ts:runDestroyCommand] [list.ts:runListCommand] diff --git a/src/cli/commands/create.ts b/src/cli/commands/create.ts index 34bded83..544d55ff 100644 --- a/src/cli/commands/create.ts +++ b/src/cli/commands/create.ts @@ -180,6 +180,17 @@ function withSessionId(error: unknown, sessionId: string): CliError { }); } +// A probe that throws, such as EPERM from a process of another user that +// took the host's pid, counts as an exited host, so the create still reports +// its own error. +function hostRuns(pid: number): boolean { + try { + return isProcessAlive(pid); + } catch { + return false; + } +} + // A failed write is logged, so the create still reports its own error. function writeMarkerOrLog( path: string, @@ -310,7 +321,7 @@ export async function runCreateCommand(options: CommandOptions): Promise { !marked && manifest?.childPid == null && attempt <= MARKER_RETRY_MAX_ATTEMPTS && - isProcessAlive(host.pid); + hostRuns(host.pid); attempt += 1 ) { await delay(MARKER_RETRY_INTERVAL_MS); From f2f2a7ce7140e22363a9b5faa0132f59bf44e867 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 08:50:21 +0000 Subject: [PATCH 20/28] test: wait for the marker watch to stop instead of a fixed time The two cases where the watch must not stop the host waited 300 ms and 500 ms. They now spy on the timers, wait until clearInterval runs on the host's 100 ms watch, write the marker and check at once that the host still serves: a stopped watch never checks again. With a watch that never stops, or a probe error that leaves the timer, they fail. --- test/unit/host/hostMarker.test.ts | 54 ++++++++++++++++++++++--------- 1 file changed, 38 insertions(+), 16 deletions(-) diff --git a/test/unit/host/hostMarker.test.ts b/test/unit/host/hostMarker.test.ts index 3e24fd7f..1b285cbf 100644 --- a/test/unit/host/hostMarker.test.ts +++ b/test/unit/host/hostMarker.test.ts @@ -81,6 +81,37 @@ async function expectHostStopped(group: number): Promise { } } +// Spies on the timers before runHost starts. The returned function waits +// until the host's marker watch, its only 100 ms interval, has stopped. A +// stopped watch never checks for the marker again. +function trackMarkerWatch(): () => Promise { + const setSpy = vi.spyOn(globalThis, 'setInterval'); + const clearSpy = vi.spyOn(globalThis, 'clearInterval'); + return async () => { + const deadline = Date.now() + 10_000; + for (;;) { + const watches = setSpy.mock.calls.flatMap((call, index) => + call[1] === 100 ? [setSpy.mock.results[index]?.value as unknown] : [], + ); + expect(watches).toHaveLength(1); + if (clearSpy.mock.calls.some(([timer]) => timer === watches[0])) { + return; + } + expect(Date.now()).toBeLessThan(deadline); + await delay(20); + } + }; +} + +// Stops the host as a SIGTERM would. +function sendSigterm(): void { + for (const listener of process.rawListeners('SIGTERM')) { + if (!sigtermListeners.has(listener)) { + (listener as () => void)(); + } + } +} + beforeEach(async () => { // The host resolves its Home to the real path, and the socket path is // derived from that path, as on macOS, where tmpdir() is a symlink. @@ -110,6 +141,7 @@ beforeEach(async () => { }); afterEach(async () => { + vi.restoreAllMocks(); hooks.afterProgramRecord = () => {}; // runHost adds a SIGTERM listener that would outlive the test. for (const listener of process.rawListeners('SIGTERM')) { @@ -165,29 +197,23 @@ describe('runHost and the create-failed marker', () => { it('keeps serving when the marker appears after its creator has exited', async () => { const creator = spawn('sleep', ['30'], { stdio: 'ignore' }); expect(creator.pid).toBeGreaterThan(0); + const watchStopped = trackMarkerWatch(); await runHost(SESSION_ID, creator.pid as number); expect(existsSync(socketPath(directory))).toBe(true); creator.kill('SIGKILL'); await once(creator, 'exit'); - // Two polls see the creator gone and stop the watch. - await delay(300); + await watchStopped(); await writeCreateFailedMarker( createFailedMarkerPath(directory), SESSION_ID, ); - await delay(500); expect((await readManifest(manifestPath(directory))).status).toBe( 'running', ); expect(existsSync(socketPath(directory))).toBe(true); - // Stop the host as a SIGTERM would. - for (const listener of process.rawListeners('SIGTERM')) { - if (!sigtermListeners.has(listener)) { - (listener as () => void)(); - } - } + sendSigterm(); await expectHostStopped(readProgramGroup()); }, 15_000); @@ -198,6 +224,7 @@ describe('runHost and the create-failed marker', () => { }); const creatorPid = creator.pid as number; expect(creatorPid).toBeGreaterThan(0); + const watchStopped = trackMarkerWatch(); await runHost(SESSION_ID, creatorPid); expect(existsSync(socketPath(directory))).toBe(true); // From here on, the probe of the creator's pid answers EPERM. @@ -208,24 +235,19 @@ describe('runHost and the create-failed marker', () => { } return kill(pid, signal); }); - await delay(300); + await watchStopped(); await writeCreateFailedMarker( createFailedMarkerPath(directory), SESSION_ID, ); - await delay(500); expect((await readManifest(manifestPath(directory))).status).toBe( 'running', ); expect(existsSync(socketPath(directory))).toBe(true); vi.restoreAllMocks(); - for (const listener of process.rawListeners('SIGTERM')) { - if (!sigtermListeners.has(listener)) { - (listener as () => void)(); - } - } + sendSigterm(); await expectHostStopped(readProgramGroup()); }, 15_000); }); From 8d742ffcee61f388e6f6afc021f16a561fcfcac9 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 10:42:17 +0000 Subject: [PATCH 21/28] chore(skills): sync the lifecycle coverage record and state counts after the merge of main --- .agents/skills/verify-session-lifecycle/SKILL.md | 4 ++-- .../verify-session-lifecycle/coverage.json | 16 ++++++++++------ 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index d2df5a78..dcf2d0cd 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -65,7 +65,7 @@ From the repo root: .agents/skills/verify-session-lifecycle/scripts/check.sh ``` -It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. On a CI runner with 4 vCPUs and the default `CHECK_JOBS` of 4 it takes about an hour, so CI runs it in four shares. Ten runs explore more than 20 million distinct states each, so `CHECK_JOBS=84` starts every run at once and takes about as long as the longest run. `JAVA=/path/to/java` picks another Java. `TLA2TOOLS_JAR=/path/to/tla2tools.jar` uses a jar you already have, which must be the same 1.7.4 build. `CHECK_OUT=` keeps the results in that folder (default: a new temp folder, printed at the end). +It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. On a CI runner with 4 vCPUs and the default `CHECK_JOBS` of 4 it takes about an hour, so CI runs it in four shares. Eleven runs explore more than 20 million distinct states each, so `CHECK_JOBS=84` 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: @@ -556,7 +556,7 @@ To bring the check back in line after changes that skipped it, use `/maintain-fo ## Scope -The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 29,309,460 distinct states, and without one 29,186,546. The check prints both counts. +The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 64,052,288 distinct states, and without one 63,127,914. The check prints both counts. It assumes: diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index cfb65dd6..d0b376b8 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -11,6 +11,8 @@ "CreateRecordsHost": true, "CreateStopsOnGiveUp": true, "HostChecksCreateFailed": true, + "HostPollsCreateFailed": true, + "CreateRetriesMarker": true, "HostWaitsForManifest": true, "HostSerializesWrites": true, "HostStopsAfterTerminalWrite": true, @@ -39,8 +41,10 @@ "Terminal": ["destroyed", "exited", "failed"] }, "fingerprints": { - "src/cli/commands/create.ts#runCreateCommand": "131d2707818ea283", + "src/cli/commands/create.ts#runCreateCommand": "bb4fa596cc1e4af7", "src/cli/commands/create.ts#waitForReadyHost": "a7fd2ba345b6bfd6", + "src/cli/commands/create.ts#writeMarkerOrLog": "abf293bd80df1c3d", + "src/cli/commands/create.ts#hostRuns": "b80eac3bb9523aaf", "src/cli/commands/destroy.ts#runDestroyCommand": "ecaa8b1d572da7c6", "src/cli/commands/destroy.ts#rerunInNewSession": "cf32d7d082758522", "src/cli/commands/gc.ts#gcSessions": "a2ac8bd10f100332", @@ -133,13 +137,13 @@ "src/storage/manifests.ts#writeCreateFailedMarker": "587c8047e563db4e", "src/storage/manifests.ts#writeEmptyMarker": "143325689100f36c", "src/protocol/sessionStatusPolicy.ts#SESSION_STATUS_POLICIES": "83827f9f7f6b8e1d", - "src/host/hostMain.ts#runHost(parts)": "1d75544221b3c6c1", - "src/host/hostMain.ts#runHost(final try)": "251f1e68a4ec17cc", + "src/host/hostMain.ts#runHost(parts)": "e3879ee94370dcfd", + "src/host/hostMain.ts#runHost(final try)": "e0615a9709fefb67", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "19775a9a74c5ca9a", - "skill:scripts/facts.mjs": "4aff1bce5c8ba086", - "skill:scripts/check.sh": "0e69ddb1068b5df4" + "skill:model/SessionLifecycle.tla": "c54afe56f71248d7", + "skill:scripts/facts.mjs": "5f72f2721e51f3e5", + "skill:scripts/check.sh": "1e7360997d154202" }, "callSites": { "writeManifest": [ From 8da31541fb772e98277ce56b63584cbf49665315 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 11:45:30 +0000 Subject: [PATCH 22/28] chore(skills): sync the lifecycle coverage record after the merge of #326 --- .../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 cafb794e..ed875149 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -12,6 +12,8 @@ "CreateRecordsHost": true, "CreateStopsOnGiveUp": true, "HostChecksCreateFailed": true, + "HostPollsCreateFailed": true, + "CreateRetriesMarker": true, "HostWaitsForManifest": true, "HostSerializesWrites": true, "HostStopsAfterTerminalWrite": true, @@ -40,8 +42,10 @@ "Terminal": ["destroyed", "exited", "failed"] }, "fingerprints": { - "src/cli/commands/create.ts#runCreateCommand": "131d2707818ea283", + "src/cli/commands/create.ts#runCreateCommand": "bb4fa596cc1e4af7", "src/cli/commands/create.ts#waitForReadyHost": "a7fd2ba345b6bfd6", + "src/cli/commands/create.ts#writeMarkerOrLog": "abf293bd80df1c3d", + "src/cli/commands/create.ts#hostRuns": "b80eac3bb9523aaf", "src/cli/commands/destroy.ts#runDestroyCommand": "ecaa8b1d572da7c6", "src/cli/commands/destroy.ts#rerunInNewSession": "cf32d7d082758522", "src/cli/commands/gc.ts#gcSessions": "a2ac8bd10f100332", @@ -135,13 +139,13 @@ "src/storage/manifests.ts#writeCreateFailedMarker": "587c8047e563db4e", "src/storage/manifests.ts#writeEmptyMarker": "143325689100f36c", "src/protocol/sessionStatusPolicy.ts#SESSION_STATUS_POLICIES": "83827f9f7f6b8e1d", - "src/host/hostMain.ts#runHost(parts)": "1d75544221b3c6c1", - "src/host/hostMain.ts#runHost(final try)": "251f1e68a4ec17cc", + "src/host/hostMain.ts#runHost(parts)": "e3879ee94370dcfd", + "src/host/hostMain.ts#runHost(final try)": "e0615a9709fefb67", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "77ec28d60359f635", - "skill:scripts/facts.mjs": "eded6c52629e3523", - "skill:scripts/check.sh": "e33db0960de216fe" + "skill:model/SessionLifecycle.tla": "7f1c6dd7943968c3", + "skill:scripts/facts.mjs": "07dba02a98497dcb", + "skill:scripts/check.sh": "b48bc5fd343aefb5" }, "callSites": { "writeManifest": [ From f64e17a182887fa12f0c64940df8e886029a205a Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 11:47:08 +0000 Subject: [PATCH 23/28] docs(host): say when the destroy marker is written in the marked-repair comment recordDestroyed writes it for a terminal manifest too, where destroy stops no host, so the host can still be in its shutdown tail. It is ending either way, so the repair needs no liveness check. --- src/host/lifecycle.ts | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index a3efad11..5f7a184a 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -1132,9 +1132,10 @@ export async function reconcileSession( const manifestFile = manifestPath(sessionDirectory); const manifest = await readManifestIfExists(manifestFile); - // Only a destroy writes the marker, after it stopped the host, so no host - // listens on either socket, and the repair removes both without a liveness - // check. + // Only recordDestroyed writes the marker, and only for a terminal manifest + // or once the host and the program's group are dead. So the host has + // ended or is ending, and the repair removes both sockets without a + // liveness check. if (manifest !== null && isMarkedDestroyed(sessionDirectory, manifest)) { if (await writeMarkedDestroyed(manifestFile, manifest)) { const socketFile = socketPath(sessionDirectory); From 7563fe194efa2963c5a784ab8e028a81ff11db54 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 11:47:08 +0000 Subject: [PATCH 24/28] test: pin the order of the watch's probe and check, and stop it for a zombie creator A creator that writes the marker and exits between the watch's probe and its check must still stop the host: with the check before the probe, the watch stops without the marker. A zombie creator has exited, but kill(pid, 0) still finds it, so the watch ticks for as long as its parent does not reap it. The zombie case fails on the head. --- test/unit/host/hostMarker.test.ts | 63 +++++++++++++++++++++++++++++++ 1 file changed, 63 insertions(+) diff --git a/test/unit/host/hostMarker.test.ts b/test/unit/host/hostMarker.test.ts index 1b285cbf..228bccbb 100644 --- a/test/unit/host/hostMarker.test.ts +++ b/test/unit/host/hostMarker.test.ts @@ -18,6 +18,7 @@ import { } from 'vitest'; import { runHost } from '../../../src/host/hostMain.js'; +import { readProcStat } from '../../../src/host/programGroup.js'; import type * as ProgramGroupModule from '../../../src/host/programGroup.js'; import type { SessionRecord } from '../../../src/protocol/schemas.js'; import { @@ -250,4 +251,66 @@ describe('runHost and the create-failed marker', () => { sendSigterm(); await expectHostStopped(readProgramGroup()); }, 15_000); + + it('stops when the creator writes the marker and exits between its probe and its check', async () => { + const creator = spawn('sleep', ['30'], { stdio: 'ignore' }); + onTestFinished(() => { + creator.kill('SIGKILL'); + }); + const creatorPid = creator.pid as number; + expect(creatorPid).toBeGreaterThan(0); + await runHost(SESSION_ID, creatorPid); + expect(existsSync(socketPath(directory))).toBe(true); + // The next probe finds the creator gone, and it wrote the marker first. + const kill = process.kill.bind(process); + vi.spyOn(process, 'kill').mockImplementation((pid, signal) => { + if (pid === creatorPid && signal === 0) { + writeFileSync(createFailedMarkerPath(directory), ''); + throw Object.assign(new Error('kill ESRCH'), { code: 'ESRCH' }); + } + return kill(pid, signal); + }); + + await expectHostStopped(readProgramGroup()); + }, 15_000); + + // kill(pid, 0) succeeds for a zombie, so only /proc shows that the creator + // has exited while its parent has yet to reap it. + it.runIf(process.platform === 'linux')( + 'stops the watch when its creator is a zombie', + async () => { + const parent = spawn( + '/bin/sh', + ['-c', 'sleep 0 & echo $!; exec sleep 30'], + { stdio: ['ignore', 'pipe', 'ignore'] }, + ); + onTestFinished(() => { + parent.kill('SIGKILL'); + }); + const [line] = (await once(parent.stdout, 'data')) as [Buffer]; + const zombie = Number(line.toString('utf8').trim()); + expect(zombie).toBeGreaterThan(1); + const deadline = Date.now() + 10_000; + while (readProcStat(zombie)?.state !== 'Z') { + expect(Date.now()).toBeLessThan(deadline); + await delay(20); + } + const watchStopped = trackMarkerWatch(); + await runHost(SESSION_ID, zombie); + expect(existsSync(socketPath(directory))).toBe(true); + await watchStopped(); + + await writeCreateFailedMarker( + createFailedMarkerPath(directory), + SESSION_ID, + ); + + expect((await readManifest(manifestPath(directory))).status).toBe( + 'running', + ); + sendSigterm(); + await expectHostStopped(readProgramGroup()); + }, + 20_000, + ); }); From e030d75d61f752dd0b623a08c45321748bebcc5b Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 11:48:37 +0000 Subject: [PATCH 25/28] fix(host): count a zombie creator as exited in the marker watch kill(pid, 0) finds a zombie until its parent reaps it, so the watch ticked at 10 Hz for as long as a parent that never waits lived. The watch now also counts a creator that readProcStat shows as Z as exited. facts.mjs reads the new probe, and the docs name it. --- .agents/skills/verify-session-lifecycle/SKILL.md | 2 +- .agents/skills/verify-session-lifecycle/scripts/facts.mjs | 6 +++--- src/host/README.md | 2 +- src/host/hostMain.ts | 8 ++++++-- 4 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 09adaa35..fc3d465d 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -402,7 +402,7 @@ Now the catch of the readiness wait first writes an empty marker, `/cre The order of the marker write and the manifest read closes the race only while that read works. When the host's start-up write and its marker check came before `create` gave up, the host listens without the marker, and `create` reads the manifest to send the SIGTERM. When that read fails, for example on an unreadable file, `create` on Windows takes the manifest as naming no program and sends nothing, and the host serves the failed session. -Now `runHost` starts `watchCreateFailed` right after its start-up check. Every 100 ms it checks whether its creator still runs and then whether the marker exists. On the marker it calls `startShutdown`, as for a SIGTERM. Once a check after the creator's exit found no marker, it stops: `create` writes the marker before it exits, so no marker comes later. A liveness probe that throws, such as EPERM from a process of another user that took the creator's pid, counts as an exited creator, so no error leaves the timer and ends the host. In the model, `CreateStopsHostOnWindows` reads the manifest or fails to read it, and `HostPollsMarker` is the watch from `"sockdir"` on. `mutant-HostPollsCreateFailed-win32` breaks R17, and `mutant-HostPollsCreateFailed` passes, because off Windows the SIGTERM does not need the read. The integration test `a create on Windows whose manifest read fails after it gave up` holds the host's socket-directory `mkdir` until `create` has exited and makes `create`'s manifest reads fail once the marker exists. +Now `runHost` starts `watchCreateFailed` right after its start-up check. Every 100 ms it checks whether its creator still runs and then whether the marker exists. On the marker it calls `startShutdown`, as for a SIGTERM. Once a check after the creator's exit found no marker, it stops: `create` writes the marker before it exits, so no marker comes later. A liveness probe that throws, such as EPERM from a process of another user that took the creator's pid, counts as an exited creator, so no error leaves the timer and ends the host. So does a zombie creator, which `kill(pid, 0)` still finds until its parent reaps it: `readProcStat` shows it as `Z` on Linux. In the model, `CreateStopsHostOnWindows` reads the manifest or fails to read it, and `HostPollsMarker` is the watch from `"sockdir"` on. `mutant-HostPollsCreateFailed-win32` breaks R17, and `mutant-HostPollsCreateFailed` passes, because off Windows the SIGTERM does not need the read. The integration test `a create on Windows whose manifest read fails after it gave up` holds the host's socket-directory `mkdir` until `create` has exited and makes `create`'s manifest reads fail once the marker exists. ### `CreateRetriesMarker`: on Windows, a failed marker write leaves a host serving a failed create (R17) diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 8fdaab11..525f9858 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -416,8 +416,8 @@ function retriesMarker(body) { // runHost's watchCreateFailed checks, every CREATE_FAILED_POLL_INTERVAL_MS, // whether the creator still runs and then whether the create-failed marker -// exists. A probe that throws counts as an exited creator, so no error leaves -// the timer. On the marker it calls startShutdown, and it stops once a check +// exists. A probe that throws, and a zombie creator, count as an exited +// creator, so no error leaves the timer. On the marker it calls startShutdown, and it stops once a check // after the creator's exit found none. The start-up try calls it right after // the check that follows the start-up write. function pollsCreateFailed() { @@ -426,7 +426,7 @@ function pollsCreateFailed() { const watches = watch >= 0 && normalize(run.statements[watch].getText().replace(/\/\/[^\n]*/g, '')) === - 'const watchCreateFailed = (): void => { const timer = setInterval(() => { let creatorGone = true; try { creatorGone = !isProcessAlive(creatorPid); } catch { } if (existsSync(createFailedMarkerPath(sessDir))) { clearInterval(timer); startShutdown(); } else if (creatorGone) { clearInterval(timer); } }, CREATE_FAILED_POLL_INTERVAL_MS); timer.unref(); };'; + "const watchCreateFailed = (): void => { const timer = setInterval(() => { let creatorGone = true; try { creatorGone = !isProcessAlive(creatorPid) || readProcStat(creatorPid)?.state === 'Z'; } catch { } if (existsSync(createFailedMarkerPath(sessDir))) { clearInterval(timer); startShutdown(); } else if (creatorGone) { clearInterval(timer); } }, CREATE_FAILED_POLL_INTERVAL_MS); timer.unref(); };"; const last = run.statements.at(-1); const tried = last !== undefined && ts.isTryStatement(last) diff --git a/src/host/README.md b/src/host/README.md index 16e0f424..e52580d3 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -80,7 +80,7 @@ - `runHost` spawns the PTY with `createPty` (`src/pty/createPty.ts`), writes input to it, resizes it and kills it on idle timeout and shutdown. It writes `TerminalQueryResponder` replies to the PTY without logging them. [hostMain.ts:runHost] - `runHost` polls `session.json` with `readManifestIfExists` and probes the creator process with `isProcessAlive` until the manifest appears or the creator exits. It writes `session.json` through `createSerialManifestWriter`, creates the socket directory with mode `0o700` and listens with `RpcServer` through `listenInSocketDirectory` and writes snapshot and screenshot artifacts through `src/snapshot/capture.ts` and `src/screenshot/capture.ts`. [hostMain.ts:runHost] - `runHost` registers a `process.on('SIGTERM')` handler that starts shutdown, sends signals to the child with `process.kill` and starts `setInterval` timers for idle and wait polling. [hostMain.ts:runHost] -- `runHost` checks for the `create-failed` marker with `existsSync` before it spawns the program, and returns when it finds it. It checks again right after its start-up manifest write, before it listens, and then shuts down. From there on, `watchCreateFailed` checks for the marker every `CREATE_FAILED_POLL_INTERVAL_MS` (100 ms) while the creator process lives and once after it exited (a liveness probe that throws, such as EPERM from a process of another user that took the pid, counts as exited), and starts the shutdown when it finds the marker. [hostMain.ts:runHost] +- `runHost` checks for the `create-failed` marker with `existsSync` before it spawns the program, and returns when it finds it. It checks again right after its start-up manifest write, before it listens, and then shuts down. From there on, `watchCreateFailed` checks for the marker every `CREATE_FAILED_POLL_INTERVAL_MS` (100 ms) while the creator process lives and once after it exited (a liveness probe that throws, such as EPERM from a process of another user that took the pid, and a zombie creator that `readProcStat` shows as `Z` count as exited), and starts the shutdown when it finds the marker. [hostMain.ts:runHost] - `runHost` rethrows a PTY-ingestion, event-log append, exit-handling or shutdown error in `process.nextTick`. The uncaught exception crashes the host process. [hostMain.ts:rethrowAsync] - `resolveHostRendererName` reads `process.env.AGENT_TTY_HOST_RENDERER` and `process.env.AGENT_TTY_RENDERER`. [hostMain.ts:resolveHostRendererName] - `EventLog.open` opens the file in append mode and runs `chmod 0o600`. `append` writes with `fileHandle.appendFile`, one call at a time. `close` calls `fileHandle.sync()` and then closes the file. [eventLog.ts:EventLog] diff --git a/src/host/hostMain.ts b/src/host/hostMain.ts index 192a7383..f2ec81e9 100644 --- a/src/host/hostMain.ts +++ b/src/host/hostMain.ts @@ -20,6 +20,7 @@ import { createSerialManifestWriter } from './manifestWriter.js'; import { captureProgram, programWithoutToken, + readProcStat, stopProgramGroup, writeProgramRecord, } from './programGroup.js'; @@ -1280,10 +1281,13 @@ export async function runHost( const watchCreateFailed = (): void => { const timer = setInterval(() => { // An error of the probe, such as EPERM from a process of another user - // that took the pid, means that the creator has exited. + // that took the pid, means that the creator has exited. So does a + // zombie, which kill(pid, 0) still finds until its parent reaps it. let creatorGone = true; try { - creatorGone = !isProcessAlive(creatorPid); + creatorGone = + !isProcessAlive(creatorPid) || + readProcStat(creatorPid)?.state === 'Z'; } catch { // creatorGone stays true. } From 600068767cdd569989da2970ab50d9847998cb1c Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 12:50:16 +0000 Subject: [PATCH 26/28] chore(skills): sync the lifecycle coverage record after the zombie check --- .agents/skills/verify-session-lifecycle/coverage.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index ed875149..94b58db2 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -139,12 +139,12 @@ "src/storage/manifests.ts#writeCreateFailedMarker": "587c8047e563db4e", "src/storage/manifests.ts#writeEmptyMarker": "143325689100f36c", "src/protocol/sessionStatusPolicy.ts#SESSION_STATUS_POLICIES": "83827f9f7f6b8e1d", - "src/host/hostMain.ts#runHost(parts)": "e3879ee94370dcfd", + "src/host/hostMain.ts#runHost(parts)": "7bd4c6553a831b9d", "src/host/hostMain.ts#runHost(final try)": "e0615a9709fefb67", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", "skill:model/SessionLifecycle.tla": "7f1c6dd7943968c3", - "skill:scripts/facts.mjs": "07dba02a98497dcb", + "skill:scripts/facts.mjs": "6ee4da3ef9b6bac3", "skill:scripts/check.sh": "b48bc5fd343aefb5" }, "callSites": { From 968edc5a777c7b52892b9d35cc05209a6477eb64 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 13:40:14 +0000 Subject: [PATCH 27/28] ci: give the lifecycle-model shares 90 minutes The model of #324 has about twice the states of main's. On its head the four shares took 38, 40, 46 and 48 min of the 50 min timeout, and a share cannot be shorter than its longest run. --- .github/workflows/ci.yml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 2852aa39..65c92028 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -221,13 +221,15 @@ jobs: # Model-checks the session lifecycle with the verify-session-lifecycle # skill. Share 1 checks that coverage.json matches the facts and the - # covered code. The TLC runs took 63 min in one job of 4 vCPUs and take 13 - # to 17 min in each of 4 shares. They run only when coverage.json differs - # from the base, which every change to the model, its scripts, the covered - # code or a fact needs. + # covered code. The TLC runs took 63 min in one job of 4 vCPUs and took 13 + # to 17 min in each of 4 shares. The model of #324 has about twice the + # states: its shares took 38 to 48 min, and a share cannot be shorter than + # its longest run, so the job has 90 min. They run only when coverage.json + # differs from the base, which every change to the model, its scripts, the + # covered code or a fact needs. lifecycle-model: runs-on: ubuntu-latest - timeout-minutes: 50 + timeout-minutes: 90 strategy: fail-fast: false matrix: From a3e6590ff4fc3dbae8bdf590e8d174d3e0b5c26b Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 13:43:32 +0000 Subject: [PATCH 28/28] ci: split the lifecycle-model job into 8 shares that start all their runs at once A timeout raise alone leaves #324's 48 min share at the merge queue's 60 min limit. check.sh waits for each batch of CHECK_JOBS runs, so a share took the sum of its longest runs. With 8 shares and CHECK_JOBS 12, every share starts all its runs at once and takes about as long as its longest run. The job timeout goes to 45 min. --- .github/workflows/ci.yml | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 65c92028..9d08c4a7 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -223,18 +223,21 @@ jobs: # skill. Share 1 checks that coverage.json matches the facts and the # covered code. The TLC runs took 63 min in one job of 4 vCPUs and took 13 # to 17 min in each of 4 shares. The model of #324 has about twice the - # states: its shares took 38 to 48 min, and a share cannot be shorter than - # its longest run, so the job has 90 min. They run only when coverage.json - # differs from the base, which every change to the model, its scripts, the - # covered code or a fact needs. + # states, and its 4 shares took 38 to 48 min. check.sh starts CHECK_JOBS + # runs at a time and waits for all of them before the next ones, so a share + # took as long as the sum of its longest runs. Now each of 8 shares starts + # all its runs at once (with the model of #324, 10 to 12 runs, of which at + # most 2 are long, on 4 vCPUs) and takes about as long as its longest run. + # They run only when coverage.json differs from the base, which every + # change to the model, its scripts, the covered code or a fact needs. lifecycle-model: runs-on: ubuntu-latest - timeout-minutes: 90 + timeout-minutes: 45 strategy: fail-fast: false matrix: - shard: [1, 2, 3, 4] - name: lifecycle-model (${{ matrix.shard }}/4) + shard: [1, 2, 3, 4, 5, 6, 7, 8] + name: lifecycle-model (${{ matrix.shard }}/8) steps: - name: Check out repository uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6 @@ -269,8 +272,8 @@ jobs: - name: Model-check the session lifecycle if: steps.inputs.outputs.tlc == 'true' env: - CHECK_JOBS: '4' - CHECK_SHARD: ${{ matrix.shard }}/4 + CHECK_JOBS: '12' + CHECK_SHARD: ${{ matrix.shard }}/8 run: .agents/skills/verify-session-lifecycle/scripts/check.sh quality-gates: