From 4314dee53ede737c15aa52b53c42e0566f18fe7c Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 15:10:26 +0000 Subject: [PATCH 1/8] test: stop the marker watch once the host has a new parent, and after 60 s A process of the same user that takes the creator's pid keeps the probe answering, so the watch ticked for as long as that process lived. On Linux and macOS the host is the creator's child and gets a new parent when the creator exits, and the watch should stop then. It should also stop 60 s after it started, as on Windows, where the parent pid stays. Both new cases fail on the head. The tests now set the host's parent pid, because runHost runs in the test process. The zombie case gives way to the new-parent case: a zombie creator also gives the host a new parent. --- test/unit/host/hostMarker.test.ts | 104 +++++++++++++++++++----------- 1 file changed, 65 insertions(+), 39 deletions(-) diff --git a/test/unit/host/hostMarker.test.ts b/test/unit/host/hostMarker.test.ts index 228bccbb..fb46ca14 100644 --- a/test/unit/host/hostMarker.test.ts +++ b/test/unit/host/hostMarker.test.ts @@ -18,7 +18,6 @@ import { } from 'vitest'; import { runHost } from '../../../src/host/hostMain.js'; -import { readProcStat } from '../../../src/host/programGroup.js'; import type * as ProgramGroupModule from '../../../src/host/programGroup.js'; import type { SessionRecord } from '../../../src/protocol/schemas.js'; import { @@ -57,6 +56,10 @@ const SESSION_ID = 'session-01'; let home = ''; let directory = ''; let sigtermListeners: ReadonlySet = new Set(); +// runHost runs in this process, so a test sets the host's parent pid: Linux +// and macOS give a process a new parent when its parent exits. +const ppidDescriptor = Object.getOwnPropertyDescriptor(process, 'ppid'); +let hostParent = 0; function readProgramGroup(): number { const { pid } = JSON.parse( @@ -139,6 +142,12 @@ beforeEach(async () => { }; await writeManifest(manifestPath(directory), record); sigtermListeners = new Set(process.rawListeners('SIGTERM')); + hostParent = process.pid; + Object.defineProperty(process, 'ppid', { + configurable: true, + enumerable: true, + get: () => hostParent, + }); }); afterEach(async () => { @@ -154,6 +163,9 @@ afterEach(async () => { killGroupIfAlive(readProgramGroup()); } vi.unstubAllEnvs(); + if (ppidDescriptor !== undefined) { + Object.defineProperty(process, 'ppid', ppidDescriptor); + } await rm(home, { recursive: true, force: true }); }); @@ -198,11 +210,13 @@ describe('runHost and the create-failed marker', () => { it('keeps serving when the marker appears after its creator has exited', async () => { const creator = spawn('sleep', ['30'], { stdio: 'ignore' }); expect(creator.pid).toBeGreaterThan(0); + hostParent = creator.pid as number; const watchStopped = trackMarkerWatch(); await runHost(SESSION_ID, creator.pid as number); expect(existsSync(socketPath(directory))).toBe(true); creator.kill('SIGKILL'); await once(creator, 'exit'); + hostParent = 1; await watchStopped(); await writeCreateFailedMarker( @@ -225,6 +239,8 @@ describe('runHost and the create-failed marker', () => { }); const creatorPid = creator.pid as number; expect(creatorPid).toBeGreaterThan(0); + // The host keeps its parent pid, as on Windows, so only the probe tells. + hostParent = creatorPid; const watchStopped = trackMarkerWatch(); await runHost(SESSION_ID, creatorPid); expect(existsSync(socketPath(directory))).toBe(true); @@ -259,6 +275,7 @@ describe('runHost and the create-failed marker', () => { }); const creatorPid = creator.pid as number; expect(creatorPid).toBeGreaterThan(0); + hostParent = creatorPid; await runHost(SESSION_ID, creatorPid); expect(existsSync(socketPath(directory))).toBe(true); // The next probe finds the creator gone, and it wrote the marker first. @@ -274,43 +291,52 @@ describe('runHost and the create-failed marker', () => { await expectHostStopped(readProgramGroup()); }, 15_000); - // kill(pid, 0) succeeds for a zombie, so only /proc shows that the creator - // has exited while its parent has yet to reap it. - it.runIf(process.platform === 'linux')( - 'stops the watch when its creator is a zombie', - async () => { - const parent = spawn( - '/bin/sh', - ['-c', 'sleep 0 & echo $!; exec sleep 30'], - { stdio: ['ignore', 'pipe', 'ignore'] }, - ); - onTestFinished(() => { - parent.kill('SIGKILL'); - }); - const [line] = (await once(parent.stdout, 'data')) as [Buffer]; - const zombie = Number(line.toString('utf8').trim()); - expect(zombie).toBeGreaterThan(1); - const deadline = Date.now() + 10_000; - while (readProcStat(zombie)?.state !== 'Z') { - expect(Date.now()).toBeLessThan(deadline); - await delay(20); - } - const watchStopped = trackMarkerWatch(); - await runHost(SESSION_ID, zombie); - expect(existsSync(socketPath(directory))).toBe(true); - await watchStopped(); - - await writeCreateFailedMarker( - createFailedMarkerPath(directory), - SESSION_ID, - ); + // The creator exited, and a process of the same user, or a zombie that its + // parent has yet to reap, holds its pid, so the probe still finds it. + it('stops the watch once the host has a new parent, whatever holds the creator pid', async () => { + const holder = spawn('sleep', ['30'], { stdio: 'ignore' }); + onTestFinished(() => { + holder.kill('SIGKILL'); + }); + const creatorPid = holder.pid as number; + expect(creatorPid).toBeGreaterThan(0); + hostParent = creatorPid; + const watchStopped = trackMarkerWatch(); + await runHost(SESSION_ID, creatorPid); + expect(existsSync(socketPath(directory))).toBe(true); + hostParent = 1; + await watchStopped(); - expect((await readManifest(manifestPath(directory))).status).toBe( - 'running', - ); - sendSigterm(); - await expectHostStopped(readProgramGroup()); - }, - 20_000, - ); + await writeCreateFailedMarker( + createFailedMarkerPath(directory), + SESSION_ID, + ); + + expect((await readManifest(manifestPath(directory))).status).toBe( + 'running', + ); + sendSigterm(); + await expectHostStopped(readProgramGroup()); + }, 15_000); + + it('stops the watch 60 s after it started, also while its creator runs', async () => { + const watchStopped = trackMarkerWatch(); + await runHost(SESSION_ID, process.pid); + expect(existsSync(socketPath(directory))).toBe(true); + const now = Date.now.bind(Date); + vi.spyOn(Date, 'now').mockImplementation(() => now() + 60_000); + await watchStopped(); + + await writeCreateFailedMarker( + createFailedMarkerPath(directory), + SESSION_ID, + ); + + expect((await readManifest(manifestPath(directory))).status).toBe( + 'running', + ); + vi.restoreAllMocks(); + sendSigterm(); + await expectHostStopped(readProgramGroup()); + }, 15_000); }); From 89ff0401c903377262171a11582b86312907a0cd Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 15:12:51 +0000 Subject: [PATCH 2/8] fix(host): stop the marker watch once the host has a new parent, and after 60 s A process of the same user that took the creator's pid kept the watch's probe answering, so the watch ticked at 10 Hz for that process's life. 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 its pid can be reused. So off Windows, a process.ppid other than the creator's pid ends the watch, and the /proc zombie read goes. On Windows the probe still decides. The watch also stops after 60 s in any case. facts.mjs reads the new watch, and SKILL.md states the bound as a residual. --- .../skills/verify-session-lifecycle/SKILL.md | 3 +- .../scripts/facts.mjs | 17 +++++++--- src/host/README.md | 2 +- src/host/hostMain.ts | 33 ++++++++++++------- 4 files changed, 36 insertions(+), 19 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index fc3d465d..50f01362 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.agents/skills/verify-session-lifecycle/SKILL.md @@ -402,7 +402,7 @@ Now the catch of the readiness wait first writes an empty marker, `/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) @@ -578,6 +578,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. diff --git a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs b/.agents/skills/verify-session-lifecycle/scripts/facts.mjs index 525f9858..cd568211 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/facts.mjs +++ b/.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) diff --git a/src/host/README.md b/src/host/README.md index e52580d3..7c7b7688 100644 --- a/src/host/README.md +++ b/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] diff --git a/src/host/hostMain.ts b/src/host/hostMain.ts index f2ec81e9..f01f07c9 100644 --- a/src/host/hostMain.ts +++ b/src/host/hostMain.ts @@ -20,7 +20,6 @@ import { createSerialManifestWriter } from './manifestWriter.js'; import { captureProgram, programWithoutToken, - readProcStat, stopProgramGroup, writeProgramRecord, } from './programGroup.js'; @@ -108,6 +107,9 @@ export const MAX_CONSECUTIVE_POLL_FAILURES = 10; const IDLE_CHECK_CAP_MS = 5_000; const MANIFEST_WAIT_INTERVAL_MS = 20; const CREATE_FAILED_POLL_INTERVAL_MS = 100; +// A create ends well within this time after its host's start-up check: its +// readiness wait and its marker retries take about 20 s at most. +const CREATE_FAILED_WATCH_MAX_MS = 60_000; // How long the host waits after SIGHUP before it kills the program's process // group. nvim takes about 1 s to exit on SIGHUP, and `destroy` waits about 5 s. const SHUTDOWN_KILL_GRACE_MS = 2_000; @@ -1278,19 +1280,26 @@ export async function runHost( // Windows it sends nothing when its manifest read fails. It writes the // create-failed marker before it exits, so the host watches for the marker // while its creator runs, and once more after the creator has exited. + // The host is the creator's child. 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. Windows keeps the parent pid, so there + // only the probe tells, and an error of the probe, such as EPERM from a + // process of another user that took the pid, means that the creator has + // exited. The watch stops after CREATE_FAILED_WATCH_MAX_MS in any case. + const creatorRuns = (): boolean => { + if (process.platform !== 'win32' && process.ppid !== creatorPid) { + return false; + } + try { + return isProcessAlive(creatorPid); + } catch { + return false; + } + }; const watchCreateFailed = (): void => { + const deadline = Date.now() + CREATE_FAILED_WATCH_MAX_MS; const timer = setInterval(() => { - // An error of the probe, such as EPERM from a process of another user - // that took the pid, means that the creator has exited. So does a - // zombie, which kill(pid, 0) still finds until its parent reaps it. - let creatorGone = true; - try { - creatorGone = - !isProcessAlive(creatorPid) || - readProcStat(creatorPid)?.state === 'Z'; - } catch { - // creatorGone stays true. - } + const creatorGone = !creatorRuns() || Date.now() >= deadline; if (existsSync(createFailedMarkerPath(sessDir))) { clearInterval(timer); startShutdown(); From c92d212d194f977ba4d7eb1dd23e20cd29877311 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 15:13:41 +0000 Subject: [PATCH 3/8] fix(skills): give the runs that explore the whole model more TLC workers A share of CI's lifecycle-model job took as long as its longest run, which TLC checked with 1 worker: 43 min for mutant-ReconcileSkipsTerminal. The runs that expect pass now share the CPUs, each with at least 1 worker. A run that expects a violation keeps 1 worker, so its trace stays the shortest. --- .../verify-session-lifecycle/scripts/check.sh | 24 +++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/scripts/check.sh b/.agents/skills/verify-session-lifecycle/scripts/check.sh index 061e278c..a8bfa173 100755 --- a/.agents/skills/verify-session-lifecycle/scripts/check.sh +++ b/.agents/skills/verify-session-lifecycle/scripts/check.sh @@ -337,12 +337,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" } From 6dfedf9d6d69c0be36ee185645e850a769e88108 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 15:45:42 +0000 Subject: [PATCH 4/8] docs: say how check.sh runs the TLC runs and how CI shares them The ci.yml comment of #328 said that check.sh waits for each batch of CHECK_JOBS runs. On Linux it keeps a pool and starts a new run as soon as one ends; only the bash 3.2 of macOS waits for each batch. SKILL.md still said that CI runs the check in four shares, and that it takes about an hour. Both now describe the 8 shares, CHECK_JOBS 12 and the TLC workers of the runs that expect pass. --- .../skills/verify-session-lifecycle/SKILL.md | 4 ++-- .github/workflows/ci.yml | 19 ++++++++----------- 2 files changed, 10 insertions(+), 13 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 50f01362..593d8fd3 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.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=/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=/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. ## 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=85` 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. `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=85` 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: diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6e223cc6..92e2990c 100644 --- a/.github/workflows/ci.yml +++ b/.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 #324, 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 1 + # TLC worker per run, the shares took 16 to 43 min, and the 43 min share + # held only the longest run. 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. lifecycle-model: runs-on: ubuntu-latest timeout-minutes: 55 From d9aa04226d227ec0c6047b83d5d81577c8392edf Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 17:10:48 +0000 Subject: [PATCH 5/8] chore(skills): sync lifecycle coverage after the marker watch and worker changes --- .agents/skills/verify-session-lifecycle/coverage.json | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index 94b58db2..5b0937b6 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.agents/skills/verify-session-lifecycle/coverage.json @@ -139,13 +139,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": "7f1c6dd7943968c3", - "skill:scripts/facts.mjs": "6ee4da3ef9b6bac3", - "skill:scripts/check.sh": "b48bc5fd343aefb5" + "skill:scripts/facts.mjs": "5958522d300c08cf", + "skill:scripts/check.sh": "f5f50d3ddf522857" }, "callSites": { "writeManifest": [ From 996c8759cb2645ab8962e22cba6100593c23d8a6 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 17:54:41 +0000 Subject: [PATCH 6/8] docs: give the measured times of the lifecycle-model shares On #330, where the runs that expect pass get the 4 vCPUs as TLC workers, the 8 shares took 11 to 33 min. With 1 worker per run they took 15 to 43 min (#329). --- .agents/skills/verify-session-lifecycle/SKILL.md | 2 +- .github/workflows/ci.yml | 9 ++++----- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 593d8fd3..910dccc4 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.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 eight jobs with `CHECK_SHARD=/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. +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=/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. On #330 a share took 11 to 33 min. ## Run it diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 92e2990c..081e18b2 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -224,11 +224,10 @@ jobs: # covered code. Each of the 8 shares starts all its runs at once # (CHECK_JOBS 12: with the model of #324, 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 1 - # TLC worker per run, the shares took 16 to 43 min, and the 43 min share - # held only the longest run. 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. + # TLC workers. So a share takes about as long as its longest run: 11 to + # 33 min on #330. With 1 TLC worker per run, the shares took 15 to 43 min. + # 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 From 505f28bfa522dfd3b681594cf8886d2c8930e3e4 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 18:42:05 +0000 Subject: [PATCH 7/8] docs: name the model that the share times and run counts belong to The times of 996c8759 were measured with the model of #324. #327 adds runs, and a share still holds 10 to 12 runs, of which at most 2 expect pass. --- .agents/skills/verify-session-lifecycle/SKILL.md | 2 +- .github/workflows/ci.yml | 11 ++++++----- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/SKILL.md b/.agents/skills/verify-session-lifecycle/SKILL.md index 820085be..0804a2bd 100644 --- a/.agents/skills/verify-session-lifecycle/SKILL.md +++ b/.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 eight jobs with `CHECK_SHARD=/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. On #330 a share took 11 to 33 min. +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=/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 diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 081e18b2..79e8ab2d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -222,12 +222,13 @@ 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. Each of the 8 shares starts all its runs at once - # (CHECK_JOBS 12: with the model of #324, 10 to 12 runs, of which at most + # (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: 11 to - # 33 min on #330. With 1 TLC worker per run, the shares took 15 to 43 min. - # 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. + # 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 From f7d7da2bb3fb9681d8a6bf1429a30241f84294cb Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Wed, 4 Nov 2026 19:38:04 +0000 Subject: [PATCH 8/8] chore(skills): sync lifecycle coverage after the merge with #327 --- .agents/skills/verify-session-lifecycle/coverage.json | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.agents/skills/verify-session-lifecycle/coverage.json b/.agents/skills/verify-session-lifecycle/coverage.json index ed8dd56b..e89f55bd 100644 --- a/.agents/skills/verify-session-lifecycle/coverage.json +++ b/.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": [