diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 89802115..0191988c 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -41,7 +41,7 @@ The tool is TLC, the TLA+ model checker, pinned to release 1.7.4 by sha256. The Yes, when the diff changes any of these: - `src/host/lifecycle.ts`: `allocateSession` (and the order of its `launch` call and first manifest write), `launchHost`, `isProcessAlive`, the host proof (`readSessionHost`, `psShowsSessionHost`, `isHostAlive`, `hostMatches`, `killHostBestEffort`), `cliRunsInsideProgramSession` with `ownLinuxSessionId`, `ownProcessGroupId`, `controllingTerminal` and `sharesControllingTerminal`, `reconcileSession`, and `destroySession` with its local `stopLeftoversThenRecordDestroyed` and its helpers `recordDestroyed`, `stopSessionProcesses`, `readSessionManifestOrThrow`, `waitForTerminalManifest`, `waitForProcessesToExit` and `killProcessBestEffort`, and `removeDeadHostSocket`, which `gc` and `destroySession` call. -- `src/host/programGroup.ts`: the token capture (`captureProgram`, `captureToken`, `readAutogroup`, `parseAutogroup`, `parseProcStat`), the `/proc` reads (`readProcFileIfExists`, `readLiveThreadState`, `readProcStat`, `readShownProcStat`, `isRefusedRead`, `readBootId`), the record (`writeProgramRecord`, `readProgramRecord`, `readProvenProgramGroup`, `readProgramGroup`), the verdict (`judgeProgramGroup`, `readGroupMembers`), and the kill and the probe (`stopProgramGroup`, `isProgramGroupAlive`, `processGroupTarget`, `isProcessGroupAlive` with `groupHasLiveProcess` and `procHidesOtherUsers`, `killProcessGroupBestEffort`, `signalProcessGroup`). +- `src/host/programGroup.ts`: the token capture (`captureProgram`, `captureToken`, `readAutogroup`, `parseAutogroup`, `parseProcStat`), the `/proc` reads (`readProcFileIfExists`, `readLiveThreadState`, `readProcStat`, `readShownProcStat`, `isRefusedRead`, `readBootId`), the record (`writeProgramRecord`, `readProgramRecord`, `readProvenProgramGroup`, `readProgramGroup`), `procShowsOwnPidSpace`, the verdict (`judgeProgramGroup`, `readGroupMembers`), and the kill and the probe (`stopProgramGroup`, `isProgramGroupAlive`, `processGroupTarget`, `isProcessGroupAlive` with `groupHasLiveProcess` and `procHidesOtherUsers`, `killProcessGroupBestEffort`, `signalProcessGroup`). - `src/host/hostMain.ts`: `waitForManifestFromCreate`, `isSessionCommandable`, and in `runHost` the start-up statements (the manifest wait, the `hostPid === process.pid` check, the `host.json` write with `captureHost` and `writeHostRecord`, `createSerialManifestWriter`, `EventLog.open`, `createPty`, `setChildPid`, `captureProgram`), `hangUpProgram` with its kill timer and the `SHUTDOWN_KILL_GRACE_MS` constant, `startIdlePolling` (the idle time-out), `initiateShutdown`, `startShutdown`, `handlePtyExit` with its wait for the program's group, `pty.onExit`, the `SIGTERM` handler, the `resize` and `destroy` handlers, and the last `try` block (the `program.json` write, the start-up manifest write and `rpcServer.listen`). - `src/host/manifestWriter.ts` `createSerialManifestWriter`. - `src/cli/commands/gc.ts` `gcSessions`, `src/cli/commands/create.ts` `runCreateCommand` with `waitForReadyHost`, and `src/cli/commands/destroy.ts` `runDestroyCommand` with `rerunInNewSession`. @@ -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=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). +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=72` 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-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. +1. `scripts/facts.mjs` reads the code with the TypeScript compiler. It finds the thirty-two 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 71 times and prints one line per run. +3. It runs TLC 72 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. @@ -94,7 +94,7 @@ At the sync commit, the expected results are: | `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. | +| `mutant-UnsharedGroupReadsUnknown-otherspace`, `mutant-CreateRecordsHost-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`. @@ -446,7 +446,7 @@ Now `captureToken` reads the program's stat, then its autogroup, then its stat a A CLI without `/proc`, with an empty `/proc`, in another pid namespace or on another machine than the host sees none of the program's processes: its scan lists none, and its probe `kill(-pgid, 0)` ends ESRCH, or reaches a group of its own pid space that carries another autogroup. Without the guard, such a group with a token read gone, so `destroy` of an exited session recorded destroyed while a process that the program left still ran (Codex on coder/agent-tty#274). -Now `readProgramGroup` and `readProvenProgramGroup` return the unshared group when `sharesHostPids` reads false: `host.json` names another pid namespace or machine, or this process cannot read `/proc/self/ns/pid`. It reads alive, so the wait times out with `HOST_TIMEOUT`, and it gets no kill and no SIGSTOP. A session without `host.json`, as from an agent-tty version before it, keeps the old answer. `stopLeftoversThenRecordDestroyed` trusts a `destroyed` record of such a session without the wait, because only a process that saw the group wrote it, after a wait that read the group gone. So a plain `destroy` of a live session still ends `ok`, which `WitnessUnsharedDestroyCompletes` checks. The guard reads all of these statements and `sharesHostPids`. +Now `readProgramGroup` and `readProvenProgramGroup` return the unshared group when `sharesHostPids` reads false: `host.json` names another pid namespace or machine, this process cannot read `/proc/self/ns/pid`, or its `/proc/self` names another pid, as a `/proc` of another pid namespace does. It reads alive, so the wait times out with `HOST_TIMEOUT`, and it gets no kill and no SIGSTOP. A record with a token but no `host.json` gives the unshared group too, because nothing names the host's pid space. Only an agent-tty version between `program.json` and `host.json`, which no release holds, wrote such a session: the host now records a token only when it wrote `host.json` (`RecordsProgramSync` reads that statement). A session without a token and without `host.json`, as from a release before them, keeps the old answer. `stopLeftoversThenRecordDestroyed` trusts a `destroyed` record of such a session without the wait, because only a process that saw the group wrote it, after a wait that read the group gone. So a plain `destroy` of a live session still ends `ok`, which `WitnessUnsharedDestroyCompletes` checks. The guard reads all of these statements and `sharesHostPids`. ```sh id=$(node --import tsx src/cli/main.ts create --json -- sh -c 'trap "" HUP; sleep 300 & exit 0' | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))') @@ -456,6 +456,12 @@ AGENT_TTY_TEST_OTHER_PIDS=1 NODE_OPTIONS=--import=./test/fixtures/no-proc.ts nod node -e 'console.log(require(process.argv[1]).status)' "$d/session.json" # before: destroyed; now: exited ``` +### `CreateRecordsHost`: a CLI in another pid space reads a starting host dead (R2) + +A CLI in another pid namespace finds no process with the host's pid, so `judgeHost` reads the host dead unless `host.json` names it. The host wrote `host.json` only once it had read its manifest. A `list`, `inspect` or `gc` in another pid namespace that read the session between create's first manifest write and that record recorded a live host `failed`, and `gc` could then remove its folder. + +Now `allocateSession` reads the launched host with `captureHost` and writes `host.json` with `writeHostRecord` right after the launch, before the first manifest names the host. The host writes the record again when it starts. A capture that fails (no `/proc`, or off Linux) writes nothing, and then only the host writes the record. In the model, `CliHostAlive` is the CLI's view of the host: in another pid space a host that `host.json` names reads alive, and one that it does not name reads dead. `mutant-CreateRecordsHost-otherspace` must violate R2. `witness-WitnessUnrecordedHostMeetsKill` runs without the guard, because a live host that `host.json` does not name is out of the model's reach with it. + ### `ReusedIdReadsGone`: a wait that never ends while an unrelated group holds the id `isProgramGroupAlive` reads a group with a token alive while the check finds a live member with the token (`owned`), while it cannot run (`unknown`), and while it finds no live member and the probe of the id reads alive. A group whose live members carry another autogroup (`unproven`) reads gone. Without the guard, a group that took the program's id after the program's group ended read alive. `destroy` of the exited session then waited until it ended with `HOST_TIMEOUT`, and every reconcile waited and wrote nothing, until that unrelated group ended. @@ -482,7 +488,7 @@ kill -0 "$other" && echo alive # alive With a token, a kill needs a live member of the group in view, and a wait reads the group gone once no scan shows one. A program whose processes each fork their successor and end within about 2 ms, a fork chain, is almost never in view: by the time a scan reads a pid that its `/proc` listing showed, that process has ended, and the listing missed its successor. `stopProgramGroup` then killed nothing, the wait after it read the group gone, and `destroy` recorded `destroyed` while the chain ran (coder/agent-tty#244). -Now `stopProgramGroup` sends a group that `judgeLiveGroup` reads gone SIGSTOP and judges it again, until the loop's attempts run out. The kernel delivers a group signal also to a child that a member forks during the delivery, so the whole chain stops, and a stopped process stays in view. The next judge finds a stopped member with the token, and the group gets the kill. A frozen group that gets no kill, because its members carry another autogroup, only zombies are left, or a scan throws, gets SIGCONT from a `finally` block. In the model, the constant `Unseen` hides every process of the program from the scans: without the guard the kill through the token kills nothing, and the wait reads the group gone. `current-unseen` checks every rule with `Unseen`, and `mutant-FreezesUnseenGroup-unseen` must violate R11. The integration test "destroy ends a fork chain that no scan of /proc shows" in `test/integration/lifecycle.test.ts` runs `test/fixtures/fork-chain.py` in a session. +Now `stopProgramGroup` sends a group that `judgeLiveGroup` reads gone SIGSTOP and judges it again, until the loop's attempts run out. Each judgement that reads gone sends SIGSTOP again, so a member that a SIGCONT from elsewhere resumed stops again. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace, so `procShowsOwnPidSpace` reads false and no SIGSTOP goes out: the group id can name the CLI's own group there. The kernel delivers a group signal also to a child that a member forks during the delivery, so the whole chain stops, and a stopped process stays in view. The next judge finds a stopped member with the token, and the group gets the kill. A frozen group that gets no kill, because its members carry another autogroup, only zombies are left, or a scan throws, gets SIGCONT from a `finally` block. In the model, the constant `Unseen` hides every process of the program from the scans: without the guard the kill through the token kills nothing, and the wait reads the group gone. `current-unseen` checks every rule with `Unseen`, and `mutant-FreezesUnseenGroup-unseen` must violate R11. The integration test "destroy ends a fork chain that no scan of /proc shows" in `test/integration/lifecycle.test.ts` runs `test/fixtures/fork-chain.py` in a session. ```sh id=$(node --import tsx src/cli/main.ts create --json -- sh -c "python3 test/fixtures/fork-chain.py 30 0.002 $PWD/beat & wait" | node -e 'let s="";process.stdin.on("data",(d)=>(s+=d)).on("end",()=>console.log(JSON.parse(s).result.sessionId))') @@ -504,14 +510,14 @@ 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 25,534,376 distinct states, and without one 24,675,744. The check prints both counts. +The model checks every order of these steps for one session: one `create` that can give up on its host, its host, one `gc` pass over that session (not `--dry-run`), one other command that reconciles twice, one resize, one `destroy` (with or without `--force`, from outside or from inside the program's session), one SIGTERM to the host, a program exit at any time, a process of another user in the program's group that starts and ends at any time, a process that the program leaves when it exits on its own, the host's `host.json` and `program.json` writes, an unrelated group that takes the program's group id once the whole group has ended, an unrelated process that takes the host's pid once the host has ended, the kill timer of the host's shutdown, and a host crash at any time. With a token the model has 24,686,944 distinct states, and without one 24,467,356. The check prints both counts. It assumes: -- `isHostAlive` reads the host dead only on proof, through `judgeHost`: no process has `hostPid` (`kill(pid, 0)` gives ESRCH), `/proc//stat` shows a zombie, or `host.json` names another boot id or another start time than that process has. A missing or unreadable `host.json` (a host that has not written it yet, or an agent-tty version without it), a `/proc` that is not mounted or refuses the read, and a CLI in another pid namespace or on another machine than the ones that `host.json` names leave the host `unknown`, which reads alive and gets no kill. A CLI in another time namespace, where `/proc` adds another boottime offset to the start time, reads a host that a process still runs as `unknown` too. For a CLI in another pid namespace or on another machine, `readProgramGroup` without a token names no group either (`sharesHostPids`), so the `childPid` fallback gets no kill, and the `unknown` host keeps the session from a terminal write. The host writes `host.json` right after it read its manifest, with no `await` between. So on Linux with `/proc`, `isHostAlive` is true exactly while the host lives, as the model's `hostAlive` is, also for a host whose command line `--title` replaced. `destroy --force` sends SIGKILL to `hostPid` only when `hostMatches` proves the host: on Linux the boot id and start time match `host.json`, off Linux `/bin/ps -o command=` shows `_host `. A pid has one start time per boot, so a process that took the pid never matches (R19, coder/agent-tty#218). The check and the kill are separate system calls, the same window as for the program's group. Off Linux `isHostAlive` is `kill(pid, 0)`, so a zombie host or a process that took the pid reads alive: `list` keeps such a session running, and `destroy --force` kills nothing and ends with `HOST_TIMEOUT`. On Windows the check never passes, so `destroy --force` never kills the host there. The model's host record (`hrec`) is written in the host's manifest read, and the model lets an unrelated process take the pid of an ended host at any step (`HostPidReused`). It has no zombies. +- `isHostAlive` reads the host dead only on proof, through `judgeHost`: no process has `hostPid` (`kill(pid, 0)` gives ESRCH), `/proc//stat` shows a zombie, or `host.json` names another boot id or another start time than that process has. A missing or unreadable `host.json` (a create and a host that could not read `/proc`, or an agent-tty version without it), a `/proc` that is not mounted or refuses the read, and a CLI in another pid namespace or on another machine than the ones that `host.json` names leave the host `unknown`, which reads alive and gets no kill. A CLI in another time namespace, where `/proc` adds another boottime offset to the start time, reads a host that a process still runs as `unknown` too. For a CLI in another pid namespace or on another machine, `readProgramGroup` without a token names no group either (`sharesHostPids`), so the `childPid` fallback gets no kill, and the `unknown` host keeps the session from a terminal write. `create` writes `host.json` right after it launched the host, and the host writes it again right after it read its manifest, with no `await` between. So on Linux with `/proc`, `isHostAlive` is true exactly while the host lives, as the model's `hostAlive` is, also for a host whose command line `--title` replaced. `destroy --force` sends SIGKILL to `hostPid` only when `hostMatches` proves the host: on Linux the boot id and start time match `host.json`, off Linux `/bin/ps -o command=` shows `_host `. A pid has one start time per boot, so a process that took the pid never matches (R19, coder/agent-tty#218). The check and the kill are separate system calls, the same window as for the program's group. Off Linux `isHostAlive` is `kill(pid, 0)`, so a zombie host or a process that took the pid reads alive: `list` keeps such a session running, and `destroy --force` kills nothing and ends with `HOST_TIMEOUT`. On Windows the check never passes, so `destroy --force` never kills the host there. The model's host record (`hrec`) is written when `create` launches the host and in the host's manifest read, and the model lets an unrelated process take the pid of an ended host at any step (`HostPidReused`). It has no zombies. - The kernel does not reuse a pid while a process group with that id exists, so a kill of the program's group id reaches only that group while a process of it runs. Once the whole group has ended, a new process can get that id and lead an unrelated group (case 5 of coder/agent-tty#203). The model lets that happen at any step after the group ended. With a token, `stopProgramGroup` kills only right after it read a live member that carries the token again, and the model takes that check and the kill as one step. No API holds a process group the way a pidfd holds one process, so a gap stays between the check and the `kill(2)`: from the start of the member's re-read to the kill call it took p50 24 µs, p99 69 µs and at most 81 µs over 300 kills at a load average of 43. A group that takes the id inside that gap needs every member to exit, the pid counter to wrap onto the id, and the new process to lead a group, all within those microseconds. - The program runs from the spawn on, but `program.json` names it only after `captureProgram` read its token and `writeProgramRecord` renamed the file, in the same synchronous block. A host death inside that block leaves a program that no file names, and R16 exempts it (case 2 of coder/agent-tty#203). Over 150 sequential `create` calls on Linux, from the return of node-pty's spawn to the renamed `program.json`, at 1-minute load averages of 38 to 83, that took a median of 2.8 ms, a 90th percentile of 4.3 ms and at most 66 ms. A scratch build of `runHost` timed it with `performance.now()`. `captureProgram` took a median of 1.3 ms and at most 7.3 ms of that, so the long tail lies in the rest of the block and the write. node-pty returns before the child has called `setsid()`, so the capture polls for at most 250 ms until the child leads its own session. -- `OtherPidSpace` changes only how `destroy`, `list` and `gc` see the program's group. Their view of the host stays as in the shared pid space. In the code, `judgeHost` reads a host that `host.json` names in another pid space as `unknown`, which only keeps more sessions running. Before the host has written `host.json`, `judgeHost` probes the pid in the CLI's own pid space, a start-up window that the model leaves out. +- `OtherPidSpace` changes only how `destroy`, `list` and `gc` see the program's group. Their view of the host stays as in the shared pid space. `CliHostAlive` gives their view of the host: `judgeHost` reads a host that `host.json` names in another pid space as `unknown`, also after the host ended, so they never record it failed, and `hostMatches` never proves it, so `destroy --force` kills no host there. Without `host.json` they probe the pid in their own pid space, where no process has it, and read the host dead. `create` writes `host.json` before the first manifest names the host, so only a capture that failed, which the model leaves out, leaves that window open. - `current` describes Linux with autogroups, where the capture finds the token. The model reads every autogroup and the boot id. When `/proc` refuses the boot id, or shows no autogroup id for a live member in the program's session (a refused read, or an empty or malformed file), `judgeProgramGroup` gives `unknown`: no kill, and `isProgramGroupAlive` reads the group alive, so `destroy` ends with `HOST_TIMEOUT` and a reconcile writes nothing, as while a process of another user runs. A CLI that cannot list `/proc` at all, as in a chroot, sees no member. `judgeProgramGroup` then gives `gone`, so nothing gets the kill, and the probe of the group decides whether it reads alive. The model leaves those refused reads out. Without a token, `readProgramGroup` falls back to the childPid of the manifest, as before `program.json` existed: on macOS and Windows, on a kernel without `CONFIG_SCHED_AUTOGROUP`, when the capture read no autogroup or no boot id, and for a session that an older agent-tty created. There a reconcile and `destroy --force` kill that childPid as it is, `destroy` of a terminal session kills nothing, and a kill can still reach an unrelated group that took the id. `current-no-token` checks that fallback: the constant `Token` is FALSE there, so `program.json` names no group, and the host kills and probes the program's pid as it is. R15 and R16 do not hold on that path, so the run checks R1 to R14. The fallback kills only while the session folder exists. gc's real `rm` deletes file by file, so while it runs the folder can exist after `program.json` is gone, and a fallback kill in that moment can use a childPid that gc's removal made stale. - A `program.json` that does not parse, or that another version wrote, proves nothing: it gets no kill, and reconcile and `destroy` do not throw. A missing one gets the childPid fallback above. - A manifest write is atomic, because `writeManifest` renames a temp file. A write that fails counts as a host crash or a failed command. That covers a host write into a removed folder, which only a state that already breaks R1 reaches. diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 78085326..f0cedaf5 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -5,7 +5,7 @@ "src/cli/commands/destroy.ts#runDestroyCommand": "ecaa8b1d572da7c6", "src/cli/commands/destroy.ts#rerunInNewSession": "cf32d7d082758522", "src/cli/commands/gc.ts#gcSessions": "667e4ebc3ca3029c", - "src/host/lifecycle.ts#allocateSession": "77dab09b34fedce5", + "src/host/lifecycle.ts#allocateSession": "43819af8c6c271ec", "src/host/lifecycle.ts#launchHost": "597a5a6b9eb58cc8", "src/host/lifecycle.ts#isProcessAlive": "1ca1fe6ad6c41711", "src/host/lifecycle.ts#killProcessBestEffort": "1dd0cb4ee9bbc676", @@ -19,12 +19,12 @@ "src/host/hostRecord.ts#readHostRecord": "6e0fc70b53f945bc", "src/host/hostRecord.ts#pidExists": "d539275a0f6041ea", "src/host/hostRecord.ts#judgeHost": "85b37d524df156a4", - "src/host/hostRecord.ts#inPidNamespace": "4f4858fadf4acf81", + "src/host/hostRecord.ts#inPidNamespace": "aaa5cdfdfbb99f33", "src/host/hostRecord.ts#readTimeNamespace": "cd26abbdf639f1b8", "src/host/hostRecord.ts#inTimeNamespace": "3aa522616ace5b7a", "src/host/hostRecord.ts#readMachineId": "0873b5375df35f8f", "src/host/hostRecord.ts#inHostPidSpace": "66124bf9c4e33e0b", - "src/host/hostRecord.ts#sharesHostPids": "7669f6af0754088d", + "src/host/hostRecord.ts#sharesHostPids": "0c2a1fd9532efab5", "src/host/lifecycle.ts#ownLinuxSessionId": "e5f4eb175dab90da", "src/host/lifecycle.ts#ownProcessGroupId": "b480c93782250b9a", "src/host/lifecycle.ts#controllingTerminal": "d7c4b308f169a1fe", @@ -54,11 +54,11 @@ "src/host/programGroup.ts#readAutogroup": "2023ceccd585dcd8", "src/host/programGroup.ts#readBootId": "ceccda3fef7163f2", "src/host/programGroup.ts#captureToken": "4e948dddc8d0dba9", - "src/host/programGroup.ts#captureProgram": "f07d6160f3f22aed", + "src/host/programGroup.ts#captureProgram": "a8efb46d449ad2e6", "src/host/programGroup.ts#writeProgramRecord": "1845322710155185", "src/host/programGroup.ts#readProgramRecord": "b02c48c2bff248a7", - "src/host/programGroup.ts#readProvenProgramGroup": "a81172c2ed27f450", - "src/host/programGroup.ts#readProgramGroup": "ec7a4a291705bcbc", + "src/host/programGroup.ts#readProvenProgramGroup": "79abfacfdeb33135", + "src/host/programGroup.ts#readProgramGroup": "c783266ad349892e", "src/host/programGroup.ts#judgeProgramGroup": "b8b3053a25f95bbf", "src/host/programGroup.ts#readGroupMembers": "8f8103d1d5186e91", "src/host/programGroup.ts#judgeLiveGroup": "29c9c4bfd01c4338", @@ -70,7 +70,8 @@ "src/host/programGroup.ts#killProcessGroupBestEffort": "6d5d47cb5697681b", "src/host/programGroup.ts#signalProcessGroup": "c5a3a84361b67aa1", "src/host/programGroup.ts#isProgramGroupAlive": "f6fe01a280824f82", - "src/host/programGroup.ts#stopProgramGroup": "b6cfc91dd3027346", + "src/host/programGroup.ts#stopProgramGroup": "2a512f574e7bd5ae", + "src/host/programGroup.ts#procShowsOwnPidSpace": "ac852506311bb328", "src/host/rpcClient.ts#toTransportCliError": "dd6531349c62bcbd", "src/host/sessionState.ts#SessionState.setDimensions": "08c4f06122d157e9", "src/host/sessionState.ts#SessionState.requestDestroy": "f66074e815527ff1", @@ -86,13 +87,13 @@ "src/storage/manifests.ts#writeManifest": "1bcc99f09acfc577", "src/storage/manifests.ts#writeDestroyMarker": "7387a50b983a97c6", "src/protocol/sessionStatusPolicy.ts#SESSION_STATUS_POLICIES": "83827f9f7f6b8e1d", - "src/host/hostMain.ts#runHost(parts)": "10d2a8569f3b263e", + "src/host/hostMain.ts#runHost(parts)": "37e8ce5dc771d29c", "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": "f7270faba013acff", - "skill:scripts/facts.mjs": "82adfcc9fbc7fbb7", - "skill:scripts/check.sh": "3a47553300cb217a" + "skill:model/SessionLifecycle.tla": "7986bb289034aa6c", + "skill:scripts/facts.mjs": "ea6bebdccb255054", + "skill:scripts/check.sh": "66a765237f244773" }, "callSites": { "writeManifest": [ diff --git a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla index c4909cea..8c2f76f0 100644 --- a/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla +++ b/.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla @@ -103,6 +103,9 @@ CONSTANTS ReusedIdReadsGone, \* programGroup.ts: isProgramGroupAlive reads a \* group gone when its live members carry \* another autogroup (unproven) + CreateRecordsHost, \* lifecycle.ts: allocateSession writes host.json + \* for the launched host before the first + \* manifest ProvesHostPid, \* lifecycle.ts, hostRecord.ts: destroy --force \* kills the host only while its pid shows the \* boot id and start time that host.json holds @@ -144,7 +147,7 @@ ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, ReconcileSkipsTerminal, FallbackNeedsFolder, CreateStopsOnGiveUp, ReconcileRepairsDestroyed, ReconcileRepairsMarked, TokenNamesProgram, - ReusedIdReadsGone, ProvesHostPid, + ReusedIdReadsGone, ProvesHostPid, CreateRecordsHost, FreezesUnseenGroup, UnsharedGroupReadsUnknown} : b \in BOOLEAN Readers == {"gc", "list"} \* the two processes that run reconcileSession @@ -386,8 +389,8 @@ GroupSeen(kind) == \* sharesHostPids reads host.json. With UnsharedGroupReadsUnknown, \* readProgramGroup and readProvenProgramGroup give a group with a token \* that reads alive instead, so their waits time out. The host always runs -\* in its own pid space, so it keeps GroupSeen and HostKill. OtherPidSpace -\* leaves the CLI's view of the host as it is (see Scope). +\* in its own pid space, so it keeps GroupSeen and HostKill. CliHostAlive +\* gives the CLI's view of the host. CliGroupSeen(kind) == IF OtherPidSpace THEN kind = "proven" /\ UnsharedGroupReadsUnknown @@ -439,14 +442,21 @@ CreateWritesManifest == /\ UNCHANGED <> -\* launchHost spawns the detached `_host` process. +\* launchHost spawns the detached `_host` process. With CreateRecordsHost, +\* captureHost reads the new host in the same synchronous block, and +\* writeHostRecord writes host.json, which fails once gc removed the folder. +\* The model leaves out a capture that fails (no /proc, or off Linux), after +\* which only the host writes the record. CreateLaunchesHost == /\ cpc = "launch" /\ hostAlive' = TRUE /\ hpc' = "boot" /\ cpc' = IF CreateRecordsHostPid THEN "write" ELSE "done" + /\ hrec' = (CreateRecordsHost /\ dir) /\ UNCHANGED <> + shutVars, readerVars, destroyVars, rec, reused, + hitUnrelated, diedUnrecorded, passedReused, hreused, + hitUnrelatedHost>> \* runCreateCommand's readiness loop gives up after 50 inspect RPCs that \* fail, which the model lets happen at any step after the start-up, since @@ -815,9 +825,15 @@ HostPidReused == AfterReconcile(p) == IF p = "gc" THEN "readafter" ELSE "idle" +\* isHostAlive as destroy, list and gc see it. In another pid space, +\* judgeHost reads a host that host.json names as unknown, which reads alive +\* also after the host ended. Before host.json exists it probes the pid in +\* its own pid space, where no process has it, and reads the host dead. +CliHostAlive == IF OtherPidSpace THEN hrec ELSE hostAlive + \* `if (manifest.hostPid !== null && hostAlive) return`, where hostAlive is -\* isProcessAlive(manifest.hostPid). A null hostPid reads as a dead host. -SkipsHost(read) == ReconcileSkipsLiveHost /\ read.pid /\ hostAlive +\* isHostAlive(manifest.hostPid). A null hostPid reads as a dead host. +SkipsHost(read) == ReconcileSkipsLiveHost /\ read.pid /\ CliHostAlive \* readManifestIfExists. With ReconcileRepairsMarked, a terminal manifest \* other than destroyed next to the destroy marker (isMarkedDestroyed) goes @@ -1018,7 +1034,7 @@ GcFinalRead == /\ pc["gc"] = "final" /\ IF GcFinalCheck /\ mst # "none" /\ mst \notin Collectable THEN GcSkips - ELSE GcGoesTo(IF mpid /\ hostAlive THEN "rm" ELSE "rmsock") + ELSE GcGoesTo(IF mpid /\ CliHostAlive THEN "rm" ELSE "rmsock") /\ UNCHANGED <> @@ -1138,7 +1154,7 @@ DestroyReads == THEN /\ dpc' = "kill" /\ drd' = ReadCopy /\ UNCHANGED <> ELSE /\ dpc' = "rpc" /\ UNCHANGED <> - /\ sock' = (sock /\ (mst # "destroyed" \/ (mpid /\ hostAlive))) + /\ sock' = (sock /\ (mst # "destroyed" \/ (mpid /\ CliHostAlive))) /\ UNCHANGED <> @@ -1197,9 +1213,10 @@ DestroyUnlinksSocket == \* ProvesHostPid it kills only a host that hostMatches proves: the live host \* once host.json names it, never a process that took its pid. Without it, \* the kill reaches whatever has the pid. The copy that destroy read after -\* the first kill names the same host. +\* the first kill names the same host. In another pid space, hostMatches +\* never proves the host, so nothing gets the kill. KillsHost == - IF dpc \in {"kill", "rkill"} /\ drd.pid /\ hostAlive + IF dpc \in {"kill", "rkill"} /\ drd.pid /\ hostAlive /\ ~OtherPidSpace /\ (hrec \/ ~ProvesHostPid) THEN /\ HostDies /\ dkill' = TRUE /\ UNCHANGED hitUnrelatedHost ELSE IF dpc \in {"kill", "rkill"} /\ drd.pid /\ hreused /\ ~ProvesHostPid @@ -1237,7 +1254,7 @@ DestroyPollsGroup == /\ DestroyAt({"kwait", "rwait", "twait"}) /\ passedReused' = (passedReused \/ (reused /\ drd.grp = "proven" /\ ~CliGroupSeen(drd.grp))) - /\ IF CliGroupSeen(drd.grp) \/ (dpc # "twait" /\ drd.pid /\ hostAlive) + /\ IF CliGroupSeen(drd.grp) \/ (dpc # "twait" /\ drd.pid /\ CliHostAlive) THEN DestroyEnds("error") ELSE IF dpc = "kwait" THEN /\ dpc' = IF DestroyRecordsDestroyed THEN "reread" ELSE "final" diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index 7916c000..82664fe3 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/check.sh +++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh @@ -122,7 +122,7 @@ TERMINAL=$(node -e ' const c = JSON.parse(require("node:fs").readFileSync(process.argv[1], "utf8")).constants; console.log("{" + c.Terminal.map((s) => JSON.stringify(s)).join(", ") + "}"); ' "$OUT/facts.json") -GUARDS="GcSkipsNonCollectable GcFinalCheck ReconcileSkipsTerminal ReconcileSkipsLiveHost CreateRecordsHostPid HostWaitsForManifest ReconcileRereads HostSerializesWrites HostStopsAfterTerminalWrite ShutdownChecksCommandable DestroyRecordsDestroyed DestroyKeepsExitCode ManifestWriteNeedsFolder KillsProgramGroup ProbeCountsDeniedGroup HostWaitsForGroup ReconcileWaitsForGroup ReRunsInNewSession InsideCheckReadsEnv RecordsProgramSync ProvesGroupOwnership DestroyStopsLeftovers FallbackNeedsFolder ReconcileRepairsDestroyed ReconcileRepairsMarked CreateStopsOnGiveUp 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 CreateRecordsHost FreezesUnseenGroup UnsharedGroupReadsUnknown" # One "Guard=TRUE|FALSE" word per guard, read from the code by facts.mjs. FACTS_LINE=$(node -e ' const c = JSON.parse(require("node:fs").readFileSync(process.argv[1], "utf8")).constants; @@ -136,7 +136,7 @@ NO_TOKEN_RULES="NoLiveSessionDeleted HostDeathOnlyWhenDead TerminalIsFinal Recor # R15 and R16 are what the token adds, so only the runs with Token check them. RULES="$NO_TOKEN_RULES NoUnrelatedGroupKilled DestroyedSessionStopped" NO_TOKEN_WITNESSES="WitnessCreateGivesUp WitnessCrashReconciled WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessReconcileRepairs" -WITNESSES="WitnessGcRemovesSession WitnessCreateGivesUp WitnessSessionServes WitnessResizeLands WitnessCleanExitRecorded WitnessCrashReconciled WitnessDestroyCompletes WitnessSigtermRecorded WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessLeftoverMeetsDestroy WitnessReusedIdMeetsKill WitnessRecordNamesProgram WitnessUnrecordedProgramOutlives WitnessReconcileRepairs WitnessMarkedRepaired 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" # --- 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 witness-WitnessUnrecordedHostMeetsKill violated WitnessUnrecordedHostMeetsKill "CreateRecordsHost=FALSE" "without a record from create, as when its capture fails, a kill meets a host that host.json does not name yet" write_run mutant-ReconcileRepairsMarked pass DestroyedStaysDestroyed "ReconcileRepairsMarked=FALSE" "redundant in the model: it has no crash of a reconciling process, so the repair after the reconcile's own write always runs" write_run mutant-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" @@ -229,6 +230,7 @@ OTHER=TRUE write_run current-otherspace pass "$RULES" "" "the code with destroy, list and gc in another pid space: every rule holds" write_run witness-WitnessUnsharedDestroyCompletes-otherspace violated WitnessUnsharedDestroyCompletes "" "a plain destroy from another pid space still succeeds" write_run mutant-UnsharedGroupReadsUnknown-otherspace violated DestroyedSessionStopped "UnsharedGroupReadsUnknown=FALSE" "with the group read gone where no scan or probe shows it, destroy of an exited session records destroyed while a process it left runs" DestroyedSessionStopped +write_run mutant-CreateRecordsHost-otherspace violated HostDeathOnlyWhenDead "CreateRecordsHost=FALSE" "without the record from create, a reconcile in another pid space reads the starting host dead and records it failed" HostDeathOnlyWhenDead OTHER=FALSE # Without a token every kill falls back to the id that a manifest or the diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 9c7a8f23..ae7bdbee 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs @@ -242,9 +242,19 @@ function createFacts() { } return false; }); + // Right after the launch, captureHost reads the new host and + // writeHostRecord writes host.json, before the first manifest names it. + const recordsHost = + launch >= 0 && + write > launch + 2 && + normalize(body.statements[launch + 1].getText()) === + 'const hostRecord = captureHost(hostPid);' && + normalize(body.statements[launch + 2].getText()) === + 'if (hostRecord !== null) { writeHostRecord(sessionDirectory, hostRecord); }'; return { CreateRecordsHostPid: launch >= 0 && launch < write && pidInManifest && onlyThroughCallback, + CreateRecordsHost: recordsHost, CreateStopsOnGiveUp: stopsOnGiveUp(create.body), }; } @@ -629,7 +639,7 @@ function destroyFacts() { // that a process which saw the group recorded destroyed gets no wait for an // unshared group (trustsDestroyed). const UNSHARED_RETURN = - 'return (await sharesHostPids(sessionDirectory)) ? record : UNSHARED_GROUP;'; + 'return (await sharesHostPids(sessionDirectory, false)) ? record : UNSHARED_GROUP;'; const STOP_UNLESS_TRUSTED = "await stopSessionProcesses( sessionId, null, terminal.status === 'destroyed' && group !== null && 'unshared' in group ? null : group, sessionDirectory, signal, );"; const STOP_ALWAYS = @@ -895,7 +905,8 @@ function noAwaitIn(statements) { return !found; } -// runHost captures the program's token right after setChildPid and writes +// runHost captures the program's token right after setChildPid, only when it +// wrote host.json, and writes // program.json as the first statement of its last try, before // `await persistManifest()`, and no statement between createPty and that try // awaits. So the record is written in the synchronous block that spawns the @@ -904,9 +915,10 @@ function programRecordFacts() { const body = requireDeclaration('src/host/hostMain.ts', 'runHost').body; const spawn = indexOfStatement(body, /= createPty\(/); const named = indexOfStatement(body, /^state\.setChildPid\(pty\.pid\);$/); - const captured = indexOfStatement( - body, - /^const program = captureProgram\(pty\.pid\);$/, + const captured = body.statements.findIndex( + (s) => + normalize(s.getText()) === + 'const program = hostRecord === null ? programWithoutToken(pty.pid) : captureProgram(pty.pid);', ); const last = body.statements.at(-1); const tried = @@ -1006,10 +1018,11 @@ function ownershipFacts() { }; } -// In stopProgramGroup's loop, a judgement of gone sends SIGSTOP to the -// group once and judges again, so a member that a scan never shows stops and -// comes into view. The finally block sends a frozen group that got no kill -// SIGCONT, also when a scan throws. +// In stopProgramGroup's loop, each judgement of gone sends SIGSTOP to the +// group and judges again, so a member that a scan never shows stops and +// comes into view, while /proc names this process by its pid. The finally +// block sends a frozen group that got no kill SIGCONT, also when a scan +// throws. function freezeFacts(body) { const guarded = body.statements.find(ts.isTryStatement); const loop = guarded?.tryBlock.statements.find(ts.isForStatement); @@ -1029,7 +1042,14 @@ function freezeFacts(body) { before.at(-1) === 'let killed = false;' && guarded.tryBlock.statements.length === 1 && st[1] === - "if (judgement.verdict === 'gone') { frozen ||= signalProcessGroup(group.pid, 'SIGSTOP'); if (frozen) { continue; } }" && + "if (judgement.verdict === 'gone' && procShowsOwnPidSpace()) { frozen = signalProcessGroup(group.pid, 'SIGSTOP') || frozen; if (frozen) { continue; } }" && + normalize( + requireDeclaration( + 'src/host/programGroup.ts', + 'procShowsOwnPidSpace', + ).body.getText(), + ) === + "{ try { return readlinkSync('/proc/self') === String(process.pid); } catch { return false; } }" && normalize(guarded.finallyBlock.getText()) === "{ if (frozen && !killed) { signalProcessGroup(group.pid, 'SIGCONT'); } }" ); @@ -1124,7 +1144,7 @@ function unsharedFacts() { statement('stopProgramGroup', 2) === "if ('unshared' in group) { return; }" && shares === - "{ if (process.platform !== 'linux') { return true; } const record = await readHostRecord(sessionDirectory); return record === null || inHostPidSpace(record); }" && + "{ if (process.platform !== 'linux') { return true; } const record = await readHostRecord(sessionDirectory); return record === null ? sharedWithoutRecord : inHostPidSpace(record); }" && stopLeftoversThenRecordDestroyed( requireDeclaration('src/host/lifecycle.ts', 'destroySession'), ).trustsDestroyed, @@ -1373,6 +1393,7 @@ const COVERED = [ ['src/host/programGroup.ts', 'signalProcessGroup'], ['src/host/programGroup.ts', 'isProgramGroupAlive'], ['src/host/programGroup.ts', 'stopProgramGroup'], + ['src/host/programGroup.ts', 'procShowsOwnPidSpace'], ['src/host/rpcClient.ts', 'toTransportCliError'], ['src/host/sessionState.ts', 'SessionState.setDimensions'], ['src/host/sessionState.ts', 'SessionState.requestDestroy'], @@ -1397,7 +1418,7 @@ const RUN_HOST_PARTS = [ /= await EventLog\.open\(/, /= createPty\(/, /state\.setChildPid\(/, - /^const program = captureProgram\(/, + /^const program =/, /^const hangUpProgram = /, /^const startIdlePolling = /, /^const initiateShutdown = /, diff --git a/docs/USAGE.md b/docs/USAGE.md index 8ce3dd65..27fae573 100644 --- a/docs/USAGE.md +++ b/docs/USAGE.md @@ -344,27 +344,27 @@ Before each kill, agent-tty checks that a live process in the group has that aut If no process passes the check, agent-tty kills nothing, for example when an unrelated program now uses the group id. If `/proc` refuses to show the boot id, or shows no autogroup id for a live process whose group and session id are the program's pid (it refuses the read, or the file is empty or malformed), agent-tty cannot run the check. It then kills nothing and counts the group as running. -When the CLI cannot list `/proc` at all, as in a chroot or a container without it, it sees no process of the group, and nothing proves a kill. For a session without an autogroup record or without `host.json`, the group then counts as running while `kill(-pgid, 0)` finds a process. A plain `destroy` still ends a live session through its host, and `destroy --force` of a session with an autogroup record fails with `HOST_TIMEOUT`. End it with a plain `destroy`, or run `destroy --force` from a process that can read `/proc`. +When the CLI cannot list `/proc` at all, as in a chroot or a container without it, it sees no process of the group, and nothing proves a kill. For a session without an autogroup record, the group then counts as running while `kill(-pgid, 0)` finds a process. A session with an autogroup record but without `host.json` counts as running whatever the probe finds. A plain `destroy` still ends a live session through its host, and `destroy --force` of a session with an autogroup record fails with `HOST_TIMEOUT`. End it with a plain `destroy`, or run `destroy --force` from a process that can read `/proc`. On Linux, a CLI that cannot prove that it shares the host's pid space cannot prove that the program's group ended either: it cannot read `/proc/self/ns/pid` (no `/proc`, or an empty one), or `host.json` names another pid namespace or another machine. For a session with an autogroup record and a `host.json`, such a CLI counts the group as running and sends it no signal. On the host's machine, a plain `destroy` of a live session still ends it through its host. From another machine the host's socket does not answer, so a plain `destroy` fails with `HOST_UNREACHABLE`: run it on the machine that started the session. A `destroy` of a session whose program exited fails with `HOST_TIMEOUT` and keeps the session `exited`, also when no process of the group is left. This trade-off keeps `destroy` from recording `destroyed` while a process that the program left runs where the CLI cannot see it. Run such a `destroy` from a process in the host's pid namespace that can read `/proc`. `gc` still removes the folder of an `exited` session, as it does on every system. If the proven group, or a group that agent-tty cannot check, does not end within the destroy wait (about 5 s), `destroy` fails with `HOST_TIMEOUT` and does not record the session as `destroyed`. `destroy --force` and reconcile also check the host's pid from `session.json` before they trust it. -On Linux the host records its pid, the boot id, its start time from `/proc/self/stat`, its pid and time namespaces and the machine id (`/etc/machine-id`) in an internal file, `host.json`, when it starts. +On Linux the host records its pid, the boot id, its start time from `/proc/self/stat`, its pid and time namespaces and the machine id (`/etc/machine-id`) in an internal file, `host.json`. `create` writes it for the new host before `session.json` names the host, and the host writes it again when it starts. Reconcile counts the host as ended only when no process has its pid, when that process is a zombie, or when `host.json` names another boot or another start time than that process has. That covers a crashed host that stays a zombie under a container init that never reaps, and a later process that got the same pid. Reconcile then records the session as `failed`. `destroy --force` sends the host SIGKILL only when the boot id and the start time of the process match `host.json`, so it does not signal a process that got the pid before that check. The check and the kill are two system calls. A process that gets the pid between them still gets the signal, which needs the host to end, be reaped and its pid to go to a new process in that gap. When agent-tty cannot read `/proc` or `host.json`, it counts a host whose pid exists as running and does not kill it. With `host.json` but an unreadable `/proc/self/ns/pid`, it counts the host as running even when no process has its pid. When it runs in another pid namespace than the one that `host.json` names, or on another machine (another machine id), where the recorded pid can name an unrelated process, it counts the host as running and kills nothing, whatever that pid shows. Without a session token, it also kills no process group through the program's recorded pid there. In another time namespace than the host's, `/proc` shows start times with another boottime offset. There agent-tty counts the host as ended only when no process has its pid or that process is a zombie, and it does not kill the host. -Without `host.json`, as for a session that an agent-tty version without it started, agent-tty cannot tell that it runs in another pid namespace. There a pid that no process has, or a zombie, reads as an ended host, and a kill without a session token goes to the group that the program's recorded pid names there. +Without `host.json`, as for a session that an agent-tty version without it started, agent-tty cannot tell that it runs in another pid namespace. There a pid that no process has, or a zombie, reads as an ended host, and a kill without a session token goes to the group that the program's recorded pid names there. A session with an autogroup record but no `host.json`, which only unreleased development builds wrote, counts as out of the CLI's pid space: its group counts as running and gets no signal. A `hostPid` in `session.json` that differs from the pid in `host.json` never matches, so the session stays `running` and `destroy --force` kills nothing until `session.json` names the host again. That does not happen in normal use, because the host checks that `session.json` names its own pid. On macOS and the BSDs, `destroy --force` kills the host only when `/bin/ps` shows the pid running `_host `, the arguments that agent-tty starts the host with. Limits: 1. `destroy` does not kill a process that has left the program's process group. A process leaves the group when it calls `setsid` (for example `setsid cmd` or a daemon), or when an interactive shell with job control runs it as a job (for example `cmd &` typed into `bash -i`). Stop such a process yourself, or keep it in the program's group. -2. Some sessions have no autogroup record: sessions on macOS and Windows, on Linux kernels without autogroups (`/proc/self/autogroup` is missing), on Linux when `/proc` refuses to show the autogroup or the boot id at start-up, and sessions that an agent-tty version without `program.json` created. For these sessions, `destroy --force`, reconcile and the host's own kill at shutdown or at the idle time-out kill the process group (on Windows, the process) that `session.json` names, without the check, so such a kill can reach an unrelated process that took the group id after the program's group ended. `destroy` of a session whose program has already exited kills nothing. A `program.json` that agent-tty cannot read as a record, for example one that a newer version wrote, proves nothing: `destroy` and reconcile kill nothing for that session. -3. The check and the kill are separate system calls, a few microseconds apart. If every process of the group exits and an unrelated process takes the group id in that time, the kill reaches the unrelated process. No system call kills a process group through a handle, so this window remains. A group that no scan shows gets SIGSTOP before the check and SIGCONT when the check fails. If agent-tty itself dies between the two signals (SIGKILL, SIGINT, SIGTERM, SIGHUP, or the out-of-memory killer), an unrelated group that took the id stays stopped, and a later `destroy` does not resume it. Resume it with `kill -CONT -- -`, where `` is the Child PID that `inspect` shows. +2. Some sessions have no autogroup record: sessions on macOS and Windows, on Linux kernels without autogroups (`/proc/self/autogroup` is missing), on Linux when `/proc` refuses to show the autogroup, the boot id or the host's pid namespace at start-up, and sessions that an agent-tty version without `program.json` created. For these sessions, `destroy --force`, reconcile and the host's own kill at shutdown or at the idle time-out kill the process group (on Windows, the process) that `session.json` names, without the check, so such a kill can reach an unrelated process that took the group id after the program's group ended. `destroy` of a session whose program has already exited kills nothing. A `program.json` that agent-tty cannot read as a record, for example one that a newer version wrote, proves nothing: `destroy` and reconcile kill nothing for that session. +3. The check and the kill are separate system calls, a few microseconds apart. If every process of the group exits and an unrelated process takes the group id in that time, the kill reaches the unrelated process. No system call kills a process group through a handle, so this window remains. A group that no scan shows gets SIGSTOP before each check and SIGCONT when the checks fail. A CLI whose `/proc` belongs to another pid namespace sends no SIGSTOP. If the unrelated group is a job of an interactive shell, the shell reports the job as stopped, and after the SIGCONT the job runs in the background. If agent-tty itself dies between the two signals (SIGKILL, SIGINT, SIGTERM, SIGHUP, or the out-of-memory killer), an unrelated group that took the id stays stopped, and a later `destroy` does not resume it. Resume it with `kill -CONT -- -`, where `` is the Child PID that `inspect` shows. 4. The host writes `program.json` a few milliseconds after it starts the program. We timed 150 `create` calls on Linux, from the return of node-pty's spawn to the renamed `program.json`, at 1-minute load averages of 38 to 83: the median was 2.8 ms, the 90th percentile 4.3 ms, and the longest 66 ms. If the host dies in that window and the program ignores the hang-up signal, no file names the program, and `destroy` cannot end it. 5. `gc` removes `program.json` with the session folder, and `gc` kills nothing. Run `destroy` before `gc` when a program can leave processes behind. 6. Two cases where agent-tty cannot run the check end differently from a session that stays running: diff --git a/src/host/README.md b/src/host/README.md index 83f0efea..7c859ecf 100644 --- a/src/host/README.md +++ b/src/host/README.md @@ -12,7 +12,7 @@ - `isSessionCommandable(state)` and `assertSessionCommandable(state)` check that the session status is commandable. The assert throws `SESSION_NOT_RUNNING`. [hostMain.ts:isSessionCommandable] [hostMain.ts:assertSessionCommandable] - `resolveHostRendererName(input?)` picks the renderer name from the input, then `AGENT_TTY_HOST_RENDERER`, then `AGENT_TTY_RENDERER`, then `DEFAULT_RENDERER_NAME` (from `src/renderer/names.ts`). It throws `INVALID_INPUT` for an unknown renderer name. [hostMain.ts:resolveHostRendererName] - `MAX_CONSECUTIVE_POLL_FAILURES` (10) is the number of failed polls in a row after which a `waitForRender` wait rejects with the last poll error. A `CliError` keeps its code. The RPC server sends any other error as an RPC error, which the CLI reports as `RPC_ERROR`. [hostMain.ts:MAX_CONSECUTIVE_POLL_FAILURES] -- `allocateSession(config, launch)` validates an `AllocateConfig`, creates the session directory, calls `launch(sessionId)` and writes the first `running` manifest with the returned PID as `hostPid`. It returns an `AllocateResult` with `sessionId` and `sessionDirectory`. [lifecycle.ts:allocateSession] [lifecycle.ts:AllocateConfig] [lifecycle.ts:AllocateResult] +- `allocateSession(config, launch)` validates an `AllocateConfig`, creates the session directory, calls `launch(sessionId)`, writes `host.json` for the launched host when `captureHost` can read it, and writes the first `running` manifest with the returned PID as `hostPid`. It returns an `AllocateResult` with `sessionId` and `sessionDirectory`. [lifecycle.ts:allocateSession] [lifecycle.ts:AllocateConfig] [lifecycle.ts:AllocateResult] - `launchHost(config)` spawns the host process for a `LaunchHostConfig` and returns a `LaunchedHost`: its PID and a `stop()` that sends the host SIGTERM through the `ChildProcess` handle, and nothing once the host has exited. `create` calls it from the `launch` callback of `allocateSession`, and calls `stop()` on any error after `allocateSession` returned, such as a give-up on the host. [lifecycle.ts:launchHost] [lifecycle.ts:LaunchHostConfig] [lifecycle.ts:LaunchedHost] [src/cli/commands/create.ts:runCreateCommand] - `removeSocketDirectoryIfEmpty(socketFile)` removes the Home's socket directory with `rmdir`. A directory that still holds a socket (`ENOTEMPTY` or `EEXIST`) or is already gone (`ENOENT`) stays as it is. `destroySession` and `reconcileSession` call it after they unlink a socket. The host's shutdown and `doctor`'s socket check call `removeSocketDirectoryBestEffort`, which logs any other `rmdir` error at debug level instead of throwing it. [lifecycle.ts:removeSocketDirectoryIfEmpty] [lifecycle.ts:removeSocketDirectoryBestEffort] - `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] @@ -25,8 +25,8 @@ - `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] -- `stopProgramGroup(group)` SIGKILLs the group when the record proves it. A group that no scan shows first gets SIGSTOP and a second judgement, and SIGCONT when it gets no kill. `isProgramGroupAlive(group)` reports whether the group still holds a process that the kill would target. `judgeProgramGroup(record, bootId, rows)` is the pure decision: `owned`, `gone`, `unproven` or `unknown`. `parseProcStat` and `parseAutogroup` parse `/proc//stat` and `/proc//autogroup`. `parseAutogroup` returns `null` for text that names no autogroup, and a member whose autogroup file cannot be read or parsed carries no token. [programGroup.ts:stopProgramGroup] [programGroup.ts:isProgramGroupAlive] [programGroup.ts:judgeProgramGroup] [programGroup.ts:parseProcStat] +- `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 missing `host.json`, a CLI that cannot read `/proc/self/ns/pid` and a CLI whose `/proc/self` does not name its own 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] +- `stopProgramGroup(group)` SIGKILLs the group when the record proves it. A group that no scan shows gets SIGSTOP and another judgement, at each of up to 5 judgements while `/proc/self` names this process's pid, and SIGCONT when it gets no kill. `isProgramGroupAlive(group)` reports whether the group still holds a process that the kill would target. `judgeProgramGroup(record, bootId, rows)` is the pure decision: `owned`, `gone`, `unproven` or `unknown`. `parseProcStat` and `parseAutogroup` parse `/proc//stat` and `/proc//autogroup`. `parseAutogroup` returns `null` for text that names no autogroup, and a member whose autogroup file cannot be read or parsed carries no token. [programGroup.ts:stopProgramGroup] [programGroup.ts:isProgramGroupAlive] [programGroup.ts:judgeProgramGroup] [programGroup.ts:parseProcStat] - `captureHost(pid)` returns a `HostRecord` (`version`, `pid`, `bootId`, `startTicks`, `pidNamespace`, `timeNamespace`, `machineId`) on Linux when `/proc` shows the process and the boot id, else `null`. `machineId` is the first of `/etc/machine-id` and `/var/lib/dbus/machine-id` that holds 32 hex characters, else `null`. A record without `timeNamespace` and `machineId`, which a build between #260 and #267 wrote, still reads, and only the checks of those two fields are skipped. `writeHostRecord(sessionDirectory, record)` writes it as `host.json`, and `readHostRecord(sessionDirectory)` returns it, or `null` when it is missing or unreadable. `judgeHost(pid, record)` returns `dead` only when no process has the pid, a zombie has it, or the record names another boot id or start time, `alive` when both match, and `unknown` otherwise: also off Linux for a pid that exists, for a CLI in another pid namespace or on another machine than the record names, and, instead of a start time mismatch, for a CLI in another time namespace. [hostRecord.ts:captureHost] [hostRecord.ts:writeHostRecord] [hostRecord.ts:readHostRecord] [hostRecord.ts:judgeHost] - `SessionState` holds the host's in-memory `SessionRecord` (type from `src/protocol/schemas.ts`). Methods: `snapshot`, `setChildPid`, `setDimensions`, `setFailureOrigin`, `requestDestroy`, `recordDestroyed` and `recordExit`. [sessionState.ts:SessionState] - `createSerialManifestWriter(path, snapshot, write?)` returns a function that writes `snapshot()` to `path`. The default `write` is `writeManifest` (`src/storage/manifests.ts`). `runHost` sends every manifest write through one such function. [manifestWriter.ts:createSerialManifestWriter] [hostMain.ts:runHost] @@ -57,7 +57,7 @@ - `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` writes `destroyed` (both PIDs `null`, the exit code kept, no failure fields) over a terminal manifest other than `destroyed` when the destroy marker exists (`writeMarkedDestroyed`). It then unlinks the socket, removes the Home's socket directory if it is empty, removes the old socket at `legacySocketPath` when `isOwnLegacySocket` accepts it, and returns. 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] +- 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) 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, up to 5 times, and each judgement that reads `gone` sends SIGSTOP again, for a member that a SIGCONT from elsewhere resumed. When `/proc/self` does not name this process's pid, `/proc` belongs to another pid namespace and no SIGSTOP goes out. 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 }`, which a record with a token gives when `host.json` names another pid space or is missing, 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] - `buildReplayInput` validates the manifest with `SessionRecordSchema` and requires its `sessionId` to match. It validates the events with `validateEventRecords` unless `trustValidated` is set. `targetSeq` is -1 for no events, else from 0 to the last `seq`. [replay.ts:buildReplayInput] @@ -73,7 +73,7 @@ ## Side Effects - `launchHost` runs `child_process.spawn(process.execPath, [...process.execArgv, process.argv[1], '_host', sessionId, String(process.pid)])` with `detached: true`, `stdio: 'ignore'` and an environment of the CLI's `process.env` merged with `config.env`, plus `AGENT_TTY_HOME` and `TERM`, then calls `unref()`. The last argument is the creator PID that the host passes to `waitForManifestFromCreate`. [lifecycle.ts:launchHost] [src/cli/main.ts:main] -- `allocateSession` calls `ensureHome`, creates the session directory with mode `0o700`, calls `launch` (in `create`, this starts the host process) and then writes `session.json` with `writeManifest` (`src/storage/manifests.ts`). It calls `ensureHome` before it checks `cwd`, because the `cwd` can be a new Home. It checks `cwd`, the shell path and the command segments before it creates the session directory, so a failed check leaves no session directory. A `chmod` failure after `mkdir` leaves an empty session directory under `/sessions`. [lifecycle.ts:allocateSession] +- `allocateSession` calls `ensureHome`, creates the session directory with mode `0o700`, calls `launch` (in `create`, this starts the host process), writes `host.json` for that host with `captureHost` and `writeHostRecord`, and then writes `session.json` with `writeManifest` (`src/storage/manifests.ts`). It calls `ensureHome` before it checks `cwd`, because the `cwd` can be a new Home. It checks `cwd`, the shell path and the command segments before it creates the session directory, so a failed check leaves no session directory. A `chmod` failure after `mkdir` leaves an empty session directory under `/sessions`. [lifecycle.ts:allocateSession] - `destroySession` and `reconcileSession` call `process.kill` (signal 0 as a liveness probe, `SIGKILL` to stop, `SIGSTOP` and `SIGCONT` to freeze a group that no scan shows), read `program.json` and `host.json`, read `/proc//stat` and the boot id on Linux, run `/bin/ps -o command=` before a host kill off Linux, write the manifest with `writeManifest`, unlink the socket file and call `removeSocketDirectoryIfEmpty`. `destroySession` also calls `sendRpc(..., 'destroy')` and writes the destroy marker with `writeDestroyMarker`, and `reconcileSession` checks whether that marker exists with `existsSync`. [lifecycle.ts:destroySession] [lifecycle.ts:reconcileSession] - `listSessions` reads `/sessions` and each manifest, and can call `reconcileSession`. [lifecycle.ts:listSessions] - `stopProgramGroup` and `isProgramGroupAlive` read, without yielding, `/proc//stat` of every process, `/proc//task//stat` of each process that shows Z, `/proc//autogroup` of the group's members and `/proc/sys/kernel/random/boot_id`. `captureProgram` reads the same files for the program and the host. `writeProgramRecord` writes `/program.json` through `writeValidatedJsonFileSync` (`src/storage/manifests.ts`), which creates no folder. `runHost` writes `/host.json` the same way with `writeHostRecord`, right after it read its manifest. [programGroup.ts:stopProgramGroup] [programGroup.ts:captureProgram] [programGroup.ts:writeProgramRecord] [hostRecord.ts:writeHostRecord] diff --git a/src/host/hostMain.ts b/src/host/hostMain.ts index f75b5be6..0c9bc07d 100644 --- a/src/host/hostMain.ts +++ b/src/host/hostMain.ts @@ -18,6 +18,7 @@ import { import { createSerialManifestWriter } from './manifestWriter.js'; import { captureProgram, + programWithoutToken, stopProgramGroup, writeProgramRecord, } from './programGroup.js'; @@ -346,7 +347,12 @@ export async function runHost( 'PTY child PID must be a positive integer', ); state.setChildPid(pty.pid); - const program = captureProgram(pty.pid); + // A token proves the group only beside host.json, which names the pid + // space of its pid, so a host that could not record itself records none. + const program = + hostRecord === null + ? programWithoutToken(pty.pid) + : captureProgram(pty.pid); // Answer the terminal-capability queries programs emit at startup (OSC 10/11 // color probes, the `ESC [ 5 n` DSR sentinel, XTGETTCAP/DECRQSS 24-bit color diff --git a/src/host/hostRecord.ts b/src/host/hostRecord.ts index 18efa662..90a34be4 100644 --- a/src/host/hostRecord.ts +++ b/src/host/hostRecord.ts @@ -68,9 +68,14 @@ export function captureHost(pid: number): HostRecord | null { } } +// A /proc of another pid namespace names this process by another pid, and +// its listing shows none of this namespace's processes. function inPidNamespace(pidNamespace: string): boolean { try { - return readlinkSync('/proc/self/ns/pid') === pidNamespace; + return ( + readlinkSync('/proc/self/ns/pid') === pidNamespace && + readlinkSync('/proc/self') === String(process.pid) + ); } catch { return false; } @@ -152,14 +157,19 @@ export async function readHostRecord( } } +// Without host.json nothing names the host's pid space: a session from an +// agent-tty version before it, or one whose create and host could not read +// /proc. Since the host writes host.json before program.json, only a version +// between the two files, which no release holds, wrote a token without it. export async function sharesHostPids( sessionDirectory: string, + sharedWithoutRecord: boolean, ): Promise { if (process.platform !== 'linux') { return true; } const record = await readHostRecord(sessionDirectory); - return record === null || inHostPidSpace(record); + return record === null ? sharedWithoutRecord : inHostPidSpace(record); } function pidExists(pid: number): boolean { diff --git a/src/host/lifecycle.ts b/src/host/lifecycle.ts index 8d2694c8..1ffc620a 100644 --- a/src/host/lifecycle.ts +++ b/src/host/lifecycle.ts @@ -41,7 +41,13 @@ import { stopProgramGroup, type ProgramGroup, } from './programGroup.js'; -import { judgeHost, readHostRecord, type HostRecord } from './hostRecord.js'; +import { + captureHost, + judgeHost, + readHostRecord, + writeHostRecord, + type HostRecord, +} from './hostRecord.js'; import { sendRpc } from './rpcClient.js'; import { ensureSocketRoot, isOwnLegacySocket } from './socketRoot.js'; @@ -717,6 +723,13 @@ export async function allocateSession( await chmod(sessionDirectory, 0o700); const hostPid = launch(sessionId); + // Before the first manifest names the host, so that a CLI in another pid + // namespace reads the starting host by its record, not by a pid that its + // own namespace lacks. The host writes the record again once it starts. + const hostRecord = captureHost(hostPid); + if (hostRecord !== null) { + writeHostRecord(sessionDirectory, hostRecord); + } const now = new Date().toISOString(); await writeManifest(manifestPath(sessionDirectory), { diff --git a/src/host/programGroup.ts b/src/host/programGroup.ts index c460268a..6f0681f5 100644 --- a/src/host/programGroup.ts +++ b/src/host/programGroup.ts @@ -1,4 +1,4 @@ -import { existsSync, readdirSync, readFileSync } from 'node:fs'; +import { existsSync, readdirSync, readFileSync, readlinkSync } from 'node:fs'; import process from 'node:process'; import { z } from 'zod'; @@ -47,7 +47,7 @@ interface ChildPidGroup { // A group with a token in a pid space that this process cannot prove it // shares with the host: without /proc, with an empty /proc, in another pid -// namespace or on another machine. No scan or probe here shows the +// namespace or on another machine, or without host.json. No scan or probe here shows the // program's processes, so the group reads alive and gets no kill. interface UnsharedGroup { readonly unshared: true; @@ -232,10 +232,14 @@ function captureToken( return null; } +export function programWithoutToken(pid: number): ProgramRecord { + return { version: 1, pid, bootId: null, autogroup: null }; +} + export function captureProgram(pid: number): ProgramRecord { const token = captureToken(pid); return token === null - ? { version: 1, pid, bootId: null, autogroup: null } + ? programWithoutToken(pid) : { version: 1, pid, ...token }; } @@ -299,7 +303,9 @@ export async function readProvenProgramGroup( if (typeof record !== 'object' || !hasToken(record)) { return null; } - return (await sharesHostPids(sessionDirectory)) ? record : UNSHARED_GROUP; + return (await sharesHostPids(sessionDirectory, false)) + ? record + : UNSHARED_GROUP; } export async function readProgramGroup( @@ -308,12 +314,14 @@ export async function readProgramGroup( ): Promise { const record = await readProgramRecord(sessionDirectory); if (typeof record === 'object' && hasToken(record)) { - return (await sharesHostPids(sessionDirectory)) ? record : UNSHARED_GROUP; + return (await sharesHostPids(sessionDirectory, false)) + ? record + : UNSHARED_GROUP; } if ( record === 'invalid' || childPid === null || - !(await sharesHostPids(sessionDirectory)) + !(await sharesHostPids(sessionDirectory, true)) ) { return null; } @@ -547,6 +555,18 @@ function signalProcessGroup( } } +// /proc names this process by its own pid only when /proc belongs to this +// process's pid namespace. A /proc of another namespace, as after +// `unshare --pid --fork` without --mount-proc, shows none of this +// namespace's processes, and the group id can name this process's own group. +function procShowsOwnPidSpace(): boolean { + try { + return readlinkSync('/proc/self') === String(process.pid); + } catch { + return false; + } +} + export function isProgramGroupAlive(group: ProgramGroup | null): boolean { if (group === null) { return false; @@ -596,15 +616,16 @@ export function stopProgramGroup(group: ProgramGroup | null): void { // A member that forks its successor and ends between scans is never in // view. SIGSTOP freezes the group, also a child that a member forks while // the kernel delivers it, and a stopped member stays in view, so a frozen - // group that reads gone is judged again. A frozen group that gets no kill - // gets SIGCONT, also when a scan throws. + // group that reads gone is judged again. Each such judgement sends SIGSTOP + // again, for a member that a SIGCONT from elsewhere resumed. A frozen group + // that gets no kill gets SIGCONT, also when a scan throws. let frozen = false; let killed = false; try { for (let attempt = 0; attempt < STOP_ATTEMPTS; attempt += 1) { const judgement = judgeLiveGroup(group); - if (judgement.verdict === 'gone') { - frozen ||= signalProcessGroup(group.pid, 'SIGSTOP'); + if (judgement.verdict === 'gone' && procShowsOwnPidSpace()) { + frozen = signalProcessGroup(group.pid, 'SIGSTOP') || frozen; if (frozen) { continue; } diff --git a/test/fixtures/denied-pid-namespace.ts b/test/fixtures/denied-pid-namespace.ts new file mode 100644 index 00000000..f820f9f6 --- /dev/null +++ b/test/fixtures/denied-pid-namespace.ts @@ -0,0 +1,22 @@ +// Preload (`--import`) that makes every read of a /proc//ns/pid link fail +// with EACCES, as a /proc that shows the autogroup but not the namespace does. +import fs from 'node:fs'; +import { syncBuiltinESMExports } from 'node:module'; + +const readlinkSync = fs.readlinkSync as (...args: unknown[]) => unknown; + +fs.readlinkSync = ((path: unknown, ...rest: unknown[]) => { + if (typeof path === 'string' && /^\/proc\/(\d+|self)\/ns\/pid$/.test(path)) { + throw Object.assign( + new Error(`EACCES: permission denied, readlink '${path}'`), + { + errno: -13, + code: 'EACCES', + syscall: 'readlink', + path, + }, + ); + } + return readlinkSync(path, ...rest); +}) as typeof fs.readlinkSync; +syncBuiltinESMExports(); diff --git a/test/integration/lifecycle.test.ts b/test/integration/lifecycle.test.ts index d7ad5e77..d4128115 100644 --- a/test/integration/lifecycle.test.ts +++ b/test/integration/lifecycle.test.ts @@ -1012,6 +1012,43 @@ describe('lifecycle integration', { timeout: 60_000 }, () => { }, ); + // A token proves the group only beside host.json, which names its pid + // space, so a host that cannot record itself records no token. + it.runIf(capturesToken)( + 'destroy of an exited session whose host could not read its pid namespace ends ok', + async () => { + const result = runCli( + ['create', '--json', '--', '/bin/sh', '-c', 'exit 0'], + { + AGENT_TTY_HOME: testHome, + NODE_OPTIONS: [ + process.env.NODE_OPTIONS ?? '', + `--import=${pathToFileURL(resolve('test/fixtures/denied-pid-namespace.ts')).href}`, + ].join(' '), + }, + ); + const { sessionId } = ( + JSON.parse(result.stdout) as SuccessEnvelope<{ sessionId: string }> + ).result; + const directory = sessionDir(testHome, sessionId); + const deadline = Date.now() + 10_000; + while (inspectSession(testHome, sessionId).status !== 'exited') { + expect(Date.now()).toBeLessThan(deadline); + await sleep(100); + } + expect(existsSync(join(directory, 'host.json'))).toBe(false); + expect( + JSON.parse(await readFile(programRecordPath(directory), 'utf8')), + ).toMatchObject({ bootId: null, autogroup: null }); + + const destroyed = runCli(['destroy', sessionId, '--json'], { + AGENT_TTY_HOME: testHome, + }); + expect(JSON.parse(destroyed.stdout)).toMatchObject({ ok: true }); + expect(inspectSession(testHome, sessionId).status).toBe('destroyed'); + }, + ); + // Only a session with a token checks the autogroup. it.runIf(capturesToken)( 'destroy times out while it cannot read the autogroup of a process that the program left', diff --git a/test/unit/host/lifecycle.test.ts b/test/unit/host/lifecycle.test.ts index b267fbc2..55afaeba 100644 --- a/test/unit/host/lifecycle.test.ts +++ b/test/unit/host/lifecycle.test.ts @@ -18,6 +18,7 @@ import { afterEach, beforeEach, describe, expect, it, vi } from 'vitest'; const fsHooks = vi.hoisted(() => ({ afterReadFile: undefined as ((path: string) => Promise) | undefined, + beforeRename: undefined as ((target: string) => void) | undefined, // /proc//stat by pid, or the error that its read throws. proc: undefined as Map | undefined, mountinfo: undefined as string | undefined, @@ -143,6 +144,14 @@ vi.mock('node:fs/promises', async () => { } return contents; }; + const rename = async ( + ...args: Parameters + ): Promise => { + if (typeof args[1] === 'string') { + fsHooks.beforeRename?.(args[1]); + } + await actual.rename(...args); + }; const rmdir = async ( ...args: Parameters ): Promise => { @@ -151,7 +160,7 @@ vi.mock('node:fs/promises', async () => { } await actual.rmdir(...args); }; - return { ...actual, readFile, rmdir }; + return { ...actual, readFile, rename, rmdir }; }); // destroy and reconcile poll for about 5 s. These tests skip the waits. @@ -197,6 +206,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 { + hostRecordPath, legacySocketPath, manifestPath, sessionDir, @@ -225,9 +235,18 @@ afterEach(async () => { fsHooks.ownStat = undefined; fsHooks.files = undefined; fsHooks.links = undefined; + fsHooks.beforeRename = undefined; await rm(home, { recursive: true, force: true }); }); +// A token proves the group only with a host.json that names this pid space. +function recordOwnPidSpace(directory: string): void { + writeHostRecord(directory, { + ...(captureHost(process.pid) as HostRecord), + pid: HOST_PID, + }); +} + function errno(code: string): Error { return Object.assign(new Error(code), { code }); } @@ -346,6 +365,45 @@ describe('allocateSession', () => { }); }); + // A CLI in another pid namespace finds no process with the host's pid. A + // host.json from the start on keeps it from reading the host dead. + it.runIf(process.platform === 'linux')( + 'records the host before the first manifest names it', + async () => { + const host = spawn('sleep', ['30'], { detached: true, stdio: 'ignore' }); + try { + await once(host, 'spawn'); + const hostPid = host.pid as number; + const hostRecordAtFirstManifest: boolean[] = []; + fsHooks.beforeRename = (target) => { + if (target.endsWith('/session.json')) { + hostRecordAtFirstManifest.push( + existsSync(hostRecordPath(dirname(target))), + ); + } + }; + const result = await allocateSession(makeConfig(), () => hostPid); + expect(hostRecordAtFirstManifest).toEqual([true]); + fsHooks.links = new Map([['/proc/self/ns/pid', 'pid:[1]']]); + const kill = process.kill.bind(process); + vi.spyOn(process, 'kill').mockImplementation((pid, signal) => { + if (pid === hostPid && signal === 0) { + throw errno('ESRCH'); + } + return kill(pid, signal); + }); + + await reconcileSession(result.sessionDirectory); + + expect( + await readManifest(manifestPath(result.sessionDirectory)), + ).toMatchObject({ status: 'running', hostPid }); + } finally { + host.kill('SIGKILL'); + } + }, + ); + it('does not launch a host when the working directory does not exist', async () => { const launch = vi.fn(() => 4242); @@ -731,6 +789,7 @@ describe('reconcileSession', () => { expect(record.autogroup).not.toBeNull(); const directory = await seedSession(makeRecord({ childPid: group })); writeProgramRecord(directory, change(record)); + recordOwnPidSpace(directory); const send = process.kill.bind(process); const kill = vi .spyOn(process, 'kill') @@ -895,6 +954,7 @@ describe('destroySession', () => { expect(record.autogroup).not.toBeNull(); const directory = await seedSession(exited); writeProgramRecord(directory, record); + recordOwnPidSpace(directory); return directory; } diff --git a/test/unit/host/programGroup.test.ts b/test/unit/host/programGroup.test.ts index 279e5f3a..b976eeca 100644 --- a/test/unit/host/programGroup.test.ts +++ b/test/unit/host/programGroup.test.ts @@ -49,6 +49,8 @@ const procHooks = vi.hoisted(() => ({ mountinfo: undefined as string | undefined, // The error that the /proc listing throws. listError: undefined as Error | undefined, + // What /proc/self names, when not this process's pid. + self: undefined as string | undefined, })); const autogroupFile = vi.hoisted(() => ({ @@ -116,7 +118,16 @@ vi.mock('node:fs', async () => { } return stat; }) as typeof actual.readFileSync; - return { ...actual, readdirSync, readFileSync }; + // A faked /proc names this process at /proc/self, also on macOS. + const readlinkSync = ((path: string, ...rest: unknown[]) => + path === '/proc/self' && + (procHooks.self !== undefined || procHooks.stat !== undefined) + ? (procHooks.self ?? String(process.pid)) + : (actual.readlinkSync as (...args: unknown[]) => unknown)( + path, + ...rest, + )) as typeof actual.readlinkSync; + return { ...actual, readdirSync, readFileSync, readlinkSync }; }); const platform = process.platform; @@ -128,6 +139,7 @@ afterEach(() => { procHooks.taskErrors.clear(); procHooks.mountinfo = undefined; procHooks.listError = undefined; + procHooks.self = undefined; autogroupFile.read = null; Object.defineProperty(process, 'platform', { value: platform }); }); @@ -1099,12 +1111,14 @@ describe('a program group with a token, as a faked /proc shows it', () => { stopProgramGroup(group); expect(kill.mock.calls).toEqual([ + [-CHILD_PID, 'SIGSTOP'], [-CHILD_PID, 'SIGSTOP'], [-CHILD_PID, 'SIGKILL'], ]); }); - it('continues a frozen group that reads gone at each of its 5 judgements', () => { + // A SIGCONT from elsewhere can resume a member between two judgements. + it('stops a group that reads gone again at each of its 5 judgements, then continues it', () => { procShowsTokenGroup(); let judged = 0; autogroupFile.read = (file) => { @@ -1123,11 +1137,23 @@ describe('a program group with a token, as a faked /proc shows it', () => { expect(judged).toBe(5); expect(kill.mock.calls).toEqual([ - [-CHILD_PID, 'SIGSTOP'], + ...Array.from({ length: 5 }, () => [-CHILD_PID, 'SIGSTOP']), [-CHILD_PID, 'SIGCONT'], ]); }); + // There the scan shows none of this namespace's processes, and the group + // id can name the CLI's own group. + it('sends no SIGSTOP when /proc belongs to another pid namespace', () => { + procShowsTokenGroup(); + procHooks.self = String(process.pid + 1); + const kill = vi.spyOn(process, 'kill').mockReturnValue(true); + + stopProgramGroup(group); + + expect(kill).not.toHaveBeenCalled(); + }); + it('continues a frozen group when a scan after the SIGSTOP throws', () => { procShowsTokenGroup(); const kill = vi @@ -1393,6 +1419,34 @@ describe.runIf(platform === 'linux')('a program record with a token', () => { expect(await readProvenProgramGroup(directory)).toEqual(record); }); + // A /proc of another pid namespace names this process by another pid, and + // its scan shows none of the program's processes. + it("reads alive in the host's pid namespace when /proc belongs to another one", async () => { + recordHostIn(readlinkSync('/proc/self/ns/pid')); + procHooks.self = String(process.pid + 1); + + expect(await readProgramGroup(directory, 4242)).toEqual({ unshared: true }); + expect(await readProvenProgramGroup(directory)).toEqual({ + unshared: true, + }); + }); + + // Only an agent-tty version between program.json and host.json wrote a + // token without host.json, and nothing names its pid space. + it('reads alive and gets no kill without a host record', async () => { + const kill = vi.spyOn(process, 'kill'); + + for (const group of [ + await readProgramGroup(directory, 4242), + await readProvenProgramGroup(directory), + ]) { + expect(group).toEqual({ unshared: true }); + expect(isProgramGroupAlive(group)).toBe(true); + stopProgramGroup(group); + } + expect(kill).not.toHaveBeenCalled(); + }); + // No scan or probe here shows the program's processes. it("reads alive and gets no kill in a pid namespace other than the host's", async () => { recordHostIn('pid:[1]');