fix(destroy): freeze a group whose member ends between two reads before destroy gives up on it

.agents/skills/verify-session-lifecycle/SKILL.md

@@ -546,7 +546,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. 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.
+Now `stopProgramGroup` sends a group that `judgeLiveGroup` reads gone SIGSTOP and judges it again, until the loop's attempts run out. A scan can also show a member that ends before its autogroup read, so the judgement reads `unknown`, or a witness that ends before it is read again. Those judgements get SIGSTOP and another judgement too: every judgement that gets no kill freezes the group, except `unproven` and an `unknown` whose members without an autogroup are all stopped (`running` false) or whose boot id `/proc` refuses. A stopped member cannot end, so `/proc` refused its autogroup, and a group that job control stopped gets no signal. Without that, a loaded CI runner saw `destroy` record `destroyed` after such a judgement while the chain ran. That freezes only a group id that a judgement of gone would freeze too, never one that reads `unproven`. Each judgement that freezes 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, `/proc` refuses the autogroup of its stopped member, or a scan throws, gets SIGCONT from a `finally` block. The model has no member that a scan shows and then cannot read, so it relies on this freeze. 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))')

.agents/skills/verify-session-lifecycle/coverage.json

@@ -114,7 +114,7 @@
     "src/host/programGroup.ts#readProgramRecord": "b02c48c2bff248a7",
     "src/host/programGroup.ts#readProvenProgramGroup": "79abfacfdeb33135",
     "src/host/programGroup.ts#readProgramGroup": "c783266ad349892e",
-    "src/host/programGroup.ts#judgeProgramGroup": "b8b3053a25f95bbf",
+    "src/host/programGroup.ts#judgeProgramGroup": "dddd91cb209eafa1",
     "src/host/programGroup.ts#readGroupMembers": "8f8103d1d5186e91",
     "src/host/programGroup.ts#judgeLiveGroup": "29c9c4bfd01c4338",
     "src/host/programGroup.ts#processGroupTarget": "88de1544b1553e54",
@@ -125,7 +125,7 @@
     "src/host/programGroup.ts#killProcessGroupBestEffort": "6d5d47cb5697681b",
     "src/host/programGroup.ts#signalProcessGroup": "c5a3a84361b67aa1",
     "src/host/programGroup.ts#isProgramGroupAlive": "f6fe01a280824f82",
-    "src/host/programGroup.ts#stopProgramGroup": "2a512f574e7bd5ae",
+    "src/host/programGroup.ts#stopProgramGroup": "215a685d9337aeb3",
     "src/host/programGroup.ts#procShowsOwnPidSpace": "ac852506311bb328",
     "src/host/rpcClient.ts#toTransportCliError": "dd6531349c62bcbd",
     "src/host/sessionState.ts#SessionState.setDimensions": "08c4f06122d157e9",
@@ -149,7 +149,7 @@
     "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542",
     "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac",
     "skill:model/SessionLifecycle.tla": "cd8639012467f13e",
-    "skill:scripts/facts.mjs": "69cbe689f7e9713d",
+    "skill:scripts/facts.mjs": "ff97d3d2dfab5811",
     "skill:scripts/check.sh": "17f2ce5bd1b1b090"
   },
   "callSites": {

.agents/skills/verify-session-lifecycle/scripts/facts.mjs

@@ -1205,16 +1205,14 @@ function ownershipFacts() {
       return;
     }
     const st = node.statement.statements.map((s) => normalize(s.getText()));
-    const owned = st.findIndex((s) =>
-      /^if \(judgement\.verdict !== 'owned'\) \{ (return|break); \}$/.test(s),
-    );
+    // The only kill follows a judgement of owned and a read of its witness
+    // that owns the group too.
     checkedKill =
       st[0] === 'const judgement = judgeLiveGroup(group);' &&
-      owned > 0 &&
-      st[owned + 1] === 'const witness = readProcessRow(judgement.witness);' &&
-      /^if \( witness !== null && judgeProgramGroup\(group, group\.bootId, \[witness\]\)\.verdict === 'owned' \) \{ killProcessGroupBestEffort\(group\.pid\); killed = true; return; \}$/.test(
-        st[owned + 2] ?? '',
-      );
+      st[1] ===
+        "if ( judgement.verdict === 'unproven' || (judgement.verdict === 'unknown' && !judgement.running) ) { return; }" &&
+      st[2] ===
+        "if (judgement.verdict === 'owned') { const witness = readProcessRow(judgement.witness); if ( witness !== null && judgeProgramGroup(group, group.bootId, [witness]).verdict === 'owned' ) { killProcessGroupBestEffort(group.pid); killed = true; return; } }";
   });
   const judge = normalize(
     requireDeclaration(module, 'judgeProgramGroup').getText(),
@@ -1278,11 +1276,12 @@ function ownershipFacts() {
   };
 }
 
