fix: on Windows, stop a late host after a failed create in more cases, and name the session in text mode

.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;/,

docs/USAGE.md

@@ -326,7 +326,7 @@ A `list`, `inspect` or `gc` that reads the session between those two writes sees
 If `destroy` fails after it wrote the file, for example because its manifest write fails, the file stays, and the next reconcile records the session as `destroyed`, also when the session had already ended. Nothing deletes the file before `gc` removes the session folder, because a reconcile that read before the destroy can still write after it.
 A host that died after it recorded the session as ended leaves its socket. `gc`, and a `destroy` of a `destroyed` session, remove that socket when the manifest names no host pid or the host check below reads the host as ended.
 When `create` cannot reach its new host, it fails and tells the host to stop. It fails with `HOST_UNREACHABLE` (exit 6) after about 6 s when nothing listens on the socket, and with `HOST_TIMEOUT` (exit 5) after about 10 s when the host accepts the connection but does not answer.
-`create` also tells the host to stop when it fails for another reason after it wrote the session's first manifest, for example when it cannot read that manifest again. Each such error names the session in `details.sessionId`.
+`create` also tells the host to stop when it fails for another reason after it wrote the session's first manifest, for example when it cannot read that manifest again. Each such error names the session in `details.sessionId`, and in text mode `create` prints `Session <id> failed to start.` before the error line.
 When that first manifest write fails, `create` removes the session folder. The host waits for the manifest only while `create` runs, so it then exits without starting the program.
 On Linux and macOS it sends the host SIGTERM, and the host stops the program the way `destroy` does and records the session as `destroyed` once the program's group has ended, also while its start-up is still slow.
 `create` exits before the host has ended the session, so a caller that checks at once can still read `running` or `destroying`.
@@ -337,7 +337,7 @@ When the host cannot end the program's group, for example a process of another u
 A host stopped with SIGSTOP, or with a blocked event loop, handles the SIGTERM only when it runs again. Until then the program runs and the session reads `running`. A plain `destroy` fails because the host does not answer, and only `destroy --force` ends the session sooner.
 On Windows, SIGTERM ends the host at once, so the host cannot stop the program itself. There `create` sends it only once the manifest names the program: the session then reads `running` with a dead host until the next reconcile records it `failed` and ends the program. Before the host's start-up write, `create` sends nothing.
 For that case, on every platform, `create` first writes an empty internal file, `create-failed`, in the session folder, and then reads the manifest. The host checks for that file before it starts the program, and returns then, so no program runs and the next reconcile records the session `failed`. It checks again right after its start-up write, and then ends the session the way a SIGTERM does on Linux: it stops the program and records `destroyed`.
-On Windows, a host whose start-up write lands before `create` reads the manifest is named by that read and gets the SIGTERM, and a host whose write lands after it finds the file. When the file write fails, for example on a full disk, a Windows host that starts late can still serve the session. This path is not tested on a real Windows host.
+On Windows, a host whose start-up write lands before `create` reads the manifest is named by that read and gets the SIGTERM, and a host whose write lands after it finds the file. After its start-up write, the host also checks for the file every 100 ms while `create` runs, and once after `create` exits, so it ends the session also when `create` cannot read the manifest. When the file write fails, `create` writes it again every 100 ms, up to 50 times, while the host runs and the manifest names no program. When every write fails, for example on a full disk, a Windows host that starts late can still serve the session. This path is not tested on a real Windows host.
 
 On Linux, `destroy` and reconcile never kill a process group that they cannot prove is the session's.
 When the host starts the program, it records the program's pid, the boot id and the program's autogroup id in an internal file, `program.json`.