diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index a6d2c87c..53886fa8 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -62,13 +62,13 @@ From the repo root: .agents/skills/verify-session-lifecycle/scripts/check.sh ``` -It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. On this repo it takes about eleven minutes with the default `CHECK_JOBS` of 4. Eight runs explore the whole model, so `CHECK_JOBS=69` 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. Eight runs explore the whole model, so `CHECK_JOBS=71` 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 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-one 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 69 times and prints one line per run. +3. It runs TLC 71 times and prints one line per run. 4. It compares the hashes and call sites with `coverage.json`. Exit codes: 0 means every run gave the expected result and the covered code matches the sync record. 1 means at least one run gave an unexpected result; the line says `UNEXPECTED`. 3 means every result was as expected, but covered code changed since the sync commit; that is not a pass, so follow "When you change covered code on purpose". 2 means a tool could not run. When both 1 and 3 apply, the exit code is 1. @@ -77,23 +77,24 @@ Exit codes: 0 means every run gave the expected result and the covered code matc At the sync commit, the expected results are: -| Runs | Expected | Why | -| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -| `current`, the code as it is with the program's session token, every rule | pass | No order of the modelled steps breaks a rule. This is the run that catches a new bug. | -| `current-no-token`, the code as it is without a token, R1 to R14 and R17 to R19 | pass | The same for a session whose `program.json` holds no token: on macOS, on a kernel without autogroups, when the capture read none, and for a session that an older agent-tty created. Every kill then falls back to the id that a manifest or the host's own record names. R15 and R16 are what the token adds, so this run leaves them out (see Scope). | -| `current-unseen`, the code as it is with a token and a program that no scan of `/proc` shows, every rule | pass | A fork chain: each process of the program forks its successor and ends between scans, so the kill through the token sees a member only once the group is frozen. | -| `witness-*` without a suffix | violated | Each witness is a state that must be reachable: a `create` that gave up recorded the session destroyed, gc removes a session, a session serves, a resize lands, a clean exit is recorded, a crash is reconciled, a plain destroy completes, a SIGTERM shutdown is recorded, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` (which ends with `HOST_TIMEOUT` and leaves the session destroying) and `destroy --force` (which ends with `HOST_TIMEOUT` too), a process that the program left meets the kill of `destroy`, an unrelated group has the program's group id when `destroy --force` kills, `destroy --force` stops a program that only `program.json` names, a program whose host died before `program.json` named it outlives `destroy`, a wait of `destroy` through `program.json` reads the group gone while an unrelated group holds its id, a reconcile writes destroyed again over the failed that it wrote, `destroy --force` reaches its kill while a process that took the ended host's pid runs, and `destroy --force` reaches its kill while a live host has not written `host.json` yet. A witness that passes means the model can no longer reach that state, and the passing rules prove nothing. | -| `witness-*-no-token` | violated | Eight of those states without a token: a `create` that gave up recorded the session destroyed, a crash is reconciled, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` and `destroy --force`, and a reconcile writes destroyed again over the failed that it wrote. They show that `current-no-token` reaches the fallback kill and the EPERM probe. | -| `mutant-CreateRecordsHostPid`, `mutant-HostWaitsForManifest`, `mutant-ReconcileRereads`, `mutant-HostSerializesWrites`, `mutant-ReconcileSkipsLiveHost`, `mutant-HostStopsAfterTerminalWrite`, `mutant-DestroyRecordsDestroyed`, `mutant-DestroyKeepsExitCode`, `mutant-ManifestWriteNeedsFolder`, `mutant-KillsProgramGroup`, `mutant-HostWaitsForGroup`, `mutant-ReconcileWaitsForGroup`, `mutant-ReRunsInNewSession`, `mutant-InsideCheckReadsEnv`, `mutant-RecordsProgramSync`, `mutant-ProvesGroupOwnership`, `mutant-DestroyStopsLeftovers`, `mutant-FallbackNeedsFolder`, `mutant-ReconcileRepairsDestroyed`, `mutant-CreateStopsOnGiveUp`, `mutant-TokenNamesProgram`, `mutant-ProvesHostPid`, `mutant-GcBothChecks`, `mutant-ShutdownBothChecks` | violated | Each run removes a guard from the model and checks only the rule that the guard protects. That rule must break, which shows the check can fail. | -| `mutant-ProbeCountsDeniedGroup-no-token`, `mutant-KillsProgramGroup-no-token`, `mutant-HostWaitsForGroup-no-token`, `mutant-ReconcileWaitsForGroup-no-token` | violated | The same without a token. The fallback depends on these guards as the code before `program.json` did. With a token, the token check reads a process of another user in view, so only this path checks `ProbeCountsDeniedGroup`. | -| `mutant-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-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. | -| `current-otherspace`, the code as it is with `destroy`, `list` and `gc` in another pid space than the host, every rule | pass | `OtherPidSpace`: no scan and no probe of those commands shows the program's processes, as without `/proc`, with an empty `/proc`, in another pid namespace or on another machine. | -| `witness-WitnessUnsharedDestroyCompletes-otherspace` | violated | A plain `destroy` from another pid space still reports success, because it trusts the host's `destroyed` record. | -| `mutant-UnsharedGroupReadsUnknown-otherspace` | violated | R16: without the guard, the group reads gone where nothing shows it, and `destroy` of an exited session records destroyed while a process that the program left runs. | +| Runs | Expected | Why | +| --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | -------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `current`, the code as it is with the program's session token, every rule | pass | No order of the modelled steps breaks a rule. This is the run that catches a new bug. | +| `current-no-token`, the code as it is without a token, R1 to R14 and R17 to R19 | pass | The same for a session whose `program.json` holds no token: on macOS, on a kernel without autogroups, when the capture read none, and for a session that an older agent-tty created. Every kill then falls back to the id that a manifest or the host's own record names. R15 and R16 are what the token adds, so this run leaves them out (see Scope). | +| `current-unseen`, the code as it is with a token and a program that no scan of `/proc` shows, every rule | pass | A fork chain: each process of the program forks its successor and ends between scans, so the kill through the token sees a member only once the group is frozen. | +| `witness-*` without a suffix | violated | Each witness is a state that must be reachable: a `create` that gave up recorded the session destroyed, gc removes a session, a session serves, a resize lands, a clean exit is recorded, a crash is reconciled, a plain destroy completes, a SIGTERM shutdown is recorded, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` (which ends with `HOST_TIMEOUT` and leaves the session destroying) and `destroy --force` (which ends with `HOST_TIMEOUT` too), a process that the program left meets the kill of `destroy`, an unrelated group has the program's group id when `destroy --force` kills, `destroy --force` stops a program that only `program.json` names, a program whose host died before `program.json` named it outlives `destroy`, a wait of `destroy` through `program.json` reads the group gone while an unrelated group holds its id, a reconcile writes destroyed again over the failed that it wrote, a reconcile's first read writes destroyed over a marked terminal manifest, `destroy --force` reaches its kill while a process that took the ended host's pid runs, and `destroy --force` reaches its kill while a live host has not written `host.json` yet. A witness that passes means the model can no longer reach that state, and the passing rules prove nothing. | +| `witness-*-no-token` | violated | Eight of those states without a token: a `create` that gave up recorded the session destroyed, a crash is reconciled, an exited session is destroyed, `destroy --force` records a live session as destroyed, a program outlives its host, a process of another user outlives a plain `destroy` and `destroy --force`, and a reconcile writes destroyed again over the failed that it wrote. They show that `current-no-token` reaches the fallback kill and the EPERM probe. | +| `mutant-CreateRecordsHostPid`, `mutant-HostWaitsForManifest`, `mutant-ReconcileRereads`, `mutant-HostSerializesWrites`, `mutant-ReconcileSkipsLiveHost`, `mutant-HostStopsAfterTerminalWrite`, `mutant-DestroyRecordsDestroyed`, `mutant-DestroyKeepsExitCode`, `mutant-ManifestWriteNeedsFolder`, `mutant-KillsProgramGroup`, `mutant-HostWaitsForGroup`, `mutant-ReconcileWaitsForGroup`, `mutant-ReRunsInNewSession`, `mutant-InsideCheckReadsEnv`, `mutant-RecordsProgramSync`, `mutant-ProvesGroupOwnership`, `mutant-DestroyStopsLeftovers`, `mutant-FallbackNeedsFolder`, `mutant-ReconcileRepairsDestroyed`, `mutant-CreateStopsOnGiveUp`, `mutant-TokenNamesProgram`, `mutant-ProvesHostPid`, `mutant-GcBothChecks`, `mutant-ShutdownBothChecks` | violated | Each run removes a guard from the model and checks only the rule that the guard protects. That rule must break, which shows the check can fail. | +| `mutant-ProbeCountsDeniedGroup-no-token`, `mutant-KillsProgramGroup-no-token`, `mutant-HostWaitsForGroup-no-token`, `mutant-ReconcileWaitsForGroup-no-token` | violated | The same without a token. The fallback depends on these guards as the code before `program.json` did. With a token, the token check reads a process of another user in view, so only this path checks `ProbeCountsDeniedGroup`. | +| `mutant-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-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. | +| `current-otherspace`, the code as it is with `destroy`, `list` and `gc` in another pid space than the host, every rule | pass | `OtherPidSpace`: no scan and no probe of those commands shows the program's processes, as without `/proc`, with an empty `/proc`, in another pid namespace or on another machine. | +| `witness-WitnessUnsharedDestroyCompletes-otherspace` | violated | A plain `destroy` from another pid space still reports success, because it trusts the host's `destroyed` record. | +| `mutant-UnsharedGroupReadsUnknown-otherspace` | violated | R16: without the guard, the group reads gone where nothing shows it, and `destroy` of an exited session records destroyed while a process that the program left runs. | 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`. @@ -417,6 +418,24 @@ wait node -e 'console.log(require(process.argv[1]).status)' "$AGENT_TTY_HOME/sessions/$id/session.json" # destroyed ``` +### `ReconcileRepairsMarked`: a marked session that a killed reconcile left `failed` + +`ReconcileRepairsDestroyed` repairs a destroyed record in the reconcile that replaced it, right after its own write. A reconcile process that was killed between that write and the repair left `failed`, after `destroy` had printed `destroyed: true`, and every later reconcile skipped the terminal manifest (coder/agent-tty#265). A `destroy` of an ended session that failed after its marker write left the marker next to `exited` or `failed` the same way. + +Now `reconcileSession` first checks a terminal manifest other than destroyed for the marker. When the marker is there, `writeMarkedDestroyed` writes destroyed from that copy, with `hostPid` and `childPid` null, the exit code kept and no failure fields, and the reconcile unlinks the socket, which a `destroy` whose write failed left, and returns. Only a `destroy` writes the marker, after it stopped the session and right before its destroyed write, so the marker means that `destroy` chose destroyed. `scanHome` skips a session with the marker, so `home list` and the dashboard picker do not count it while its manifest reads `failed`. The replay holds the repair write of the reconcile in `list` and kills that process: + +```sh +id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'exec cat' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))') +kill -KILL "$(node -e 'console.log(require(process.argv[1]).hostPid)' "$AGENT_TTY_HOME/sessions/$id/session.json")" +LOG=$(mktemp) +REPLAY_LOG=$LOG REPLAY_HOLD='list:rename:/session.json:1:4000,list:rename:/session.json:2:60000' NODE_OPTIONS="$HOLD" node --import tsx src/cli/main.ts list --json >/dev/null & +until grep -q 'hold rename' "$LOG"; do sleep 0.1; done +node --import tsx src/cli/main.ts destroy "$id" --force --json # ok: true, destroyed: true +until [ "$(grep -c 'hold rename' "$LOG")" -ge 2 ]; do sleep 0.1; done +kill -KILL $! # the reconcile dies before its repair +node --import tsx src/cli/main.ts list --all --json # the session reads destroyed +``` + ### `TokenNamesProgram`: a token that no member of the group carries (R16) node-pty returns before the program calls `setsid()`, so the first reads of the program often show the host's own session and autogroup. Without the guard, `captureToken` could keep an autogroup that it read before the program's `setsid()`, while its next read of the program's stat already showed the new session. The record then held the host's autogroup. No member of the program's group carries that id, so every kill through the record killed nothing and every wait through it read the group gone. `destroy` then recorded destroyed while a process of the program's group ran. @@ -485,7 +504,7 @@ To bring the check back in line after changes that skipped it, use `/maintain-fo ## Scope -The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 23,479,528 distinct states, and without one 22,893,820. The check prints both counts. +The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 25,534,376 distinct states, and without one 24,675,744. The check prints both counts. It assumes: @@ -503,7 +522,7 @@ It assumes: - A program can outlive its host: the PTY closes with the host and sends the program SIGHUP, which a program can ignore. The model keeps such a program running until a kill of its group ends it, the worst case for R11. A SIGKILL of the group ends every process of our user in it at once. - A process of another user can run in the program's group, such as the root child of `sudo cmd &`. Our SIGKILL does not reach it, and once only such processes are left, `kill(-pgid)` fails with EPERM. `isProcessGroupAlive` reads EPERM as alive unless `/proc` shows only zombies of the group, and `killProcessGroupBestEffort` ignores it. While such a process runs, three things take about 5 seconds, the length of `waitForProcessesToExit`. The host waits that long after the program's exit, then leaves the manifest destroying and ends. `destroy` and `destroy --force` end with `HOST_TIMEOUT`. Every reconcile of the session (`list`, `inspect`, `gc`, the dashboard) waits that long and writes nothing. The model lets each wait give up at any poll that reads the group alive. With a token, the model lets such a process carry the token in view. Where `/proc` hides or refuses it, the token check reads it through `isProcessGroupAlive`, which reads it alive in the same states while `ProbeCountsDeniedGroup` holds. - A killed process stays a zombie until its parent, or init once its parent has died, reaps it, and `kill(-pgid, 0)` still finds a zombie. On Linux, `isProcessGroupAlive` then reads `/proc//stat` of every process and reads the group gone when two scans in a row each show processes of it and only zombies, because a process can fork and end while one scan runs. When a scan shows no process of the group, the probe decides: EPERM reads alive and a found group reads gone. So a group whose last processes are never reaped, as under a container's PID 1 without an init, reads gone. A process whose main thread called `pthread_exit` while another thread runs also shows Z there, so `readProcStat` reads `/proc//task` of every process that shows Z and gives it the state of a thread that is not a zombie. Such a process counts as live in the scan and in the token check, where it can carry the token. On macOS it does not scan, so a zombie still reads alive until launchd reaps it. The model has no zombies: a killed process ends at once. A process that `/proc` refuses to show, as `hidepid=1` (EPERM) or a security module (EACCES) does for other users, reads alive. With `hidepid=2` or `hidepid=4` (`invisible` and `ptraceable` on newer kernels), `/proc` can leave such a process out of its listing, so the probe reads the last `/proc` line of `/proc/self/mountinfo`, skips the scan and reads a group with a zombie alive, as on macOS. With a token, neither a zombie nor a process that `/proc` refuses to show witnesses the token. When no live member is in view, `isProgramGroupAlive` reads the group as `isProcessGroupAlive` does, with the zombie scan, the refused reads and the same `hidepid` check. So under any of those `hidepid` modes, a group that a process of another user took after the program's group ended reads alive, and `destroy` ends with `HOST_TIMEOUT` until that process ends. -- A destroy that lands between reconcile's last read and its write is still overwritten with failed, for the time until that reconcile finds the destroy marker and writes destroyed again (`ReconcileRepairsDestroyed`). A `list` or `gc` that reads in that time sees `failed`, a terminal status, so gc can remove the folder as it would remove a destroyed one. A reconcile whose process dies in that time leaves `failed`, because every later reconcile skips a terminal manifest. The model has no crash of a reconciling process. +- A destroy that lands between reconcile's last read and its write is still overwritten with failed, for the time until that reconcile finds the destroy marker and writes destroyed again (`ReconcileRepairsDestroyed`). A `list` or `gc` that reads in that time sees `failed`, a terminal status, so gc can remove the folder as it would remove a destroyed one. A reconcile whose process dies in that time leaves `failed` until the next reconcile reads it: that read finds the marker and writes destroyed (`ReconcileRepairsMarked`). `home list` and the dashboard count a session with the marker as destroyed, also in that time. The model has no crash of a reconciling process, so it checks that the repair at the read breaks no rule, not that it heals the crash. - The idle time-out calls the same `hangUpProgram` as `initiateShutdown`: SIGHUP, then the group kill after `SHUTDOWN_KILL_GRACE_MS`. When the program exits on that SIGHUP, `handlePtyExit` kills the group too, so a process that ignores SIGHUP does not outlive the idle time-out. An idle time-out still ends exited. When the check cannot run (`unknown`), the idle kill sends nothing, and the session ends exited with that process running, as after a program that exits on its own and leaves a process (coder/agent-tty#222). The model leaves both group kills out: they go through `stopProgramGroup` like every kill, and a process that outlives them is one that the program left, which the model keeps after a normal exit anyway. - Windows has no process groups, so there `processGroupTarget` gives the program's pid, and every kill reaches only that process. `destroy` never re-runs on Windows. There SIGTERM ends the host at once, so a `create` that gives up stops its host only once the manifest names the program, and the next reconcile records `failed` and ends the program. Before that write, `create` leaves the host alone. `CreateStopsOnGiveUp` checks the stop for Linux and macOS. - A destroy that the program runs, or that someone types into the program's interactive shell, runs inside the program's session, and `rerunInNewSession` runs it again in a new session. The model lets such a destroy start while the program's leader runs, and assumes that it kept `AGENT_TTY_SESSION_ID`, which every process of the program inherits at spawn. A destroy whose environment lost the variable, or whose `create --env` overrode it, is seen through the id comparison only. On Linux that compares the CLI's session id with `childPid`, so it misses such a destroy only before the host's start-up write. Other POSIX systems compare the process group and the controlling terminal, through `/bin/ps`. A terminal is the controlling terminal of one session and of every process in it, so that also finds a job of an interactive shell, which runs in a group of its own. A process without a controlling terminal is seen only through the group. diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index c6b3ea55..2687578b 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -34,9 +34,11 @@ "src/host/lifecycle.ts#waitForProcessesToExit": "bdab1d674a6856b8", "src/host/lifecycle.ts#stopSessionProcesses": "d1abb608b1d2160a", "src/host/lifecycle.ts#recordDestroyed": "d3a74237a9c8459c", - "src/host/lifecycle.ts#removeDeadHostSocket": "e4044ea706544ff8", + "src/host/lifecycle.ts#removeDeadHostSocket": "34ce07ab7b7e8d7b", "src/host/lifecycle.ts#destroySession": "d840dd07a0e481f5", - "src/host/lifecycle.ts#reconcileSession": "c2904456d54b87c8", + "src/host/lifecycle.ts#isMarkedDestroyed": "d178f4a63473915c", + "src/host/lifecycle.ts#writeMarkedDestroyed": "4863c35f70699757", + "src/host/lifecycle.ts#reconcileSession": "4e5dac8144a0d9fb", "src/host/hostMain.ts#waitForManifestFromCreate": "fd500651f83683eb", "src/host/hostMain.ts#isSessionCommandable": "260060f07b068ec1", "src/host/hostMain.ts#SHUTDOWN_KILL_GRACE_MS": "51171d9c5aa6c510", @@ -87,16 +89,17 @@ "src/host/hostMain.ts#runHost(final try)": "16789dd4e2534bc7", "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542", "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac", - "skill:model/SessionLifecycle.tla": "25bc78980b0d67cd", - "skill:scripts/facts.mjs": "86ec94456c10cb37", - "skill:scripts/check.sh": "422878fda4460ac0" + "skill:model/SessionLifecycle.tla": "f7270faba013acff", + "skill:scripts/facts.mjs": "6ae4fd3279517f42", + "skill:scripts/check.sh": "3a47553300cb217a" }, "callSites": { "writeManifest": [ "src/host/lifecycle.ts#allocateSession", "src/host/lifecycle.ts#reconcileSession", "src/host/lifecycle.ts#reconcileSession", - "src/host/lifecycle.ts#recordDestroyed" + "src/host/lifecycle.ts#recordDestroyed", + "src/host/lifecycle.ts#writeMarkedDestroyed" ], "persistManifest": [ "src/host/hostMain.ts#runHost", @@ -142,6 +145,7 @@ "reconcileSession": [ "src/cli/commands/gc.ts#gcSessions", "src/cli/commands/inspect.ts#runInspectCommand", + "src/cli/commands/inspect.ts#runInspectCommand", "src/host/lifecycle.ts#destroySession", "src/host/lifecycle.ts#destroySession", "src/host/lifecycle.ts#listSessions" diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index 36b6735e..c4909cea 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -90,6 +90,9 @@ CONSTANTS \* destroy marker before destroyed, and a \* reconcile that finds it after its own write \* writes destroyed again + ReconcileRepairsMarked, \* lifecycle.ts: a reconcile that reads a + \* terminal manifest other than destroyed next + \* to the destroy marker writes destroyed CreateStopsOnGiveUp, \* create.ts: a create that gives up on its \* host sends it SIGTERM, so the host stops \* its program and ends the session @@ -139,7 +142,8 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, ReconcileSkipsTerminal, InsideCheckReadsEnv, RecordsProgramSync, ProvesGroupOwnership, DestroyStopsLeftovers, FallbackNeedsFolder, CreateStopsOnGiveUp, - ReconcileRepairsDestroyed, TokenNamesProgram, + ReconcileRepairsDestroyed, ReconcileRepairsMarked, + TokenNamesProgram, ReusedIdReadsGone, ProvesHostPid, FreezesUnseenGroup, UnsharedGroupReadsUnknown} : b \in BOOLEAN @@ -164,6 +168,8 @@ VARIABLES dmark, \* the destroy marker file exists in the session directory rec, \* program.json names the program with its token startFailed, \* ghost: the host died because its files were missing + readRepaired, \* ghost: a reconcile wrote destroyed from its first read + \* next to the destroy marker sock, \* the RPC socket file exists (it is outside the directory) cpc, \* create: "alloc", "write", "launch", "done", "failed" \* (it gave up on its host) @@ -226,7 +232,7 @@ VARIABLES diskVars == <> -ghostVars == <> +ghostVars == <> hostVars == <> groupVars == <> @@ -241,7 +247,7 @@ Init == /\ mcode = FALSE /\ mchild = FALSE /\ wasTerminal = FALSE /\ wasExited = FALSE /\ wasNamed = FALSE /\ dmark = FALSE - /\ rec = FALSE /\ startFailed = FALSE + /\ rec = FALSE /\ startFailed = FALSE /\ readRepaired = FALSE /\ sock = FALSE /\ cpc = "alloc" /\ hostAlive = FALSE /\ hpc = "none" /\ hex = "none" /\ rsz = "none" @@ -391,6 +397,7 @@ CliKillThrough(named) == IF OtherPidSpace THEN NoKill ELSE KillThrough(named) \* The host fails to start because its files are missing or were rewritten. HostFailsToStart == /\ startFailed' = TRUE + /\ readRepaired' = readRepaired /\ hostAlive' = FALSE /\ hpc' = "dead" /\ hex' = IF hex = "none" THEN "none" ELSE "gone" @@ -812,18 +819,29 @@ AfterReconcile(p) == IF p = "gc" THEN "readafter" ELSE "idle" \* isProcessAlive(manifest.hostPid). A null hostPid reads as a dead host. SkipsHost(read) == ReconcileSkipsLiveHost /\ read.pid /\ hostAlive -\* readManifestIfExists; return when it is null or terminal. +\* readManifestIfExists. With ReconcileRepairsMarked, a terminal manifest +\* other than destroyed next to the destroy marker (isMarkedDestroyed) goes +\* to the repair write from this copy ("r_marked"). Otherwise it returns when +\* the manifest is null or terminal. ReconcileReads(p) == /\ pc[p] = "r_read" - /\ IF mst = "none" \/ (ReconcileSkipsTerminal /\ mst \in Terminal) + /\ IF ReconcileRepairsMarked /\ dmark /\ mst \in Terminal + /\ mst # "destroyed" + THEN /\ pc' = [pc EXCEPT ![p] = "r_marked"] + /\ rd' = [rd EXCEPT ![p] = [st |-> mst, pid |-> mpid, + code |-> mcode, child |-> mchild, + grp |-> "none"]] + /\ UNCHANGED <> + ELSE IF mst = "none" \/ (ReconcileSkipsTerminal /\ mst \in Terminal) THEN /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)] - /\ UNCHANGED rd + /\ UNCHANGED <> ELSE /\ pc' = [pc EXCEPT ![p] = "r_check"] /\ rd' = [rd EXCEPT ![p] = [st |-> mst, pid |-> mpid, code |-> mcode, child |-> mchild, grp |-> "none"]] - /\ UNCHANGED <> + /\ UNCHANGED <> + /\ UNCHANGED <> \* After its group kill, reconcileSession waits for the group, or, without \* ReconcileWaitsForGroup, writes at once. @@ -931,6 +949,21 @@ ReconcileRepairs(p) == /\ UNCHANGED <> +\* writeMarkedDestroyed: writeManifest destroyed from the copy that the read +\* took, with hostPid and childPid null and the exit code kept. When gc +\* removed the folder in the meantime, the write throws SESSION_NOT_FOUND, +\* and reconcile returns. Otherwise it unlinks the socket and returns. +ReconcileWritesMarked(p) == + /\ pc[p] = "r_marked" + /\ IF WriteLands + THEN /\ Write("destroyed", FALSE, "none", rd[p].code, FALSE) + /\ pc' = [pc EXCEPT ![p] = "r_unlink"] + /\ readRepaired' = TRUE + ELSE /\ pc' = [pc EXCEPT ![p] = AfterReconcile(p)] + /\ UNCHANGED <> + /\ UNCHANGED <> + \* unlinkIfPresent(socketPath(sessionDirectory)) ReconcileUnlinksSocket(p) == /\ pc[p] = "r_unlink" @@ -1295,7 +1328,7 @@ Next == \/ ReconcileRereadsManifest(p) \/ ReconcileReadsRecord(p) \/ ReconcilePollsGroup(p) \/ ReconcileWrites(p) \/ ReconcileRepairs(p) - \/ ReconcileUnlinksSocket(p) + \/ ReconcileWritesMarked(p) \/ ReconcileUnlinksSocket(p) \/ GcFindsDirectory \/ GcReadsManifest \/ GcReadsReconciled \/ GcFinalRead \/ GcRemoves \/ ListStartsReconcile @@ -1315,7 +1348,7 @@ Spec == Init /\ [][Next]_vars TypeOK == /\ dmark => dir /\ {dir, mpid, mchild, wasTerminal, wasExited, wasNamed, dmark, startFailed, - sock, + readRepaired, sock, hostAlive, prog, foreign, sig, dforce, dinside, dsaw, dkill, rec, left, reused, hitUnrelated, diedUnrecorded, passedReused, hrec, hreused, hitUnrelatedHost} @@ -1446,6 +1479,7 @@ NoUnrelatedHostKilled == ~hitUnrelatedHost WitnessGcRemovesSession == gres # "removed" WitnessReconcileRepairs == ~(dmark /\ mst = "failed" /\ \E p \in Readers : pc[p] = "r_repair") +WitnessMarkedRepaired == ~readRepaired 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 b80959ee..7916c000 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/check.sh +++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh @@ -122,7 +122,7 @@ TERMINAL=$(node -e ' const c = JSON.parse(require("node:fs").readFileSync(process.argv[1], "utf8")).constants; console.log("{" + c.Terminal.map((s) => JSON.stringify(s)).join(", ") + "}"); ' "$OUT/facts.json") -GUARDS="GcSkipsNonCollectable GcFinalCheck ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed CreateStopsOnGiveUp TokenNamesProgram ReusedIdReadsGone ProvesHostPid 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 TokenNamesProgram ReusedIdReadsGone ProvesHostPid 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 WitnessWaitPassesReusedId WitnessReusedHostMeetsKill WitnessUnrecordedHostMeetsKill" +WITNESSES="WitnessGcRemovesSession WitnessCreateGivesUp WitnessSessionServes WitnessResizeLands WitnessCleanExitRecorded WitnessCrashReconciled WitnessDestroyCompletes WitnessSigtermRecorded WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessLeftoverMeetsDestroy WitnessReusedIdMeetsKill WitnessRecordNamesProgram WitnessUnrecordedProgramOutlives WitnessReconcileRepairs WitnessMarkedRepaired WitnessWaitPassesReusedId WitnessReusedHostMeetsKill WitnessUnrecordedHostMeetsKill" # --- runs ---------------------------------------------------------------- @@ -207,6 +207,7 @@ write_run mutant-CreateStopsOnGiveUp violated FailedCreateStopped "CreateStopsOn write_run mutant-TokenNamesProgram violated DestroyedSessionStopped "TokenNamesProgram=FALSE" "with the host's autogroup as the token, no member carries it, and destroy records destroyed while the program's group runs" DestroyedSessionStopped write_run mutant-ReusedIdReadsGone pass WitnessWaitPassesReusedId "ReusedIdReadsGone=FALSE" "with a group that took the id read alive, no wait of destroy passes while that group runs" write_run mutant-ProvesHostPid violated NoUnrelatedHostKilled "ProvesHostPid=FALSE" "without the start-up record, destroy --force kills a process that took the host's pid" NoUnrelatedHostKilled +write_run mutant-ReconcileRepairsMarked pass DestroyedStaysDestroyed "ReconcileRepairsMarked=FALSE" "redundant in the model: it has no crash of a reconciling process, so the repair after the reconcile's own write always runs" write_run mutant-ReconcileSkipsTerminal pass RecordedExitKept "ReconcileSkipsTerminal=FALSE" "redundant: the re-read returns on a terminal manifest" write_run mutant-GcSkipsNonCollectable pass NoLiveSessionDeleted "GcSkipsNonCollectable=FALSE" "redundant: the final check still skips" write_run mutant-GcFinalCheck pass NoLiveSessionDeleted "GcFinalCheck=FALSE" "redundant: the first check still skips" diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index e59d599f..aaec7eaa 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -464,12 +464,36 @@ function repairFacts() { 'src/storage/manifests.ts', 'writeDestroyMarker', ).getText(); + const reconcile = requireDeclaration(lifecycle, 'reconcileSession').body; + const marked = indexOfStatement( + reconcile, + /^if \(manifest !== null && isMarkedDestroyed\(sessionDirectory, manifest\)\) \{\s*if \(await writeMarkedDestroyed\(manifestFile, manifest\)\) \{\s*const socketFile = socketPath\(sessionDirectory\);\s*await unlinkIfPresent\(socketFile\);\s*await removeSocketDirectoryIfEmpty\(socketFile\);\s*\}\s*return;\s*\}$/, + ); + const markedCheck = normalize( + requireDeclaration(lifecycle, 'isMarkedDestroyed').body.getText(), + ); + const terminal = guardIndex( + reconcile, + 'manifest === null || isTerminalSessionStatus(manifest.status)', + ts.SyntaxKind.ReturnStatement, + ); + const rewrite = normalize( + requireDeclaration(lifecycle, 'writeMarkedDestroyed').body.getText(), + ); return { ReconcileRepairsDestroyed: marks && repairs && marker.includes("await replaceFileAtomic(path, '')") && !marker.includes('mkdir'), + ReconcileRepairsMarked: + marked >= 0 && + marked < terminal && + markedCheck === + '{ return ( isTerminalSessionStatus(manifest.status) && !isDestroyedSessionStatus(manifest.status) && existsSync(destroyMarkerPath(sessionDirectory)) ); }' && + rewrite.includes( + "await writeManifest(manifestFile, { ...rest, status: 'destroyed',", + ), }; } @@ -1318,6 +1342,8 @@ const COVERED = [ ['src/host/lifecycle.ts', 'recordDestroyed'], ['src/host/lifecycle.ts', 'removeDeadHostSocket'], ['src/host/lifecycle.ts', 'destroySession'], + ['src/host/lifecycle.ts', 'isMarkedDestroyed'], + ['src/host/lifecycle.ts', 'writeMarkedDestroyed'], ['src/host/lifecycle.ts', 'reconcileSession'], ['src/host/hostMain.ts', 'waitForManifestFromCreate'], ['src/host/hostMain.ts', 'isSessionCommandable'], diff --git a/docs/USAGE.md b/docs/USAGE.md index 06ca6ecc..57565482 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -320,8 +320,8 @@ The session's terminal is closed by then, so redirect stdout to keep the result, Ctrl-C or SIGTERM to that `destroy` reaches the copy outside the session too, and the `destroy` then exits as the copy did, 130 or 143. A destroy request that already reached the host still ends the session. When `destroy` records `destroyed` itself, as with `--force`, for a session whose host died or for a session that has already ended, it first writes an empty internal file, `destroyed`, in the session folder. When the host records `destroyed`, as after a plain `destroy` of a live session, nobody writes that file. A reconcile that writes over the record at the same moment finds the file right after its own write and records `destroyed` again. -A `list`, `inspect` or `gc` that reads the session between those two writes sees `failed`. If the reconciling process is killed between them, the session stays `failed`. -If `destroy` fails after it wrote the file, for example because its manifest write fails, the file stays. For a session that had not ended yet, the next reconcile then records it as `destroyed`. A reconcile skips a session that has already ended, so for such a session run `destroy` again. +A `list`, `inspect` or `gc` that reads the session between those two writes sees `failed`, and `home list` and the dashboard count a session that has ended and has that file as destroyed. If the reconciling process is killed between them, the next reconcile finds the file and records the session as `destroyed`. When that repair fails, for example on a full disk, `list` and `inspect` show the session as it reads. +If `destroy` fails after it wrote the file, for example because its manifest write fails, the file stays, and the next reconcile records the session as `destroyed`, also when the session had already ended. Nothing deletes the file before `gc` removes the session folder, because a reconcile that read before the destroy can still write after it. 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 within about 6 s, it fails with `HOST_UNREACHABLE` or `HOST_TIMEOUT` and tells the host to stop. On Linux and macOS it sends the host SIGTERM, and the host stops the program the way `destroy` does and records the session as `destroyed` once the program's group has ended, also while its start-up is still slow. @@ -377,7 +377,7 @@ Each session's RPC socket lies outside the Home, at `/tmp/agent-tty-/<8 hex Known limits: 1. Any user can create `/tmp/agent-tty-` before you do, because `/tmp` is shared. `create`, and every command that talks to a host that this version started, then fails as above until that user or an admin removes it. agent-tty never connects to a socket in such a folder. A host that an older version started stays reachable at the old path (limit 2). -2. A host that an older version started listens at `/tmp/agent-tty/<8 hex>/<12 hex>`. This version still reaches it there when that socket and its folder belong to your uid, no other user can write the folder, and `/tmp/agent-tty` belongs to you or to root and either no other user can write it or it has the sticky bit. `destroy` and `gc` remove that old socket. An older version cannot reach a host that this version started: destroy your sessions before you downgrade. +2. A host that an older version started listens at `/tmp/agent-tty/<8 hex>/<12 hex>`. This version still reaches it there when that socket and its folder belong to your uid, no other user can write the folder, and `/tmp/agent-tty` belongs to you or to root and either no other user can write it or it has the sticky bit. An older version created `/tmp/agent-tty` with your umask, so under umask `002` that folder has mode `0775`. Your group can then write it, and this version does not reach an old host there until you run `chmod g-w /tmp/agent-tty`. `destroy` and `gc` remove that old socket. An older version cannot reach a host that this version started: destroy your sessions before you downgrade. 3. The socket root belongs to the uid of the CLI. A CLI that runs as another uid, for example `sudo agent-tty ...` or `docker exec -u root`, looks under its own root and cannot reach a host that your uid started (`HOST_UNREACHABLE`). Run every command of a session as the uid that created it. For tests and automation, prefer an absolute temp directory: diff --git a/src/cli/commands/README.md b/src/cli/commands/README.md index a99415c5..7fbc7323 100644 --- a/src/cli/commands/README.md +++ b/src/cli/commands/README.md @@ -46,7 +46,7 @@ This directory holds one handler module per agent-tty CLI command. `src/cli/main - Session commands send RPCs over the session socket through `sendRpc`. The method names are `run`, `type`, `paste`, `sendKeys`, `mouse`, `mark`, `resize`, `signal`, `snapshot`, `screenshot`, `wait`, `waitForRender` and `inspect`. `create` also sends `inspect` while it polls. [run.ts:runRunCommand] [send-keys.ts:runSendKeysCommand] [wait.ts:runWaitCommand] [create.ts:runCreateCommand] - `create` calls `allocateSession` (`src/host/lifecycle.ts`) with a `launch` callback that records the session ID and starts the host process through `launchHost`. If `launchHost` or a later step of `allocateSession` throws, `create` removes the session directory with `fs.rm`. A bad `cwd`, shell path or command segment fails before `allocateSession` creates the directory, so no session directory is left behind. A failure between `mkdir` and the callback, such as a failed `chmod`, leaves the empty session directory in place. A readiness-poll failure rethrows and leaves the session directory in place. It registers the Home through `upsertHome`. [create.ts:runCreateCommand] - `gc` reads session directories, calls `reconcileSession` (which can rewrite manifests), deletes collectable session directories with `fs.rm` outside dry-run mode, and deregisters Homes through `forgetHome`. [gc.ts:gcSessions] [gc.ts:runGcCommand] -- `inspect` calls `reconcileSession` when the host is unreachable. [inspect.ts:runInspectCommand] +- `inspect` calls `reconcileSession` when the host is unreachable, and for an ended session other than destroyed whose folder holds the destroy marker. When that repair throws, it shows the manifest as it reads. [inspect.ts:runInspectCommand] - `destroy` and `list` call `destroySession` and `listSessions` from `src/host/lifecycle.ts`. [destroy.ts:runDestroyCommand] [list.ts:runListCommand] - `snapshot`, `screenshot`, `wait` and `record diff` run offline replay through `withOfflineReplayRenderer` (`src/replay/offlineReplay.ts`). `record diff` sends no RPC. [wait.ts:runOfflineRenderWait] [record-diff.ts:runRecordDiffCommand] - Offline `snapshot` and `screenshot` write artifact files into the session artifacts directory and append artifact-manifest entries through `publishArtifactWithRollback` (`src/storage/artifactManifest.ts`). `snapshot` writes a temp JSON file through `writeTextFileAtomic`, and `screenshot` gets a temp PNG from the renderer. `publishArtifactWithRollback` links or copies the temp file into place without replacing an existing file. [src/snapshot/capture.ts:captureSnapshotResult] [src/snapshot/capture.ts:persistSnapshotArtifact] [src/screenshot/capture.ts:captureScreenshotResult] diff --git a/src/cli/commands/home/README.md b/src/cli/commands/home/README.md index 85d7b4b7..6a1f1c3f 100644 --- a/src/cli/commands/home/README.md +++ b/src/cli/commands/home/README.md @@ -16,7 +16,7 @@ This directory holds the handlers for the `home list` and `home forget` CLI subc - The Home path must be a non-empty string. `normalizeHomePath` enforces this with `invariant` before the registry is called. [src/storage/homeRegistry.ts:normalizeHomePath] - `forget` returns `null` and writes nothing when no entry matches the path as written or its normalized form. [src/storage/homeRegistry.ts:createHomeRegistry] - The registry path must be absolute (`invariant`). A relative `XDG_STATE_HOME` is ignored. [src/storage/homeRegistry.ts:resolveHomeRegistryPath] -- `listRegisteredHomes` drops Homes with zero visible sessions. The count leaves out destroyed sessions and sessions whose manifest is missing or unreadable, so a Home whose sessions are all destroyed is dropped too. In `'active'` scope it also drops Homes with zero active sessions. It sorts the result by `lastSeenAt`, newest first. [src/storage/homeScope.ts:listRegisteredHomes] [src/storage/homeScope.ts:scanHome] +- `listRegisteredHomes` drops Homes with zero visible sessions. The count leaves out destroyed sessions, ended sessions whose folder holds the destroy marker, and sessions whose manifest is missing or unreadable, so a Home whose sessions are all destroyed is dropped too. In `'active'` scope it also drops Homes with zero active sessions. It sorts the result by `lastSeenAt`, newest first. [src/storage/homeScope.ts:listRegisteredHomes] [src/storage/homeScope.ts:scanHome] - With an empty list, human output is the single line `No registered Homes.`. [list.ts:buildHomeListLines] ## Side Effects diff --git a/src/cli/commands/inspect.ts b/src/cli/commands/inspect.ts index 70601277..4d94228d 100644 --- a/src/cli/commands/inspect.ts +++ b/src/cli/commands/inspect.ts @@ -15,7 +15,7 @@ import { countEventLogEntries, statEventLogBytes, } from '../../host/eventLog.js'; -import { reconcileSession } from '../../host/lifecycle.js'; +import { isMarkedDestroyed, reconcileSession } from '../../host/lifecycle.js'; import { sendRpc } from '../../host/rpcClient.js'; import { isCommandableSessionStatus, @@ -208,6 +208,22 @@ export async function runInspectCommand( }); } + // A reconcile records destroyed for an ended session that a destroy marked + // but did not finish (see reconcileSession). + if (isMarkedDestroyed(sessionDirectory, session)) { + const read = session; + try { + await reconcileSession(sessionDirectory); + session = await readManifest(manifestFile); + } catch { + // A marked session that ended shows as it reads when its repair fails, + // as in list. The repair write can have landed before a later step + // threw. + session = + (await readManifestIfExists(manifestFile).catch(() => read)) ?? read; + } + } + const isLiveHostEligible = isLiveHostEligibleSessionStatus(session.status); let hostInfo: HostInspectResult | undefined; if (isLiveHostEligible) { diff --git a/src/dashboard/README.md b/src/dashboard/README.md index 59fdd4c4..8602828e 100644 --- a/src/dashboard/README.md +++ b/src/dashboard/README.md @@ -28,7 +28,7 @@ The Session Dashboard is an Ink/React terminal UI that lists the Sessions in a h ## Side Effects - `EventLogTailSource.poll()` reads the Event Log with `node:fs/promises` `stat` and `open`/`read`/`close`. [eventSource.ts:EventLogTailSource] -- `listDashboardSessions` reads manifests through `listSessions` (`src/host/lifecycle.ts`) and `readManifestIfExists` (`src/storage/manifests.ts`). `listSessions` calls `reconcileSession` for active Sessions, and that function can rewrite a manifest with `writeManifest` and remove the socket file. [sessionScope.ts:listDashboardSessions] +- `listDashboardSessions` reads manifests through `listSessions` (`src/host/lifecycle.ts`) and `readManifestIfExists` (`src/storage/manifests.ts`). `listSessions` calls `reconcileSession` for active Sessions and for ended Sessions other than destroyed whose folder holds the destroy marker, and that function can rewrite a manifest with `writeManifest` and remove the socket file. [sessionScope.ts:listDashboardSessions] - `runDashboardApp` renders to the terminal with Ink `render()` and waits for `waitUntilExit()`. `App` reads keys with `useInput`, and `q` or Ctrl-C calls `exit()`. [app.tsx:runDashboardApp] [app.tsx:App] - `useFollower` polls with `setInterval` every 33 ms (`FRAME_INTERVAL_MS`) and creates a `libghostty-vt` renderer backend with `createRendererBackend` and the `reference-dark` profile. Cleanup aborts, clears the interval and disposes the follower. [app.tsx:useFollower] - `App` refreshes the Session list with `setInterval` every 1500 ms (`LIST_REFRESH_MS`) and calls `listRegisteredHomes` (`src/storage/homeScope.ts`) for the home picker. [app.tsx:App] diff --git a/src/host/README.md b/src/host/README.md index 38cb104e..41c4fe21 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -18,11 +18,11 @@ - `ensureSocketRoot(root = socketRootDirectory())` creates the socket root with `mkdir` mode `0o700` and then `chmod 0o700` when it is missing. It throws `STORAGE_WRITE_ERROR`, with the path, the owner's uid and the mode in `details`, unless `lstat` shows a directory of the caller's uid with no group or other mode bit: a symlink, a file, a directory of another uid or a group or other bit fails. A private root without all owner bits, as another `create` shows it while umask took them and its `chmod` is pending, gets `chmod 0o700`. It does nothing where `process.getuid` is missing (Windows). `create` calls it before it allocates a session, because the host's errors reach nobody. [socketRoot.ts:ensureSocketRoot] - `socketRootExists(root = socketRootDirectory())` returns `false` for a missing root and `true` for a private one (a directory of the caller's uid with no group or other bit), after the same `chmod 0o700` of a private root without all owner bits. It throws the same `STORAGE_WRITE_ERROR` for any other root. [socketRoot.ts:socketRootExists] - `isOwnLegacySocket(socketFile)` is true when `lstat` shows a socket of the caller's uid, in a Home folder of that uid that no group or other user can write, under a root of that uid or of root that no group or other user can write or that has the sticky bit. No other user can then rename or replace a folder on the path before the connect. [socketRoot.ts:isOwnLegacySocket] -- `removeDeadHostSocket(sessionDirectory, manifest)` unlinks the session's socket and removes the Home's socket directory if it is empty, when the manifest names no host pid or `judgeHost` reads the host as dead. It also removes the socket at `legacySocketPath` when `isOwnLegacySocket` accepts it. It logs errors instead of throwing them. `gc` calls it before it removes a session folder, and `destroySession` calls it before it throws `SESSION_ALREADY_DESTROYED`. [lifecycle.ts:removeDeadHostSocket] +- `removeDeadHostSocket(sessionDirectory, manifest)` unlinks the session's socket and removes the Home's socket directory if it is empty, when the manifest names no host pid or `judgeHost` reads the host as dead. It also removes the socket at `legacySocketPath` when `isOwnLegacySocket` accepts it. When the host check throws, it removes neither socket. It logs errors instead of throwing them. `gc` calls it before it removes a session folder, and `destroySession` calls it before it throws `SESSION_ALREADY_DESTROYED`. [lifecycle.ts:removeDeadHostSocket] - `listenInSocketDirectory(socketFile, listen)` calls `ensureSocketRoot`, then runs `mkdir`, `chmod 0o700` and `listen` up to 5 times when the socket directory vanished before the `chmod` or the bind, because a teardown in the same Home removed it. libuv reports such a bind as `EACCES`. The host and `doctor`'s socket check use it. [lifecycle.ts:listenInSocketDirectory] - `isProcessAlive(pid)` returns `false` for `null` and for a PID that `process.kill(pid, 0)` reports as `ESRCH`, and `true` when the probe succeeds. It asserts a positive integer PID and rethrows other errors, such as `EPERM`. [lifecycle.ts:isProcessAlive] - `destroySession(sessionId, force?, options?)` destroys a session and waits until its manifest shows a terminal status. `DestroySessionOptions` has an optional `AbortSignal`. [lifecycle.ts:destroySession] [lifecycle.ts:DestroySessionOptions] -- `listSessions(home, all?)` returns `SessionSummary[]`. It reconciles active sessions first and hides terminal sessions unless `all` is true. A missing `/sessions` gives `[]`, and any other read error throws `STORAGE_READ_ERROR`. [lifecycle.ts:listSessions] [lifecycle.ts:SessionSummary] +- `listSessions(home, all?)` returns `SessionSummary[]`. It reconciles active sessions, and ended sessions other than destroyed whose folder holds the destroy marker, first. It hides terminal sessions unless `all` is true. A missing `/sessions` gives `[]`, and any other read error throws `STORAGE_READ_ERROR`. [lifecycle.ts:listSessions] [lifecycle.ts:SessionSummary] - `reconcileSession(sessionDirectory)` moves a non-terminal session to a terminal status when its host process is gone. [lifecycle.ts:reconcileSession] - `captureProgram(pid)` returns a `ProgramRecord` (`version`, `pid`, `bootId`, `autogroup`) for the program that the host just spawned, and `writeProgramRecord(sessionDirectory, record)` writes it to `program.json`. `bootId` is a string and `autogroup` a number, or both are `null`. [programGroup.ts:captureProgram] [programGroup.ts:writeProgramRecord] - `readProvenProgramGroup(sessionDirectory)` returns the `program.json` record when it has a token and `sharesHostPids` reads true, the unshared group (below) when it has a token and `sharesHostPids` reads false, else `null`. `readProgramGroup(sessionDirectory, childPid)` returns the same for a record with a token, else `{ childPid, sessionDirectory }`, or `null` when `childPid` is `null` or, on Linux, when `host.json` names another pid namespace or machine id than the CLI's (`sharesHostPids`). For a record with a token where `sharesHostPids` reads false, which includes a CLI that cannot read `/proc/self/ns/pid`, both return the unshared group `{ unshared: true }`: no scan or probe of this process shows the program's processes, so `isProgramGroupAlive` reads it alive and `stopProgramGroup` sends it nothing. A `program.json` that does not validate reads as `null` in both, so it gets no kill and no throw. [programGroup.ts:readProgramRecord] [programGroup.ts:readProvenProgramGroup] [programGroup.ts:readProgramGroup] [hostRecord.ts:sharesHostPids] @@ -56,7 +56,7 @@ - The `run` handler waits 30,000 ms by default. The `wait` handler needs exactly one of `exit` or `idleMs`, else it throws `INVALID_DURATION`. `waitForRender` polls every `RENDER_WAIT_POLL_INTERVAL_MS` (200 ms, `src/renderWait/limits.ts`). [hostMain.ts:runHost] - `runHost` handles PTY exit once. If the status is `destroying` it records `destroyed`, else `exited`. Shutdown runs once. [hostMain.ts:runHost] - `destroySession` throws `SESSION_NOT_FOUND` when there is no manifest, or when the session directory is gone at its `destroyed` write, and `SESSION_ALREADY_DESTROYED` for a destroyed session. When it records `destroyed` itself, `recordDestroyed` first writes the empty `/destroyed` marker with `writeDestroyMarker`. Before it records a terminal session as `destroyed`, it calls `stopProgramGroup` with the group from `readProvenProgramGroup`, so only a group with a token gets a signal, and it throws `HOST_TIMEOUT` while that group lives. A session already recorded `destroyed` with the unshared group gets no wait, because only a process that saw the group recorded it, after its wait. A running session gets the `destroy` RPC. With `force` it gets `SIGKILL` for the program's group and, only when `hostMatches` proves the host, for the host: on Linux `judgeHost` must return `alive`, elsewhere `/bin/ps` must show `_host `, and on Windows the host gets no signal. It polls every 100 ms for at most 50 attempts and throws `HOST_TIMEOUT` if the status is still not terminal. [lifecycle.ts:destroySession] -- `reconcileSession` does nothing when the manifest is missing, the status is terminal or the host can be alive: `judgeHost` with the record from `host.json` does not return `dead`. A null `hostPid` counts as a dead host. `allocateSession` writes the host PID into the first manifest, so a new session already has a `hostPid`. After the liveness check, `reconcileSession` reads the manifest again and does nothing when it is now missing or terminal. Otherwise it maps the status it read again: `running` to `failed` (failure origin `host-death`), `exiting` to `exited`, `destroying` to `destroyed` and any other status to `failed` (origin `unknown`), and sets both PIDs to `null`. Right after that write, when its status was not `destroyed` and the destroy marker exists, it writes `destroyed` again from the same copy, with both PIDs `null` and no failure fields. When the session directory is gone at either write, it returns. [lifecycle.ts:reconcileSession] +- `reconcileSession` writes `destroyed` (both PIDs `null`, the exit code kept, no failure fields) over a terminal manifest other than `destroyed` when the destroy marker exists, and returns (`writeMarkedDestroyed`). Otherwise it does nothing when the manifest is missing, the status is terminal or the host can be alive: `judgeHost` with the record from `host.json` does not return `dead`. A null `hostPid` counts as a dead host. `allocateSession` writes the host PID into the first manifest, so a new session already has a `hostPid`. After the liveness check, `reconcileSession` reads the manifest again and does nothing when it is now missing or terminal. Otherwise it maps the status it read again: `running` to `failed` (failure origin `host-death`), `exiting` to `exited`, `destroying` to `destroyed` and any other status to `failed` (origin `unknown`), and sets both PIDs to `null`. Right after that write, when its status was not `destroyed` and the destroy marker exists, it writes `destroyed` again from the same copy, with both PIDs `null` and no failure fields. When the session directory is gone at any of these writes, it returns. [lifecycle.ts:reconcileSession] [lifecycle.ts:writeMarkedDestroyed] - Every kill of the program's process group goes through `stopProgramGroup`. For a record with a token, `judgeProgramGroup` returns `owned` only when a process that is not a zombie (a process whose main thread exited is not one while another of its threads runs) has the program's pid as its process group and session id, and the recorded autogroup on the recorded boot. A scan that finds no live member runs once more, because a member can fork and end after the scan listed `/proc`. `stopProgramGroup` reads that process again right before the kill. `unproven` (another boot id, or only members with another session id or autogroup) and `unknown` kill nothing. `gone` (no live member) first sends the group SIGSTOP with `signalProcessGroup`, because a fork chain whose members each live about 2 ms is never in view, and a stopped member is. The judge then runs again, and a frozen group that gets no kill gets SIGCONT, also when a scan throws. So a group id that an unrelated group took, whose members no scan shows either, gets a SIGSTOP and a SIGCONT. `unknown` means that `/proc` refused the boot id, or showed a member with the program's session id but no autogroup, so `isProgramGroupAlive` reads it alive. A record without a token gets the kill of its `pid`. A `{ childPid, sessionDirectory }` group gets the kill of `childPid`, and reads alive, only while `sessionDirectory` exists, checked in the same synchronous block. The unshared group `{ unshared: true }` gets no signal and reads alive. [programGroup.ts:stopProgramGroup] [programGroup.ts:judgeProgramGroup] - `captureProgram` records a token only on Linux, for its own child that leads its own session and has an autogroup other than the host's, within 250 ms, and only when `/proc` shows the boot id. `runHost` calls it right after `createPty` and writes the record before its first manifest write, with no `await` in between. [programGroup.ts:captureProgram] [hostMain.ts:runHost] - `allocateSession` throws `INVALID_DIMENSIONS` for non-positive `cols` or `rows`, `STORAGE_READ_ERROR` when `cwd` is not a directory and `INVALID_INPUT` when the shell path is not a file. An empty `command` defaults to the shell path. It creates the session directory and calls `launch` only after these checks pass. [lifecycle.ts:allocateSession] diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index 065dff28..727902d0 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -454,10 +454,18 @@ export async function removeDeadHostSocket( manifest: SessionRecord, ): Promise { const socketFile = socketPath(sessionDirectory); + let alive: boolean; + try { + alive = isHostAlive(await readSessionHost(sessionDirectory, manifest)); + } catch (error) { + // A host that the check cannot judge may still listen on either socket. + console.debug('could not judge the host of a socket:', error); + return; + } + if (alive) { + return; + } try { - if (isHostAlive(await readSessionHost(sessionDirectory, manifest))) { - return; - } await unlinkIfPresent(socketFile); await removeSocketDirectoryIfEmpty(socketFile); } catch (error) { @@ -1028,12 +1036,21 @@ export async function listSessions( continue; } - if (isActiveSessionStatus(manifest.status)) { + if ( + isActiveSessionStatus(manifest.status) || + isMarkedDestroyed(sessionDirectory, manifest) + ) { + const read = manifest; try { await reconcileSession(sessionDirectory); manifest = await readManifestIfExists(manifestFile); } catch { - continue; + if (isActiveSessionStatus(read.status)) { + continue; + } + // A marked session that ended lists as it reads when its repair + // fails. The repair write can have landed before a later step threw. + manifest = await readManifestIfExists(manifestFile).catch(() => read); } if (manifest === null) { @@ -1058,12 +1075,57 @@ export async function listSessions( return summaries; } +export function isMarkedDestroyed( + sessionDirectory: string, + manifest: SessionRecord, +): boolean { + return ( + isTerminalSessionStatus(manifest.status) && + !isDestroyedSessionStatus(manifest.status) && + existsSync(destroyMarkerPath(sessionDirectory)) + ); +} + +// false when gc removed the session folder. +async function writeMarkedDestroyed( + manifestFile: string, + manifest: SessionRecord, +): Promise { + const { failureReason: _reason, failureOrigin: _origin, ...rest } = manifest; + try { + await writeManifest(manifestFile, { + ...rest, + status: 'destroyed', + updatedAt: new Date().toISOString(), + hostPid: null, + childPid: null, + }); + return true; + } catch (error) { + if ( + error instanceof CliError && + error.code === ERROR_CODES.SESSION_NOT_FOUND + ) { + return false; + } + throw error; + } +} + export async function reconcileSession( sessionDirectory: string, ): Promise { const manifestFile = manifestPath(sessionDirectory); const manifest = await readManifestIfExists(manifestFile); + if (manifest !== null && isMarkedDestroyed(sessionDirectory, manifest)) { + if (await writeMarkedDestroyed(manifestFile, manifest)) { + const socketFile = socketPath(sessionDirectory); + await unlinkIfPresent(socketFile); + await removeSocketDirectoryIfEmpty(socketFile); + } + return; + } if (manifest === null || isTerminalSessionStatus(manifest.status)) { return; } diff --git a/src/storage/README.md b/src/storage/README.md index ef119a6b..4fc02ab5 100644 --- a/src/storage/README.md +++ b/src/storage/README.md @@ -42,7 +42,7 @@ - `computeArtifactHealth` maps only `MANIFEST_VALIDATION_ERROR` to health `manifest-invalid` and rethrows other errors. It validates its result with `ArtifactHealthSummarySchema`. [artifactHealth.ts:computeArtifactHealth] - The registry read returns `[]` on a read error, invalid JSON or a schema failure. The read checks each `homes` entry on its own and drops an invalid entry, so the valid entries survive. `resolveHomeRegistryPath` ignores an empty or relative `XDG_STATE_HOME`. [homeRegistry.ts:createHomeRegistry] [homeRegistry.ts:resolveHomeRegistryPath] - `upsert` reads and then writes the registry with no lock. A code comment states that concurrent creates can race and drop an entry, which registers again on the next create. [homeRegistry.ts:createHomeRegistry] -- The `scanHome` doc comment states that it does not reconcile sessions, does not write manifests and does not throw. It skips destroyed sessions and unreadable manifests. [homeScope.ts:scanHome] +- The `scanHome` doc comment states that it does not reconcile sessions, does not write manifests and does not throw. It skips destroyed sessions, ended sessions whose folder holds the destroy marker, and unreadable manifests. [homeScope.ts:scanHome] - `listRegisteredHomes` leaves out Homes with no visible sessions, and the `active` scope also leaves out Homes with no active session. Its doc comment states that it does not rewrite the registry file. [homeScope.ts:listRegisteredHomes] ## Side Effects @@ -57,7 +57,7 @@ - `publishArtifactWithRollback` has the side effects of `publishArtifactFile` and `appendArtifactWithRollback`. It also removes the temp file with `rm({ force: true })` when an earlier failure in the queue stops its publish step from running. [artifactManifest.ts:publishArtifactWithRollback] - `computeArtifactHealth` calls `fs.promises.access` on each artifact file. [artifactHealth.ts:computeArtifactHealth] - `resolveHomeRegistryPath` reads `XDG_STATE_HOME` and calls `os.homedir()`. `upsertHome` and `forgetHome` read and write the real `homes.json`. `readHomeRegistry` only reads it. [homeRegistry.ts:resolveHomeRegistryPath] [homeRegistry.ts:upsertHome] [homeRegistry.ts:readHomeRegistry] -- `scanHome` and `listRegisteredHomes` only read: `readdir(/sessions)`, each `session.json` and the registry. [homeScope.ts:scanHome] [homeScope.ts:listRegisteredHomes] +- `scanHome` and `listRegisteredHomes` only read: `readdir(/sessions)`, each `session.json`, whether each `destroyed` marker exists, and the registry. [homeScope.ts:scanHome] [homeScope.ts:listRegisteredHomes] ## Verification diff --git a/src/storage/homeScope.ts b/src/storage/homeScope.ts index ebe9a3cf..4525286e 100644 --- a/src/storage/homeScope.ts +++ b/src/storage/homeScope.ts @@ -1,14 +1,16 @@ +import { existsSync } from 'node:fs'; import { readdir } from 'node:fs/promises'; import { resolve } from 'node:path'; import { isActiveSessionStatus, isDestroyedSessionStatus, + isTerminalSessionStatus, } from '../protocol/sessionStatusPolicy.js'; import type { SessionRecord } from '../protocol/schemas.js'; import { createHomeRegistry, type HomeRegistry } from './homeRegistry.js'; import { readManifestIfExists } from './manifests.js'; -import { manifestPath, sessionDir } from './sessionPaths.js'; +import { destroyMarkerPath, manifestPath, sessionDir } from './sessionPaths.js'; /** * Active/all scope for listing Homes. Structurally identical to the dashboard's @@ -37,11 +39,13 @@ export interface HomeSessionCounts { export interface ScanHomeDependencies { readdir: (path: string) => Promise; readManifestIfExists: (path: string) => Promise; + pathExists: (path: string) => boolean; } const defaultScanDependencies: ScanHomeDependencies = { readdir, readManifestIfExists, + pathExists: existsSync, }; /** @@ -53,8 +57,9 @@ const defaultScanDependencies: ScanHomeDependencies = { * still shows `running` until something reconciles it); entering a Home in the * dashboard, or running `gc`, reconciles for real. * - * "Visible" excludes destroyed Sessions, mirroring the dashboard's `all` scope - * (a destroyed Session's Event Log may already be collected). It never throws: + * "Visible" excludes destroyed Sessions and ended Sessions whose folder holds + * the destroy marker, mirroring the dashboard's `all` scope (a destroyed Session's + * Event Log may already be collected). It never throws: * a missing/unreadable sessions tree, or a corrupt individual manifest, counts * as zero/skip so a single bad Session can't break discovery. */ @@ -84,7 +89,12 @@ export async function scanHome( continue; } - if (manifest === null || isDestroyedSessionStatus(manifest.status)) { + if ( + manifest === null || + isDestroyedSessionStatus(manifest.status) || + (isTerminalSessionStatus(manifest.status) && + dependencies.pathExists(destroyMarkerPath(sessionDir(home, entry)))) + ) { continue; } diff --git a/test/unit/commands/inspect.test.ts b/test/unit/commands/inspect.test.ts index 6e406ec0..afc02b09 100644 --- a/test/unit/commands/inspect.test.ts +++ b/test/unit/commands/inspect.test.ts @@ -9,6 +9,7 @@ const mocks = vi.hoisted(() => ({ deriveTerminationCategory: vi.fn(), emitSuccess: vi.fn(), reconcileSession: vi.fn(), + isMarkedDestroyed: vi.fn(), sendRpc: vi.fn(), readManifest: vi.fn(), readManifestIfExists: vi.fn(), @@ -29,6 +30,7 @@ vi.mock('../../../src/host/eventLog.js', () => ({ vi.mock('../../../src/host/lifecycle.js', () => ({ reconcileSession: mocks.reconcileSession, + isMarkedDestroyed: mocks.isMarkedDestroyed, })); vi.mock('../../../src/host/rpcClient.js', () => ({ @@ -410,6 +412,79 @@ describe('inspect command', () => { ); }); + it('reconciles a failed session that a destroy marked and reports destroyed', async () => { + const failedSession = createSessionRecord('failed'); + mocks.readManifestIfExists.mockResolvedValueOnce(failedSession); + mocks.isMarkedDestroyed.mockReturnValueOnce(true); + mocks.readManifest.mockResolvedValueOnce({ + ...failedSession, + status: 'destroyed', + }); + mocks.countEventLogEntries.mockResolvedValueOnce(3); + + await runInspectCommand({ + context: TEST_CONTEXT, + json: true, + sessionId: 'session-01', + }); + + expect(mocks.reconcileSession).toHaveBeenCalledTimes(1); + const emitted = getLastEmitSuccessPayload() as { + result: { session: { status: string } }; + }; + expect(emitted.result.session.status).toBe('destroyed'); + }); + + it('shows the record it read when the repair of a marked session fails', async () => { + const failedSession = createSessionRecord('failed'); + mocks.readManifestIfExists + .mockResolvedValueOnce(failedSession) + .mockResolvedValueOnce(failedSession); + mocks.isMarkedDestroyed.mockReturnValueOnce(true); + mocks.reconcileSession.mockRejectedValueOnce( + makeCliError(ERROR_CODES.STORAGE_WRITE_ERROR, { + message: 'disk full', + }), + ); + mocks.countEventLogEntries.mockResolvedValueOnce(3); + + await runInspectCommand({ + context: TEST_CONTEXT, + json: true, + sessionId: 'session-01', + }); + + const emitted = getLastEmitSuccessPayload() as { + result: { session: { status: string } }; + }; + expect(emitted.result.session.status).toBe('failed'); + }); + + it('shows destroyed when the repair write of a marked session landed before a later step threw', async () => { + const failedSession = createSessionRecord('failed'); + mocks.readManifestIfExists + .mockResolvedValueOnce(failedSession) + .mockResolvedValueOnce({ ...failedSession, status: 'destroyed' }); + mocks.isMarkedDestroyed.mockReturnValueOnce(true); + mocks.reconcileSession.mockRejectedValueOnce( + Object.assign(new Error('EPERM: operation not permitted, unlink'), { + code: 'EPERM', + }), + ); + mocks.countEventLogEntries.mockResolvedValueOnce(3); + + await runInspectCommand({ + context: TEST_CONTEXT, + json: true, + sessionId: 'session-01', + }); + + const emitted = getLastEmitSuccessPayload() as { + result: { session: { status: string } }; + }; + expect(emitted.result.session.status).toBe('destroyed'); + }); + it('reports offline replay renderer runtime for exited sessions', async () => { const exitedSession = createSessionRecord('exited'); mocks.readManifestIfExists.mockResolvedValueOnce(exitedSession); diff --git a/test/unit/host/lifecycle.test.ts b/test/unit/host/lifecycle.test.ts index dd60098b..afe5837a 100644 --- a/test/unit/host/lifecycle.test.ts +++ b/test/unit/host/lifecycle.test.ts @@ -8,7 +8,8 @@ import { symlinkSync, writeFileSync, } from 'node:fs'; -import { mkdir, mkdtemp, realpath, rm } from 'node:fs/promises'; +import { chmod, mkdir, mkdtemp, realpath, rm } from 'node:fs/promises'; +import { createServer, type Server } from 'node:net'; import { tmpdir } from 'node:os'; import { dirname, join } from 'node:path'; import process from 'node:process'; @@ -160,6 +161,7 @@ import type * as TimersPromises from 'node:timers/promises'; import { allocateSession, destroySession, + listSessions, cliRunsInsideProgramSession, reconcileSession, removeSocketDirectoryBestEffort, @@ -180,6 +182,7 @@ import { ensureSocketRoot } from '../../../src/host/socketRoot.js'; import type { SessionRecord } from '../../../src/protocol/schemas.js'; import { readManifest, writeManifest } from '../../../src/storage/manifests.js'; import { + legacySocketPath, manifestPath, sessionDir, socketPath, @@ -407,6 +410,166 @@ describe('reconcileSession', () => { expect(manifest.failureReason).toBeUndefined(); }); + it('records destroyed for a failed session whose reconcile died before it repaired a destroy', async () => { + const directory = await seedSession( + makeRecord({ + status: 'failed', + failureOrigin: 'host-death', + failureReason: 'host process died unexpectedly', + hostPid: null, + childPid: null, + }), + ); + writeFileSync(join(directory, 'destroyed'), ''); + + await reconcileSession(directory); + + const manifest = await readManifest(manifestPath(directory)); + expect(manifest).toMatchObject({ status: 'destroyed' }); + expect(manifest.failureOrigin).toBeUndefined(); + expect(manifest.failureReason).toBeUndefined(); + }); + + it('records destroyed for an exited session whose destroy failed after the marker', async () => { + const directory = await seedSession( + makeRecord({ + status: 'exited', + exitCode: 3, + hostPid: null, + childPid: null, + }), + ); + writeFileSync(join(directory, 'destroyed'), ''); + + await reconcileSession(directory); + + expect(await readManifest(manifestPath(directory))).toMatchObject({ + status: 'destroyed', + exitCode: 3, + }); + }); + + it('list shows destroyed for a failed session next to the destroy marker', async () => { + const directory = await seedSession( + makeRecord({ + status: 'failed', + failureOrigin: 'host-death', + hostPid: null, + childPid: null, + }), + ); + writeFileSync(join(directory, 'destroyed'), ''); + + const [summary] = await listSessions(home, true); + + expect(summary).toMatchObject({ + sessionId: 'session-01', + status: 'destroyed', + }); + }); + + it('removes the socket that a dead host left when it repairs a destroy', async () => { + const directory = await seedSession( + makeRecord({ + status: 'failed', + failureOrigin: 'host-death', + hostPid: null, + childPid: null, + }), + ); + writeFileSync(join(directory, 'destroyed'), ''); + const socketFile = socketPath(directory); + await mkdir(dirname(socketFile), { recursive: true, mode: 0o700 }); + writeFileSync(socketFile, ''); + + try { + await reconcileSession(directory); + + expect(existsSync(socketFile)).toBe(false); + expect(existsSync(dirname(socketFile))).toBe(false); + } finally { + await rm(dirname(socketFile), { recursive: true, force: true }); + } + }); + + it('leaves a running session with a live host as it is next to the destroy marker', async () => { + const running = makeRecord({ hostPid: process.pid, childPid: null }); + const directory = await seedSession(running); + const own = captureHost(process.pid); + if (own !== null) { + writeHostRecord(directory, own); + } + writeFileSync(join(directory, 'destroyed'), ''); + + await reconcileSession(directory); + expect(await readManifest(manifestPath(directory))).toEqual(running); + expect(await listSessions(home, true)).toMatchObject([ + { sessionId: 'session-01', status: 'running' }, + ]); + }); + + it('list shows destroyed when the socket cleanup fails after the repair write', async () => { + const directory = await seedSession( + makeRecord({ + status: 'failed', + failureOrigin: 'host-death', + hostPid: null, + childPid: null, + }), + ); + writeFileSync(join(directory, 'destroyed'), ''); + // unlink of a directory fails with EISDIR (EPERM on macOS). + const socketFile = socketPath(directory); + await mkdir(socketFile, { recursive: true }); + + try { + expect(await listSessions(home, true)).toMatchObject([ + { sessionId: 'session-01', status: 'destroyed' }, + ]); + } finally { + await rm(dirname(socketFile), { recursive: true, force: true }); + } + }); + + // A root process can write into a folder of mode 0500. + it.skipIf(process.platform === 'win32' || process.getuid?.() === 0)( + 'list keeps a marked failed session when its repair write fails', + async () => { + const directory = await seedSession( + makeRecord({ + status: 'failed', + failureOrigin: 'host-death', + hostPid: null, + childPid: null, + }), + ); + writeFileSync(join(directory, 'destroyed'), ''); + await chmod(directory, 0o500); + + try { + expect(await listSessions(home, true)).toMatchObject([ + { sessionId: 'session-01', status: 'failed' }, + ]); + } finally { + await chmod(directory, 0o700); + } + }, + ); + + it('leaves an exited session without the marker as it is', async () => { + const exited = makeRecord({ + status: 'exited', + exitCode: 0, + hostPid: null, + childPid: null, + }); + const directory = await seedSession(exited); + + await reconcileSession(directory); + + expect(await readManifest(manifestPath(directory))).toEqual(exited); + }); + it('writes nothing while the program group survives its kill', async () => { const record = makeRecord(); const directory = await seedSession(record); @@ -1444,6 +1607,64 @@ describe('removeSocketDirectoryBestEffort', () => { }); }); +// A host of an older version listens at the old path under /tmp/agent-tty. +describe.skipIf(process.platform === 'win32')( + 'the old socket of a destroyed session', + () => { + let oldSocketFile = ''; + let server: Server | undefined; + + beforeEach(async () => { + vi.stubEnv('AGENT_TTY_HOME', home); + const old = legacySocketPath(socketPath(sessionDir(home, 'session-01'))); + expect(old).not.toBeNull(); + oldSocketFile = old as string; + await mkdir(dirname(oldSocketFile), { recursive: true, mode: 0o700 }); + const listening = createServer(); + server = listening; + await new Promise((resolve) => { + listening.listen(oldSocketFile, resolve); + }); + }); + + afterEach(async () => { + await new Promise((resolve) => server?.close(resolve)); + server = undefined; + await rm(dirname(oldSocketFile), { recursive: true, force: true }); + }); + + it('destroy removes it when the host is dead', async () => { + await seedSession(makeRecord({ status: 'destroyed', childPid: null })); + killProbeReportsDead(); + + await expect(destroySession('session-01')).rejects.toMatchObject({ + code: 'SESSION_ALREADY_DESTROYED', + }); + expect(existsSync(oldSocketFile)).toBe(false); + }); + + it('destroy keeps it when the host check throws', async () => { + await seedSession(makeRecord({ status: 'destroyed', childPid: null })); + const failure = Object.assign(new Error('kill EINVAL'), { + code: 'EINVAL', + }); + vi.spyOn(process, 'kill').mockImplementation(() => { + throw failure; + }); + const debug = vi.spyOn(console, 'debug').mockImplementation(() => {}); + + await expect(destroySession('session-01')).rejects.toMatchObject({ + code: 'SESSION_ALREADY_DESTROYED', + }); + expect(existsSync(oldSocketFile)).toBe(true); + expect(debug).toHaveBeenCalledWith( + expect.stringContaining('could not judge the host'), + failure, + ); + }); + }, +); + describe.skipIf(process.platform === 'win32')( 'destroy of a destroyed session', () => { diff --git a/test/unit/storage/homeScope.test.ts b/test/unit/storage/homeScope.test.ts index a5a657df..773ac2dd 100644 --- a/test/unit/storage/homeScope.test.ts +++ b/test/unit/storage/homeScope.test.ts @@ -1,4 +1,4 @@ -import { mkdir, mkdtemp, realpath, rm } from 'node:fs/promises'; +import { mkdir, mkdtemp, realpath, rm, writeFile } from 'node:fs/promises'; import { tmpdir } from 'node:os'; import { join } from 'node:path'; @@ -73,6 +73,16 @@ describe('scanHome (read-only Session counts)', () => { }); }); + it('skips a failed Session whose folder holds the destroy marker', async () => { + await seedSession({ sessionId: 'failed-1', status: 'failed' }); + await writeFile(join(sessionDir(home, 'failed-1'), 'destroyed'), ''); + + expect(await scanHome(home)).toEqual({ + activeSessions: 0, + totalSessions: 0, + }); + }); + it('treats a missing Home as having no Sessions', async () => { expect(await scanHome(join(home, 'does-not-exist'))).toEqual({ activeSessions: 0, @@ -104,6 +114,39 @@ describe('scanHome (read-only Session counts)', () => { expect(after.status).toBe('running'); }); + it('asks its dependencies whether a Session folder holds the destroy marker', async () => { + const dependencies: ScanHomeDependencies = { + readdir: () => Promise.resolve(['marked', 'plain']), + readManifestIfExists: (path) => + Promise.resolve( + makeRecord({ + sessionId: path.includes('marked') ? 'marked' : 'plain', + status: 'failed', + }), + ), + pathExists: (path) => path === '/fake/home/sessions/marked/destroyed', + }; + + expect(await scanHome('/fake/home', dependencies)).toEqual({ + activeSessions: 0, + totalSessions: 1, + }); + }); + + it('counts an active Session that holds the destroy marker', async () => { + const dependencies: ScanHomeDependencies = { + readdir: () => Promise.resolve(['marked']), + readManifestIfExists: () => + Promise.resolve(makeRecord({ sessionId: 'marked', status: 'running' })), + pathExists: () => true, + }; + + expect(await scanHome('/fake/home', dependencies)).toEqual({ + activeSessions: 1, + totalSessions: 1, + }); + }); + it('skips a Session whose manifest fails to read and counts the rest', async () => { // A single corrupt/unreadable manifest must not break discovery of the Home. const dependencies: ScanHomeDependencies = { @@ -114,6 +157,7 @@ describe('scanHome (read-only Session counts)', () => { : Promise.resolve( makeRecord({ sessionId: 'good', status: 'running' }), ), + pathExists: () => false, }; expect(await scanHome('/fake/home', dependencies)).toEqual({