-// 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.
+// In stopProgramGroup's loop, each judgement that gets no kill and is not
+// unproven sends SIGSTOP to the group and judges again: gone, unknown, and
+// owned with a witness that ended before its read. So a member that a scan
+// never shows, or that ends between two reads, stops and stays in 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);
@@ -1301,8 +1300,17 @@ function freezeFacts(body) {
     before.at(-2) === 'let frozen = false;' &&
     before.at(-1) === 'let killed = false;' &&
     guarded.tryBlock.statements.length === 1 &&
+    st.length === 7 &&
     st[1] ===
-      "if (judgement.verdict === 'gone' && procShowsOwnPidSpace()) { frozen = signalProcessGroup(group.pid, 'SIGSTOP') || frozen; if (frozen) { continue; } }" &&
+      "if ( judgement.verdict === 'unproven' || (judgement.verdict === 'unknown' && !judgement.running) ) { return; }" &&
+    st[2].startsWith("if (judgement.verdict === 'owned') {") &&
+    st.slice(3).join('\n') ===
+      [
+        'if (!procShowsOwnPidSpace()) { return; }',
+        "frozen = signalProcessGroup(group.pid, 'SIGSTOP') || frozen;",
+        'if (!frozen) { return; }',
+        'Atomics.wait(settleCell, 0, 0, STOP_SETTLE_MS);',
+      ].join('\n') &&
     normalize(
       requireDeclaration(
         'src/host/programGroup.ts',

docs/USAGE.md

@@ -314,7 +314,7 @@ agent-tty record diff <session-id> <session-id> --at-seq-a 0 --json
 
 `destroy` ends the session's program and every process that the program left in its process group, then records the session as `destroyed`.
 On Linux it also ends those processes when the program has already exited or the session has failed.
-A group whose processes each fork their successor and end too fast for any scan of `/proc` to show one, a fork chain, gets SIGSTOP first. Its stopped processes stay in view, so `destroy` can prove the group and kill it. A frozen group that agent-tty cannot prove is the session's gets SIGCONT.
+A group whose processes each fork their successor and end too fast for any scan of `/proc` to show or read one, a fork chain, gets SIGSTOP first. Its stopped processes stay in view, so `destroy` can prove the group and kill it. A frozen group that agent-tty cannot prove is the session's gets SIGCONT.
 `destroy --force` kills the host and the program's group without asking the host first.
 When a read of the program's group fails with an error that every later read repeats, such as `program.json` that refuses the read (EACCES) or a `/proc` scan that fails (EIO), `gc` keeps the session and reports "failed to check the session's program group (destroy --force removes it)", or "failed to reconcile session (destroy --force removes it)" for a session whose host died. Those errors are EACCES, EPERM, EIO, EISDIR, ENOTDIR, ELOOP and ENAMETOOLONG. A plain `destroy` fails on the same read. When the read of `program.json` or the first check of the group fails that way twice, 100 ms apart, `destroy --force` stops the host alone, without the group, and records the session as `destroyed` once the host has ended, so the next `gc` removes it. A process that the program left can outlive such a `destroy --force`. When the second read passes, `destroy --force` stops the group as usual. A read that fails after that first check, a group that reads alive, or a host that does not end (`HOST_TIMEOUT`) still fails it. Other errors, such as EMFILE, ENOMEM or EAGAIN, can pass, so `gc` gives no such hint and `destroy --force` fails on them too. A `host.json` that cannot be read counts as missing, so the group reads as out of view, as in another pid namespace: `destroy --force` fails with `HOST_TIMEOUT`, and its message names `host.json` and the error. When the read was refused (EACCES or EPERM), make that file readable and run `destroy` again. Until then, `gc` removes such a session once it has ended, but a session whose host died while it ran stays `running`, because its group reads alive.
 `list`, `inspect`, `destroy` and `gc` reconcile a session whose host died: they kill the program's group and record the session as `failed` (or `exited` or `destroyed`).
@@ -367,7 +367,7 @@ 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, 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. `gc` sends the same two signals to a group whose scans show only zombies while its id still names a process (see item 5). 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 -- -<pgid>`, where `<pgid>` is the Child PID that `inspect` shows.
+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, or whose process ends while agent-tty reads it, gets SIGSTOP before each check and SIGCONT when the checks fail. `gc` sends the same two signals to a group whose scans show only zombies while its id still names a process (see item 5). 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 -- -<pgid>`, where `<pgid>` 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` kills nothing. It keeps the folder of a session that is not `destroyed` only while it proves that the program's group runs: the autogroup record in `program.json` proves that a live process of the group is the program's, or the group id still names a process that no scan of `/proc` shows, such as a fast fork chain. When the scans show only zombies of the group while its id still names a process, as for a fork chain under a PID 1 that never reaps, `gc` sends the group SIGSTOP, checks it again, and sends SIGCONT, up to twice in each of up to ten checks of the group, and it keeps the session only when such a check proves the group. A group that has ended gets all 20 frozen checks: with about 2,300 processes in `/proc`, they took about 3.5 s at a load of 90. Another `gc` or a `destroy` that runs at the same time can send SIGCONT before a frozen check. Only when that happens before all 20 of them can a live process of the chain escape every scan, and `gc` then removes the folder of a session whose group still runs. A kept session gets the reason "the session's program group still runs (destroy ends it)". When `gc` cannot check the group, it removes `program.json` with the folder, as it does without an autogroup record (see item 2). That happens in another pid namespace than the one that `host.json` names, for example after a container restart that keeps the agent-tty home, when `host.json` cannot be read, and when `/proc` refuses the boot id or the autogroup of a live process of the group, or hides the processes of other users. Otherwise such a session would stay forever, because no `destroy` can prove its group gone. A process that the program left can then no longer be stopped by agent-tty. 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: