fix(gc): freeze a fork chain behind its zombies before gc reads it ended

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

@@ -7,6 +7,7 @@
     "GcFinalCheck": true,
     "GcKeepsLiveGroup": true,
     "GcProbesUnseenGroup": true,
+    "GcFreezesUnseenGroup": true,
     "CreateRecordsHostPid": true,
     "CreateRecordsHost": true,
     "CreateStopsOnGiveUp": true,
@@ -46,7 +47,8 @@
     "src/cli/commands/gc.ts#gcSessions": "a2ac8bd10f100332",
     "src/cli/commands/gc.ts#defaultDependencies": "81a9894438cb5be7",
     "src/host/programGroup.ts#provenProgramGroupRuns": "7b50817618b4b769",
-    "src/host/programGroup.ts#judgeGroupForGc": "e0cd1b46a60eb1fe",
+    "src/host/programGroup.ts#judgeGroupForGc": "fb133ba2739116d1",
+    "src/host/programGroup.ts#judgeFrozenGroup": "d18458e7d70a5664",
     "src/host/programGroup.ts#GC_JUDGEMENTS": "180a0af01a4b81c7",
     "src/host/programGroup.ts#probeFindsGroup": "31ea7b5e835c0509",
     "src/host/lifecycle.ts#allocateSession": "43819af8c6c271ec",
@@ -137,9 +139,9 @@
     "src/host/hostMain.ts#runHost(final try)": "251f1e68a4ec17cc",
     "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542",
     "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac",
