test: trial of the 8-share lifecycle-model job on #324 (do not merge)

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

@@ -12,6 +12,8 @@
     "CreateRecordsHost": true,
     "CreateStopsOnGiveUp": true,
     "HostChecksCreateFailed": true,
+    "HostPollsCreateFailed": true,
+    "CreateRetriesMarker": true,
     "HostWaitsForManifest": true,
     "HostSerializesWrites": true,
     "HostStopsAfterTerminalWrite": true,
@@ -40,8 +42,10 @@
     "Terminal": ["destroyed", "exited", "failed"]
   },
   "fingerprints": {
-    "src/cli/commands/create.ts#runCreateCommand": "131d2707818ea283",
+    "src/cli/commands/create.ts#runCreateCommand": "bb4fa596cc1e4af7",
     "src/cli/commands/create.ts#waitForReadyHost": "a7fd2ba345b6bfd6",
+    "src/cli/commands/create.ts#writeMarkerOrLog": "abf293bd80df1c3d",
+    "src/cli/commands/create.ts#hostRuns": "b80eac3bb9523aaf",
     "src/cli/commands/destroy.ts#runDestroyCommand": "ecaa8b1d572da7c6",
     "src/cli/commands/destroy.ts#rerunInNewSession": "cf32d7d082758522",
     "src/cli/commands/gc.ts#gcSessions": "a2ac8bd10f100332",
@@ -135,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)": "1d75544221b3c6c1",
-    "src/host/hostMain.ts#runHost(final try)": "251f1e68a4ec17cc",
+    "src/host/hostMain.ts#runHost(parts)": "7bd4c6553a831b9d",
+    "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": "77ec28d60359f635",
-    "skill:scripts/facts.mjs": "eded6c52629e3523",
-    "skill:scripts/check.sh": "e33db0960de216fe"
+    "skill:model/SessionLifecycle.tla": "7f1c6dd7943968c3",
+    "skill:scripts/facts.mjs": "6ee4da3ef9b6bac3",
+    "skill:scripts/check.sh": "b48bc5fd343aefb5"
   },
   "callSites": {
     "writeManifest": [

.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 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"
+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 HostPollsCreateFailed CreateRetriesMarker"
 # 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;
@@ -181,7 +181,7 @@ NO_TOKEN_RULES="NoLiveSessionDeleted HostDeathOnlyWhenDead TerminalIsFinal Recor
 # check them.
 RULES="$NO_TOKEN_RULES NoUnrelatedGroupKilled DestroyedSessionStopped RemovedSessionStopped"
 NO_TOKEN_WITNESSES="WitnessCreateGivesUp WitnessCrashReconciled WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessReconcileRepairs"
-WITNESSES="WitnessGcRemovesSession WitnessCreateGivesUp WitnessSessionServes WitnessResizeLands WitnessCleanExitRecorded WitnessCrashReconciled WitnessDestroyCompletes WitnessSigtermRecorded WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessLeftoverMeetsDestroy WitnessReusedIdMeetsKill WitnessRecordNamesProgram WitnessUnrecordedProgramOutlives WitnessReconcileRepairs WitnessMarkedRepaired WitnessWaitPassesReusedId WitnessReusedHostMeetsKill"
+WITNESSES="WitnessGcRemovesSession WitnessCreateGivesUp WitnessSessionServes WitnessResizeLands WitnessCleanExitRecorded WitnessCrashReconciled WitnessDestroyCompletes WitnessSigtermRecorded WitnessDestroyExitedSession WitnessForceDestroyRecorded WitnessProgramOutlivesHost WitnessForeignOutlivesDestroy WitnessForeignOutlivesForce WitnessLeftoverMeetsDestroy WitnessReusedIdMeetsKill WitnessRecordNamesProgram WitnessUnrecordedProgramOutlives WitnessReconcileRepairs WitnessMarkedRepaired WitnessDeadRepairRepaired WitnessWaitPassesReusedId WitnessReusedHostMeetsKill WitnessMarkerPolled"
 
 # --- runs ----------------------------------------------------------------
 
@@ -257,11 +257,12 @@ write_run mutant-FallbackNeedsFolder violated NoUnrelatedGroupKilled "FallbackNe
 write_run mutant-ReconcileRepairsDestroyed violated DestroyedStaysDestroyed "ReconcileRepairsDestroyed=FALSE" "without the marker, a reconcile writes failed over the destroyed that destroy reported" DestroyedStaysDestroyed
 write_run mutant-CreateStopsOnGiveUp violated FailedCreateStopped "CreateStopsOnGiveUp=FALSE" "without the SIGTERM, a create that gave up leaves its host serving the session" FailedCreateStopped
 write_run mutant-HostChecksCreateFailed pass FailedCreateStopped "HostChecksCreateFailed=FALSE" "redundant off Windows: the SIGTERM stops the host"
+write_run mutant-HostPollsCreateFailed pass FailedCreateStopped "HostPollsCreateFailed=FALSE" "redundant off Windows: the SIGTERM stops the host"
 write_run mutant-TokenNamesProgram violated DestroyedSessionStopped "TokenNamesProgram=FALSE" "with the host's autogroup as the token, no member carries it, and destroy records destroyed while the program's group runs" DestroyedSessionStopped
 write_run mutant-ReusedIdReadsGone pass WitnessWaitPassesReusedId "ReusedIdReadsGone=FALSE" "with a group that took the id read alive, no wait of destroy passes while that group runs"
 write_run mutant-ProvesHostPid violated NoUnrelatedHostKilled "ProvesHostPid=FALSE" "without the start-up record, destroy --force kills a process that took the host's pid" NoUnrelatedHostKilled
 write_run witness-WitnessUnrecordedHostMeetsKill violated WitnessUnrecordedHostMeetsKill "CreateRecordsHost=FALSE" "without a record from create, as when its capture fails, a kill meets a host that host.json does not name yet"
-write_run mutant-ReconcileRepairsMarked pass DestroyedStaysDestroyed "ReconcileRepairsMarked=FALSE" "redundant in the model: it has no crash of a reconciling process, so the repair after the reconcile's own write always runs"
+write_run mutant-ReconcileRepairsMarked violated DestroyedStaysDestroyed "ReconcileRepairsMarked=FALSE" "without the repair at the first read, a list that died between its write and its repair leaves failed, and the next reconcile skips it" DestroyedStaysDestroyed
 write_run mutant-ReconcileSkipsTerminal pass RecordedExitKept "ReconcileSkipsTerminal=FALSE" "redundant: the re-read returns on a terminal manifest"
 write_run mutant-GcSkipsNonCollectable pass NoLiveSessionDeleted "GcSkipsNonCollectable=FALSE" "redundant: the final check still skips"
 write_run mutant-GcFinalCheck pass NoLiveSessionDeleted "GcFinalCheck=FALSE" "redundant: the first check still skips"
@@ -311,6 +312,9 @@ write_run mutant-ReconcileWaitsForGroup-no-token violated LiveGroupStaysNamed "R
 WIN32=TRUE
 write_run current-win32 pass "$NO_TOKEN_RULES" "" "the code on Windows: R1 to R14 and R17 to R19 hold"
 write_run mutant-HostChecksCreateFailed-win32 violated FailedCreateStopped "HostChecksCreateFailed=FALSE" "without the marker, a host that the manifest does not name yet keeps serving after create gave up" FailedCreateStopped
+write_run mutant-HostPollsCreateFailed-win32 violated FailedCreateStopped "HostPollsCreateFailed=FALSE" "without the watch, a host that checked for the marker before create wrote it keeps serving when create cannot read the manifest" FailedCreateStopped
+write_run mutant-CreateRetriesMarker-win32 violated FailedCreateStopped "CreateRetriesMarker=FALSE" "without the retries, a marker write that fails once leaves a host that the manifest does not name yet serving after create gave up" FailedCreateStopped
+write_run witness-WitnessMarkerRetried-win32 violated WitnessMarkerRetried "" "the model reaches this state on Windows"
 WIN32=FALSE
 
 # A run that expects pass explores the whole model and takes minutes, and a

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

@@ -257,6 +257,8 @@ function createFacts() {
     CreateRecordsHost: recordsHost,
     CreateStopsOnGiveUp: stopsOnGiveUp(create.body),
     HostChecksCreateFailed: checksCreateFailed(create.body),
+    HostPollsCreateFailed: pollsCreateFailed(),
+    CreateRetriesMarker: retriesMarker(create.body),
   };
 }
 
@@ -281,22 +283,25 @@ function giveUpCatch(body) {
       tried[0] ===
         'result = await waitForReadyHost(socketFile, sessionDirectory, sessionId);'
     ) {
-      return s.catchClause.block.statements.map((t) => normalize(t.getText()));
+      // The text-mode line that names the session changes no process or
+      // file, so the facts skip it.
+      return s.catchClause.block.statements
+        .map((t) => normalize(t.getText()))
+        .filter(
+          (t) => !t.startsWith('if (!options.json) { writeHumanErrorLines('),
+        );
     }
   }
   return null;
 }
 
 function stopsOnGiveUp(body) {
   const st = giveUpCatch(body) ?? [];
+  // No statement before the stop leaves the catch.
   const stops =
     st.length >= 4 &&
     st[0].startsWith('invariant(host !== undefined,') &&
-    st
-      .at(-3)
-      .startsWith(
-        'const manifest = await readManifestIfExists( manifestPath(sessionDirectory), )',
-      ) &&
+    st.slice(1, -2).every((t) => !/\b(return|throw|break)\b/.test(t)) &&
     st.at(-2) ===
       "if (process.platform !== 'win32' || manifest?.childPid != null) { host.stop(); }" &&
     st.at(-1) === 'throw withSessionId(error, sessionId);';
@@ -330,11 +335,14 @@ function stopsOnGiveUp(body) {
 function checksCreateFailed(body) {
   const st = giveUpCatch(body) ?? [];
   const marks =
-    st.length === 5 &&
-    st[1].startsWith(
-      'await writeCreateFailedMarker( createFailedMarkerPath(sessionDirectory), sessionId, ).catch(',
-    ) &&
-    st[2].startsWith('const manifest = await readManifestIfExists(');
+    st.length >= 8 &&
+    st[1] === 'const markerFile = createFailedMarkerPath(sessionDirectory);' &&
+    st[2] === 'const manifestFile = manifestPath(sessionDirectory);' &&
+    st[4] ===
+      'let marked = await writeMarkerOrLog(markerFile, sessionId, logger);' &&
+    st[5] ===
+      'let manifest = await readManifestIfExists(manifestFile).catch(() => null);' &&
+    writesMarker();
   const run = requireDeclaration('src/host/hostMain.ts', 'runHost').body;
   const check = indexOfStatement(
     run,
@@ -364,6 +372,72 @@ function checksCreateFailed(body) {
   );
 }
 
+// writeMarkerOrLog writes the create-failed marker and reports whether the
+// write landed.
+function writesMarker() {
+  const helper = normalize(
+    requireDeclaration(
+      'src/cli/commands/create.ts',
+      'writeMarkerOrLog',
+    ).body.getText(),
+  );
+  return helper.startsWith(
+    '{ return writeCreateFailedMarker(path, sessionId).then( () => true, (error: unknown) => {',
+  );
+}
+
+// On Windows, while the marker write fails and the manifest names no
+// program, the give-up catch writes the marker again and reads the manifest
+// after each write, a bounded number of times while the host runs, before
+// its stop. So a host that the manifest does not name yet gets the marker,
+// or the last read names its program and create stops it.
+function retriesMarker(body) {
+  const st = giveUpCatch(body) ?? [];
+  const loop =
+    'for ( let attempt = 1; ' +
+    "process.platform === 'win32' && !marked && manifest?.childPid == null && " +
+    'attempt <= MARKER_RETRY_MAX_ATTEMPTS && hostRuns(host.pid); ' +
+    'attempt += 1 ) { ' +
+    'await delay(MARKER_RETRY_INTERVAL_MS); ' +
+    'marked = await writeMarkerOrLog(markerFile, sessionId, logger); ' +
+    'manifest = await readManifestIfExists(manifestFile).catch(() => null); }';
+  // A probe that throws counts as an exited host.
+  const probe = normalize(
+    requireDeclaration('src/cli/commands/create.ts', 'hostRuns').body.getText(),
+  );
+  return (
+    st.length === 9 &&
+    st[6] === loop &&
+    probe ===
+      '{ try { return isProcessAlive(pid); } catch { return false; } }' &&
+    checksCreateFailed(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
+// 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 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(); };";
+  const last = run.statements.at(-1);
+  const tried =
+    last !== undefined && ts.isTryStatement(last)
+      ? last.tryBlock.statements.map((t) => normalize(t.getText()))
+      : [];
+  const check = tried.indexOf(
+    'if (existsSync(createFailedMarkerPath(sessDir))) { await initiateShutdown(); return; }',
+  );
+  return watches && check >= 0 && tried[check + 1] === 'watchCreateFailed();';
+}
+
 // runHost waits for create's manifest, and every host write of session.json
 // goes through one createSerialManifestWriter.
 function hostFacts() {
@@ -1516,6 +1590,8 @@ function policyFacts() {
 const COVERED = [
   ['src/cli/commands/create.ts', 'runCreateCommand'],
   ['src/cli/commands/create.ts', 'waitForReadyHost'],
+  ['src/cli/commands/create.ts', 'writeMarkerOrLog'],
+  ['src/cli/commands/create.ts', 'hostRuns'],
   ['src/cli/commands/destroy.ts', 'runDestroyCommand'],
   ['src/cli/commands/destroy.ts', 'rerunInNewSession'],
   ['src/cli/commands/gc.ts', 'gcSessions'],
@@ -1628,6 +1704,7 @@ const RUN_HOST_PARTS = [
   /^process\.on\('SIGTERM'/,
   /^let onSigterm = /,
   /^if \(existsSync\(createFailedMarkerPath\(sessDir\)\)\) \{/,
+  /^const watchCreateFailed = /,
   /^if \(sigterm\.received\) \{/,
   /^invariant\(!sigterm\.received/,
   /^onSigterm = startShutdown;/,

.github/workflows/ci.yml

@@ -221,18 +221,23 @@ 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 take 13
-  # to 17 min in each of 4 shares. 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. 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.
+  # 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: 50
+    timeout-minutes: 45
     strategy:
       fail-fast: false
       matrix:
-        shard: [1, 2, 3, 4]
-    name: lifecycle-model (${{ matrix.shard }}/4)
+        shard: [1, 2, 3, 4, 5, 6, 7, 8]
+    name: lifecycle-model (${{ matrix.shard }}/8)
     steps:
       - name: Check out repository
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6
@@ -267,8 +272,8 @@ jobs:
       - name: Model-check the session lifecycle
         if: steps.inputs.outputs.tlc == 'true'
         env:
-          CHECK_JOBS: '4'
-          CHECK_SHARD: ${{ matrix.shard }}/4
+          CHECK_JOBS: '12'
+          CHECK_SHARD: ${{ matrix.shard }}/8
         run: .agents/skills/verify-session-lifecycle/scripts/check.sh
 
   quality-gates: