🤖 fix: keep a refused or failed migration pending until its command exits

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 <<stopped, spc, sLive, sReg, fg, bg, mPending, mAdmitted, rpc, seals,
                         snapshot, deleted>>
-\* ... 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 <<stopped, spc, sLive, sReg, fLive, fg, bg, mPending, mAdmitted, rpc,
                                seals, snapshot, deleted>>
+MStopped == /\ mpc = "stopping" /\ ~fLive /\ mpc' = "end"        \* exitCode settles
+            /\ UNCHANGED <<stopped, spc, sLive, sReg, fLive, fg, bg, mPending, mAdmitted, rpc,
+                           seals, snapshot, deleted>>
 MEnd == /\ mpc = "end" /\ mPending' = mPending - 1 /\ mpc' = "done"
         /\ fg' = (fg /\ fLive)                                   \* :1605 unregister on exit
         /\ UNCHANGED <<stopped, spc, sLive, sReg, fLive, bg, mAdmitted, rpc, seals, snapshot,
@@ -199,7 +208,8 @@ RDelete == /\ rpc = "delete" /\ deleted' = TRUE /\ rpc' = "done"  \* :7710 check
                           snapshot>>
 
 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
 =============================================================================

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

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

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

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

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

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

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

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

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

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

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

src/node/services/backgroundProcessesFormalRepro.test.ts

@@ -413,17 +413,23 @@ 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", () => {
   /**
    * 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<void>();
@@ -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());
@@ -481,7 +495,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 +504,35 @@ 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);
+  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);
+  }
 
-  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" }
-    );
+  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);
 });

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,18 @@ ${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).
+            // 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.then(
+              () => migration?.[Symbol.dispose](),
+              () => undefined
+            );
             await raceWithAbortAndTimeout(execStream.exitCode, {
               timeoutMs: FAILED_MIGRATION_EXIT_JOIN_MS,
             }).catch(() => undefined);