-    "skill:model/SessionLifecycle.tla": "19775a9a74c5ca9a",
-    "skill:scripts/facts.mjs": "4aff1bce5c8ba086",
-    "skill:scripts/check.sh": "0e69ddb1068b5df4"
+    "skill:model/SessionLifecycle.tla": "77ec28d60359f635",
+    "skill:scripts/facts.mjs": "eded6c52629e3523",
+    "skill:scripts/check.sh": "e33db0960de216fe"
   },
   "callSites": {
     "writeManifest": [

.agents/skills/verify-session-lifecycle/model/SessionLifecycle.tla

@@ -50,6 +50,9 @@ CONSTANTS
     GcProbesUnseenGroup,    \* programGroup.ts: provenProgramGroupRuns also
                             \*   counts a group id that the probe finds
                             \*   while no scan shows a member
+    GcFreezesUnseenGroup,   \* programGroup.ts: gc sends SIGSTOP to a group
+                            \*   whose scans show only zombies while the
+                            \*   probe finds its id, and judges it again
     ReconcileSkipsTerminal, \* lifecycle.ts: return when the manifest is terminal
     ReconcileSkipsLiveHost, \* lifecycle.ts: return when hostPid is set and alive
     CreateRecordsHostPid,   \* lifecycle.ts: launch the host, then write the
@@ -134,6 +137,9 @@ CONSTANTS
     Unseen,                 \* the environment: no scan of /proc shows a
                             \*   live process of the program, as for a fork
                             \*   chain whose processes each live about 2 ms
+    ZombiesInView,          \* the environment: with Unseen, the scans show
+                            \*   zombies of the program's group, as under a
+                            \*   PID 1 that never reaps
     OtherPidSpace,          \* the environment: destroy, list and gc run
                             \*   where no scan and no probe shows the host's
                             \*   processes (no /proc, an empty /proc,
@@ -147,10 +153,11 @@ CONSTANTS
 ASSUME MaxListReconciles \in 1..3
 ASSUME Token \in BOOLEAN
 ASSUME Unseen \in BOOLEAN
+ASSUME ZombiesInView \in BOOLEAN
 ASSUME OtherPidSpace \in BOOLEAN
 ASSUME Win32 \in BOOLEAN
 ASSUME \A b \in {GcSkipsNonCollectable, GcFinalCheck, GcKeepsLiveGroup,
-                 GcProbesUnseenGroup,
+                 GcProbesUnseenGroup, GcFreezesUnseenGroup,
                  ReconcileSkipsTerminal,
                  ReconcileSkipsLiveHost, CreateRecordsHostPid,
                  HostWaitsForManifest, ReconcileRereads,
@@ -1088,20 +1095,25 @@ GcReadsReconciled ==
 
 \* provenProgramGroupRuns reads program.json and judges the group, as the
 \* waits of destroy do, but it counts only a group that it proves: a live
-\* member carries the token. gc sends no SIGSTOP, so with Unseen no scan
-\* shows the program's processes, and with GcProbesUnseenGroup the probe
-\* kill(-pgid, 0) then finds them. An unrelated group that took the id is
-\* in view and reads unproven. With OtherPidSpace gc cannot check the group
-\* and reads it not proven, so that a session whose pid space is gone, as
-\* after a container restart, does not stay forever. With GcKeepsLiveGroup
-\* gc skips a session that is not destroyed while it proves the group
-\* ("the session's program group still runs"). The code tests the status
-\* of manifestAfter, which cannot turn from destroyed back, so this current
-\* status skips no more often.
+\* member carries the token. With Unseen no scan shows the program's
+\* processes, and with GcProbesUnseenGroup the probe kill(-pgid, 0) then
+\* finds them while no scan shows a member, not even a zombie. With
+\* ZombiesInView the scans show zombies of the group, which the probe also
+\* finds, so gc needs GcFreezesUnseenGroup: it sends SIGSTOP, a stopped
+\* member stays in view, and the judgement after it finds the program's
+\* processes. An unrelated group that took the id is in view and reads
+\* unproven. With OtherPidSpace gc cannot check the group and reads it not
+\* proven, so that a session whose pid space is gone, as after a container
+\* restart, does not stay forever. With GcKeepsLiveGroup gc skips a session
+\* that is not destroyed while it proves the group ("the session's program
+\* group still runs"). The code tests the status of manifestAfter, which
+\* cannot turn from destroyed back, so this current status skips no more
+\* often.
 GcSeesGroup ==
     /\ ~OtherPidSpace
     /\ \/ GroupSeen("proven")
-       \/ GcProbesUnseenGroup /\ Unseen /\ (prog \/ left)
+       \/ /\ GcProbesUnseenGroup /\ Unseen /\ (prog \/ left)
+          /\ (~ZombiesInView \/ GcFreezesUnseenGroup)
 
 GcChecksGroup ==
     /\ pc["gc"] = "group"

.agents/skills/verify-session-lifecycle/scripts/check.sh

@@ -166,7 +166,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 GcKeepsLiveGroup GcProbesUnseenGroup 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 HostChecksCreateFailed"
+GUARDS="GcSkipsNonCollectable GcFinalCheck GcKeepsLiveGroup GcProbesUnseenGroup GcFreezesUnseenGroup 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 HostChecksCreateFailed"
 # 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;
@@ -192,6 +192,9 @@ RUNS=""
 TOKEN=TRUE
 # UNSEEN: whether no scan of /proc shows a live process of the program.
 UNSEEN=FALSE
+# ZOMBIES: whether, with UNSEEN, the scans show zombies of the program's
+# group, as under a PID 1 that never reaps.
+ZOMBIES=FALSE
 # OTHER: whether destroy, list and gc run in another pid space than the host.
 OTHER=FALSE
 # WIN32: whether SIGTERM ends the host at once, as on Windows.
@@ -216,6 +219,7 @@ write_run() {
     done
     echo "  Token = $TOKEN"
     echo "  Unseen = $UNSEEN"
+    echo "  ZombiesInView = $ZOMBIES"
     echo "  OtherPidSpace = $OTHER"
     echo "  Win32 = $WIN32"
     echo "  MaxListReconciles = 2"
@@ -273,6 +277,11 @@ UNSEEN=TRUE
 write_run current-unseen pass "$RULES" "" "the code with a program that no scan shows: every rule holds"
 write_run mutant-FreezesUnseenGroup-unseen violated DestroyedProgramStopped "FreezesUnseenGroup=FALSE" "without the freeze, the kill finds no member in view, and destroy records destroyed while a fork chain runs" DestroyedProgramStopped
 write_run mutant-GcProbesUnseenGroup-unseen violated RemovedSessionStopped "GcProbesUnseenGroup=FALSE" "without the probe, gc removes program.json while a fork chain that the program left runs" RemovedSessionStopped
+# Under a PID 1 that never reaps, the chain also leaves zombies in view.
+# With every guard, that changes nothing, so current-unseen covers it.
+ZOMBIES=TRUE
+write_run mutant-GcFreezesUnseenGroup-unseen-zombies violated RemovedSessionStopped "GcFreezesUnseenGroup=FALSE" "without the freeze, gc reads a fork chain behind its zombies ended and removes program.json while it runs" RemovedSessionStopped
+ZOMBIES=FALSE
 UNSEEN=FALSE
 
 # destroy, list and gc run without /proc, or in another pid namespace or on

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

@@ -1009,8 +1009,9 @@ function programRecordFacts() {
 // with a token it kills only right after it read a live member of the group
 // again and found the program's session id, autogroup and boot id on it.
 // No other code calls the raw group kill or builds a group target, except
-// the two probes, which send signal 0, and only stopProgramGroup sends the
-// SIGSTOP and SIGCONT of signalProcessGroup.
+// the two probes, which send signal 0. Only stopProgramGroup and gc's
+// judgeFrozenGroup send the SIGSTOP and SIGCONT of signalProcessGroup, which
+// kill nothing.
 function ownershipFacts() {
   const module = 'src/host/programGroup.ts';
   const stop = requireDeclaration(module, 'stopProgramGroup');
@@ -1052,13 +1053,16 @@ function ownershipFacts() {
   let stray = false;
   for (const file of listSources('src')) {
     walk(source(file), (node) => {
-      if (
-        isCall(node, 'killProcessGroupBestEffort') ||
-        isCall(node, 'signalProcessGroup')
-      ) {
+      if (isCall(node, 'killProcessGroupBestEffort')) {
         rawKills += 1;
         stray ||= file !== module || ownerPath(node) !== 'stopProgramGroup';
       }
+      if (isCall(node, 'signalProcessGroup')) {
+        rawKills += 1;
+        stray ||=
+          file !== module ||
+          !['stopProgramGroup', 'judgeFrozenGroup'].includes(ownerPath(node));
+      }
       if (isCall(node, 'processGroupTarget')) {
         targets += 1;
         const owner = ownerPath(node);
@@ -1426,16 +1430,21 @@ function gcFacts() {
       "if (verdict !== 'gone') { return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; }";
   // Then a group that reads gone, whose id the probe finds while no scan
   // shows a member, live or zombie, counts as running too. Without the
-  // probe, gone reads false.
-  const probeTail = [
+  // probe, gone reads false. When the scans show only zombies, the group is
+  // judged again frozen, or, without the freeze, reads ended.
+  const probeHead = [
     'if (!probeFindsGroup(group.pid)) { return false; }',
     'const live = groupHasLiveProcess(group.pid);',
-    'return live === null ? true : live ? null : false;',
   ];
   const tail = judge.slice(2);
+  const last = tail.at(-1);
   const probes =
     judges &&
-    tail.join('\n') === probeTail.join('\n') &&
+    tail.length === 3 &&
+    tail.slice(0, 2).join('\n') === probeHead.join('\n') &&
+    (last === 'return live === null ? true : live ? null : false;' ||
+      last ===
+        'return live === null ? true : live ? null : judgeFrozenGroup(group);') &&
     normalize(
       requireDeclaration(
         'src/host/programGroup.ts',
@@ -1445,6 +1454,19 @@ function gcFacts() {
       "{ try { process.kill(processGroupTarget(pgid), 0); return true; } catch (error) { if (hasErrorCode(error, 'ESRCH')) { return false; } if (hasErrorCode(error, 'EPERM')) { return true; } throw error; } }";
   const judgesGone =
     probes || (tail.length === 1 && tail[0] === 'return false;');
+  // judgeFrozenGroup sends SIGSTOP only where /proc shows this process's pid
+  // space, judges the stopped group, and sends SIGCONT in a finally. A
+  // frozen group that still reads gone is inconclusive, so gc freezes it
+  // again: another gc or a destroy can have resumed it.
+  const freezes =
+    probes &&
+    last ===
+      'return live === null ? true : live ? null : judgeFrozenGroup(group);' &&
+    body('judgeFrozenGroup').join('\n') ===
+      [
+        "if (!procShowsOwnPidSpace() || !signalProcessGroup(group.pid, 'SIGSTOP')) { return false; }",
+        "try { const { verdict } = judgeLiveGroup(group); return verdict === 'owned' ? true : verdict === 'unproven' ? false : null; } finally { signalProcessGroup(group.pid, 'SIGCONT'); }",
+      ].join('\n');
   return {
     GcSkipsNonCollectable: reconcile >= 0 && collectable > reconcile,
     GcFinalCheck: finalCheck,
@@ -1456,6 +1478,7 @@ function gcFacts() {
       judges &&
       judgesGone,
     GcProbesUnseenGroup: probes,
+    GcFreezesUnseenGroup: freezes,
   };
 }
 
@@ -1499,6 +1522,7 @@ const COVERED = [
   ['src/cli/commands/gc.ts', 'defaultDependencies'],
   ['src/host/programGroup.ts', 'provenProgramGroupRuns'],
   ['src/host/programGroup.ts', 'judgeGroupForGc'],
+  ['src/host/programGroup.ts', 'judgeFrozenGroup'],
   ['src/host/programGroup.ts', 'GC_JUDGEMENTS'],
   ['src/host/programGroup.ts', 'probeFindsGroup'],
   ['src/host/lifecycle.ts', 'allocateSession'],

docs/USAGE.md

@@ -366,9 +366,9 @@ 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. 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 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. It then reports "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, 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.
+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. It then reports "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, 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:
    - At the idle time-out, a host that cannot run the check kills nothing, but it still records the session as `exited` once the program has exited, while a process that the program left can still run. A later `destroy` then fails with `HOST_TIMEOUT`, and `gc` can remove the session folder.
    - When `/proc` hides the processes of other users (mounted with `hidepid=2`, `hidepid=4`, `hidepid=invisible` or `hidepid=ptraceable`), a group whose processes agent-tty cannot see counts as running. A `destroy` that cannot prove such a group gone fails with `HOST_TIMEOUT` and does not record the session as `destroyed`.