fix(host): stop the marker watch once the host has a new parent, give long TLC runs more workers

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

@@ -55,7 +55,7 @@ Yes, when the diff changes any of these:
 
 You do not have to judge this by hand. The check prints `STALE` when any of these changed since the sync commit.
 
-CI runs the check in the `lifecycle-model` job. Its first share calls `scripts/check.sh --drift-only`, which compares the guard values and the covered code with `coverage.json` and needs no Java, and fails on `STALE`. The whole check runs only when `coverage.json` differs from the base of the pull request or merge group, in four jobs with `CHECK_SHARD=<i>/4`. Each job runs every fourth run that expects pass and every fourth of the rest, because the runs that expect pass explore the whole model and take most of the time.
+CI runs the check in the `lifecycle-model` job. Its first share calls `scripts/check.sh --drift-only`, which compares the guard values and the covered code with `coverage.json` and needs no Java, and fails on `STALE`. The whole check runs only when `coverage.json` differs from the base of the pull request or merge group, in eight jobs with `CHECK_SHARD=<i>/8` and `CHECK_JOBS=12`. Each job runs every eighth run that expects pass and every eighth of the rest, because the runs that expect pass explore the whole model and take most of the time, and it starts all its runs at once. With the model of #324, a share took 11 to 33 min.
 
 ## Run it
 
@@ -65,7 +65,7 @@ From the repo root:
 .agents/skills/verify-session-lifecycle/scripts/check.sh
 ```
 
-It needs `node`, Java 11 or newer (`java -version`), and the network once: the first run downloads `tla2tools.jar` 1.7.4 into this skill's `.cache/` folder (git ignores it) and checks its sha256. On a CI runner with 4 vCPUs and the default `CHECK_JOBS` of 4 it takes about an hour, so CI runs it in four shares. Eleven runs explore more than 20 million distinct states each, so `CHECK_JOBS=90` 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=<folder>` 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. `CHECK_JOBS` runs run at a time (a new one starts as soon as one ends; the bash 3.2 of macOS waits for each batch). The runs that expect pass share the CPUs as TLC workers, at least 1 each, and the others keep 1 worker, so their traces stay the shortest. Eleven runs explore more than 20 million distinct states each, so `CHECK_JOBS=90` 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=<folder>` keeps the results in that folder (default: a new temp folder, printed at the end).
 
 What it does:
 
@@ -407,7 +407,7 @@ Now the catch of the readiness wait first writes an empty marker, `<session>/cre
 
 The order of the marker write and the manifest read closes the race only while that read works. When the host's start-up write and its marker check came before `create` gave up, the host listens without the marker, and `create` reads the manifest to send the SIGTERM. When that read fails, for example on an unreadable file, `create` on Windows takes the manifest as naming no program and sends nothing, and the host serves the failed session.
 
-Now `runHost` starts `watchCreateFailed` right after its start-up check. Every 100 ms it checks whether its creator still runs and then whether the marker exists. On the marker it calls `startShutdown`, as for a SIGTERM. Once a check after the creator's exit found no marker, it stops: `create` writes the marker before it exits, so no marker comes later. A liveness probe that throws, such as EPERM from a process of another user that took the creator's pid, counts as an exited creator, so no error leaves the timer and ends the host. So does a zombie creator, which `kill(pid, 0)` still finds until its parent reaps it: `readProcStat` shows it as `Z` on Linux. In the model, `CreateStopsHostOnWindows` reads the manifest or fails to read it, and `HostPollsMarker` is the watch from `"sockdir"` on. `mutant-HostPollsCreateFailed-win32` breaks R17, and `mutant-HostPollsCreateFailed` passes, because off Windows the SIGTERM does not need the read. The integration test `a create on Windows whose manifest read fails after it gave up` holds the host's socket-directory `mkdir` until `create` has exited and makes `create`'s manifest reads fail once the marker exists.
+Now `runHost` starts `watchCreateFailed` right after its start-up check. Every 100 ms it checks whether its creator still runs and then whether the marker exists. On the marker it calls `startShutdown`, as for a SIGTERM. Once a check after the creator's exit found no marker, it stops: `create` writes the marker before it exits, so no marker comes later. The host is the creator's child, and Linux and macOS give it a new parent when the creator exits, also while the creator is a zombie and before another process can take its pid. So there a `process.ppid` other than the creator's pid means that the creator has exited. Windows keeps the parent pid, so there only `isProcessAlive` tells, and a probe that throws, such as EPERM from a process of another user that took the creator's pid, counts as an exited creator, so no error leaves the timer and ends the host. The watch stops after `CREATE_FAILED_WATCH_MAX_MS` (60 s) in any case. In the model, `CreateStopsHostOnWindows` reads the manifest or fails to read it, and `HostPollsMarker` is the watch from `"sockdir"` on. `mutant-HostPollsCreateFailed-win32` breaks R17, and `mutant-HostPollsCreateFailed` passes, because off Windows the SIGTERM does not need the read. The integration test `a create on Windows whose manifest read fails after it gave up` holds the host's socket-directory `mkdir` until `create` has exited and makes `create`'s manifest reads fail once the marker exists.
 
 ### `CreateRetriesMarker`: on Windows, a failed marker write leaves a host serving a failed create (R17)
 
