From f475f5e634858a1f4b71d1098918c74126811782 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Fri, 2 Oct 2026 19:18:26 +0000 Subject: [PATCH 1/3] =?UTF-8?q?=F0=9F=A4=96=20tests:=20cover=20#5465=20bac?= =?UTF-8?q?kground-process=20cases=20in=20the=20TLA+=20model?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes #5465 --- formal/background-processes/BgCleanup.tla | 49 ++++++++-- .../background-processes/BgGateEvidence.tla | 72 +++++++++++---- .../MC_cleanup_archive.cfg | 2 + .../MC_cleanup_archive_fixed.cfg | 2 + .../background-processes/MC_cleanup_fixed.cfg | 2 + .../MC_cleanup_migration_remove.cfg | 2 + .../MC_cleanup_migration_timeout.cfg | 12 +++ .../MC_cleanup_refused_join_timeout.cfg | 12 +++ .../MC_cleanup_spawn_remove.cfg | 2 + .../MC_gate_crash_before_meta.cfg | 10 ++ .../MC_gate_crash_devcontainer.cfg | 10 ++ .../MC_gate_devcontainer_spawn.cfg | 2 + .../MC_gate_docker_spawn.cfg | 2 + .../MC_gate_local_spawn.cfg | 2 + .../MC_gate_migrated_ostmp.cfg | 2 + .../MC_gate_migrated_tmp.cfg | 2 + .../MC_gate_ssh_spawn.cfg | 2 + .../MC_mut_cleanup_nodrain.cfg | 2 + .../MC_mut_gate_metaless_trusted.cfg | 10 ++ .../MC_mut_gate_norecords.cfg | 2 + formal/background-processes/check.sh | 9 ++ .../backgroundProcessesFormalRepro.test.ts | 92 +++++++++++++++++++ 22 files changed, 276 insertions(+), 26 deletions(-) create mode 100644 formal/background-processes/MC_cleanup_migration_timeout.cfg create mode 100644 formal/background-processes/MC_cleanup_refused_join_timeout.cfg create mode 100644 formal/background-processes/MC_gate_crash_before_meta.cfg create mode 100644 formal/background-processes/MC_gate_crash_devcontainer.cfg create mode 100644 formal/background-processes/MC_mut_gate_metaless_trusted.cfg diff --git a/formal/background-processes/BgCleanup.tla b/formal/background-processes/BgCleanup.tla index 2a4991feda2..608fded0752 100644 --- a/formal/background-processes/BgCleanup.tla +++ b/formal/background-processes/BgCleanup.tla @@ -26,6 +26,23 @@ (* Terminate is modelled as effective (it is best-effort in the code; see *) (* BgTerminate.tla). The bash tool never checks its abort signal around *) (* spawn (bash.ts:1050-1085), so stopStream does not stop a spawn. *) +(* #5465 cases (code at 486f156905): *) +(* JoinTimeout (case 1): a refused or failed migration aborts the *) +(* command (bash.ts:1569), then joins its exit for at most *) +(* FAILED_MIGRATION_EXIT_JOIN_MS = 5 s (:1578). The foreground *) +(* 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). *) +(* 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 *) +(* lifetime of a background command (toolDefinitions.ts), and the *) +(* kill ends the same exec stream whose exitCode the migrated handle *) +(* observes and writes as exit_code (backgroundProcessExecutor.ts *) +(* :739-743). FTimeout is an ordinary exit; MC_cleanup_migration_ *) +(* timeout holds. *) (***************************************************************************) EXTENDS Naturals @@ -35,7 +52,9 @@ CONSTANTS Mutator, \* "remove" | "archive" (archive: snapshot/delete behaviour) SpawnSealed, \* fix: spawn takes a pending entry refused by the seal, like migrations ArchiveCleans, \* fix: archive seals and runs cleanup before stopping the stream or deleting - NoDrain \* mutant: cleanup does not wait for pending migrations (#4805 undone) + 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 + ExecTimeout \* case 2: the foreground exec's own timeout can kill F after the migration VARIABLES \* spawn @@ -96,10 +115,18 @@ MExitCheck == /\ mpc = "exitcheck" \* :1444-1468 MMigrate == /\ mpc = "migrate" /\ bg' = TRUE /\ mpc' = "end" \* :1507-1523 /\ UNCHANGED <> -MRefused == /\ mpc = "refused" /\ fLive' = FALSE /\ mpc' = "end" \* :1558-1567 abort + join - /\ UNCHANGED <> +\* Refused: unregister the foreground entry (:1479) and abort the command (:1569). +MRefused == /\ mpc = "refused" /\ fg' = FALSE /\ mpc' = "join" + /\ UNCHANGED <> +\* :1578 the join sees the kill take effect ... +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" + /\ UNCHANGED <> MEnd == /\ mpc = "end" /\ mPending' = mPending - 1 /\ mpc' = "done" /\ fg' = (fg /\ fLive) \* :1605 unregister on exit /\ UNCHANGED <> +\* Case 2: the original exec's timer kills F once it is (being) migrated. The migrated handle +\* observes that exit like any other (bg' = FALSE), so this is FExit restricted to those phases. +FTimeout == /\ ExecTimeout /\ fLive /\ (bg \/ mpc \in {"migrate", "end", "done"}) + /\ fLive' = FALSE /\ fg' = FALSE /\ bg' = FALSE + /\ UNCHANGED <> --------------------------------------------------------------------------- (* Mutator. *) \* Fixed archive: seal, cleanup (c_seal ... c_drain2) before its hooks, stop the stream, cleanup @@ -157,7 +190,8 @@ RDelete == /\ rpc = "delete" /\ deleted' = TRUE /\ rpc' = "done" \* :7710 check snapshot>> Next == SStart \/ SChild \/ SRegister \/ SExit - \/ MBegin \/ MClaim \/ MExitCheck \/ MMigrate \/ MRefused \/ MEnd \/ FExit + \/ MBegin \/ MClaim \/ MExitCheck \/ MMigrate \/ MRefused \/ MJoin \/ MJoinTimeout \/ MEnd + \/ FExit \/ FTimeout \/ RStart \/ RStop \/ CSeal \/ CDrain1 \/ CSnap \/ CTerm \/ CDrain2 \/ RDelete Spec == Init /\ [][Next]_vars @@ -167,7 +201,8 @@ NoLiveAfterDelete == deleted => ~sLive /\ ~fLive \* A migrating command is never both foreground and background ... 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", "end"}) +MigrationOwned == + fLive => (fg \/ bg \/ mpc \in {"claim", "exitcheck", "migrate", "refused", "join", "end"}) TypeOK == seals \in 0..2 /\ mPending \in 0..1 /\ stopped \in BOOLEAN ============================================================================= diff --git a/formal/background-processes/BgGateEvidence.tla b/formal/background-processes/BgGateEvidence.tla index 252ecf3451c..6cfd218a64e 100644 --- a/formal/background-processes/BgGateEvidence.tla +++ b/formal/background-processes/BgGateEvidence.tla @@ -18,6 +18,20 @@ (* (foreground->background) command's record is written under the *) (* manager's bgOutputDir = path.join(os.tmpdir(), "mux-bashes") *) (* (di/layers/core.ts:203), whatever the runtime. *) +(* #5465 case 3 (code at 486f156905), Crash: A's backend dies between the *) +(* spawn and writeMeta. spawnProcess creates the record directory with *) +(* output.log and clears exit_code (backgroundProcessExecutor.ts *) +(* :242-268) BEFORE it starts the child (:294); the manager writes *) +(* meta.json after (backgroundProcessManager.ts :1867). The crash drops *) +(* A's turn lease, but the scan reads a directory with neither meta.json *) +(* nor exit_code as a live orphan (recordRootHoldsOrphan :2877-2890; *) +(* tests: backgroundProcessManager.test.ts \"fails closed on unreadable *) +(* records without an exit marker\"), and the wrapper's trap writes the *) +(* marker when P exits. Benign on the scanned roots: *) +(* MC_gate_crash_before_meta and MC_gate_crash_devcontainer hold. A crash *) +(* before the child starts leaves a markerless directory that keeps *) +(* refusing (safe over-refusal). Remote roots stay unscanned (#4889). *) +(* MetalessTrusted is the mutant that skips meta-less directories. *) (***************************************************************************) EXTENDS Naturals @@ -25,7 +39,12 @@ CONSTANTS Runtime, \* "local" | "devcontainer" | "ssh" | "docker" Kind, \* "spawn" | "migrated" TmpdirIsTmp, \* os.tmpdir() = /tmp (Linux without TMPDIR); FALSE on macOS (/var/folders/...) - NoRecordScan \* mutant: the gate skips the record scan + NoRecordScan, \* mutant: the gate skips the record scan + Crash, \* case 3: A's backend can die after its turn-lease hold, before AEnd + MetalessTrusted \* mutant: the scan skips record directories without meta.json + +\* The step order below is the spawn's; a migrated command runs before its directory exists. +ASSUME Crash => Kind = "spawn" Root == IF Kind = "migrated" THEN (IF TmpdirIsTmp THEN "tmp" ELSE "ostmp") ELSE CASE Runtime = "local" -> "tmp" @@ -34,46 +53,61 @@ Root == IF Kind = "migrated" THEN (IF TmpdirIsTmp THEN "tmp" ELSE "ostmp") Scanned == {"tmp"} \cup (IF Runtime = "devcontainer" THEN {"bind"} ELSE {}) VARIABLES - apc, lease, record, alive, \* A: turn lease, P's record exists, P runs - bpc, gate, committed \* B's structural mutation + apc, lease, dir, record, alive, marker, \* A: turn lease, P's record directory, its meta.json, + \* P runs, P's exit_code marker + bpc, gate, committed \* B's structural mutation + +vars == <> -vars == <> +Init == /\ apc = "idle" /\ lease = FALSE /\ dir = FALSE /\ record = FALSE /\ alive = FALSE + /\ marker = FALSE /\ bpc = "idle" /\ gate = FALSE /\ committed = FALSE -Init == /\ apc = "idle" /\ lease = FALSE /\ record = FALSE /\ alive = FALSE - /\ bpc = "idle" /\ gate = FALSE /\ committed = FALSE +\* recordRootHoldsOrphan on one record: an exit marker settles it; meta.json says running and +\* the PID is live; no meta.json fails closed (unless the mutant trusts it). +Evidence == /\ Root \in Scanned /\ dir /\ ~marker + /\ IF record THEN alive ELSE ~MetalessTrusted \* --- A: a turn that starts P, then ends; P keeps running --- AHold == /\ apc = "idle" \* turn lease hold probes the gate /\ IF gate THEN apc' = "refused" /\ UNCHANGED lease ELSE apc' = "spawn" /\ lease' = TRUE - /\ UNCHANGED <> -ASpawn == /\ apc = "spawn" /\ record' = TRUE /\ alive' = TRUE /\ apc' = "end" - /\ UNCHANGED <> + /\ UNCHANGED <> +ADir == /\ apc = "spawn" /\ dir' = TRUE /\ apc' = "child" \* output dir, no exit_code + /\ UNCHANGED <> +AChild == /\ apc = "child" /\ alive' = TRUE /\ apc' = "meta" \* the detached child starts + /\ UNCHANGED <> +AMeta == /\ apc = "meta" /\ record' = TRUE /\ apc' = "end" \* writeMeta + /\ UNCHANGED <> AEnd == /\ apc = "end" /\ lease' = FALSE /\ apc' = "done" - /\ UNCHANGED <> -PExit == /\ alive /\ alive' = FALSE \* the trap writes exit_code - /\ UNCHANGED <> + /\ UNCHANGED <> +\* Case 3: A's backend dies; its lease goes stale, P (if started) survives under nohup/setsid. +ACrash == /\ Crash /\ apc \in {"spawn", "child", "meta", "end"} + /\ apc' = "crashed" /\ lease' = FALSE + /\ UNCHANGED <> +PExit == /\ alive /\ alive' = FALSE /\ marker' = TRUE \* the trap writes exit_code + /\ UNCHANGED <> \* --- B: the mutation gate, then the mutation --- BGate == /\ bpc = "idle" /\ gate' = TRUE /\ bpc' = "leases" - /\ UNCHANGED <> + /\ UNCHANGED <> BLeases == /\ bpc = "leases" /\ bpc' = IF lease THEN "refused" ELSE "records" /\ gate' = IF lease THEN FALSE ELSE gate - /\ UNCHANGED <> + /\ UNCHANGED <> BRecords == /\ bpc = "records" - /\ IF ~NoRecordScan /\ record /\ alive /\ Root \in Scanned + /\ IF ~NoRecordScan /\ Evidence THEN bpc' = "refused" /\ gate' = FALSE ELSE bpc' = "commit" /\ UNCHANGED gate - /\ UNCHANGED <> + /\ UNCHANGED <> BCommit == /\ bpc = "commit" /\ committed' = TRUE /\ bpc' = "done" - /\ UNCHANGED <> + /\ UNCHANGED <> -Next == AHold \/ ASpawn \/ AEnd \/ PExit \/ BGate \/ BLeases \/ BRecords \/ BCommit +Next == AHold \/ ADir \/ AChild \/ AMeta \/ AEnd \/ ACrash \/ PExit + \/ BGate \/ BLeases \/ BRecords \/ BCommit Spec == Init /\ [][Next]_vars \* B never commits its mutation while A's background process in W runs. NoMutationUnderForeignProcess == committed => ~alive -TypeOK == apc \in {"idle", "spawn", "end", "done", "refused"} +TypeOK == apc \in {"idle", "spawn", "child", "meta", "end", "done", "refused", "crashed"} ============================================================================= diff --git a/formal/background-processes/MC_cleanup_archive.cfg b/formal/background-processes/MC_cleanup_archive.cfg index 860328ece71..f48c8777beb 100644 --- a/formal/background-processes/MC_cleanup_archive.cfg +++ b/formal/background-processes/MC_cleanup_archive.cfg @@ -7,4 +7,6 @@ CONSTANTS SpawnSealed = FALSE ArchiveCleans = FALSE NoDrain = FALSE + JoinTimeout = FALSE + ExecTimeout = 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 011576e42a3..dd12a44825f 100644 --- a/formal/background-processes/MC_cleanup_archive_fixed.cfg +++ b/formal/background-processes/MC_cleanup_archive_fixed.cfg @@ -7,4 +7,6 @@ CONSTANTS SpawnSealed = TRUE ArchiveCleans = TRUE NoDrain = FALSE + JoinTimeout = FALSE + ExecTimeout = FALSE INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned diff --git a/formal/background-processes/MC_cleanup_fixed.cfg b/formal/background-processes/MC_cleanup_fixed.cfg index 48234f704af..e4f2b3fe84c 100644 --- a/formal/background-processes/MC_cleanup_fixed.cfg +++ b/formal/background-processes/MC_cleanup_fixed.cfg @@ -7,4 +7,6 @@ CONSTANTS SpawnSealed = TRUE ArchiveCleans = FALSE NoDrain = FALSE + JoinTimeout = FALSE + ExecTimeout = 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 cf49f176e36..7f1b04d246a 100644 --- a/formal/background-processes/MC_cleanup_migration_remove.cfg +++ b/formal/background-processes/MC_cleanup_migration_remove.cfg @@ -7,4 +7,6 @@ CONSTANTS SpawnSealed = FALSE ArchiveCleans = FALSE NoDrain = FALSE + JoinTimeout = FALSE + ExecTimeout = 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 new file mode 100644 index 00000000000..8f710081bb6 --- /dev/null +++ b/formal/background-processes/MC_cleanup_migration_timeout.cfg @@ -0,0 +1,12 @@ +\* #5465 case 2: the foreground exec's timeout kills a migrated command. Expect all to hold. +SPECIFICATION Spec +CONSTANTS + HasSpawn = FALSE + HasMigration = TRUE + Mutator = "remove" + SpawnSealed = FALSE + ArchiveCleans = FALSE + NoDrain = FALSE + JoinTimeout = FALSE + ExecTimeout = TRUE +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 new file mode 100644 index 00000000000..01814abd163 --- /dev/null +++ b/formal/background-processes/MC_cleanup_refused_join_timeout.cfg @@ -0,0 +1,12 @@ +\* #5465 case 1: removal refuses a migration whose killed command outlives the 5 s join. +SPECIFICATION Spec +CONSTANTS + HasSpawn = FALSE + HasMigration = TRUE + Mutator = "remove" + SpawnSealed = FALSE + ArchiveCleans = FALSE + NoDrain = FALSE + JoinTimeout = TRUE + ExecTimeout = 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 168538bb5d0..184710b14cf 100644 --- a/formal/background-processes/MC_cleanup_spawn_remove.cfg +++ b/formal/background-processes/MC_cleanup_spawn_remove.cfg @@ -7,4 +7,6 @@ CONSTANTS SpawnSealed = FALSE ArchiveCleans = FALSE NoDrain = FALSE + JoinTimeout = FALSE + ExecTimeout = FALSE INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned diff --git a/formal/background-processes/MC_gate_crash_before_meta.cfg b/formal/background-processes/MC_gate_crash_before_meta.cfg new file mode 100644 index 00000000000..cc0ab4dcae6 --- /dev/null +++ b/formal/background-processes/MC_gate_crash_before_meta.cfg @@ -0,0 +1,10 @@ +\* #5465 case 3: A's backend dies between the local spawn and writeMeta. Expect all to hold. +SPECIFICATION Spec +CONSTANTS + Runtime = "local" + Kind = "spawn" + TmpdirIsTmp = TRUE + NoRecordScan = FALSE + Crash = TRUE + MetalessTrusted = FALSE +INVARIANTS TypeOK NoMutationUnderForeignProcess diff --git a/formal/background-processes/MC_gate_crash_devcontainer.cfg b/formal/background-processes/MC_gate_crash_devcontainer.cfg new file mode 100644 index 00000000000..c41ec875273 --- /dev/null +++ b/formal/background-processes/MC_gate_crash_devcontainer.cfg @@ -0,0 +1,10 @@ +\* #5465 case 3 on the devcontainer bind-mount root. Expect all to hold. +SPECIFICATION Spec +CONSTANTS + Runtime = "devcontainer" + Kind = "spawn" + TmpdirIsTmp = TRUE + NoRecordScan = FALSE + Crash = TRUE + MetalessTrusted = FALSE +INVARIANTS TypeOK NoMutationUnderForeignProcess diff --git a/formal/background-processes/MC_gate_devcontainer_spawn.cfg b/formal/background-processes/MC_gate_devcontainer_spawn.cfg index 5aadeb1a7fd..a66dba81fa1 100644 --- a/formal/background-processes/MC_gate_devcontainer_spawn.cfg +++ b/formal/background-processes/MC_gate_devcontainer_spawn.cfg @@ -5,4 +5,6 @@ CONSTANTS Kind = "spawn" TmpdirIsTmp = TRUE NoRecordScan = FALSE + Crash = FALSE + MetalessTrusted = FALSE INVARIANTS TypeOK NoMutationUnderForeignProcess diff --git a/formal/background-processes/MC_gate_docker_spawn.cfg b/formal/background-processes/MC_gate_docker_spawn.cfg index 6fcccda6299..d3b1e09150a 100644 --- a/formal/background-processes/MC_gate_docker_spawn.cfg +++ b/formal/background-processes/MC_gate_docker_spawn.cfg @@ -5,4 +5,6 @@ CONSTANTS Kind = "spawn" TmpdirIsTmp = TRUE NoRecordScan = FALSE + Crash = FALSE + MetalessTrusted = FALSE INVARIANTS TypeOK NoMutationUnderForeignProcess diff --git a/formal/background-processes/MC_gate_local_spawn.cfg b/formal/background-processes/MC_gate_local_spawn.cfg index 1edf410a1a5..aefa4581c70 100644 --- a/formal/background-processes/MC_gate_local_spawn.cfg +++ b/formal/background-processes/MC_gate_local_spawn.cfg @@ -5,4 +5,6 @@ CONSTANTS Kind = "spawn" TmpdirIsTmp = TRUE NoRecordScan = FALSE + Crash = FALSE + MetalessTrusted = FALSE INVARIANTS TypeOK NoMutationUnderForeignProcess diff --git a/formal/background-processes/MC_gate_migrated_ostmp.cfg b/formal/background-processes/MC_gate_migrated_ostmp.cfg index 9775bb7b633..07969e6c884 100644 --- a/formal/background-processes/MC_gate_migrated_ostmp.cfg +++ b/formal/background-processes/MC_gate_migrated_ostmp.cfg @@ -5,4 +5,6 @@ CONSTANTS Kind = "migrated" TmpdirIsTmp = FALSE NoRecordScan = FALSE + Crash = FALSE + MetalessTrusted = FALSE INVARIANTS TypeOK NoMutationUnderForeignProcess diff --git a/formal/background-processes/MC_gate_migrated_tmp.cfg b/formal/background-processes/MC_gate_migrated_tmp.cfg index 855b9124d85..8eaa5af6546 100644 --- a/formal/background-processes/MC_gate_migrated_tmp.cfg +++ b/formal/background-processes/MC_gate_migrated_tmp.cfg @@ -5,4 +5,6 @@ CONSTANTS Kind = "migrated" TmpdirIsTmp = TRUE NoRecordScan = FALSE + Crash = FALSE + MetalessTrusted = FALSE INVARIANTS TypeOK NoMutationUnderForeignProcess diff --git a/formal/background-processes/MC_gate_ssh_spawn.cfg b/formal/background-processes/MC_gate_ssh_spawn.cfg index 647245e6c79..7dd430e691e 100644 --- a/formal/background-processes/MC_gate_ssh_spawn.cfg +++ b/formal/background-processes/MC_gate_ssh_spawn.cfg @@ -5,4 +5,6 @@ CONSTANTS Kind = "spawn" TmpdirIsTmp = TRUE NoRecordScan = FALSE + Crash = FALSE + MetalessTrusted = FALSE INVARIANTS TypeOK NoMutationUnderForeignProcess diff --git a/formal/background-processes/MC_mut_cleanup_nodrain.cfg b/formal/background-processes/MC_mut_cleanup_nodrain.cfg index 76ca347ff39..d7a4c2f645e 100644 --- a/formal/background-processes/MC_mut_cleanup_nodrain.cfg +++ b/formal/background-processes/MC_mut_cleanup_nodrain.cfg @@ -7,4 +7,6 @@ CONSTANTS SpawnSealed = FALSE ArchiveCleans = FALSE NoDrain = TRUE + JoinTimeout = FALSE + ExecTimeout = FALSE INVARIANTS TypeOK NoLiveAfterDelete FgBgExclusive MigrationOwned diff --git a/formal/background-processes/MC_mut_gate_metaless_trusted.cfg b/formal/background-processes/MC_mut_gate_metaless_trusted.cfg new file mode 100644 index 00000000000..c7a87b73649 --- /dev/null +++ b/formal/background-processes/MC_mut_gate_metaless_trusted.cfg @@ -0,0 +1,10 @@ +\* Mutant: the scan skips record directories without meta.json (crash before writeMeta). +SPECIFICATION Spec +CONSTANTS + Runtime = "local" + Kind = "spawn" + TmpdirIsTmp = TRUE + NoRecordScan = FALSE + Crash = TRUE + MetalessTrusted = TRUE +INVARIANTS TypeOK NoMutationUnderForeignProcess diff --git a/formal/background-processes/MC_mut_gate_norecords.cfg b/formal/background-processes/MC_mut_gate_norecords.cfg index 1eebc3b6b5e..3c91acbe474 100644 --- a/formal/background-processes/MC_mut_gate_norecords.cfg +++ b/formal/background-processes/MC_mut_gate_norecords.cfg @@ -5,4 +5,6 @@ CONSTANTS Kind = "spawn" TmpdirIsTmp = TRUE NoRecordScan = TRUE + Crash = FALSE + MetalessTrusted = FALSE INVARIANTS TypeOK NoMutationUnderForeignProcess diff --git a/formal/background-processes/check.sh b/formal/background-processes/check.sh index aeba72f6df5..d6d3a95cb69 100755 --- a/formal/background-processes/check.sh +++ b/formal/background-processes/check.sh @@ -54,6 +54,10 @@ 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" + # #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 # MC_name_remote_fixed (atomic mkdir claim) holds. [MC_name_host]="" @@ -73,6 +77,11 @@ declare -A EXPECT=( [MC_gate_migrated_tmp]="" [MC_gate_migrated_ostmp]="NoMutationUnderForeignProcess" [MC_mut_gate_norecords]="NoMutationUnderForeignProcess" + # #5465 case 3: a crash between spawn and writeMeta leaves a meta-less record, which the scan + # reads as live (fails closed); the mutant that trusts such records is caught. + [MC_gate_crash_before_meta]="" + [MC_gate_crash_devcontainer]="" + [MC_mut_gate_metaless_trusted]="NoMutationUnderForeignProcess" ) module_of() { diff --git a/src/node/services/backgroundProcessesFormalRepro.test.ts b/src/node/services/backgroundProcessesFormalRepro.test.ts index c88f68b4337..4829fb374ff 100644 --- a/src/node/services/backgroundProcessesFormalRepro.test.ts +++ b/src/node/services/backgroundProcessesFormalRepro.test.ts @@ -404,3 +404,95 @@ describe("#4889: same-name spawns from two backends on a non-host runtime", () = expect(second.outputDir === first.outputDir).toBe(false); }, 20_000); }); + +// --------------------------------------------------------------------------------------------- +// #5465 case 1 (BgCleanup.tla, MC_cleanup_refused_join_timeout): a migration refused by a +// cleanup's seal (or one that fails) unregisters the foreground entry, aborts the command and +// waits at most 5 s for its exit. A command whose exit that join does not see keeps running with +// 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. + +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. */ + async function refuseMigration(tag: string, holdKill: boolean) { + const ws = uniqueWorkspace(tag); + const manager = new BackgroundProcessManager(path.dirname(localBgWorkspaceDir(ws))); + cleanups.push(() => manager.cleanup(ws)); + const dir = await tempDir(tag); + const pidFile = path.join(dir, "pid"); + const releaseKill = Promise.withResolvers(); + /** Delivers the tool's abort to the command only once the test releases it. */ + class HeldKillRuntime extends LocalRuntime { + override exec(command: string, options: Parameters[1]) { + const delayed = new AbortController(); + options.abortSignal?.addEventListener( + "abort", + () => void releaseKill.promise.then(() => delayed.abort()), + { once: true } + ); + return super.exec(command, { ...options, abortSignal: delayed.signal }); + } + } + const runtime = holdKill ? new HeldKillRuntime(process.cwd()) : new LocalRuntime(process.cwd()); + let pid = 0; + cleanups.push(() => { + releaseKill.resolve(); + try { + if (pid > 0) process.kill(-pid, "SIGKILL"); + } catch { + // Already gone. + } + return Promise.resolve(); + }); + const config = createTestToolConfig(process.cwd(), { workspaceId: ws, runtime }); + config.runtimeTempDir = dir; + config.backgroundProcessManager = manager; + const running = createBashTool(config).execute!( + { + script: `echo $$ > "${pidFile}"; sleep 30`, + timeout_secs: 60, + run_in_background: false, + display_name: "dev", + }, + mockToolCallOptions + ) as Promise; + await waitFor(() => exists(pidFile), "the foreground command"); + pid = Number((await fs.readFile(pidFile, "utf-8")).trim()); + expect(pid).toBeGreaterThan(1); + // The seal a removal or archive holds (workspaceService.ts) while its cleanup() runs. + using _seal = manager.sealAdmissions(ws); + expect(manager.sendToBackground(mockToolCallOptions.toolCallId).success).toBe(true); + const result = await running; + expect(result.success).toBe(false); + expect(!result.success && result.error).toContain("could not be tracked"); + return { manager, ws, pid }; + } + + test("control: a refused migration's command is stopped once its kill takes effect", async () => { + const { manager, ws, pid } = await refuseMigration("join-ctl", false); + expect(await manager.list(ws)).toEqual([]); + 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. + expect(early).toBe("waiting"); + }, + { matcher: "toBe", expected: '"waiting"', received: '"finished"' } + ); + }, 20_000); +}); From ca6c233b29fe74ff64c2b63fcdc5f428c804b34f Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Sat, 3 Oct 2026 19:54:24 +0000 Subject: [PATCH 2/3] =?UTF-8?q?=F0=9F=A4=96=20tests:=20model=20failed=20mi?= =?UTF-8?q?grations=20(case=201)=20and=20track=20the=20case-3=20liveness?= =?UTF-8?q?=20gap=20(#5576)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- formal/background-processes/BgCleanup.tla | 7 +++- .../background-processes/BgGateEvidence.tla | 4 +- .../backgroundProcessesFormalRepro.test.ts | 40 +++++++++++++++++-- 3 files changed, 46 insertions(+), 5 deletions(-) diff --git a/formal/background-processes/BgCleanup.tla b/formal/background-processes/BgCleanup.tla index 608fded0752..291fe01139f 100644 --- a/formal/background-processes/BgCleanup.tla +++ b/formal/background-processes/BgCleanup.tla @@ -115,6 +115,11 @@ MExitCheck == /\ mpc = "exitcheck" \* :1444-1468 MMigrate == /\ mpc = "migrate" /\ bg' = TRUE /\ mpc' = "end" \* :1507-1523 /\ UNCHANGED <> +\* An admitted migration fails before it registers: migrateToBackground cannot create the record +\* (:1518-1557, e.g. ENOSPC/EACCES). It takes the refused path's abort and join (:1569-1580). +MMigrateFail == /\ mpc = "migrate" /\ mpc' = "join" + /\ UNCHANGED <> \* Refused: unregister the foreground entry (:1479) and abort the command (:1569). MRefused == /\ mpc = "refused" /\ fg' = FALSE /\ mpc' = "join" /\ UNCHANGED <> Next == SStart \/ SChild \/ SRegister \/ SExit - \/ MBegin \/ MClaim \/ MExitCheck \/ MMigrate \/ MRefused \/ MJoin \/ MJoinTimeout \/ MEnd + \/ MBegin \/ MClaim \/ MExitCheck \/ MMigrate \/ MMigrateFail \/ MRefused \/ MJoin \/ MJoinTimeout \/ MEnd \/ FExit \/ FTimeout \/ RStart \/ RStop \/ CSeal \/ CDrain1 \/ CSnap \/ CTerm \/ CDrain2 \/ RDelete diff --git a/formal/background-processes/BgGateEvidence.tla b/formal/background-processes/BgGateEvidence.tla index 6cfd218a64e..e4552d05ffc 100644 --- a/formal/background-processes/BgGateEvidence.tla +++ b/formal/background-processes/BgGateEvidence.tla @@ -30,7 +30,9 @@ (* marker when P exits. Benign on the scanned roots: *) (* MC_gate_crash_before_meta and MC_gate_crash_devcontainer hold. A crash *) (* before the child starts leaves a markerless directory that keeps *) -(* refusing (safe over-refusal). Remote roots stay unscanned (#4889). *) +(* refusing every structural mutation, user removal included: safe, but *) +(* a liveness gap these safety-only configs do not check (#5576). *) +(* Remote roots stay unscanned (#4889). *) (* MetalessTrusted is the mutant that skips meta-less directories. *) (***************************************************************************) EXTENDS Naturals diff --git a/src/node/services/backgroundProcessesFormalRepro.test.ts b/src/node/services/backgroundProcessesFormalRepro.test.ts index 4829fb374ff..b265d91f38f 100644 --- a/src/node/services/backgroundProcessesFormalRepro.test.ts +++ b/src/node/services/backgroundProcessesFormalRepro.test.ts @@ -11,6 +11,7 @@ import type { Runtime } from "@/node/runtime/Runtime"; import * as runtimeFactory from "@/node/runtime/runtimeFactory"; import { acquireProcessFileLock } from "@/node/utils/concurrency/fileLock"; import { expectReproFailure } from "@/node/utils/formalRepro.testHarness"; +import * as backgroundProcessExecutor from "./backgroundProcessExecutor"; import { localBgWorkspaceDir } from "./backgroundProcessExecutor"; import { BackgroundProcessManager, SPAWN_NAME_LOCK_FILENAME } from "./backgroundProcessManager"; import { BackgroundProcessManagerLive } from "./di/layers/core"; @@ -415,8 +416,11 @@ describe("#4889: same-name spawns from two backends on a non-host runtime", () = // close is late). Follow-up fix: #5522. 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. */ - async function refuseMigration(tag: string, holdKill: boolean) { + /** + * 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) { const ws = uniqueWorkspace(tag); const manager = new BackgroundProcessManager(path.dirname(localBgWorkspaceDir(ws))); cleanups.push(() => manager.cleanup(ws)); @@ -462,11 +466,21 @@ describe("#5465 case 1: a refused migration whose command outlives the kill join pid = Number((await fs.readFile(pidFile, "utf-8")).trim()); expect(pid).toBeGreaterThan(1); // The seal a removal or archive holds (workspaceService.ts) while its cleanup() runs. - using _seal = manager.sealAdmissions(ws); + using _seal = failMigration ? undefined : manager.sealAdmissions(ws); + if (failMigration) { + spyOn(backgroundProcessExecutor, "migrateToBackground").mockResolvedValue({ + success: false, + error: "ENOSPC: no space left on device", + }); + } expect(manager.sendToBackground(mockToolCallOptions.toolCallId).success).toBe(true); const result = await running; expect(result.success).toBe(false); expect(!result.success && result.error).toContain("could not be tracked"); + // The path taken: the seal's refusal, or the record that could not be created. + expect(!result.success && result.error).toContain( + failMigration ? "ENOSPC" : "being cleaned up" + ); return { manager, ws, pid }; } @@ -495,4 +509,24 @@ describe("#5465 case 1: a refused migration whose command outlives the kill join { matcher: "toBe", expected: '"waiting"', received: '"finished"' } ); }, 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. + expect(early).toBe("waiting"); + }, + { matcher: "toBe", expected: '"waiting"', received: '"finished"' } + ); + }, 20_000); }); From 6aabf6b57dd864f424279286dc1aa9c24ff23a60 Mon Sep 17 00:00:00 2001 From: Thomas Kosiewski Date: Sat, 3 Oct 2026 20:06:33 +0000 Subject: [PATCH 3/3] =?UTF-8?q?=F0=9F=A4=96=20tests:=20force=20the=20faile?= =?UTF-8?q?d-migration=20path=20in=20its=20own=20config;=20a=20fail-closed?= =?UTF-8?q?=20cleanup=20is=20safe?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- formal/background-processes/BgCleanup.tla | 8 ++++++-- formal/background-processes/MC_cleanup_archive.cfg | 1 + .../MC_cleanup_archive_fixed.cfg | 1 + .../MC_cleanup_failed_join_timeout.cfg | 13 +++++++++++++ formal/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_nodrain.cfg | 1 + formal/background-processes/check.sh | 1 + .../backgroundProcessesFormalRepro.test.ts | 14 ++++++++------ 12 files changed, 36 insertions(+), 8 deletions(-) create mode 100644 formal/background-processes/MC_cleanup_failed_join_timeout.cfg diff --git a/formal/background-processes/BgCleanup.tla b/formal/background-processes/BgCleanup.tla index 291fe01139f..16ff19b5026 100644 --- a/formal/background-processes/BgCleanup.tla +++ b/formal/background-processes/BgCleanup.tla @@ -35,6 +35,8 @@ (* 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. *) (* 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 *) @@ -54,7 +56,8 @@ 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 - ExecTimeout \* case 2: the foreground exec's own timeout can kill F after the migration + 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 VARIABLES \* spawn @@ -100,6 +103,7 @@ SExit == /\ sLive /\ sLive' = FALSE \* the command --------------------------------------------------------------------------- (* Migration of foreground command F (bash.ts). *) MBegin == /\ mpc = "fg" \* :1426 beginMigration + /\ (MigrationFails => ~Sealed) \* forced failure: admitted only /\ mAdmitted' = ~Sealed /\ mPending' = mPending + 1 /\ mpc' = IF ~Sealed THEN "claim" ELSE "refused" /\ UNCHANGED <> @@ -112,7 +116,7 @@ MExitCheck == /\ mpc = "exitcheck" \* :1444-1468 ELSE mpc' = "migrate" /\ fg' = FALSE \* unregister(): in neither map now /\ UNCHANGED <> -MMigrate == /\ mpc = "migrate" /\ bg' = TRUE /\ mpc' = "end" \* :1507-1523 +MMigrate == /\ mpc = "migrate" /\ ~MigrationFails /\ bg' = TRUE /\ mpc' = "end" \* :1507-1523 /\ UNCHANGED <> \* An admitted migration fails before it registers: migrateToBackground cannot create the record diff --git a/formal/background-processes/MC_cleanup_archive.cfg b/formal/background-processes/MC_cleanup_archive.cfg index f48c8777beb..6f60bc23e94 100644 --- a/formal/background-processes/MC_cleanup_archive.cfg +++ b/formal/background-processes/MC_cleanup_archive.cfg @@ -9,4 +9,5 @@ CONSTANTS NoDrain = FALSE JoinTimeout = 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 dd12a44825f..68cbba65a03 100644 --- a/formal/background-processes/MC_cleanup_archive_fixed.cfg +++ b/formal/background-processes/MC_cleanup_archive_fixed.cfg @@ -9,4 +9,5 @@ CONSTANTS NoDrain = FALSE JoinTimeout = 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 new file mode 100644 index 00000000000..d0b3154bf56 --- /dev/null +++ b/formal/background-processes/MC_cleanup_failed_join_timeout.cfg @@ -0,0 +1,13 @@ +\* #5465 case 1, forced failure: an admitted migration fails, and its killed command outlives the 5 s join. +SPECIFICATION Spec +CONSTANTS + HasSpawn = FALSE + HasMigration = TRUE + Mutator = "remove" + SpawnSealed = FALSE + ArchiveCleans = FALSE + NoDrain = FALSE + JoinTimeout = TRUE + 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 e4f2b3fe84c..5c18884ea0e 100644 --- a/formal/background-processes/MC_cleanup_fixed.cfg +++ b/formal/background-processes/MC_cleanup_fixed.cfg @@ -9,4 +9,5 @@ CONSTANTS NoDrain = FALSE JoinTimeout = 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 7f1b04d246a..05fa17024d3 100644 --- a/formal/background-processes/MC_cleanup_migration_remove.cfg +++ b/formal/background-processes/MC_cleanup_migration_remove.cfg @@ -9,4 +9,5 @@ CONSTANTS NoDrain = FALSE JoinTimeout = 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 8f710081bb6..189b49ef392 100644 --- a/formal/background-processes/MC_cleanup_migration_timeout.cfg +++ b/formal/background-processes/MC_cleanup_migration_timeout.cfg @@ -9,4 +9,5 @@ CONSTANTS NoDrain = FALSE JoinTimeout = 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 01814abd163..1e24221bb43 100644 --- a/formal/background-processes/MC_cleanup_refused_join_timeout.cfg +++ b/formal/background-processes/MC_cleanup_refused_join_timeout.cfg @@ -9,4 +9,5 @@ CONSTANTS NoDrain = FALSE JoinTimeout = TRUE 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 184710b14cf..8eb884ba3d1 100644 --- a/formal/background-processes/MC_cleanup_spawn_remove.cfg +++ b/formal/background-processes/MC_cleanup_spawn_remove.cfg @@ -9,4 +9,5 @@ CONSTANTS NoDrain = FALSE JoinTimeout = FALSE 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 d7a4c2f645e..db83d270dfa 100644 --- a/formal/background-processes/MC_mut_cleanup_nodrain.cfg +++ b/formal/background-processes/MC_mut_cleanup_nodrain.cfg @@ -9,4 +9,5 @@ CONSTANTS NoDrain = TRUE JoinTimeout = 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 d6d3a95cb69..23dc60668e9 100755 --- a/formal/background-processes/check.sh +++ b/formal/background-processes/check.sh @@ -56,6 +56,7 @@ declare -A EXPECT=( [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 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 b265d91f38f..4545ae0b278 100644 --- a/src/node/services/backgroundProcessesFormalRepro.test.ts +++ b/src/node/services/backgroundProcessesFormalRepro.test.ts @@ -503,10 +503,11 @@ describe("#5465 case 1: a refused migration whose command outlives the kill join () => "failed closed" ); const early = await Promise.race([cleanup, Bun.sleep(500).then(() => "waiting")]); - // Target assertion: the cleanup has not finished under the running command. - expect(early).toBe("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: '"waiting"', received: '"finished"' } + { matcher: "toBe", expected: "false", received: "true" } ); }, 20_000); @@ -523,10 +524,11 @@ describe("#5465 case 1: a refused migration whose command outlives the kill join () => "failed closed" ); const early = await Promise.race([cleanup, Bun.sleep(500).then(() => "waiting")]); - // Target assertion: the cleanup has not finished under the running command. - expect(early).toBe("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: '"waiting"', received: '"finished"' } + { matcher: "toBe", expected: "false", received: "true" } ); }, 20_000); });