From 01b34a8ce5b08371dbd4c6a3a2ae0278bacac8ba Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Sat, 3 Oct 2026 19:47:44 +0000 Subject: [PATCH 1/2] =?UTF-8?q?=F0=9F=A4=96=20fix:=20keep=20a=20refused=20?= =?UTF-8?q?or=20failed=20migration=20pending=20until=20its=20command=20exi?= =?UTF-8?q?ts?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes #5522 --- formal/background-processes/BgCleanup.tla | 27 +++++--- .../MC_cleanup_archive.cfg | 1 + .../MC_cleanup_archive_fixed.cfg | 1 + .../MC_cleanup_failed_join_timeout.cfg | 1 + .../background-processes/MC_cleanup_fixed.cfg | 1 + .../MC_cleanup_migration_remove.cfg | 1 + .../MC_cleanup_migration_timeout.cfg | 1 + .../MC_cleanup_refused_join_timeout.cfg | 1 + .../MC_cleanup_spawn_remove.cfg | 1 + .../MC_mut_cleanup_join_untracked.cfg | 14 ++++ .../MC_mut_cleanup_nodrain.cfg | 1 + formal/background-processes/check.sh | 8 ++- .../backgroundProcessesFormalRepro.test.ts | 67 +++++++------------ src/node/services/tools/bash.ts | 20 +++++- 14 files changed, 88 insertions(+), 57 deletions(-) create mode 100644 formal/background-processes/MC_mut_cleanup_join_untracked.cfg diff --git a/formal/background-processes/BgCleanup.tla b/formal/background-processes/BgCleanup.tla index 16ff19b502..26d47194f5 100644 --- a/formal/background-processes/BgCleanup.tla +++ b/formal/background-processes/BgCleanup.tla @@ -33,10 +33,14 @@ (* registration is already gone (:1479) and nothing records it, so a *) (* command whose exit the join does not see (stuck in uninterruptible *) (* I/O, or a remote exec whose close never arrives) runs on untracked *) -(* and the removal deletes its checkout: MC_cleanup_refused_join_ *) -(* timeout violates NoLiveAfterDelete and MigrationOwned (#5522). *) -(* MC_cleanup_failed_join_timeout forces the admitted-then-failed *) -(* path (MigrationFails) and violates the same invariants. *) +(* and the removal deletes its checkout (#5522). Fixed: the migration *) +(* stays pending until the command's exit settles (bash.ts:1588), so *) +(* cleanup's drains wait for it ("stopping"; a removal's 60 s drain *) +(* deadline fails it instead, not modelled: failing never deletes). *) +(* MC_cleanup_refused_join_timeout and MC_cleanup_failed_join_timeout *) +(* (MigrationFails forces the admitted-then-failed path) hold; the *) +(* mutant JoinUntracked (the code before #5522) violates *) +(* NoLiveAfterDelete and MigrationOwned. *) (* ExecTimeout (case 2): the foreground exec's timer (LocalBaseRuntime *) (* :369-377, RemoteRuntime :266-) still runs after a migration and *) (* can kill the command. Benign: timeout_secs is the documented max *) @@ -56,6 +60,7 @@ CONSTANTS ArchiveCleans, \* fix: archive seals and runs cleanup before stopping the stream or deleting NoDrain, \* mutant: cleanup does not wait for pending migrations (#4805 undone) JoinTimeout, \* case 1: the 5 s join after a refused migration's kill can expire first + JoinUntracked, \* mutant: the migration ends at the join timeout (before #5522) ExecTimeout, \* case 2: the foreground exec's own timeout can kill F after the migration MigrationFails \* case 1, forced: the migration is admitted, then migrateToBackground fails @@ -132,10 +137,14 @@ MRefused == /\ mpc = "refused" /\ fg' = FALSE /\ mpc' = "join" MJoin == /\ mpc = "join" /\ fLive' = FALSE /\ mpc' = "end" /\ UNCHANGED <> -\* ... or (case 1) gives up after 5 s with F still running; FExit can end it later. -MJoinTimeout == /\ JoinTimeout /\ mpc = "join" /\ mpc' = "end" +\* ... or (case 1) gives up after 5 s with F still running; FExit can end it later. The +\* migration stays pending until then (#5522). +MJoinTimeout == /\ JoinTimeout /\ mpc = "join" /\ mpc' = IF JoinUntracked THEN "end" ELSE "stopping" /\ UNCHANGED <> +MStopped == /\ mpc = "stopping" /\ ~fLive /\ mpc' = "end" \* exitCode settles + /\ UNCHANGED <> MEnd == /\ mpc = "end" /\ mPending' = mPending - 1 /\ mpc' = "done" /\ fg' = (fg /\ fLive) \* :1605 unregister on exit /\ UNCHANGED <> Next == SStart \/ SChild \/ SRegister \/ SExit - \/ MBegin \/ MClaim \/ MExitCheck \/ MMigrate \/ MMigrateFail \/ MRefused \/ MJoin \/ MJoinTimeout \/ MEnd + \/ MBegin \/ MClaim \/ MExitCheck \/ MMigrate \/ MMigrateFail \/ MRefused \/ MJoin + \/ MJoinTimeout \/ MStopped \/ MEnd \/ FExit \/ FTimeout \/ RStart \/ RStop \/ CSeal \/ CDrain1 \/ CSnap \/ CTerm \/ CDrain2 \/ RDelete @@ -211,7 +221,8 @@ NoLiveAfterDelete == deleted => ~sLive /\ ~fLive FgBgExclusive == ~(fg /\ bg) \* ... and while it lives, the foreground, the background or its migration block owns it. MigrationOwned == - fLive => (fg \/ bg \/ mpc \in {"claim", "exitcheck", "migrate", "refused", "join", "end"}) + fLive => (fg \/ bg \/ mpc \in {"claim", "exitcheck", "migrate", "refused", "join", "stopping", + "end"}) TypeOK == seals \in 0..2 /\ mPending \in 0..1 /\ stopped \in BOOLEAN ============================================================================= diff --git a/formal/background-processes/MC_cleanup_archive.cfg b/formal/background-processes/MC_cleanup_archive.cfg index 6f60bc23e9..acb8b2ac49 100644 --- a/formal/background-processes/MC_cleanup_archive.cfg +++ b/formal/background-processes/MC_cleanup_archive.cfg @@ -8,6 +8,7 @@ CONSTANTS ArchiveCleans = FALSE NoDrain = FALSE JoinTimeout = FALSE + JoinUntracked = FALSE ExecTimeout = FALSE MigrationFails = FALSE INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned diff --git a/formal/background-processes/MC_cleanup_archive_fixed.cfg b/formal/background-processes/MC_cleanup_archive_fixed.cfg index 68cbba65a0..a0d4956f53 100644 --- a/formal/background-processes/MC_cleanup_archive_fixed.cfg +++ b/formal/background-processes/MC_cleanup_archive_fixed.cfg @@ -8,6 +8,7 @@ CONSTANTS ArchiveCleans = TRUE NoDrain = FALSE JoinTimeout = FALSE + JoinUntracked = FALSE ExecTimeout = FALSE MigrationFails = FALSE INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned diff --git a/formal/background-processes/MC_cleanup_failed_join_timeout.cfg b/formal/background-processes/MC_cleanup_failed_join_timeout.cfg index d0b3154bf5..7a97f6d953 100644 --- a/formal/background-processes/MC_cleanup_failed_join_timeout.cfg +++ b/formal/background-processes/MC_cleanup_failed_join_timeout.cfg @@ -8,6 +8,7 @@ CONSTANTS ArchiveCleans = FALSE NoDrain = FALSE JoinTimeout = TRUE + JoinUntracked = FALSE ExecTimeout = FALSE MigrationFails = TRUE INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned diff --git a/formal/background-processes/MC_cleanup_fixed.cfg b/formal/background-processes/MC_cleanup_fixed.cfg index 5c18884ea0..1c7d5deb3f 100644 --- a/formal/background-processes/MC_cleanup_fixed.cfg +++ b/formal/background-processes/MC_cleanup_fixed.cfg @@ -8,6 +8,7 @@ CONSTANTS ArchiveCleans = FALSE NoDrain = FALSE JoinTimeout = FALSE + JoinUntracked = FALSE ExecTimeout = FALSE MigrationFails = FALSE INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned diff --git a/formal/background-processes/MC_cleanup_migration_remove.cfg b/formal/background-processes/MC_cleanup_migration_remove.cfg index 05fa17024d..783011cf7b 100644 --- a/formal/background-processes/MC_cleanup_migration_remove.cfg +++ b/formal/background-processes/MC_cleanup_migration_remove.cfg @@ -8,6 +8,7 @@ CONSTANTS ArchiveCleans = FALSE NoDrain = FALSE JoinTimeout = FALSE + JoinUntracked = FALSE ExecTimeout = FALSE MigrationFails = FALSE INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned diff --git a/formal/background-processes/MC_cleanup_migration_timeout.cfg b/formal/background-processes/MC_cleanup_migration_timeout.cfg index 189b49ef39..75b48b0fd4 100644 --- a/formal/background-processes/MC_cleanup_migration_timeout.cfg +++ b/formal/background-processes/MC_cleanup_migration_timeout.cfg @@ -8,6 +8,7 @@ CONSTANTS ArchiveCleans = FALSE NoDrain = FALSE JoinTimeout = FALSE + JoinUntracked = FALSE ExecTimeout = TRUE MigrationFails = FALSE INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned diff --git a/formal/background-processes/MC_cleanup_refused_join_timeout.cfg b/formal/background-processes/MC_cleanup_refused_join_timeout.cfg index 1e24221bb4..01b07a9005 100644 --- a/formal/background-processes/MC_cleanup_refused_join_timeout.cfg +++ b/formal/background-processes/MC_cleanup_refused_join_timeout.cfg @@ -8,6 +8,7 @@ CONSTANTS ArchiveCleans = FALSE NoDrain = FALSE JoinTimeout = TRUE + JoinUntracked = FALSE ExecTimeout = FALSE MigrationFails = FALSE INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned diff --git a/formal/background-processes/MC_cleanup_spawn_remove.cfg b/formal/background-processes/MC_cleanup_spawn_remove.cfg index 8eb884ba3d..b4f561a962 100644 --- a/formal/background-processes/MC_cleanup_spawn_remove.cfg +++ b/formal/background-processes/MC_cleanup_spawn_remove.cfg @@ -8,6 +8,7 @@ CONSTANTS ArchiveCleans = FALSE NoDrain = FALSE JoinTimeout = FALSE + JoinUntracked = FALSE ExecTimeout = FALSE MigrationFails = FALSE INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned diff --git a/formal/background-processes/MC_mut_cleanup_join_untracked.cfg b/formal/background-processes/MC_mut_cleanup_join_untracked.cfg new file mode 100644 index 0000000000..c2857f2fd4 --- /dev/null +++ b/formal/background-processes/MC_mut_cleanup_join_untracked.cfg @@ -0,0 +1,14 @@ +\* Mutant (the code before #5522): a refused migration ends at the 5 s join, so its command runs untracked. +SPECIFICATION Spec +CONSTANTS + HasSpawn = FALSE + HasMigration = TRUE + Mutator = "remove" + SpawnSealed = FALSE + ArchiveCleans = FALSE + NoDrain = FALSE + JoinTimeout = TRUE + JoinUntracked = TRUE + ExecTimeout = FALSE + MigrationFails = FALSE +INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned diff --git a/formal/background-processes/MC_mut_cleanup_nodrain.cfg b/formal/background-processes/MC_mut_cleanup_nodrain.cfg index db83d270df..9b58860370 100644 --- a/formal/background-processes/MC_mut_cleanup_nodrain.cfg +++ b/formal/background-processes/MC_mut_cleanup_nodrain.cfg @@ -8,6 +8,7 @@ CONSTANTS ArchiveCleans = FALSE NoDrain = TRUE JoinTimeout = FALSE + JoinUntracked = FALSE ExecTimeout = FALSE MigrationFails = FALSE INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned diff --git a/formal/background-processes/check.sh b/formal/background-processes/check.sh index 23dc60668e..0614dfc701 100755 --- a/formal/background-processes/check.sh +++ b/formal/background-processes/check.sh @@ -54,9 +54,11 @@ declare -A EXPECT=( [MC_cleanup_fixed]="" [MC_cleanup_archive_fixed]="" [MC_mut_cleanup_nodrain]="NoLiveAfterDelete" - # #5465 case 1: a refused migration whose command outlives the 5 s kill join runs untracked (#5522). - [MC_cleanup_refused_join_timeout]="NoLiveAfterDelete MigrationOwned" - [MC_cleanup_failed_join_timeout]="NoLiveAfterDelete MigrationOwned" + # #5465 case 1: a refused or failed migration whose command outlives the 5 s kill join stays + # pending until it exits (#5522); the mutant drops it at the join, as the code before #5522 did. + [MC_cleanup_refused_join_timeout]="" + [MC_cleanup_failed_join_timeout]="" + [MC_mut_cleanup_join_untracked]="NoLiveAfterDelete MigrationOwned" # #5465 case 2: the foreground exec's timeout killing a migrated command is an observed exit. [MC_cleanup_migration_timeout]="" # Record names: host-local holds; remote runtimes are #4889 at f30a1945a6, and diff --git a/src/node/services/backgroundProcessesFormalRepro.test.ts b/src/node/services/backgroundProcessesFormalRepro.test.ts index 4545ae0b27..1dddfe2dd6 100644 --- a/src/node/services/backgroundProcessesFormalRepro.test.ts +++ b/src/node/services/backgroundProcessesFormalRepro.test.ts @@ -413,7 +413,7 @@ describe("#4889: same-name spawns from two backends on a non-host runtime", () = // no manager entry and no record, so the removal waiting on the migration goes on to delete its // checkout. The runtime below holds the abort until the test releases it: it stands in for a kill // that takes effect after the join (a command stuck in uninterruptible I/O, or a remote exec whose -// close is late). Follow-up fix: #5522. +// close is late). Fixed in #5522: the migration stays pending until the command's exit settles. describe("#5465 case 1: a refused migration whose command outlives the kill join", () => { /** @@ -481,7 +481,7 @@ describe("#5465 case 1: a refused migration whose command outlives the kill join expect(!result.success && result.error).toContain( failMigration ? "ENOSPC" : "being cleaned up" ); - return { manager, ws, pid }; + return { manager, ws, pid, releaseKill: () => releaseKill.resolve() }; } test("control: a refused migration's command is stopped once its kill takes effect", async () => { @@ -490,45 +490,26 @@ describe("#5465 case 1: a refused migration whose command outlives the kill join expect(isAlive(pid)).toBe(false); }, 20_000); - test("a refused migration does not leave its command running untracked", async () => { - await expectReproFailure( - async () => { - const { manager, ws, pid } = await refuseMigration("join", true); - // The join gave up: the command the tool reported as terminated still runs. - expect(isAlive(pid)).toBe(true); - // A removal's cleanup (workspaceService.ts) deletes the checkout once it returns, so it - // must keep waiting (or fail closed at its drain deadline) while the command runs. - const cleanup = manager.cleanup(ws, { failClosedAfterDrainTimeout: true }).then( - () => "finished", - () => "failed closed" - ); - const early = await Promise.race([cleanup, Bun.sleep(500).then(() => "waiting")]); - // Target assertion: the cleanup has not finished under the running command (waiting or - // failing closed are both safe). - expect(early === "finished").toBe(false); - }, - { matcher: "toBe", expected: "false", received: "true" } - ); - }, 20_000); - - test("a failed migration does not leave its command running untracked", async () => { - await expectReproFailure( - async () => { - const { manager, ws, pid } = await refuseMigration("join-fail", true, true); - // The join gave up: the command the tool reported as terminated still runs. - expect(isAlive(pid)).toBe(true); - // A removal's cleanup (workspaceService.ts) deletes the checkout once it returns, so it - // must keep waiting (or fail closed at its drain deadline) while the command runs. - const cleanup = manager.cleanup(ws, { failClosedAfterDrainTimeout: true }).then( - () => "finished", - () => "failed closed" - ); - const early = await Promise.race([cleanup, Bun.sleep(500).then(() => "waiting")]); - // Target assertion: the cleanup has not finished under the running command (waiting or - // failing closed are both safe). - expect(early === "finished").toBe(false); - }, - { matcher: "toBe", expected: "false", received: "true" } - ); - }, 20_000); + for (const failMigration of [false, true]) { + test(`a ${failMigration ? "failed" : "refused"} migration keeps its command tracked until it exits`, async () => { + const { manager, ws, pid, releaseKill } = await refuseMigration( + failMigration ? "join-fail" : "join", + true, + failMigration + ); + // The join gave up: the command the tool reported as terminated still runs. + expect(isAlive(pid)).toBe(true); + // A removal's cleanup (workspaceService.ts) deletes the checkout once it returns, so it must + // keep waiting (or fail closed at its drain deadline) while the command runs. + const cleanup = manager.cleanup(ws, { failClosedAfterDrainTimeout: true }).then( + () => "finished", + () => "failed closed" + ); + expect(await Promise.race([cleanup, Bun.sleep(500).then(() => "waiting")])).toBe("waiting"); + // Once the kill takes effect, the exit settles the migration and the cleanup finishes. + releaseKill(); + expect(await cleanup).toBe("finished"); + expect(isAlive(pid)).toBe(false); + }, 20_000); + } }); diff --git a/src/node/services/tools/bash.ts b/src/node/services/tools/bash.ts index fea1091bec..4a6a5fac99 100644 --- a/src/node/services/tools/bash.ts +++ b/src/node/services/tools/bash.ts @@ -1434,10 +1434,18 @@ ${scriptWithEnv}`; // migration, or found exited: a cleanup() in between waits for it (#4805), including // the awaited name claim and exit grace (#4967). Refused (not admitted) once cleanup // has started for the workspace (#4967). - using migration = + const migration = config.backgroundProcessManager && config.workspaceId ? config.backgroundProcessManager.beginMigration(config.workspaceId) : undefined; + // Ends the migration with this block, unless the failed-migration path below hands it + // to the terminated command's exit (#5522). + let migrationHandedToExit = false; + using _endMigration = { + [Symbol.dispose]: () => { + if (!migrationHandedToExit) migration?.[Symbol.dispose](); + }, + }; // Claim the migrated record's name across backends BEFORE the exit check below // (#4878): the claim may wait on another backend's spawn lock, and a command that // exits during that wait must take the normal completion path, not be reported as @@ -1573,8 +1581,14 @@ ${scriptWithEnv}`; stderrForMigration.cancel().catch(() => { /* ignore */ return; }); - // Keep the migration pending (the `using` above) until the terminated command exits, - // so a removal's cleanup() cannot delete the checkout while it is still stopping. + // Keep the migration pending until the terminated command's exit settles, even past + // the bounded join below, so a removal's cleanup() keeps waiting (and fails closed at + // its drain deadline) instead of deleting the checkout under a command whose kill + // has not taken effect yet (#5522). + migrationHandedToExit = true; + void execStream.exitCode + .catch(() => undefined) + .finally(() => migration?.[Symbol.dispose]()); await raceWithAbortAndTimeout(execStream.exitCode, { timeoutMs: FAILED_MIGRATION_EXIT_JOIN_MS, }).catch(() => undefined); From 7ee1ce85ed2cf19e0c5745e75288eb5c8b12664d Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Sat, 3 Oct 2026 20:54:19 +0000 Subject: [PATCH 2/2] =?UTF-8?q?=F0=9F=A4=96=20fix:=20a=20rejected=20exit?= =?UTF-8?q?=20observation=20keeps=20the=20failed=20migration=20pending?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../backgroundProcessesFormalRepro.test.ts | 29 +++++++++++++++++-- src/node/services/tools/bash.ts | 10 +++++-- 2 files changed, 33 insertions(+), 6 deletions(-) diff --git a/src/node/services/backgroundProcessesFormalRepro.test.ts b/src/node/services/backgroundProcessesFormalRepro.test.ts index 1dddfe2dd6..720eacae96 100644 --- a/src/node/services/backgroundProcessesFormalRepro.test.ts +++ b/src/node/services/backgroundProcessesFormalRepro.test.ts @@ -420,10 +420,16 @@ describe("#5465 case 1: a refused migration whose command outlives the kill join * Backend A: a foreground command sent to the background while cleanup seals the workspace, or * (`failMigration`) an admitted migration whose record cannot be created. */ - async function refuseMigration(tag: string, holdKill: boolean, failMigration = false) { + async function refuseMigration( + tag: string, + holdKill: boolean, + failMigration = false, + rejectExit = false + ) { const ws = uniqueWorkspace(tag); const manager = new BackgroundProcessManager(path.dirname(localBgWorkspaceDir(ws))); - cleanups.push(() => manager.cleanup(ws)); + // A rejected exit observation keeps the migration pending for good, so cleanup() would hang. + if (!rejectExit) cleanups.push(() => manager.cleanup(ws)); const dir = await tempDir(tag); const pidFile = path.join(dir, "pid"); const releaseKill = Promise.withResolvers(); @@ -436,7 +442,15 @@ describe("#5465 case 1: a refused migration whose command outlives the kill join () => void releaseKill.promise.then(() => delayed.abort()), { once: true } ); - return super.exec(command, { ...options, abortSignal: delayed.signal }); + return super.exec(command, { ...options, abortSignal: delayed.signal }).then((stream) => + rejectExit + ? { + ...stream, + // The transport fails instead of reporting the exit (RemoteRuntime's child error). + exitCode: stream.exitCode.then(() => Promise.reject(new Error("transport lost"))), + } + : stream + ); } } const runtime = holdKill ? new HeldKillRuntime(process.cwd()) : new LocalRuntime(process.cwd()); @@ -512,4 +526,13 @@ describe("#5465 case 1: a refused migration whose command outlives the kill join expect(isAlive(pid)).toBe(false); }, 20_000); } + + test("a migration whose exit observation fails stays pending", async () => { + const { manager, ws, releaseKill } = await refuseMigration("join-reject", true, false, true); + // The kill takes effect, but the runtime reports an error instead of the exit: that does not + // confirm the stop, so a removal's cleanup must not finish. + releaseKill(); + const cleanup = manager.cleanup(ws).then(() => "finished"); + expect(await Promise.race([cleanup, Bun.sleep(500).then(() => "waiting")])).toBe("waiting"); + }, 20_000); }); diff --git a/src/node/services/tools/bash.ts b/src/node/services/tools/bash.ts index 4a6a5fac99..6a9f6fd941 100644 --- a/src/node/services/tools/bash.ts +++ b/src/node/services/tools/bash.ts @@ -1585,10 +1585,14 @@ ${scriptWithEnv}`; // the bounded join below, so a removal's cleanup() keeps waiting (and fails closed at // its drain deadline) instead of deleting the checkout under a command whose kill // has not taken effect yet (#5522). + // A rejected exitCode (e.g. a remote transport error) does not confirm the stop, so the + // migration then stays pending for the session: removal and archive keep failing + // closed rather than deleting the checkout under a command that may still run. migrationHandedToExit = true; - void execStream.exitCode - .catch(() => undefined) - .finally(() => migration?.[Symbol.dispose]()); + void execStream.exitCode.then( + () => migration?.[Symbol.dispose](), + () => undefined + ); await raceWithAbortAndTimeout(execStream.exitCode, { timeoutMs: FAILED_MIGRATION_EXIT_JOIN_MS, }).catch(() => undefined);