@@ -589,6 +589,7 @@ It assumes:
 - A destroy that lands between reconcile's last read and its write is still overwritten with failed, for the time until that reconcile finds the destroy marker and writes destroyed again (`ReconcileRepairsDestroyed`). A `list` or `gc` that reads in that time sees `failed`, a terminal status, so gc can remove the folder as it would remove a destroyed one. A reconcile whose process dies in that time leaves `failed` until the next reconcile reads it: that read finds the marker and writes destroyed (`ReconcileRepairsMarked`). `home list` and the dashboard count a session with the marker as destroyed, also in that time. The model kills the `list` process in that time (`ListDiesBeforeRepair`), so it checks that the repair at the read heals the death. A `gc` that dies there leaves the same record, and the model leaves it out.
 - The idle time-out calls the same `hangUpProgram` as `initiateShutdown`: SIGHUP, then the group kill after `SHUTDOWN_KILL_GRACE_MS`. When the program exits on that SIGHUP, `handlePtyExit` kills the group too, so a process that ignores SIGHUP does not outlive the idle time-out. An idle time-out still ends exited. When the check cannot run (`unknown`), the idle kill sends nothing, and the session ends exited with that process running, as after a program that exits on its own and leaves a process (coder/agent-tty#222). The model leaves both group kills out: they go through `stopProgramGroup` like every kill, and a process that outlives them is one that the program left, which the model keeps after a normal exit anyway.
 - Windows has no process groups, so there `processGroupTarget` gives the program's pid, and every kill reaches only that process. `destroy` never re-runs on Windows. There SIGTERM ends the host at once, so a `create` that gives up sends it only once the manifest names the program, and the next reconcile records `failed` and ends the program. Before that write, the host finds the create-failed marker (`HostChecksCreateFailed`), and after it the host's watch finds it when `create`'s manifest read fails (`HostPollsCreateFailed`). `current-win32` checks this with a SIGTERM that is a host crash and without a token, and keeps the process groups of Linux. When the marker write fails on Windows, `create` writes it again every 100 ms, up to 50 times, while the manifest names no program and the host runs (`CreateRetriesMarker`). When every write fails, for example on a full disk, a host that the manifest does not name yet serves the session. The model ends such a `create` as `"exhausted"`, which R17 does not cover.
+- The host's marker watch stops 60 s after it started. A `create` ends well before, since its readiness wait and its marker retries take about 20 s at most. A `create` that writes its marker later than that, for example after a SIGSTOP, leaves a host that passed its start-up check serving. The model has no clock and does not show this.
 - A host stopped with SIGSTOP, or with a blocked event loop, takes the SIGTERM of a `create` that gave up only when it runs again. Until then its program runs and the session reads `running`, which R17 allows because the SIGTERM is still on its way. A plain `destroy` fails because the host does not answer, and only `destroy --force` ends such a session sooner.
 - A destroy that the program runs, or that someone types into the program's interactive shell, runs inside the program's session, and `rerunInNewSession` runs it again in a new session. The model lets such a destroy start while the program's leader runs, and assumes that it kept `AGENT_TTY_SESSION_ID`, which every process of the program inherits at spawn. A destroy whose environment lost the variable, or whose `create --env` overrode it, is seen through the id comparison only. On Linux that compares the CLI's session id with `childPid`, so it misses such a destroy only before the host's start-up write. Other POSIX systems compare the process group and the controlling terminal, through `/bin/ps`. A terminal is the controlling terminal of one session and of every process in it, so that also finds a job of an interactive shell, which runs in a group of its own. A process without a controlling terminal is seen only through the group.
 - The program's processes stay in its process group. A process that leaves the group (`setsid`, or the job control of an interactive shell) is out of reach of the group kill, and it is no witness for the token either. That is case 4 of coder/agent-tty#203, a documented limit with no code change.

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

@@ -143,13 +143,13 @@
     "src/storage/manifests.ts#writeCreateFailedMarker": "587c8047e563db4e",
     "src/storage/manifests.ts#writeEmptyMarker": "143325689100f36c",
     "src/protocol/sessionStatusPolicy.ts#SESSION_STATUS_POLICIES": "83827f9f7f6b8e1d",
-    "src/host/hostMain.ts#runHost(parts)": "7bd4c6553a831b9d",
+    "src/host/hostMain.ts#runHost(parts)": "2a0651c9dd9ea23f",
     "src/host/hostMain.ts#runHost(final try)": "e0615a9709fefb67",
     "src/host/hostMain.ts#runHost>handlers.resize": "d601680963309542",
     "src/host/hostMain.ts#runHost>handlers.destroy": "ccff44951e711dac",
     "skill:model/SessionLifecycle.tla": "cd8639012467f13e",
-    "skill:scripts/facts.mjs": "2de6761bed77fb19",
-    "skill:scripts/check.sh": "fe2da7911682462a"
+    "skill:scripts/facts.mjs": "3ef7fa152ec0af36",
+    "skill:scripts/check.sh": "cad764a01b6eee50"
   },
   "callSites": {
     "writeManifest": [

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

@@ -360,12 +360,32 @@ if [ "$SHARD_COUNT" -gt 1 ]; then
   echo "Share $SHARD of the runs:$RUNS"
 fi
 
+# A run that expects pass explores the whole model and takes the longest, so
+# the runs that expect pass and run at the same time share the CPUs, each
+# with at least 1 TLC worker. A run that expects a violation keeps 1 worker,
+# which finds the shortest trace.
+CPUS=$(getconf _NPROCESSORS_ONLN 2>/dev/null || echo 1)
+passes=0
+for name in $RUNS; do
+  if [ "$(cut -f1 "$OUT/$name/expect.txt")" = pass ]; then
+    passes=$((passes + 1))
+  fi
+done
+concurrent=$((passes < JOBS ? passes : JOBS))
+PASS_WORKERS=1
+if [ "$concurrent" -gt 0 ] && [ "$CPUS" -gt "$concurrent" ]; then
+  PASS_WORKERS=$((CPUS / concurrent))
+fi
+
 run_tlc() {
-  local dir rc=0
+  local dir rc=0 workers=1
   dir=$(cd "$OUT/$1" && pwd)
   mkdir -p "$dir/tmp"
+  if [ "$(cut -f1 "$dir/expect.txt")" = pass ]; then
+    workers=$PASS_WORKERS
+  fi
   (cd "$dir" && "$JAVA" -XX:+UseParallelGC -Xmx2g -Djava.io.tmpdir="$dir/tmp" \
-    -cp "$JAR" tlc2.TLC -workers 1 -config SessionLifecycle.cfg \
+    -cp "$JAR" tlc2.TLC -workers "$workers" -config SessionLifecycle.cfg \
     -metadir "$dir/states" SessionLifecycle.tla >tlc.out 2>&1) || rc=$?
   echo "$rc" >"$dir/rc"
 }

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

@@ -416,17 +416,24 @@ function retriesMarker(body) {
 
 // runHost's watchCreateFailed checks, every CREATE_FAILED_POLL_INTERVAL_MS,
 // whether the creator still runs and then whether the create-failed marker
-// exists. A probe that throws, and a zombie creator, count as an exited
-// creator, so no error leaves the timer. On the marker it calls startShutdown, and it stops once a check
+// exists. On Linux and macOS a new parent of the host means that the
+// creator exited. A probe that throws counts as an exited creator, so no
+// error leaves the timer, and the watch stops after
+// CREATE_FAILED_WATCH_MAX_MS. On the marker it calls startShutdown, and it stops once a check
 // after the creator's exit found none. The start-up try calls it right after
 // the check that follows the start-up write.
 function pollsCreateFailed() {
   const run = requireDeclaration('src/host/hostMain.ts', 'runHost').body;
+  const strip = (node) => normalize(node.getText().replace(/\/\/[^\n]*/g, ''));
+  const probe = indexOfStatement(run, /^const creatorRuns = /);
   const watch = indexOfStatement(run, /^const watchCreateFailed = /);
   const watches =
-    watch >= 0 &&
-    normalize(run.statements[watch].getText().replace(/\/\/[^\n]*/g, '')) ===
-      "const watchCreateFailed = (): void => { const timer = setInterval(() => { let creatorGone = true; try { creatorGone = !isProcessAlive(creatorPid) || readProcStat(creatorPid)?.state === 'Z'; } catch { } if (existsSync(createFailedMarkerPath(sessDir))) { clearInterval(timer); startShutdown(); } else if (creatorGone) { clearInterval(timer); } }, CREATE_FAILED_POLL_INTERVAL_MS); timer.unref(); };";
+    probe >= 0 &&
+    probe < watch &&
+    strip(run.statements[probe]) ===
+      "const creatorRuns = (): boolean => { if (process.platform !== 'win32' && process.ppid !== creatorPid) { return false; } try { return isProcessAlive(creatorPid); } catch { return false; } };" &&
+    strip(run.statements[watch]) ===
+      'const watchCreateFailed = (): void => { const deadline = Date.now() + CREATE_FAILED_WATCH_MAX_MS; const timer = setInterval(() => { const creatorGone = !creatorRuns() || Date.now() >= deadline; if (existsSync(createFailedMarkerPath(sessDir))) { clearInterval(timer); startShutdown(); } else if (creatorGone) { clearInterval(timer); } }, CREATE_FAILED_POLL_INTERVAL_MS); timer.unref(); };';
   const last = run.statements.at(-1);
   const tried =
     last !== undefined && ts.isTryStatement(last)

.github/workflows/ci.yml

@@ -221,17 +221,14 @@ jobs:
 
   # Model-checks the session lifecycle with the verify-session-lifecycle
   # skill. Share 1 checks that coverage.json matches the facts and the
-  # covered code. The TLC runs took 63 min in one job of 4 vCPUs and took 13
-  # to 17 min in each of 4 shares. The model of #324 has about twice the
-  # states, and its 4 shares took 38 to 48 min. check.sh starts CHECK_JOBS
-  # runs at a time and waits for all of them before the next ones, so a share
-  # took as long as the sum of its longest runs. Now each of 8 shares starts
-  # all its runs at once (with the model of #324, 10 to 12 runs, of which at
-  # most 2 are long, on 4 vCPUs) and takes about as long as its longest run:
-  # 15 to 43 min, where the 43 min share holds only the longest run, which
-  # TLC checks with 1 worker. They run only when coverage.json differs from
-  # the base, which every change to the model, its scripts, the covered code
-  # or a fact needs.
+  # covered code. Each of the 8 shares starts all its runs at once
+  # (CHECK_JOBS 12: with the model of #327, 10 to 12 runs, of which at most
+  # 2 explore the whole model), and check.sh gives those runs the 4 vCPUs as
+  # TLC workers. So a share takes about as long as its longest run. With the
+  # model of #324, the shares took 11 to 33 min, and 15 to 43 min with 1 TLC
+  # worker per run. TLC runs only when coverage.json differs from the base,
+  # which every change to the model, its scripts, the covered code or a fact
+  # needs.
   lifecycle-model:
     runs-on: ubuntu-latest
     timeout-minutes: 55

src/host/README.md

@@ -80,7 +80,7 @@
 - `runHost` spawns the PTY with `createPty` (`src/pty/createPty.ts`), writes input to it, resizes it and kills it on idle timeout and shutdown. It writes `TerminalQueryResponder` replies to the PTY without logging them. [hostMain.ts:runHost]
 - `runHost` polls `session.json` with `readManifestIfExists` and probes the creator process with `isProcessAlive` until the manifest appears or the creator exits. It writes `session.json` through `createSerialManifestWriter`, creates the socket directory with mode `0o700` and listens with `RpcServer` through `listenInSocketDirectory` and writes snapshot and screenshot artifacts through `src/snapshot/capture.ts` and `src/screenshot/capture.ts`. [hostMain.ts:runHost]
 - `runHost` registers a `process.on('SIGTERM')` handler that starts shutdown, sends signals to the child with `process.kill` and starts `setInterval` timers for idle and wait polling. [hostMain.ts:runHost]
-- `runHost` checks for the `create-failed` marker with `existsSync` before it spawns the program, and returns when it finds it. It checks again right after its start-up manifest write, before it listens, and then shuts down. From there on, `watchCreateFailed` checks for the marker every `CREATE_FAILED_POLL_INTERVAL_MS` (100 ms) while the creator process lives and once after it exited (a liveness probe that throws, such as EPERM from a process of another user that took the pid, and a zombie creator that `readProcStat` shows as `Z` count as exited), and starts the shutdown when it finds the marker. [hostMain.ts:runHost]
+- `runHost` checks for the `create-failed` marker with `existsSync` before it spawns the program, and returns when it finds it. It checks again right after its start-up manifest write, before it listens, and then shuts down. From there on, `watchCreateFailed` checks for the marker every `CREATE_FAILED_POLL_INTERVAL_MS` (100 ms) while the creator process lives and once after it exited (off Windows, a `process.ppid` other than the creator's pid means that the creator exited; on Windows, a liveness probe that throws counts as exited; the watch stops after `CREATE_FAILED_WATCH_MAX_MS`, 60 s, in any case), and starts the shutdown when it finds the marker. [hostMain.ts:runHost]
 - `runHost` rethrows a PTY-ingestion, event-log append, exit-handling or shutdown error in `process.nextTick`. The uncaught exception crashes the host process. [hostMain.ts:rethrowAsync]
 - `resolveHostRendererName` reads `process.env.AGENT_TTY_HOST_RENDERER` and `process.env.AGENT_TTY_RENDERER`. [hostMain.ts:resolveHostRendererName]
 - `EventLog.open` opens the file in append mode and runs `chmod 0o600`. `append` writes with `fileHandle.appendFile`, one call at a time. `close` calls `fileHandle.sync()` and then closes the file. [eventLog.ts:EventLog]