diff --git a/formal/background-processes/BgCleanup.tla b/formal/background-processes/BgCleanup.tla index 2a4991feda2..16ff19b5026 100644 --- a/formal/background-processes/BgCleanup.tla +++ b/formal/background-processes/BgCleanup.tla @@ -26,6 +26,25 @@ (* 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). *) +(* 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 *) +(* 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 +54,10 @@ 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 + MigrationFails \* case 1, forced: the migration is admitted, then migrateToBackground fails VARIABLES \* spawn @@ -81,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 <> @@ -93,13 +116,26 @@ 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 <> -MRefused == /\ mpc = "refused" /\ fLive' = FALSE /\ mpc' = "end" \* :1558-1567 abort + join - /\ 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 <> +\* :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 +199,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 \/ MMigrateFail \/ MRefused \/ MJoin \/ MJoinTimeout \/ MEnd + \/ FExit \/ FTimeout \/ RStart \/ RStop \/ CSeal \/ CDrain1 \/ CSnap \/ CTerm \/ CDrain2 \/ RDelete Spec == Init /\ [][Next]_vars @@ -167,7 +210,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..e4552d05ffc 100644 --- a/formal/background-processes/BgGateEvidence.tla +++ b/formal/background-processes/BgGateEvidence.tla @@ -18,6 +18,22 @@ (* (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 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 @@ -25,7 +41,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 +55,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..6f60bc23e94 100644 --- a/formal/background-processes/MC_cleanup_archive.cfg +++ b/formal/background-processes/MC_cleanup_archive.cfg @@ -7,4 +7,7 @@ CONSTANTS SpawnSealed = FALSE ArchiveCleans = FALSE 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 011576e42a3..68cbba65a03 100644 --- a/formal/background-processes/MC_cleanup_archive_fixed.cfg +++ b/formal/background-processes/MC_cleanup_archive_fixed.cfg @@ -7,4 +7,7 @@ CONSTANTS SpawnSealed = TRUE ArchiveCleans = TRUE 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 48234f704af..5c18884ea0e 100644 --- a/formal/background-processes/MC_cleanup_fixed.cfg +++ b/formal/background-processes/MC_cleanup_fixed.cfg @@ -7,4 +7,7 @@ CONSTANTS SpawnSealed = TRUE ArchiveCleans = FALSE 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 cf49f176e36..05fa17024d3 100644 --- a/formal/background-processes/MC_cleanup_migration_remove.cfg +++ b/formal/background-processes/MC_cleanup_migration_remove.cfg @@ -7,4 +7,7 @@ CONSTANTS SpawnSealed = FALSE ArchiveCleans = FALSE 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 new file mode 100644 index 00000000000..189b49ef392 --- /dev/null +++ b/formal/background-processes/MC_cleanup_migration_timeout.cfg @@ -0,0 +1,13 @@ +\* #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 + 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 new file mode 100644 index 00000000000..1e24221bb43 --- /dev/null +++ b/formal/background-processes/MC_cleanup_refused_join_timeout.cfg @@ -0,0 +1,13 @@ +\* #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 + 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 168538bb5d0..8eb884ba3d1 100644 --- a/formal/background-processes/MC_cleanup_spawn_remove.cfg +++ b/formal/background-processes/MC_cleanup_spawn_remove.cfg @@ -7,4 +7,7 @@ CONSTANTS SpawnSealed = FALSE ArchiveCleans = FALSE NoDrain = FALSE + JoinTimeout = FALSE + ExecTimeout = FALSE + MigrationFails = 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..db83d270dfa 100644 --- a/formal/background-processes/MC_mut_cleanup_nodrain.cfg +++ b/formal/background-processes/MC_mut_cleanup_nodrain.cfg @@ -7,4 +7,7 @@ CONSTANTS SpawnSealed = FALSE ArchiveCleans = FALSE NoDrain = TRUE + JoinTimeout = FALSE + ExecTimeout = FALSE + MigrationFails = 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..23dc60668e9 100755 --- a/formal/background-processes/check.sh +++ b/formal/background-processes/check.sh @@ -54,6 +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 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 +78,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..4545ae0b278 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"; @@ -404,3 +405,130 @@ 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, 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)); + 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 = 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 }; + } + + 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 (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); +});