diff --git a/dag/gunbc/product/fabric/sanitation.dag b/dag/gunbc/product/fabric/sanitation.dag index 5d1c837075b..127795208bb 100644 --- a/dag/gunbc/product/fabric/sanitation.dag +++ b/dag/gunbc/product/fabric/sanitation.dag @@ -47,26 +47,49 @@ type SanitationFact | CgroupEmpty | MountsRemoved | NetworkNamespaceRemoved + | SlotNetworkQuiescent | WritableLayersDeleted | SecretsRemoved +// THE NETWORK FACT DEPENDS ON WHO OWNS THE NETWORK, AND THE TWO OWNERS OWE DIFFERENT FACTS. +// +// A sandbox whose network namespace is created per attempt owes its REMOVAL: a namespace that +// survives can hold the previous tenant's listening socket. A sandbox attached to network state the +// SLOT owns across attempts -- a microVM's tap and nft rules, converged per slot -- owes no removal, +// because that state exists by design between attempts. What it owes instead is QUIESCENCE: nothing +// holds the slot's interface, no connection-tracking state for the reused guest address survives, +// and the ruleset is the converged one. These are different contracts, so they are different facts +// rather than one name read two ways; and the scope is declared on the readback, so which one is +// required is decided here rather than by whichever consumer maps its observation onto a name. +type SandboxNetworkScope + = AttemptScopedNetwork + | SlotScopedNetwork + fn sanitation_fact_label(fact: SanitationFact) -> String { match fact { NoSurvivingProcesses => "no-surviving-processes" CgroupEmpty => "cgroup-empty" MountsRemoved => "mounts-removed" NetworkNamespaceRemoved => "network-namespace-removed" + SlotNetworkQuiescent => "slot-network-quiescent" WritableLayersDeleted => "writable-layers-deleted" SecretsRemoved => "secrets-removed" } } -fn required_sanitation_facts() -> List { +fn network_sanitation_fact(scope: SandboxNetworkScope) -> SanitationFact { + match scope { + AttemptScopedNetwork => NetworkNamespaceRemoved + SlotScopedNetwork => SlotNetworkQuiescent + } +} + +fn required_sanitation_facts(scope: SandboxNetworkScope) -> List { [ NoSurvivingProcesses, CgroupEmpty, MountsRemoved, - NetworkNamespaceRemoved, + network_sanitation_fact(scope: scope), WritableLayersDeleted, SecretsRemoved, ] @@ -105,6 +128,7 @@ fn observation_confirms(observation: SanitationObservation) -> Bool { type SanitationReadback { cell: CellId sandbox: SandboxId + network_scope: SandboxNetworkScope observations: List } @@ -153,7 +177,7 @@ fn unproven_for_required( } fn unproven_facts(readback: SanitationReadback) -> List { - fold(required_sanitation_facts(), init: [], f: (acc, required) => + fold(required_sanitation_facts(scope: readback.network_scope), init: [], f: (acc, required) => concat(acc, unproven_for_required(readback: readback, required: required))) } @@ -203,10 +227,11 @@ fn cell_readiness_line(readiness: CellReadiness) -> String { // a missing report as nothing-to-clean. That is the same narrow one level out: no observation // becomes no problem. An absent readback yields every required fact unobserved, so the cell // quarantines with a full list rather than returning to supply. -fn readiness_without_readback(cell: CellId, sandbox: SandboxId) -> CellReadiness { +fn readiness_without_readback(cell: CellId, sandbox: SandboxId, network_scope: SandboxNetworkScope) -> CellReadiness { cell_readiness_after(readback: SanitationReadback { cell: cell, sandbox: sandbox, + network_scope: network_scope, observations: [], }) } diff --git a/dag/gunbc/runner/runner_microvm.dag b/dag/gunbc/runner/runner_microvm.dag index 908643b51fc..fbe09e281de 100644 --- a/dag/gunbc/runner/runner_microvm.dag +++ b/dag/gunbc/runner/runner_microvm.dag @@ -46,6 +46,11 @@ import gunbc.runner_unit { lifecycle_intent_stops_finished_incarnation, gunbc_runner_main_exits_when_incarnation_ends, } +import product.fabric.sanitation { CellId } +import gunbc.runner_microvm_cell_readiness { + CellIncarnationAdmission, CellIncarnationAdmitted, CellRecoveryRequired, CellWithdrawn, + HostWithdrawn, HostWithdrawal, CellWithdrawal, CellBoundAttempt, +} import extdeps.github.actions_runner { ActionsRunnerRelease, actions_runner_release_2_337_0, actions_runner_jitconfig_env_name, } @@ -815,15 +820,22 @@ type VmmProcessTopology = VmmIsMainProcess | VmmUnderLifecycleController // re-deriving it. Stating the dependency in prose would have left it satisfiable by an author who // never read the paragraph. // -// THIS IS A NECESSARY GATE, NOT A SUFFICIENT ONE, and the gap is a declared frontier. The predicate -// is static: it says a finished incarnation makes systemd issue a stop that reaches the cgroup. It -// cannot say the VMM is gone afterwards -- a task in uninterruptible sleep survives SIGKILL, and a -// main process that outlives its incarnation issues no stop at all -- nor that the cell is safe to -// reuse. That is gunbc.product.fabric.sanitation's CellReadiness, established by a terminalizer's -// readback, which this admission will consume once the terminalizer lands. Until then an Admitted -// verdict here is not sufficient grounds to run customer work. +// THE TOPOLOGY GATE IS NECESSARY, NOT SUFFICIENT, and the cell's readiness is the other half. The +// predicate is static: it says a finished incarnation makes systemd issue a stop that reaches the +// cgroup. It cannot say the VMM is gone afterwards -- a task in uninterruptible sleep survives +// SIGKILL -- nor that the cell is safe to reuse. That is gunbc.product.fabric.sanitation's +// CellReadiness as held across incarnations by gunbc.runner_microvm_cell_readiness, whose admission +// joins the allocation generation to the readiness recorded at the previous one. It is consumed +// FIRST, before any static gate: a cell that is withdrawn is withdrawn whatever the VM looks like, +// and reporting a malformed VM for a quarantined cell would send the operator to the wrong fact. +// Its three non-admitting arms stay three arms here, because their remedies differ: host grain (fix +// the store; no cell on the host may start), cell grain (this cell's readback), and recovery required +// (not a refusal to act but the instruction to run the lost attempt's teardown first). type RunnerMicroVmAdmission = RunnerMicroVmAdmitted + | RunnerMicroVmRefusedHostWithdrawn { withdrawal: HostWithdrawal } + | RunnerMicroVmRefusedCellWithdrawn { cell: CellId, withdrawal: CellWithdrawal } + | RunnerMicroVmRecoveryRequired { bound: CellBoundAttempt } | RunnerMicroVmRefusedOrphanableUnit { reason: String } | RunnerMicroVmRefusedSharedCredential { reason: String } | RunnerMicroVmRefusedMalformedVm { reason: String } @@ -843,6 +855,31 @@ type RunnerMicroVmAdmission // instead of writing it. Collapsing them into one cause is the state-space conflation DESIGN names, // and it would send an operator to the wrong module. fn runner_microvm_admission( + cell: CellIncarnationAdmission, + topology: VmmProcessTopology, + intent: RunnerUnitLifecycleIntent, + main_exits_when_incarnation_ends: Bool, + transport: JitCredentialTransport, + config: FirecrackerVmConfig, + reserve: RealizationReserve, +) -> RunnerMicroVmAdmission { + match cell { + HostWithdrawn { withdrawal: w } => RunnerMicroVmRefusedHostWithdrawn { withdrawal: w } + CellWithdrawn { cell: c, withdrawal: w } => RunnerMicroVmRefusedCellWithdrawn { cell: c, withdrawal: w } + CellRecoveryRequired { bound: b } => RunnerMicroVmRecoveryRequired { bound: b } + CellIncarnationAdmitted { cell: _, generation: _ } => + runner_microvm_admission_after_cell( + topology: topology, + intent: intent, + main_exits_when_incarnation_ends: main_exits_when_incarnation_ends, + transport: transport, + config: config, + reserve: reserve, + ) + } +} + +fn runner_microvm_admission_after_cell( topology: VmmProcessTopology, intent: RunnerUnitLifecycleIntent, main_exits_when_incarnation_ends: Bool, @@ -1026,10 +1063,12 @@ fn attach_workspace_drive(config: FirecrackerVmConfig, path: FilePath) -> Firecr // gunbc_runner_lifecycle_intent rather than by an author's assertion. It moves the day that intent // is deployed, and not before. fn gunbc_runner_microvm_admission( + cell: CellIncarnationAdmission, topology: VmmProcessTopology, config: FirecrackerVmConfig, ) -> RunnerMicroVmAdmission { runner_microvm_admission( + cell: cell, topology: topology, intent: gunbc_runner_lifecycle_intent, main_exits_when_incarnation_ends: gunbc_runner_main_exits_when_incarnation_ends, diff --git a/dag/gunbc/runner/runner_microvm_attempt.dag b/dag/gunbc/runner/runner_microvm_attempt.dag index 86ef678b3ff..42d6543c931 100644 --- a/dag/gunbc/runner/runner_microvm_attempt.dag +++ b/dag/gunbc/runner/runner_microvm_attempt.dag @@ -32,7 +32,10 @@ data runner_microvm_attempt_disposition: Disposition = SingleAuthority // BOUNDARY the VMM runs in the cell's slice, so the guest's CPU, memory and task consumption is // accounted to the cell that was reserved -- a VM outside the slice is invisible to // every limit the cell carries and to every observation that reads them. -// LIFETIME the cell is not releasable until teardown is PROVEN, not attempted. +// LIFETIME the cell is not releasable until teardown is PROVEN, not attempted. That verdict is +// gunbc.product.fabric.sanitation's CellReadiness, derived from host readbacks by +// gunbc.runner_microvm_lifecycle and held across incarnations by +// gunbc.runner_microvm_cell_readiness; this module owns no second release verdict. // // A guest missing any one of these is refused rather than downgraded, because each failure is // silent in production: unbound storage looks like a working VM until two attempts collide, @@ -242,36 +245,3 @@ fn bind_owned_attempt(attempt: MicroVmAttempt, owned: Bool) -> MicroVmCellBindin } } } - -// TEARDOWN IS PROVEN, NOT ATTEMPTED, AND THE CELL IS NOT RELEASABLE WITHOUT THE PROOF. -// -// The arms are separate because they are different events with different remedies. A VMM that -// exited but left its attempt directory populated is a cleanup bug; a VMM still running is a -// LEAK, and releasing the cell under it would hand a reserved boundary to a second guest while the -// first still executes in it. There is deliberately no arm meaning "probably fine". -type MicroVmTeardownVerdict - = TeardownProven - | TeardownVmmStillRunning { unit: NonEmptyStr } - | TeardownResidueRemains { path: String } - | TeardownNotObserved { cause: String } - -fn microvm_cell_releasable(verdict: MicroVmTeardownVerdict) -> Bool { - match verdict { - TeardownProven => true - TeardownVmmStillRunning { unit: _ } => false - TeardownResidueRemains { path: _ } => false - TeardownNotObserved { cause: _ } => false - } -} - -fn microvm_teardown_verdict_text(v: MicroVmTeardownVerdict) -> String { - match v { - TeardownProven => "teardown=proven" - TeardownVmmStillRunning { unit: u } => - join(["teardown=REFUSED vmm still running (", u as String, "); releasing the cell would hand a live boundary to a second guest"], "") - TeardownResidueRemains { path: p } => - join(["teardown=REFUSED residue remains at ", p], "") - TeardownNotObserved { cause: c } => - join(["teardown=REFUSED not observed (", c, "); an unobserved teardown is not a completed one"], "") - } -} diff --git a/dag/gunbc/runner/runner_microvm_cell_readiness.dag b/dag/gunbc/runner/runner_microvm_cell_readiness.dag new file mode 100644 index 00000000000..5634c7e272c --- /dev/null +++ b/dag/gunbc/runner/runner_microvm_cell_readiness.dag @@ -0,0 +1,430 @@ +module gunbc.runner_microvm_cell_readiness + +import std.types { String, NonEmptyStr, Bool, List, Int, Map } +import std.disposition { Disposition, SingleAuthority } +import product.fabric.sanitation { + CellId, CellReadiness, CellReady, CellQuarantined, UnprovenFact, FactNotObserved, + required_sanitation_facts, SlotScopedNetwork, +} +import gunbc.build_cache_instance { runner_slot_instance_name } +import gunbc.runner_microvm_attempt { MicroVmAttempt, runner_microvm_attempt_unit_name } + +data runner_microvm_cell_readiness_disposition: Disposition = SingleAuthority + +// THE HOST-LOCAL RECORD OF WHETHER A CELL MAY RUN ITS NEXT INCARNATION. +// +// product.fabric.sanitation decides CellReadiness from ONE readback. This module holds what that +// verdict means ACROSS attempts, which is a different question with its own failure modes: a +// readback can arrive late, a controller can die between staging and readback, and the store the +// verdict lives in can itself be unreadable or writable by someone other than root. None of those +// may turn into admission, so each is a typed arm rather than a default. +// +// THE UNIT OF THE STORE IS (cell, generation). A generation is the allocation generation an +// incarnation ran as; the next incarnation runs as generation + 1 and is admitted only when the +// record for generation says CellReady. Keying on the cell alone is what would let a readback of +// attempt N clear the quarantine of attempt N + 1: the verdicts would be indistinguishable. +// +// A record is either IN FLIGHT or SETTLED, and the in-flight arm is the durable half of boot +// recovery. It is written before anything is staged, so a controller lost at any later point +// leaves a record that says "cleanup owed" rather than a settled Ready from the previous attempt +// that would readmit a cell whose VMM may still be running. +// +// THE IN-FLIGHT RECORD PERSISTS THE ATTEMPT ITSELF, NOT A NAME FOR IT. An opaque attempt string lets a +// record keyed for cell A carry an attempt that belongs to cell B, and recovery would then tear down +// -- and settle -- the wrong cell's attempt under A's key (side-chat ruling on #11670). The attempt's +// slot DERIVES its cell, so the key and the attempt are checked against each other where the store is +// read, and an attempt the key disagrees with makes the store unsound rather than recoverable. +type InFlightAttempt { + attempt: MicroVmAttempt + invocation_id: NonEmptyStr + jit_registration_id: NonEmptyStr +} + +type CellReadinessRecord + = CellAttemptInFlight { cell: CellId, generation: Int, attempt: InFlightAttempt } + | CellSettled { cell: CellId, generation: Int, readiness: CellReadiness } + +fn in_flight_attempt_cell(attempt: InFlightAttempt) -> CellId { + runner_slot_instance_name(slot: attempt.attempt.slot) as CellId +} + +fn in_flight_attempt_unit(attempt: InFlightAttempt) -> NonEmptyStr { + runner_microvm_attempt_unit_name(attempt: attempt.attempt) +} + +fn in_flight_attempt_same(a: InFlightAttempt, b: InFlightAttempt) -> Bool { + (in_flight_attempt_unit(attempt: a) as String) == (in_flight_attempt_unit(attempt: b) as String) + && (a.invocation_id as String) == (b.invocation_id as String) + && (a.jit_registration_id as String) == (b.jit_registration_id as String) +} + +// THE ONE CARRIER FOR "THIS ATTEMPT, ON THIS CELL, AT THIS GENERATION". Sealed, and constructible only +// by bind_attempt_to_cell, which refuses an attempt whose derived cell is not the cell it is bound to. +// Every write that names an attempt, every recovery, and every teardown settlement takes this rather +// than a cell and an attempt supplied independently. +type CellBoundAttempt sole_constructor { + cell: CellId + generation: Int + attempt: InFlightAttempt +} + +type AttemptCellBinding + = AttemptBoundToCell { bound: CellBoundAttempt } + | AttemptCellMismatch { cell: CellId, attempt_cell: CellId } + +fn bind_attempt_to_cell(cell: CellId, generation: Int, attempt: InFlightAttempt) -> AttemptCellBinding { + if (in_flight_attempt_cell(attempt: attempt) as String) == (cell as String) { + AttemptBoundToCell { bound: CellBoundAttempt { cell: cell, generation: generation, attempt: attempt } } + } else { + AttemptCellMismatch { cell: cell, attempt_cell: in_flight_attempt_cell(attempt: attempt) } + } +} + +fn record_cell(record: CellReadinessRecord) -> CellId { + match record { + CellAttemptInFlight { cell: c, generation: _, attempt: _ } => c + CellSettled { cell: c, generation: _, readiness: _ } => c + } +} + +fn record_generation(record: CellReadinessRecord) -> Int { + match record { + CellAttemptInFlight { cell: _, generation: g, attempt: _ } => g + CellSettled { cell: _, generation: g, readiness: _ } => g + } +} + +// ROOT OWNERSHIP IS OBSERVED, NOT ASSUMED, because a store any tenant can write is a store any +// tenant can mark Ready. The observation is the host's stat of the store, and a store that is not +// root-owned and root-only-writable withdraws the WHOLE HOST: every record in it is suspect, not +// one cell's. +type CellReadinessStoreOwnership + = StoreRootOwned + | StoreNotRootOwned { owner_uid: Int, mode: NonEmptyStr } + +// AN UNREADABLE STORE IS A THIRD STATE, NOT AN EMPTY ONE. Reading "no records" out of a store that +// could not be opened is the empty-observation narrow: it would report every cell as never +// settled -- which refuses, so it is safe -- but it would report it at CELL grain and send an +// operator to every cell instead of to the store. It is kept distinct so the withdrawal lands at +// the grain whose remedy it is. +type CellReadinessStoreRead + = StoreRead { ownership: CellReadinessStoreOwnership, records: List } + | StoreUnreadable { reason: NonEmptyStr } + +// WITHDRAWAL HAS TWO GRAINS AND THEY ARE NOT INTERCHANGEABLE. +// +// HOST grain: the evidence every cell's admission rests on is itself unsound -- the store cannot be +// read, is not root's, holds two records for one cell, or holds a settled record whose readiness names +// a different cell -- so no cell on the host may start, +// including cells whose last record happens to read Ready. CELL grain: the store is sound and says +// THIS cell is not ready. Folding host grain into per-cell refusals would admit the next cell whose +// record is intact inside a store nobody should trust; folding cell grain into host grain would let +// one leaked VMM take a host's whole warm pool out of service. +type HostWithdrawal + = HostStoreUnreadable { reason: NonEmptyStr } + | HostStoreNotRootOwned { owner_uid: Int, mode: NonEmptyStr } + | HostStoreAmbiguous { cell: CellId } + | HostStoreRecordIncoherent { record_cell: CellId, named_cell: CellId } + +// THE STORE IS INDEXED ONCE, WHOLE, BEFORE ANY CELL IS PROJECTED OUT OF IT. Host grain is a property +// of the store, not of the cell being asked about: a duplicate for cell B, or a record whose +// readiness names a different cell than its key, makes the store unsound for cell A too. Filtering to +// the requested cell first and then checking would withdraw only when the defect happened to be in +// that cell, which is the host-grain fact demoted to cell grain (side-chat ruling on #11670). The +// index is sealed: the only way to hold one is to have passed both checks over every record, and the +// keyed map makes the uniqueness check one insert per record rather than a scan per record. +type CellReadinessIndex sole_constructor { + by_cell: Map +} + +type CellReadinessIndexing + = StoreIndexed { index: CellReadinessIndex } + | StoreIndexRefused { withdrawal: HostWithdrawal } + +fn readiness_cell(readiness: CellReadiness) -> CellId { + match readiness { + CellReady { cell: c } => c + CellQuarantined { cell: c, unproven: _ } => c + } +} + +// A record is coherent when everything inside it names the cell it is keyed by: a settled record's +// readiness, and an in-flight record's attempt (through the slot the attempt was built on). +fn record_incoherence(record: CellReadinessRecord) -> HostWithdrawal? { + match record { + CellAttemptInFlight { cell: c, generation: g, attempt: a } => + match bind_attempt_to_cell(cell: c, generation: g, attempt: a) { + AttemptBoundToCell { bound: _ } => none + AttemptCellMismatch { cell: rc, attempt_cell: ac } => + Present { value: HostStoreRecordIncoherent { record_cell: rc, named_cell: ac } } + } + CellSettled { cell: c, generation: _, readiness: r } => + if (readiness_cell(readiness: r) as String) == (c as String) { + none + } else { + Present { value: HostStoreRecordIncoherent { record_cell: c, named_cell: readiness_cell(readiness: r) } } + } + } +} + +// THE FIRST DEFECT IS CARRIED, not overwritten by a later one: the store is refused as a whole and the +// reader needs the first thing that made it unsound. +fn index_step(acc: CellReadinessIndexing, record: CellReadinessRecord) -> CellReadinessIndexing { + match acc { + StoreIndexRefused { withdrawal: w } => StoreIndexRefused { withdrawal: w } + StoreIndexed { index: ix } => + match record_incoherence(record: record) { + Present { value: w } => StoreIndexRefused { withdrawal: w } + Absent => + match map_get(ix.by_cell, record_cell(record: record) as String) { + Present { value: _ } => StoreIndexRefused { withdrawal: HostStoreAmbiguous { cell: record_cell(record: record) } } + Absent => StoreIndexed { index: CellReadinessIndex { by_cell: map_insert(ix.by_cell, record_cell(record: record) as String, record) } } + } + } + } +} + +fn index_cell_readiness(records: List) -> CellReadinessIndexing { + fold(records, init: StoreIndexed { index: CellReadinessIndex { by_cell: empty_map() } }, f: (acc, r) => index_step(acc: acc, record: r)) +} + +fn indexed_record(index: CellReadinessIndex, cell: CellId) -> CellReadinessRecord? { + map_get(index.by_cell, cell as String) +} + +type CellWithdrawal + = CellNeverSettled + | CellQuarantinedAt { generation: Int, unproven: List } + | CellGenerationMismatch { settled: Int, allocated: Int } + +// THE ADMISSION, AND IT JOINS THREE FACTS AT ONE PLACE: the allocation's generation, the store's +// readiness, and the generation that readiness was established at. CellRecoveryRequired is not a +// withdrawal: it says the previous incarnation never settled and a teardown must run to completion +// BEFORE this question can be asked again -- boot recovery resumes cleanup before admission. +type CellIncarnationAdmission + = CellIncarnationAdmitted { cell: CellId, generation: Int } + | CellRecoveryRequired { bound: CellBoundAttempt } + | CellWithdrawn { cell: CellId, withdrawal: CellWithdrawal } + | HostWithdrawn { withdrawal: HostWithdrawal } + +fn cell_incarnation_admission( + store: CellReadinessStoreRead, + cell: CellId, + allocation_generation: Int, +) -> CellIncarnationAdmission { + match store { + StoreUnreadable { reason: r } => HostWithdrawn { withdrawal: HostStoreUnreadable { reason: r } } + StoreRead { ownership: o, records: rs } => + match o { + StoreNotRootOwned { owner_uid: u, mode: m } => + HostWithdrawn { withdrawal: HostStoreNotRootOwned { owner_uid: u, mode: m } } + StoreRootOwned => + match index_cell_readiness(records: rs) { + StoreIndexRefused { withdrawal: w } => HostWithdrawn { withdrawal: w } + StoreIndexed { index: ix } => + admission_of_indexed_cell(index: ix, cell: cell, allocation_generation: allocation_generation) + } + } + } +} + +fn admission_of_indexed_cell( + index: CellReadinessIndex, + cell: CellId, + allocation_generation: Int, +) -> CellIncarnationAdmission { + match indexed_record(index: index, cell: cell) { + Absent => CellWithdrawn { cell: cell, withdrawal: CellNeverSettled } + Present { value: r } => admission_of_record(record: r, allocation_generation: allocation_generation) + } +} + +fn admission_of_record(record: CellReadinessRecord, allocation_generation: Int) -> CellIncarnationAdmission { + match record { + CellAttemptInFlight { cell: c, generation: g, attempt: a } => + match bind_attempt_to_cell(cell: c, generation: g, attempt: a) { + AttemptBoundToCell { bound: b } => CellRecoveryRequired { bound: b } + AttemptCellMismatch { cell: rc, attempt_cell: ac } => + HostWithdrawn { withdrawal: HostStoreRecordIncoherent { record_cell: rc, named_cell: ac } } + } + CellSettled { cell: c, generation: g, readiness: readiness } => + match readiness { + CellQuarantined { cell: _, unproven: u } => + CellWithdrawn { cell: c, withdrawal: CellQuarantinedAt { generation: g, unproven: u } } + CellReady { cell: _ } => + if g + 1 == allocation_generation { + CellIncarnationAdmitted { cell: c, generation: allocation_generation } + } else { + CellWithdrawn { cell: c, withdrawal: CellGenerationMismatch { settled: g, allocated: allocation_generation } } + } + } + } +} + +// WRITES ARE MONOTONE IN THE GENERATION, AND QUARANTINE ONLY TIGHTENS WITHIN ONE. +// +// A write at a LOWER generation than the stored record is a stale readback and is refused: it is +// how a slow readback of attempt N would clear attempt N + 1's quarantine. At the SAME generation a +// settled Ready may be tightened to Quarantined and an in-flight record may settle (its own +// attempt's readback), but a Quarantined record is never loosened: clearing a quarantine is a NEW +// readback that establishes the facts, and it is recorded at a new generation so the clearing event +// is distinguishable from a late copy of the old one. +// +// UNATTRIBUTED RESIDUE HAS NO ATTEMPT TO NAME, SO IT HAS ITS OWN WRITE AND THAT WRITE CAN ONLY +// QUARANTINE. Residue found on a cell the store called Ready belongs to no attempt the store knows, +// and inventing one -- the cell's name, the previous generation -- would be a record claiming an +// identity nobody observed. It carries no readiness parameter: its record is a quarantine with every +// sanitation fact a microVM cell owes (slot-scoped network) unobserved, at the generation that was about to run, and only a later readback at +// a higher generation that establishes the facts can clear it. +type CellReadinessWrite + = WriteAttemptStarted { bound: CellBoundAttempt } + | WriteReadbackSettled { bound: CellBoundAttempt, readiness: CellReadiness } + | WriteUnattributedResidue { cell: CellId, generation: Int } + +type CellReadinessWriteResult + = WriteAccepted { records: List } + | WriteRefusedStale { cell: CellId, stored: Int, offered: Int } + | WriteRefusedWouldLoosenQuarantine { cell: CellId, generation: Int } + | WriteRefusedAttemptMismatch { cell: CellId, stored_attempt: NonEmptyStr, offered_attempt: NonEmptyStr } + | WriteRefusedAttemptAlreadyRecorded { cell: CellId, generation: Int } + | WriteRefusedNotAdmitted { cell: CellId, admission: CellIncarnationAdmission } + | WriteRefusedStoreUnsound { withdrawal: HostWithdrawal } + | WriteRefusedRecoveryOwed { cell: CellId, in_flight_generation: Int, in_flight_attempt: NonEmptyStr } + | WriteRefusedIncoherent { withdrawal: HostWithdrawal } + +fn write_cell(write: CellReadinessWrite) -> CellId { + match write { + WriteAttemptStarted { bound: b } => b.cell + WriteReadbackSettled { bound: b, readiness: _ } => b.cell + WriteUnattributedResidue { cell: c, generation: _ } => c + } +} + +fn record_of_write(write: CellReadinessWrite) -> CellReadinessRecord { + match write { + WriteAttemptStarted { bound: b } => CellAttemptInFlight { cell: b.cell, generation: b.generation, attempt: b.attempt } + WriteReadbackSettled { bound: b, readiness: r } => CellSettled { cell: b.cell, generation: b.generation, readiness: r } + WriteUnattributedResidue { cell: c, generation: g } => + CellSettled { + cell: c, + generation: g, + readiness: CellQuarantined { cell: c, unproven: map(required_sanitation_facts(scope: SlotScopedNetwork), f => FactNotObserved { fact: f }) }, + } + } +} + +// AN ATTEMPT START IS NOT A READBACK, so a higher generation alone does not admit it: it is written +// only over a settled Ready at exactly the previous generation, which is the admission above +// restated at the write -- the store refuses to record a start the admission would have refused, +// rather than trusting every writer to have asked first. The first incarnation on a cell therefore +// needs a readback establishing the empty cell before it, exactly like every later one. +// +// THE WRITE IS JUDGED AGAINST THE SAME SEALED INDEX THE ADMISSION READS, so an unsound store refuses +// every write rather than accepting one into a store no reader will trust, and a write whose own +// record would be incoherent is refused before it can make the store unsound. +fn apply_cell_readiness_write( + records: List, + write: CellReadinessWrite, +) -> CellReadinessWriteResult { + match index_cell_readiness(records: records) { + StoreIndexRefused { withdrawal: w } => WriteRefusedStoreUnsound { withdrawal: w } + StoreIndexed { index: ix } => + match record_incoherence(record: record_of_write(write: write)) { + Present { value: w } => WriteRefusedIncoherent { withdrawal: w } + Absent => apply_indexed_write(records: records, index: ix, write: write) + } + } +} + +// AN IN-FLIGHT RECORD IS DISCHARGED ONLY BY ITS OWN ATTEMPT'S SETTLEMENT (same generation, same +// attempt; same_generation_settle). Any other write over it -- a readback at a higher generation, an +// unattributed-residue quarantine -- would replace "cleanup owed for this attempt" with a record that +// no longer names the attempt whose VMM may still be running, so it is refused (review 68576). +fn recovery_owed(stored: CellReadinessRecord) -> CellReadinessWriteResult? { + match stored { + CellAttemptInFlight { cell: c, generation: g, attempt: a } => + Present { value: WriteRefusedRecoveryOwed { cell: c, in_flight_generation: g, in_flight_attempt: in_flight_attempt_unit(attempt: a) } } + CellSettled { cell: _, generation: _, readiness: _ } => none + } +} + +fn apply_indexed_write( + records: List, + index: CellReadinessIndex, + write: CellReadinessWrite, +) -> CellReadinessWriteResult { + let cell = write_cell(write: write) + let others = filter(records, r => (record_cell(record: r) as String) != (cell as String)) + let replaced = concat(others, [record_of_write(write: write)]) + match write { + WriteAttemptStarted { bound: b } => + match admission_of_indexed_cell(index: index, cell: b.cell, allocation_generation: b.generation) { + CellIncarnationAdmitted { cell: _, generation: _ } => WriteAccepted { records: replaced } + refused => WriteRefusedNotAdmitted { cell: b.cell, admission: refused } + } + WriteUnattributedResidue { cell: c, generation: g } => + match indexed_record(index: index, cell: c) { + Absent => WriteAccepted { records: replaced } + Present { value: stored } => + match recovery_owed(stored: stored) { + Present { value: owed } => owed + Absent => + if g < record_generation(record: stored) { + WriteRefusedStale { cell: c, stored: record_generation(record: stored), offered: g } + } else { + WriteAccepted { records: replaced } + } + } + } + WriteReadbackSettled { bound: b, readiness: r } => + match indexed_record(index: index, cell: b.cell) { + Absent => WriteAccepted { records: replaced } + Present { value: stored } => { + let held = record_generation(record: stored) + if b.generation < held { + WriteRefusedStale { cell: b.cell, stored: held, offered: b.generation } + } else if b.generation > held { + match recovery_owed(stored: stored) { + Present { value: owed } => owed + Absent => WriteAccepted { records: replaced } + } + } else { + same_generation_settle(stored: stored, bound: b, readiness: r, replaced: replaced) + } + } + } + } +} + +// Called only from the WriteReadbackSettled arm, with that arm's fields rather than the write: the +// other write shapes are not representable here, so there is no arm for them to answer (review 68138). +fn same_generation_settle( + stored: CellReadinessRecord, + bound: CellBoundAttempt, + readiness: CellReadiness, + replaced: List, +) -> CellReadinessWriteResult { + let cell = bound.cell + let generation = bound.generation + match stored { + CellAttemptInFlight { cell: _, generation: _, attempt: sa } => + if in_flight_attempt_same(a: sa, b: bound.attempt) { + WriteAccepted { records: replaced } + } else { + WriteRefusedAttemptMismatch { + cell: cell, + stored_attempt: in_flight_attempt_unit(attempt: sa), + offered_attempt: in_flight_attempt_unit(attempt: bound.attempt), + } + } + CellSettled { cell: _, generation: _, readiness: held } => + match held { + CellQuarantined { cell: _, unproven: _ } => WriteRefusedWouldLoosenQuarantine { cell: cell, generation: generation } + CellReady { cell: _ } => + match readiness { + CellQuarantined { cell: _, unproven: _ } => WriteAccepted { records: replaced } + CellReady { cell: _ } => WriteRefusedAttemptAlreadyRecorded { cell: cell, generation: generation } + } + } + } +} diff --git a/dag/gunbc/runner/runner_microvm_lifecycle.dag b/dag/gunbc/runner/runner_microvm_lifecycle.dag new file mode 100644 index 00000000000..e3d67aa22ef --- /dev/null +++ b/dag/gunbc/runner/runner_microvm_lifecycle.dag @@ -0,0 +1,475 @@ +module gunbc.runner_microvm_lifecycle + +import std.types { String, NonEmptyStr, Bool, List, Int } +import std.disposition { Disposition, SingleAuthority } +import product.fabric.sanitation { + CellId, SandboxId, CellReadiness, SanitationFact, SanitationReadback, SanitationObservation, + FactConfirmed, FactRefuted, FactUnobservable, + NoSurvivingProcesses, CgroupEmpty, MountsRemoved, SlotNetworkQuiescent, SlotScopedNetwork, + WritableLayersDeleted, SecretsRemoved, cell_readiness_after, +} +import gunbc.fabric_cell_converge { fabric_cell_slice_name } +import gunbc.runner_microvm { RunnerGuestImage } +import gunbc.runner_microvm_attempt { + MicroVmAttempt, runner_microvm_attempt_unit_name, runner_microvm_attempt_dir, + runner_microvm_attempt_jail_base, runner_microvm_attempt_jit_drive_path, +} +import gunbc.runner_attempt_launch { AttemptGround, GroundClear, GroundOccupied } +import gunbc.build_cache_instance { runner_slot_identity_equal, runner_slot_instance_name } +import gunbc.runner_microvm_network { + BoundSlotNetworkReadback, SlotNetworkReadback, SlotNetworkConfirmed, SlotNetworkRefuted, + SlotNetworkUnobservable, slot_network_fact_label, + bound_slot_network_readback_slot, bound_slot_network_readback_result, +} +import gunbc.runner_microvm_cell_readiness { + CellIncarnationAdmission, CellIncarnationAdmitted, CellRecoveryRequired, + CellReadinessWrite, WriteAttemptStarted, WriteReadbackSettled, WriteUnattributedResidue, + InFlightAttempt, CellBoundAttempt, AttemptCellBinding, AttemptBoundToCell, AttemptCellMismatch, + bind_attempt_to_cell, in_flight_attempt_unit, +} + +data runner_microvm_lifecycle_disposition: Disposition = SingleAuthority + +// THE HOST-SIDE PER-ATTEMPT LIFECYCLE CONTROLLER, AS THE DECISIONS IT MAKES. +// +// gunbc.runner_microvm names the topology VmmUnderLifecycleController: a controller is the slot +// unit's MainPID, the VMM runs beneath it, and the unit's intent (ExitType=main with +// KillMode=control-group, gunbc#11662) makes systemd's stop reach the whole cgroup once the +// controller exits. This module is what the controller decides at each step, from what it has +// observed; the realization that performs the steps consumes these decisions and adds none. +// +// DECLARED FRONTIER (DESIGN 3c). In this change the module's only executing consumer is its witness; +// no production entry calls it yet. NAMED CONSUMER: gunbc.runner_microvm_lifecycle_realize, the +// controller that runs as the slot unit's MainPID and calls controller_start, advance_bring_up, +// stop_request_admission and settle_teardown, reading and writing the store through +// gunbc.runner_microvm_cell_readiness apply_cell_readiness_write. It is the next change in the +// adhoc-3faa2033-f8f lane. TRIGGER: that module lands with srv1 transient-unit receipts for the +// modeled REDs (SIGTERM-ignoring child, double-fork, unkillable task, failed cgroup read, stale stop, +// background process after success). SUFFICIENT FOR retiring this paragraph. NOT satisfied by that +// module compiling, or by it existing without an entry the slot unit execs. +// +// THE RULE THE WHOLE MODULE IS SHAPED BY: A GUEST EVENT MAY TRIGGER TEARDOWN, AND NO GUEST EVENT +// MAY ESTABLISH SANITATION. The guest is the tenant. "The runner exited 0" and "the guest powered +// off" are statements made by the code whose residue sanitation exists to find, so they can start a +// teardown and can never finish one. That is carried structurally rather than as a rule a caller +// must remember: sanitation_readback_of_teardown takes only a host-joined teardown readback, and there is no type through +// which a guest's report could reach it. + +// EVERY LIFECYCLE EVENT CARRIES THE ATTEMPT'S WHOLE IDENTITY, because every question this +// controller answers is "about WHICH incarnation". A stop request, a boot report or a readback that +// names only the slot is ambiguous across incarnations, and the ambiguity is exactly how a stop +// meant for the previous incarnation lands on the current one. The host and slot are inside +// MicroVmAttempt; the VMM identity is derived from it rather than carried beside it, so the two +// cannot disagree. +type AttemptIdentity { + attempt: MicroVmAttempt + allocation_generation: Int + invocation_id: NonEmptyStr + jit_registration_id: NonEmptyStr + guest_image: RunnerGuestImage +} + +// The guest image is not compared: two incarnations of one attempt id at one generation under one +// InvocationID with one registration are one incarnation, and a comparison on a record with no +// equality would be a second spelling of the tuple's identity. +fn attempt_identity_same(a: AttemptIdentity, b: AttemptIdentity) -> Bool { + (runner_microvm_attempt_unit_name(attempt: a.attempt) as String) == (runner_microvm_attempt_unit_name(attempt: b.attempt) as String) + && a.allocation_generation == b.allocation_generation + && (a.invocation_id as String) == (b.invocation_id as String) + && (a.jit_registration_id as String) == (b.jit_registration_id as String) +} + +// AN IDENTITY IS BOUND TO THE ADMITTED CELL BEFORE THE CONTROLLER MAY ACT ON IT, AND THE BINDING IS +// SEALED. The admission answers for one (cell, generation); the identity names its own cell through +// its slot and its own generation. Comparing only the generation would let an admission for cell A +// start an attempt whose identity is cell B's (side-chat ruling on #11670): two independently +// supplied values agreeing on one axis. CellBoundIdentity is constructible only by +// bind_identity_to_admission, which joins BOTH axes, so every consumer that holds one holds the join. +type CellBoundIdentity sole_constructor { + attempt: CellBoundAttempt + guest_image: RunnerGuestImage +} + +type CellBinding + = CellBound { bound: CellBoundIdentity } + | CellBindingRefusedCell { admitted: CellId, identity_cell: CellId } + | CellBindingRefusedGeneration { admitted: Int, identity_generation: Int } + +fn in_flight_attempt_of_identity(identity: AttemptIdentity) -> InFlightAttempt { + InFlightAttempt { + attempt: identity.attempt, + invocation_id: identity.invocation_id, + jit_registration_id: identity.jit_registration_id, + } +} + +// The cell axis is joined by gunbc.runner_microvm_cell_readiness bind_attempt_to_cell, the same +// binder the store uses at read, so the controller and the store cannot disagree about what "this +// attempt's cell" means. +fn bind_identity_to_admission(cell: CellId, generation: Int, identity: AttemptIdentity) -> CellBinding { + if identity.allocation_generation != generation { + CellBindingRefusedGeneration { admitted: generation, identity_generation: identity.allocation_generation } + } else { + match bind_attempt_to_cell(cell: cell, generation: generation, attempt: in_flight_attempt_of_identity(identity: identity)) { + AttemptBoundToCell { bound: b } => CellBound { bound: CellBoundIdentity { attempt: b, guest_image: identity.guest_image } } + AttemptCellMismatch { cell: c, attempt_cell: ac } => CellBindingRefusedCell { admitted: c, identity_cell: ac } + } + } +} + +// THE CONTROLLER STARTS ONLY FROM AN ADMITTED CELL, AND ITS FIRST DURABLE ACT IS THE IN-FLIGHT +// RECORD. The admission is gunbc.runner_microvm_cell_readiness's; the controller does not re-derive +// it. CellRecoveryRequired is not a refusal to do nothing: it is the instruction to run the terminal +// path for the attempt that never settled, before any new attempt is prepared. +type ControllerStart + = StartAttempt { bound: CellBoundIdentity, record: CellReadinessWrite } + | StartRecovery { bound: CellBoundAttempt, trigger: TerminalTrigger } + | StartQuarantineUnattributedResidue { trigger: TerminalTrigger, record: CellReadinessWrite } + | StartRefused { admission: CellIncarnationAdmission } + | StartBindingRefused { binding: CellBinding } + +// THE GROUND IS gunbc.runner_attempt_launch's AttemptGround, the host's own check for prior attempt +// resources, and it outranks an admitting record: a store that says Ready over a cell whose jail or +// attempt directory is still present is a store that missed something, and the answer is a +// quarantine, not a launch onto the residue. The residue names no attempt the store knows, so the +// controller does not invent one: it records WriteUnattributedResidue at the generation that was +// about to run, which can only quarantine (gunbc.runner_microvm_cell_readiness). Both arms act only +// on a bound identity, so the quarantine lands on the cell that was admitted AND identified. +fn controller_start( + admission: CellIncarnationAdmission, + ground: AttemptGround, + identity: AttemptIdentity, +) -> ControllerStart { + match admission { + CellIncarnationAdmitted { cell: c, generation: g } => + match bind_identity_to_admission(cell: c, generation: g, identity: identity) { + CellBound { bound: b } => start_on_bound_cell(bound: b, ground: ground) + refused => StartBindingRefused { binding: refused } + } + CellRecoveryRequired { bound: b } => StartRecovery { bound: b, trigger: ControllerLost } + refused => StartRefused { admission: refused } + } +} + +fn start_on_bound_cell(bound: CellBoundIdentity, ground: AttemptGround) -> ControllerStart { + match ground { + GroundOccupied => + StartQuarantineUnattributedResidue { + trigger: ResourcesFoundOnRecovery, + record: WriteUnattributedResidue { cell: bound.attempt.cell, generation: bound.attempt.generation }, + } + GroundClear => + StartAttempt { + bound: bound, + record: WriteAttemptStarted { bound: bound.attempt }, + } + } +} + +// THE BRING-UP PROGRESSION IS A TOTAL ORDER AND EACH STEP IS OBSERVED, NOT ASSUMED. +// +// AttemptPrepared: credential disk and workspace staged by the host, slot network converged. VmmStarted: the host saw +// the jailer's VMM running in the cell's cgroup. GuestBooted and RunnerListening: the guest reported +// them -- these are guest events, admissible here because progression only decides whether the +// slot is SERVING, never whether it is CLEAN. SlotServing: the listener is up and the host has +// nothing left to do but wait for a terminal trigger. +type BringUpPhase + = AttemptPrepared + | VmmStarted + | GuestBooted + | RunnerListening + | SlotServing + +fn bring_up_rank(phase: BringUpPhase) -> Int { + match phase { + AttemptPrepared => 0 + VmmStarted => 1 + GuestBooted => 2 + RunnerListening => 3 + SlotServing => 4 + } +} + +type BringUpEvent { + identity: AttemptIdentity + reached: BringUpPhase +} + +// A SKIPPED PHASE IS A REFUSAL, not a fast path: a runner reporting "listening" before the host saw +// a VMM means the report is not from this attempt's guest, and advancing would let an unrelated +// listener stand for this slot. An event naming a different incarnation is refused before its +// phase is even looked at. +type BringUpTransition + = BringUpAdvanced { phase: BringUpPhase } + | BringUpRefusedForeignIncarnation + | BringUpRefusedOutOfOrder { from: BringUpPhase, to: BringUpPhase } + +fn advance_bring_up(live: AttemptIdentity, at: BringUpPhase, event: BringUpEvent) -> BringUpTransition { + if !attempt_identity_same(a: live, b: event.identity) { + BringUpRefusedForeignIncarnation + } else if bring_up_rank(phase: event.reached) == bring_up_rank(phase: at) + 1 { + BringUpAdvanced { phase: event.reached } + } else { + BringUpRefusedOutOfOrder { from: at, to: event.reached } + } +} + +// THE TERMINAL TRIGGERS. Any one of them starts the same teardown, and none of them decides its +// outcome -- which is why RunnerExited carries its exit code and the code goes nowhere: a job that +// succeeded and left a background process is a dirty cell, and there is no parameter downstream +// through which "succeeded" could say otherwise. +type TerminalTrigger + = VmmExited { exit_code: Int } + | RunnerExited { exit_code: Int } + | DeadlineReached + | StopRequested + | ControllerLost + | ResourcesFoundOnRecovery + +// A STOP NAMES ITS INCARNATION, and a stop for any other is refused. The warm pool reuses slots, +// so a stop issued against incarnation N that arrives while N + 1 runs is the ordinary late +// delivery, not an exotic race -- honoring it would tear down a job that never asked to stop. +type StopAdmission + = StopAdmitted { trigger: TerminalTrigger } + | StopRefusedStaleIncarnation { live_generation: Int, requested_generation: Int } + +fn stop_request_admission(live: AttemptIdentity, requested: AttemptIdentity) -> StopAdmission { + if attempt_identity_same(a: live, b: requested) { + StopAdmitted { trigger: StopRequested } + } else { + StopRefusedStaleIncarnation { + live_generation: live.allocation_generation, + requested_generation: requested.allocation_generation, + } + } +} + +// THE STOP IS GRACEFUL, THEN FORCED, AND THE FORCE IS BOUNDED. What the controller observes is +// which of the three happened; a task that survives the bounded force-stop (uninterruptible sleep +// survives SIGKILL) is not "still stopping", it is a surviving process, and the cell quarantines on +// it whatever the cgroup readback says afterwards. +type TeardownStop + = StoppedGracefully + | StoppedByForce + | ForceStopBoundExceeded { survivors: List } + +// THE CGROUP READBACK IS RECURSIVE, AND A FAILED READ IS ITS OWN ARM. cgroup.procs of the slot's +// cgroup alone misses every process in a child cgroup -- a double-forked daemon moved one level +// down is invisible to it -- so the readback covers the subtree. A read that fails is +// Unobservable, never Empty: "could not read" is the one answer that must not release a cell. +type CgroupSubtreeReadback + = CgroupSubtreeEmpty + | CgroupSubtreePopulated { pids: List, cgroups: List } + | CgroupSubtreeReadFailed { reason: NonEmptyStr } + +// EACH ATTEMPT RESOURCE IS READ BACK ABSENT FROM THE HOST, separately, because each leaks something +// different (product.fabric.sanitation SanitationFact). +type ResourceReadback + = ResourceAbsent + | ResourcePresent { detail: NonEmptyStr } + | ResourceUnreadable { reason: NonEmptyStr } + +// THE SLOT NETWORK IS NOT AN ATTEMPT RESOURCE, SO IT IS NOT READ BACK ABSENT. The tap and nft ruleset +// are slot-scoped converge state (sunny-ant-606 ruling A); the attempt owns only its jail subtree and +// workspace. What must hold after an attempt is that the slot network is QUIESCENT -- no process holds +// the tap, conntrack for the reused guest address is empty, the ruleset digest equals the converged +// one -- which is product.fabric.sanitation's SlotNetworkQuiescent, owed by a SlotScopedNetwork +// readback, and not NetworkNamespaceRemoved, which is the attempt-scoped contract. +// +// THE SLOT NETWORK RESULT IS CONSUMED AS THE BOUND READBACK, NEVER AS A BARE VERDICT. +// +// gunbc.runner_microvm_network slot_network_readback returns a sealed BoundSlotNetworkReadback: the +// subject it was taken for travels with the result whatever the verdict. Unwrapping the result at the +// boundary and passing the verdict on would put the attempt's network fact back where every other +// subject was before the join -- a value that could have been read for any slot. So the bound +// readback is what ObservedTeardown carries, its slot is one of the subjects +// attempt_teardown_readback joins against the attempt, and only a readback that survived that join +// is mapped onto SlotNetworkQuiescent. +type ObservedStop { unit: NonEmptyStr, invocation_id: NonEmptyStr, outcome: TeardownStop } + +type ObservedCgroup { root: NonEmptyStr, readback: CgroupSubtreeReadback } + +type ObservedPath { path: String, readback: ResourceReadback } + +type ObservedTeardown { + host: String + generation: Int + stop: ObservedStop + cgroup: ObservedCgroup + mounts: ObservedPath + attempt_storage: ObservedPath + credential_disk: ObservedPath + network: BoundSlotNetworkReadback +} + +type TeardownSubject + = SubjectHost + | SubjectGeneration + | SubjectVmmUnit + | SubjectInvocation + | SubjectCgroupRoot + | SubjectJailRoot + | SubjectAttemptDirectory + | SubjectCredentialDrive + | SubjectSlotNetwork + +type AttemptTeardownReadback sole_constructor { + bound: CellBoundAttempt + observed: ObservedTeardown +} + +type TeardownReadbackBinding + = TeardownReadbackBound { readback: AttemptTeardownReadback } + | TeardownReadbackForeignSubject { subject: TeardownSubject, expected: String, observed: String } + +type SubjectPair { subject: TeardownSubject, expected: String, observed: String } + +fn teardown_subject_pairs(bound: CellBoundAttempt, o: ObservedTeardown) -> List { + let a = bound.attempt.attempt + [ + SubjectPair { subject: SubjectHost, expected: a.slot.host as String, observed: o.host }, + SubjectPair { subject: SubjectGeneration, expected: to_string(bound.generation), observed: to_string(o.generation) }, + SubjectPair { subject: SubjectVmmUnit, expected: in_flight_attempt_unit(attempt: bound.attempt) as String, observed: o.stop.unit as String }, + SubjectPair { subject: SubjectInvocation, expected: bound.attempt.invocation_id as String, observed: o.stop.invocation_id as String }, + SubjectPair { subject: SubjectCgroupRoot, expected: fabric_cell_slice_name(slot: a.slot), observed: o.cgroup.root as String }, + SubjectPair { subject: SubjectJailRoot, expected: runner_microvm_attempt_jail_base(attempt: a), observed: o.mounts.path }, + SubjectPair { subject: SubjectAttemptDirectory, expected: runner_microvm_attempt_dir(attempt: a), observed: o.attempt_storage.path }, + SubjectPair { subject: SubjectCredentialDrive, expected: runner_microvm_attempt_jit_drive_path(attempt: a), observed: o.credential_disk.path }, + ] +} + +// THE SLOT SUBJECT IS COMPARED AS A SLOT IDENTITY, not as a rendering of one: the network module owns +// the subject and hands back its RunnerSlotIdentity, so the join is that identity against the +// attempt's, through the identity's own equality. It is checked beside the string-rendered subjects +// rather than inside teardown_subject_pairs because it is the one subject that is not a path. +fn slot_network_subject_foreign(bound: CellBoundAttempt, o: ObservedTeardown) -> Bool { + !runner_slot_identity_equal( + a: bound.attempt.attempt.slot, + b: bound_slot_network_readback_slot(b: o.network), + ) +} + +fn attempt_teardown_readback(bound: CellBoundAttempt, observed: ObservedTeardown) -> TeardownReadbackBinding { + if slot_network_subject_foreign(bound: bound, o: observed) { + TeardownReadbackForeignSubject { + subject: SubjectSlotNetwork, + expected: runner_slot_instance_name(slot: bound.attempt.attempt.slot), + observed: runner_slot_instance_name(slot: bound_slot_network_readback_slot(b: observed.network)), + } + } else { + attempt_teardown_readback_after_network(bound: bound, observed: observed) + } +} + +fn attempt_teardown_readback_after_network(bound: CellBoundAttempt, observed: ObservedTeardown) -> TeardownReadbackBinding { + match filter(teardown_subject_pairs(bound: bound, o: observed), p => p.expected != p.observed).first() { + Absent => TeardownReadbackBound { readback: AttemptTeardownReadback { bound: bound, observed: observed } } + Present { value: p } => + TeardownReadbackForeignSubject { subject: p.subject, expected: p.expected, observed: p.observed } + } +} + +fn resource_observation(fact: SanitationFact, readback: ResourceReadback) -> SanitationObservation { + match readback { + ResourceAbsent => FactConfirmed { fact: fact } + ResourcePresent { detail: d } => FactRefuted { fact: fact, detail: d } + ResourceUnreadable { reason: r } => FactUnobservable { fact: fact, reason: r } + } +} + +// EACH OF THE NETWORK MODULE'S SEVEN FACTS KEEPS ITS NAME IN THE DETAIL, because "the slot network is +// not quiescent" is unactionable while "tap-unheld: refuted ..." sends an operator at the right thing. +// Its refuted and unobservable arms stay distinct here exactly as they are there. +fn slot_network_observation(result: SlotNetworkReadback) -> SanitationObservation { + match result { + SlotNetworkConfirmed => FactConfirmed { fact: SlotNetworkQuiescent } + SlotNetworkRefuted { fact: f, detail: d } => + FactRefuted { + fact: SlotNetworkQuiescent, + detail: join([slot_network_fact_label(fact: f), ": ", d as String], "") as NonEmptyStr, + } + SlotNetworkUnobservable { fact: f, reason: r } => + FactUnobservable { + fact: SlotNetworkQuiescent, + reason: join([slot_network_fact_label(fact: f), ": ", r as String], "") as NonEmptyStr, + } + } +} + +fn pid_list_text(pids: List) -> String { + join(map(pids, p => to_string(p)), ",") +} + +fn cgroup_observation(readback: CgroupSubtreeReadback) -> SanitationObservation { + match readback { + CgroupSubtreeEmpty => FactConfirmed { fact: CgroupEmpty } + CgroupSubtreePopulated { pids: p, cgroups: _ } => + FactRefuted { fact: CgroupEmpty, detail: join(["pids ", pid_list_text(pids: p), " remain in the cell's cgroup subtree"], "") as NonEmptyStr } + CgroupSubtreeReadFailed { reason: r } => FactUnobservable { fact: CgroupEmpty, reason: r } + } +} + +// NO SURVIVING PROCESS NEEDS BOTH HOST FACTS: the stop did not exceed its bound, AND the subtree +// holds no pid. Either one alone is refuted by a case the other misses -- the unkillable task +// that later leaves the cgroup listing, and the double-forked daemon the stop never waited for. +fn surviving_process_observation(stop: TeardownStop, cgroup: CgroupSubtreeReadback) -> SanitationObservation { + match stop { + ForceStopBoundExceeded { survivors: s } => + FactRefuted { fact: NoSurvivingProcesses, detail: join(["pids ", pid_list_text(pids: s), " survived the bounded force-stop"], "") as NonEmptyStr } + StoppedGracefully => process_observation_of_cgroup(cgroup: cgroup) + StoppedByForce => process_observation_of_cgroup(cgroup: cgroup) + } +} + +fn process_observation_of_cgroup(cgroup: CgroupSubtreeReadback) -> SanitationObservation { + match cgroup { + CgroupSubtreeEmpty => FactConfirmed { fact: NoSurvivingProcesses } + CgroupSubtreePopulated { pids: p, cgroups: _ } => + FactRefuted { fact: NoSurvivingProcesses, detail: join(["pids ", pid_list_text(pids: p), " are still running"], "") as NonEmptyStr } + CgroupSubtreeReadFailed { reason: r } => FactUnobservable { fact: NoSurvivingProcesses, reason: r } + } +} + +fn teardown_observations(o: ObservedTeardown) -> List { + [ + surviving_process_observation(stop: o.stop.outcome, cgroup: o.cgroup.readback), + cgroup_observation(readback: o.cgroup.readback), + resource_observation(fact: MountsRemoved, readback: o.mounts.readback), + slot_network_observation(result: bound_slot_network_readback_result(b: o.network)), + resource_observation(fact: WritableLayersDeleted, readback: o.attempt_storage.readback), + resource_observation(fact: SecretsRemoved, readback: o.credential_disk.readback), + ] +} + +// THE ONLY ROUTE FROM A TEARDOWN TO A SanitationReadback. Its one parameter is the sealed carrier, so +// the cell and sandbox it reports are the ones every observation was joined against. The trigger is +// deliberately absent: it started the teardown and has nothing to say about how it ended. +fn sanitation_readback_of_teardown(readback: AttemptTeardownReadback) -> SanitationReadback { + SanitationReadback { + cell: readback.bound.cell, + sandbox: in_flight_attempt_unit(attempt: readback.bound.attempt) as String as SandboxId, + network_scope: SlotScopedNetwork, + observations: teardown_observations(o: readback.observed), + } +} + +// THE TERMINAL PATH'S RESULT: the readiness, and the store write that records it at the attempt's +// own generation, so a readback arriving after a newer incarnation's record is refused by the store +// as stale rather than trusted by the controller. +type TeardownSettlement { + trigger: TerminalTrigger + readiness: CellReadiness + record: CellReadinessWrite +} + +// ONE SETTLEMENT FOR A LIVE TEARDOWN AND A RECOVERED ONE: both are a CellBoundAttempt torn down and +// read back, and the store write is at that attempt's own generation, so a readback arriving after a +// newer incarnation's record is refused by the store as stale rather than trusted by the controller. +fn settle_teardown(readback: AttemptTeardownReadback, trigger: TerminalTrigger) -> TeardownSettlement { + let readiness = cell_readiness_after(readback: sanitation_readback_of_teardown(readback: readback)) + TeardownSettlement { + trigger: trigger, + readiness: readiness, + record: WriteReadbackSettled { bound: readback.bound, readiness: readiness }, + } +} diff --git a/dag/gunbc/runner/runner_microvm_network.dag b/dag/gunbc/runner/runner_microvm_network.dag index 89438acb4af..f8abdb5742d 100644 --- a/dag/gunbc/runner/runner_microvm_network.dag +++ b/dag/gunbc/runner/runner_microvm_network.dag @@ -940,6 +940,22 @@ type SlotNetworkFact | ExpectationTableEmptyFact | RulesetMatchesConvergedFact +// EACH FACT HAS ITS OWN WIRE WORD, because a consumer that folds this readback into one sanitation +// fact (gunbc.runner_microvm_lifecycle maps it onto product.fabric.sanitation SlotNetworkQuiescent) +// otherwise reports "the slot network is not quiescent" and sends an operator to look at all seven. +// The label lives here, with the coproduct, rather than being spelled a second time by that consumer. +fn slot_network_fact_label(fact: SlotNetworkFact) -> String { + match fact { + TapUnheldFact => "tap-unheld" + TapIpv6DisabledFact => "tap-ipv6-disabled" + GuestOriginatedConntrackEmptyFact => "guest-originated-conntrack-empty" + GuestDestinedConntrackEmptyFact => "guest-destined-conntrack-empty" + GuestNeighbourAbsentFact => "guest-neighbour-absent" + ExpectationTableEmptyFact => "expectation-table-empty" + RulesetMatchesConvergedFact => "ruleset-matches-converged" + } +} + type TapHolderObservation = TapPresentUnheld | TapHeld { holders: Int } diff --git a/dag/test/claim/fabric/fabric_sanitation_witness_test.dag b/dag/test/claim/fabric/fabric_sanitation_witness_test.dag index 61cc8c66123..2fb9b025c08 100644 --- a/dag/test/claim/fabric/fabric_sanitation_witness_test.dag +++ b/dag/test/claim/fabric/fabric_sanitation_witness_test.dag @@ -4,7 +4,8 @@ import std.types { Bool, String, List, NonEmptyStr } import product.fabric.sanitation { CellId, SandboxId, SanitationFact, SanitationObservation, SanitationReadback, NoSurvivingProcesses, CgroupEmpty, MountsRemoved, - NetworkNamespaceRemoved, WritableLayersDeleted, SecretsRemoved, + NetworkNamespaceRemoved, SlotNetworkQuiescent, WritableLayersDeleted, SecretsRemoved, + SandboxNetworkScope, AttemptScopedNetwork, SlotScopedNetwork, FactConfirmed, FactRefuted, FactUnobservable, required_sanitation_facts, sanitation_fact_label, unproven_facts, unproven_fact_label, @@ -18,11 +19,11 @@ fn a_cell() -> CellId { "srv3-06" as CellId } fn a_sandbox() -> SandboxId { "sandbox-attempt-1-gen-4" as SandboxId } fn readback_of(obs: List) -> SanitationReadback { - SanitationReadback { cell: a_cell(), sandbox: a_sandbox(), observations: obs } + SanitationReadback { cell: a_cell(), sandbox: a_sandbox(), network_scope: AttemptScopedNetwork, observations: obs } } fn all_confirmed() -> List { - map(required_sanitation_facts(), f => FactConfirmed { fact: f }) + map(required_sanitation_facts(scope: AttemptScopedNetwork), f => FactConfirmed { fact: f }) } // A FULLY PROVEN TEARDOWN RETURNS THE CELL. The positive control: without it every assertion below @@ -103,18 +104,36 @@ test fn a_refused_teardown_names_the_fact_and_its_detail() -> Bool { // level out — no observation becoming no problem — and the case where the cell is MOST likely // dirty, since the agent vanished mid-attempt. Every required fact comes back unobserved. test fn a_lost_host_agent_quarantines_with_every_fact_unproven() -> Bool { - let readiness = readiness_without_readback(cell: a_cell(), sandbox: a_sandbox()) + let readiness = readiness_without_readback(cell: a_cell(), sandbox: a_sandbox(), network_scope: AttemptScopedNetwork) let unproven = unproven_facts(readback: readback_of(obs: [])) !cell_is_ready(readiness: readiness) - && (unproven |> count) == (required_sanitation_facts() |> count) - && (required_sanitation_facts() |> count) == 6 + && (unproven |> count) == (required_sanitation_facts(scope: AttemptScopedNetwork) |> count) + && (required_sanitation_facts(scope: AttemptScopedNetwork) |> count) == 6 } // EVERY FACT HAS ITS OWN WIRE WORD. // A label function collapsing two facts still renders a plausible quarantine line, and the collapse // would only surface as an operator inspecting the wrong subsystem. test fn the_six_facts_do_not_share_a_wire_word() -> Bool { - let labels = map(required_sanitation_facts(), f => sanitation_fact_label(fact: f)) + let labels = map(required_sanitation_facts(scope: AttemptScopedNetwork), f => sanitation_fact_label(fact: f)) (labels |> count) == 6 && !any(labels, a => (filter(labels, b => b == a) |> count) > 1) } + +// A SLOT-SCOPED SANDBOX OWES QUIESCENCE, NOT REMOVAL, AND ONE FACT DOES NOT STAND FOR THE OTHER. +// A slot-scoped readback that confirms every attempt-scoped fact -- namespace removal included -- +// still quarantines, naming slot-network-quiescent as not observed; and confirming quiescence in its +// place returns the cell. An attempt-scoped readback is untouched by the new fact. +test fn a_slot_scoped_network_owes_quiescence_and_removal_does_not_stand_for_it() -> Bool { + let attempt_facts = map(required_sanitation_facts(scope: AttemptScopedNetwork), f => FactConfirmed { fact: f }) + let slot_facts = map(required_sanitation_facts(scope: SlotScopedNetwork), f => FactConfirmed { fact: f }) + let wrong = SanitationReadback { cell: a_cell(), sandbox: a_sandbox(), network_scope: SlotScopedNetwork, observations: attempt_facts } + let right = SanitationReadback { cell: a_cell(), sandbox: a_sandbox(), network_scope: SlotScopedNetwork, observations: slot_facts } + let missing = match unproven_facts(readback: wrong).first() { + Present { value: FactNotObserved { fact: SlotNetworkQuiescent } } => (unproven_facts(readback: wrong) |> count) == 1 + _ => false + } + missing + && cell_is_ready(readiness: cell_readiness_after(readback: right)) + && cell_is_ready(readiness: cell_readiness_after(readback: readback_of(obs: attempt_facts))) +} diff --git a/dag/test/claim/runner/runner_microvm_attempt_witness_test.dag b/dag/test/claim/runner/runner_microvm_attempt_witness_test.dag index be196531393..5c8b2f47e1b 100644 --- a/dag/test/claim/runner/runner_microvm_attempt_witness_test.dag +++ b/dag/test/claim/runner/runner_microvm_attempt_witness_test.dag @@ -8,8 +8,7 @@ import gunbc.fleet_intent_network { operator_host_srv2 } import gunbc.fabric_cell_converge { fabric_cell_attempt_root_path, fabric_cell_slice_name } import gunbc.runner_microvm_attempt { MicroVmAttempt, MicroVmCellBinding, VmBoundToOwnedCell, VmUnboundCellNotOwned, - MicroVmTeardownVerdict, TeardownProven, TeardownVmmStillRunning, TeardownResidueRemains, - TeardownNotObserved, microvm_cell_releasable, bind_owned_attempt, + bind_owned_attempt, runner_microvm_attempt_dir, runner_microvm_attempt_rootfs_path, runner_microvm_attempt_unit_name, AttemptSegment, AttemptSegmentResult, AttemptSegmentAccepted, AttemptSegmentRefused, @@ -109,17 +108,6 @@ test fn two_attempts_on_one_slot_get_distinct_unit_names() -> Bool { } } -// ONLY A PROVEN TEARDOWN RELEASES THE CELL. The three refusing arms are asserted individually -// rather than as "not TeardownProven", because the red that matters is a future arm added to the -// coproduct and quietly treated as releasable -- a negation would admit it silently, and this -// will not. -test fn the_cell_is_released_only_on_proven_teardown() -> Bool { - microvm_cell_releasable(verdict: TeardownProven) - && !microvm_cell_releasable(verdict: TeardownVmmStillRunning { unit: "gunbc-microvm-srv2-01-x" as NonEmptyStr }) - && !microvm_cell_releasable(verdict: TeardownResidueRemains { path: "/x/attempts/x" }) - && !microvm_cell_releasable(verdict: TeardownNotObserved { cause: "the observation could not run" }) -} - // A TRAVERSING ATTEMPT ID MUST BE UNCONSTRUCTABLE, NOT SANITIZED. Every path in this module derives // from the segment, so "../shared" would move the rootfs, the JIT drive and the config together and // cleanup would prove the WRONG subtree empty (review 61259). Each refusing spelling is asserted diff --git a/dag/test/claim/runner/runner_microvm_lifecycle_witness_test.dag b/dag/test/claim/runner/runner_microvm_lifecycle_witness_test.dag new file mode 100644 index 00000000000..39a9d30e8e4 --- /dev/null +++ b/dag/test/claim/runner/runner_microvm_lifecycle_witness_test.dag @@ -0,0 +1,729 @@ +module gunbc.test.claim.runner.runner_microvm_lifecycle_witness_test + +import std.types { String, NonEmptyStr, Bool, Int, List } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import gunbc.build_cache_instance { RunnerSlotIdentity, runner_slot_instance_name } +import gunbc.fleet_intent_network { operator_host_srv2 } +import product.fabric.sanitation { CellId, CellReadiness, CellReady, CellQuarantined, cell_is_ready } +import gunbc.runner_microvm { gunbc_runner_guest_image } +import gunbc.runner_microvm_attempt { + MicroVmAttemptResult, MicroVmAttemptAccepted, microvm_attempt, + runner_microvm_attempt_dir, runner_microvm_attempt_jail_base, runner_microvm_attempt_jit_drive_path, + runner_microvm_attempt_unit_name, +} +import gunbc.fabric_cell_converge { fabric_cell_slice_name } +import std.nat { Nat } +import std.content_hash { Sha256Digest, Sha256DigestHex } +import gunbc.runner_microvm_network { + BoundSlotNetworkReadback, slot_network_readback, slot_network_subject, SlotNetworkSubject, + slot_network_sanitation_subject, SanitationSubjectResult, SanitationSubjectAdmitted, SanitationSubjectRefused, + SlotNetworkReadings, TapReading, TapIpv6Reading, SlotResidueReading, HostResidueReading, RulesetReading, + TapPresentUnheld, TapHeld, TapIpv6Disabled, ResidueAbsent, RulesetListed, + ConvergedSlot, ConvergedSlotNetwork, HelperStanding, AutoAssignmentAbsentFromKernel, + runner_slot_network, runner_slot_host_cidr, +} +import gunbc.runner_attempt_launch { GroundClear, GroundOccupied } +import gunbc.runner_microvm_cell_readiness { + CellReadinessRecord, CellAttemptInFlight, CellSettled, + CellReadinessStoreRead, StoreRead, StoreUnreadable, StoreRootOwned, StoreNotRootOwned, + CellIncarnationAdmission, CellIncarnationAdmitted, CellRecoveryRequired, CellWithdrawn, + HostWithdrawn, HostStoreUnreadable, HostStoreNotRootOwned, HostStoreAmbiguous, HostStoreRecordIncoherent, + CellNeverSettled, CellQuarantinedAt, CellGenerationMismatch, + CellReadinessWrite, WriteAttemptStarted, WriteReadbackSettled, WriteUnattributedResidue, + CellReadinessWriteResult, WriteAccepted, WriteRefusedStale, WriteRefusedWouldLoosenQuarantine, + WriteRefusedAttemptMismatch, WriteRefusedAttemptAlreadyRecorded, WriteRefusedNotAdmitted, + WriteRefusedRecoveryOwed, WriteUnattributedResidue, + cell_incarnation_admission, apply_cell_readiness_write, + InFlightAttempt, CellBoundAttempt, AttemptBoundToCell, bind_attempt_to_cell, +} +import gunbc.runner_microvm_lifecycle { + AttemptIdentity, + ControllerStart, StartAttempt, StartRecovery, StartQuarantineUnattributedResidue, StartRefused, StartBindingRefused, controller_start, + CellBinding, CellBindingRefusedCell, + BringUpPhase, AttemptPrepared, VmmStarted, GuestBooted, RunnerListening, SlotServing, + BringUpEvent, BringUpTransition, BringUpAdvanced, BringUpRefusedForeignIncarnation, + BringUpRefusedOutOfOrder, advance_bring_up, + TerminalTrigger, VmmExited, RunnerExited, ControllerLost, ResourcesFoundOnRecovery, StopRequested, + StopAdmission, StopAdmitted, StopRefusedStaleIncarnation, stop_request_admission, + TeardownStop, StoppedGracefully, StoppedByForce, ForceStopBoundExceeded, + CgroupSubtreeReadback, CgroupSubtreeEmpty, CgroupSubtreePopulated, CgroupSubtreeReadFailed, + ResourceReadback, ResourceAbsent, ResourcePresent, + SubjectSlotNetwork, + ObservedTeardown, ObservedStop, ObservedCgroup, ObservedPath, TeardownSettlement, + TeardownReadbackBinding, TeardownReadbackBound, TeardownReadbackForeignSubject, TeardownSubject, + SubjectInvocation, attempt_teardown_readback, settle_teardown, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data witness_slot: RunnerSlotIdentity = RunnerSlotIdentity { host: operator_host_srv2, slot_index: 4 } + +// THE CELL IS DERIVED FROM THE SAME SLOT THE IDENTITIES ARE BUILT ON, so every admission below that +// names `cell` is the identity's own cell and the cell join in controller_start is exercised, not +// assumed. `other_cell` is a different slot on the same host. +data cell: CellId = runner_slot_instance_name(slot: witness_slot) as CellId + +data other_slot: RunnerSlotIdentity = RunnerSlotIdentity { host: operator_host_srv2, slot_index: 5 } + +data other_cell: CellId = runner_slot_instance_name(slot: other_slot) as CellId + +// The identity goes through the sealed microvm_attempt constructor; a refusal there yields no +// identity, so every test below that needs one fails rather than passing on a fabricated record. +fn identity(generation: Int, invocation: String) -> AttemptIdentity? { + identity_on(slot: witness_slot, generation: generation, invocation: invocation) +} + +fn identity_on(slot: RunnerSlotIdentity, generation: Int, invocation: String) -> AttemptIdentity? { + match microvm_attempt(slot: slot, attempt_id: join(["w-", to_string(generation)], "")) { + MicroVmAttemptAccepted { attempt: a } => + Present { + value: AttemptIdentity { + attempt: a, + allocation_generation: generation, + invocation_id: invocation as NonEmptyStr, + jit_registration_id: "reg-1" as NonEmptyStr, + guest_image: gunbc_runner_guest_image, + }, + } + _ => none + } +} + +// WHAT THE HOST READ, WITHOUT ITS SUBJECTS. observed_for attaches the subjects the host would read for +// a given attempt -- its host, generation, VMM unit, InvocationID, cgroup root, jail, attempt +// directory and credential drive -- so a test can present one attempt's readback for another. +type HostFacts { + stop: TeardownStop + cgroup: CgroupSubtreeReadback + mounts: ResourceReadback + network: BoundSlotNetworkReadback + attempt_storage: ResourceReadback + credential_disk: ResourceReadback +} + +// THE SLOT-NETWORK READBACK IS OBTAINED THROUGH ITS OWN FOLD, never assembled: BoundSlotNetworkReadback +// is sealed, so a fixture that could build one directly would exercise a path production cannot reach. +// A refused subject yields none, so a claim can never pass by the readback being skipped. +data converged_generation: Int = 7 + +data converged_digest: Sha256Digest = Sha256Digest { + hex: "1111111111111111111111111111111111111111111111111111111111111111" as Sha256DigestHex, +} + +fn converged_slot_row(slot: RunnerSlotIdentity) -> ConvergedSlot { + let net = runner_slot_network(slot: slot) + ConvergedSlot { + subject: slot_network_subject(slot: slot), + host_address_cidr: runner_slot_host_cidr(net: net) as NonEmptyStr, + guest_route: join([runner_slot_host_cidr(net: net), " dev ", net.tap_device as String], "") as NonEmptyStr, + tap_ipv6: TapIpv6Disabled, + } +} + +fn witness_receipt() -> ConvergedSlotNetwork { + ConvergedSlotNetwork { + host: operator_host_srv2, + generation: converged_generation, + slots: [converged_slot_row(slot: witness_slot), converged_slot_row(slot: other_slot)], + helpers: HelperStanding { + auto_assignment: AutoAssignmentAbsentFromKernel { kernel_release: "6.8.0-138-generic" as NonEmptyStr }, + nft_ct_helper_statements: 0, + xtables_ct_helper_targets: 0, + userspace_helpers: 0, + expectations_at_generation: 0, + }, + nft_digest: converged_digest, + } +} + +fn quiet_readings(slot: RunnerSlotIdentity) -> SlotNetworkReadings { + SlotNetworkReadings { + tap: TapReading { subject: slot_network_subject(slot: slot), observation: TapPresentUnheld }, + tap_ipv6: TapIpv6Reading { subject: slot_network_subject(slot: slot), observation: TapIpv6Disabled }, + guest_originated_conntrack: SlotResidueReading { subject: slot_network_subject(slot: slot), observation: ResidueAbsent }, + guest_destined_conntrack: SlotResidueReading { subject: slot_network_subject(slot: slot), observation: ResidueAbsent }, + guest_neighbour: SlotResidueReading { subject: slot_network_subject(slot: slot), observation: ResidueAbsent }, + expectations: HostResidueReading { host: operator_host_srv2, generation: converged_generation, observation: ResidueAbsent }, + ruleset: RulesetReading { host: operator_host_srv2, generation: converged_generation, observation: RulesetListed { digest: converged_digest } }, + } +} + +fn held_tap_readings(slot: RunnerSlotIdentity) -> SlotNetworkReadings { + SlotNetworkReadings { + tap: TapReading { subject: slot_network_subject(slot: slot), observation: TapHeld { holders: 1 } }, + tap_ipv6: quiet_readings(slot: slot).tap_ipv6, + guest_originated_conntrack: quiet_readings(slot: slot).guest_originated_conntrack, + guest_destined_conntrack: quiet_readings(slot: slot).guest_destined_conntrack, + guest_neighbour: quiet_readings(slot: slot).guest_neighbour, + expectations: quiet_readings(slot: slot).expectations, + ruleset: quiet_readings(slot: slot).ruleset, + } +} + +fn network_readback(slot: RunnerSlotIdentity, readings: SlotNetworkReadings) -> BoundSlotNetworkReadback? { + match slot_network_sanitation_subject(slot: slot, receipt: witness_receipt()) { + SanitationSubjectAdmitted { subject: s } => Present { value: slot_network_readback(s: s, readings: readings) } + SanitationSubjectRefused { refusal: _ } => none + } +} + +fn clean_host(stop: TeardownStop, cgroup: CgroupSubtreeReadback) -> HostFacts? { + match quiet_network() { + Absent => none + Present { value: n } => Present { value: clean_host_with(stop: stop, cgroup: cgroup, network: n) } + } +} + +fn clean_host_with(stop: TeardownStop, cgroup: CgroupSubtreeReadback, network: BoundSlotNetworkReadback) -> HostFacts { + HostFacts { + stop: stop, + cgroup: cgroup, + mounts: ResourceAbsent, + network: network, + attempt_storage: ResourceAbsent, + credential_disk: ResourceAbsent, + } +} + +// A quiet slot network read for the witness slot, through the real fold. Absent if the subject is +// refused, which no test below tolerates. +fn quiet_network() -> BoundSlotNetworkReadback? { + network_readback(slot: witness_slot, readings: quiet_readings(slot: witness_slot)) +} + +fn in_flight(id: AttemptIdentity) -> InFlightAttempt { + InFlightAttempt { attempt: id.attempt, invocation_id: id.invocation_id, jit_registration_id: id.jit_registration_id } +} + +fn bound_of(id: AttemptIdentity) -> CellBoundAttempt? { + match bind_attempt_to_cell(cell: runner_slot_instance_name(slot: id.attempt.slot) as CellId, generation: id.allocation_generation, attempt: in_flight(id: id)) { + AttemptBoundToCell { bound: b } => Present { value: b } + _ => none + } +} + +fn observed_for(id: AttemptIdentity, facts: HostFacts) -> ObservedTeardown { + ObservedTeardown { + host: id.attempt.slot.host as String, + generation: id.allocation_generation, + stop: ObservedStop { unit: runner_microvm_attempt_unit_name(attempt: id.attempt), invocation_id: id.invocation_id, outcome: facts.stop }, + cgroup: ObservedCgroup { root: fabric_cell_slice_name(slot: id.attempt.slot) as NonEmptyStr, readback: facts.cgroup }, + mounts: ObservedPath { path: runner_microvm_attempt_jail_base(attempt: id.attempt), readback: facts.mounts }, + attempt_storage: ObservedPath { path: runner_microvm_attempt_dir(attempt: id.attempt), readback: facts.attempt_storage }, + credential_disk: ObservedPath { path: runner_microvm_attempt_jit_drive_path(attempt: id.attempt), readback: facts.credential_disk }, + network: facts.network, + } +} + +// Settlement through the real route: bind, join the readback's subjects, settle. Absent if either the +// binding or the join refuses, so a test expecting a settlement fails rather than passing on a skip. +fn settle(id: AttemptIdentity, trigger: TerminalTrigger, facts: HostFacts?) -> TeardownSettlement? { + match facts { + Absent => none + Present { value: f } => settle_facts(id: id, trigger: trigger, facts: f) + } +} + +fn settle_facts(id: AttemptIdentity, trigger: TerminalTrigger, facts: HostFacts) -> TeardownSettlement? { + match bound_of(id: id) { + Absent => none + Present { value: b } => + match attempt_teardown_readback(bound: b, observed: observed_for(id: id, facts: facts)) { + TeardownReadbackBound { readback: r } => Present { value: settle_teardown(readback: r, trigger: trigger) } + _ => none + } + } +} + +// attempt_teardown_readback over an optional fixture: Absent facts yield a refusal that no test +// below accepts, so a skipped readback cannot read as a pass. +fn teardown_binding(bound: CellBoundAttempt, id: AttemptIdentity, facts: HostFacts?) -> TeardownReadbackBinding { + match facts { + Absent => TeardownReadbackForeignSubject { subject: SubjectSlotNetwork, expected: "a readable fixture", observed: "no subject" } + Present { value: f } => attempt_teardown_readback(bound: bound, observed: observed_for(id: id, facts: f)) + } +} + +fn readiness_after(trigger: TerminalTrigger, host: HostFacts?) -> CellReadiness? { + match identity(generation: 1, invocation: "inv-a") { + Absent => none + Present { value: id } => + match settle(id: id, trigger: trigger, facts: host) { + Absent => none + Present { value: st } => Present { value: st.readiness } + } + } +} + +fn is_quarantined(r: CellReadiness?) -> Bool { + match r { + Present { value: CellQuarantined { cell: _, unproven: _ } } => true + _ => false + } +} + +fn is_ready(r: CellReadiness?) -> Bool { + match r { + Present { value: CellReady { cell: _ } } => true + _ => false + } +} + +// THE POSITIVE CONTROL: a graceful stop and a host readback confirming every resource absent returns +// the cell. Without it every quarantine below would be satisfied by a controller that quarantines +// everything. +test fn a_clean_host_readback_returns_the_cell() -> Bool { + is_ready(r: readiness_after(trigger: RunnerExited { exit_code: 0 }, host: clean_host(stop: StoppedGracefully, cgroup: CgroupSubtreeEmpty))) +} + +// A CHILD IGNORING SIGTERM is not a dirty cell by itself: the bounded force-stop is what it is for. +// The cell returns ONLY because the host then reads the subtree empty. +test fn a_sigterm_ignoring_child_is_force_stopped_and_the_cell_returns_only_on_an_empty_readback() -> Bool { + is_ready(r: readiness_after(trigger: StopRequested, host: clean_host(stop: StoppedByForce, cgroup: CgroupSubtreeEmpty))) + && is_quarantined(r: readiness_after(trigger: StopRequested, host: clean_host(stop: StoppedByForce, cgroup: CgroupSubtreePopulated { pids: [4242], cgroups: ["srv2-04.slice" as NonEmptyStr] }))) +} + +// A DOUBLE-FORK moves the survivor into a child cgroup; the recursive readback still finds it. +test fn a_double_forked_survivor_in_a_child_cgroup_quarantines() -> Bool { + is_quarantined(r: readiness_after( + trigger: VmmExited { exit_code: 0 }, + host: clean_host(stop: StoppedGracefully, cgroup: CgroupSubtreePopulated { pids: [5151], cgroups: ["srv2-04.slice/escape.scope" as NonEmptyStr] }), + )) +} + +// AN UNKILLABLE TASK quarantines on the stop outcome even when the cgroup listing reads empty +// afterwards -- the listing is a later instant, and the task that outlived SIGKILL is the fact. +test fn an_unkillable_task_quarantines_even_if_the_listing_later_reads_empty() -> Bool { + is_quarantined(r: readiness_after(trigger: StopRequested, host: clean_host(stop: ForceStopBoundExceeded { survivors: [777] }, cgroup: CgroupSubtreeEmpty))) +} + +// A FAILED CGROUP READ QUARANTINES, and the quarantine is never released by a later Ready readback +// at the same generation: that would be "could not read" converted into "empty" one write later. +test fn a_failed_cgroup_read_quarantines_and_is_never_released_at_its_generation() -> Bool { + match identity(generation: 1, invocation: "inv-a") { + Absent => false + Present { value: id } => + match settle(id: id, trigger: ControllerLost, facts: clean_host(stop: StoppedGracefully, cgroup: CgroupSubtreeReadFailed { reason: "cgroup.procs: EIO" as NonEmptyStr })) { + Absent => false + Present { value: failed } => + match settle(id: id, trigger: ControllerLost, facts: clean_host(stop: StoppedGracefully, cgroup: CgroupSubtreeEmpty)) { + Absent => false + Present { value: clean } => { + let started = [CellAttemptInFlight { cell: cell, generation: 1, attempt: in_flight(id: id) }] + match apply_cell_readiness_write(records: started, write: failed.record) { + WriteAccepted { records: after_failed } => + !cell_is_ready(readiness: failed.readiness) + && match apply_cell_readiness_write(records: after_failed, write: clean.record) { + WriteRefusedWouldLoosenQuarantine { cell: _, generation: _ } => true + _ => false + } + && match cell_incarnation_admission(store: StoreRead { ownership: StoreRootOwned, records: after_failed }, cell: cell, allocation_generation: 2) { + CellWithdrawn { cell: _, withdrawal: CellQuarantinedAt { generation: _, unproven: _ } } => true + _ => false + } + _ => false + } + } + } + } + } +} + +// A SUCCESSFUL JOB LEAVING A BACKGROUND PROCESS: the runner's exit 0 has no route to the verdict. +test fn a_successful_job_that_leaves_a_background_process_quarantines() -> Bool { + is_quarantined(r: readiness_after( + trigger: RunnerExited { exit_code: 0 }, + host: clean_host(stop: StoppedGracefully, cgroup: CgroupSubtreePopulated { pids: [9001], cgroups: ["srv2-04.slice" as NonEmptyStr] }), + )) +} + +// EACH FACT IS ITS OWN: a slot tap still held after the VMM is gone quarantines a cell whose cgroup is empty. +test fn a_held_slot_tap_quarantines_a_cell_with_no_processes() -> Bool { + match network_readback(slot: witness_slot, readings: held_tap_readings(slot: witness_slot)) { + Absent => false + Present { value: held } => + is_quarantined(r: readiness_after( + trigger: RunnerExited { exit_code: 0 }, + host: Present { value: clean_host_with(stop: StoppedGracefully, cgroup: CgroupSubtreeEmpty, network: held) }, + )) + } +} + +// A STOP FOR A PREVIOUS INCARNATION IS REFUSED, and the same stop for the live one is admitted. +test fn a_stale_incarnation_stop_is_refused() -> Bool { + match identity(generation: 2, invocation: "inv-b") { + Absent => false + Present { value: live } => + match identity(generation: 1, invocation: "inv-a") { + Absent => false + Present { value: stale } => + match stop_request_admission(live: live, requested: stale) { + StopRefusedStaleIncarnation { live_generation: 2, requested_generation: 1 } => true + _ => false + } + && match stop_request_admission(live: live, requested: live) { + StopAdmitted { trigger: StopRequested } => true + _ => false + } + } + } +} + +// A STALE READBACK CANNOT CLEAR A NEWER QUARANTINE: generation 1's Ready arriving after generation +// 2 quarantined is refused by the store, not trusted by the controller. +test fn a_stale_readback_cannot_clear_a_newer_quarantine() -> Bool { + let newer = [CellSettled { cell: cell, generation: 2, readiness: CellQuarantined { cell: cell, unproven: [] } }] + match identity(generation: 1, invocation: "inv-old") { + Absent => false + Present { value: old } => + match settle(id: old, trigger: StopRequested, facts: clean_host(stop: StoppedGracefully, cgroup: CgroupSubtreeEmpty)) { + Absent => false + Present { value: st } => + match apply_cell_readiness_write(records: newer, write: st.record) { + WriteRefusedStale { cell: _, stored: 2, offered: 1 } => true + _ => false + } + } + } +} + +// AN UNREADABLE OR NON-ROOT STORE WITHDRAWS THE HOST, not the cell -- including a cell whose record +// would otherwise admit. +test fn an_unreadable_or_foreign_owned_store_withdraws_the_host() -> Bool { + let ready = [CellSettled { cell: cell, generation: 0, readiness: CellReady { cell: cell } }] + let admits = match cell_incarnation_admission(store: StoreRead { ownership: StoreRootOwned, records: ready }, cell: cell, allocation_generation: 1) { + CellIncarnationAdmitted { cell: _, generation: 1 } => true + _ => false + } + let unreadable = match cell_incarnation_admission(store: StoreUnreadable { reason: "EACCES" as NonEmptyStr }, cell: cell, allocation_generation: 1) { + HostWithdrawn { withdrawal: HostStoreUnreadable { reason: _ } } => true + _ => false + } + let foreign = match cell_incarnation_admission(store: StoreRead { ownership: StoreNotRootOwned { owner_uid: 1000, mode: "0666" as NonEmptyStr }, records: ready }, cell: cell, allocation_generation: 1) { + HostWithdrawn { withdrawal: HostStoreNotRootOwned { owner_uid: 1000, mode: _ } } => true + _ => false + } + let ambiguous = match cell_incarnation_admission(store: StoreRead { ownership: StoreRootOwned, records: concat(ready, ready) }, cell: cell, allocation_generation: 1) { + HostWithdrawn { withdrawal: HostStoreAmbiguous { cell: _ } } => true + _ => false + } + admits && unreadable && foreign && ambiguous +} + +// A CELL NEVER SETTLED, AND A GENERATION THAT SKIPS, ARE CELL-GRAIN WITHDRAWALS. +test fn a_never_settled_or_skipped_generation_withdraws_the_cell() -> Bool { + let never = match cell_incarnation_admission(store: StoreRead { ownership: StoreRootOwned, records: [] }, cell: cell, allocation_generation: 1) { + CellWithdrawn { cell: _, withdrawal: CellNeverSettled } => true + _ => false + } + let skipped = match cell_incarnation_admission(store: StoreRead { ownership: StoreRootOwned, records: [CellSettled { cell: cell, generation: 0, readiness: CellReady { cell: cell } }] }, cell: cell, allocation_generation: 3) { + CellWithdrawn { cell: _, withdrawal: CellGenerationMismatch { settled: 0, allocated: 3 } } => true + _ => false + } + never && skipped +} + +// BOOT RECOVERY RESUMES CLEANUP BEFORE ADMISSION: an in-flight record yields a recovery start, its +// settlement is accepted by the store, and only then does the next generation admit. +test fn boot_recovery_settles_the_lost_attempt_before_the_next_admission() -> Bool { + match identity(generation: 2, invocation: "inv-c") { + Absent => false + Present { value: next } => + match identity(generation: 1, invocation: "inv-lost") { + Absent => false + Present { value: lost_id } => { + let lost = [CellAttemptInFlight { cell: cell, generation: 1, attempt: in_flight(id: lost_id) }] + let admission = cell_incarnation_admission(store: StoreRead { ownership: StoreRootOwned, records: lost }, cell: cell, allocation_generation: 2) + match controller_start(admission: admission, ground: GroundClear, identity: next) { + StartRecovery { bound: b, trigger: ControllerLost } => + match teardown_binding(bound: b, id: lost_id, facts: clean_host(stop: StoppedGracefully, cgroup: CgroupSubtreeEmpty)) { + TeardownReadbackBound { readback: r } => + match apply_cell_readiness_write(records: lost, write: settle_teardown(readback: r, trigger: ControllerLost).record) { + WriteAccepted { records: settled } => + match controller_start( + admission: cell_incarnation_admission(store: StoreRead { ownership: StoreRootOwned, records: settled }, cell: cell, allocation_generation: 2), + ground: GroundClear, + identity: next, + ) { + StartAttempt { bound: _, record: _ } => true + _ => false + } + _ => false + } + _ => false + } + _ => false + } + } + } + } +} + +// RESOURCES FOUND ON AN ADMITTED CELL OUTRANK THE RECORD, AND THE RESIDUE IS NOT GIVEN AN IDENTITY. +// The old arm wrote the cell's name as an attempt at generation g - 1 (review on #11670). Now the +// controller records an unattributed quarantine at the generation that was about to run, the store +// accepts it over the Ready record, and the next admission is withdrawn, not admitted. +test fn unattributed_residue_quarantines_at_the_admitted_generation_without_an_invented_attempt() -> Bool { + match identity(generation: 1, invocation: "inv-first") { + Absent => false + Present { value: id } => + match controller_start(admission: CellIncarnationAdmitted { cell: cell, generation: 1 }, ground: GroundOccupied, identity: id) { + StartQuarantineUnattributedResidue { trigger: ResourcesFoundOnRecovery, record: w } => + match w { + WriteUnattributedResidue { cell: _, generation: g } => + g == 1 + && match apply_cell_readiness_write(records: [CellSettled { cell: cell, generation: 0, readiness: CellReady { cell: cell } }], write: w) { + WriteAccepted { records: after } => + match cell_incarnation_admission(store: StoreRead { ownership: StoreRootOwned, records: after }, cell: cell, allocation_generation: 2) { + CellWithdrawn { cell: _, withdrawal: CellQuarantinedAt { generation: q, unproven: u } } => q == 1 && (u |> count) == 6 + _ => false + } + _ => false + } + _ => false + } + _ => false + } + } +} + +// AN ATTEMPT START IS REFUSED BY THE STORE OVER A QUARANTINE, whatever generation it names. +test fn the_store_refuses_to_record_a_start_over_a_quarantine() -> Bool { + let q = [CellSettled { cell: cell, generation: 1, readiness: CellQuarantined { cell: cell, unproven: [] } }] + match identity(generation: 2, invocation: "inv-x") { + Absent => false + Present { value: id } => + match bound_of(id: id) { + Absent => false + Present { value: b } => + match apply_cell_readiness_write(records: q, write: WriteAttemptStarted { bound: b }) { + WriteRefusedNotAdmitted { cell: _, admission: CellWithdrawn { cell: _, withdrawal: CellQuarantinedAt { generation: 1, unproven: _ } } } => true + _ => false + } + } + } +} + +// BRING-UP ADVANCES ONE OBSERVED STEP AT A TIME, and refuses a skipped step and a foreign incarnation. +test fn bring_up_refuses_a_skipped_phase_and_a_foreign_incarnation() -> Bool { + match identity(generation: 1, invocation: "inv-a") { + Absent => false + Present { value: live } => + match identity(generation: 0, invocation: "inv-z") { + Absent => false + Present { value: foreign } => { + let steps = match advance_bring_up(live: live, at: AttemptPrepared, event: BringUpEvent { identity: live, reached: VmmStarted }) { + BringUpAdvanced { phase: VmmStarted } => true + _ => false + } && match advance_bring_up(live: live, at: RunnerListening, event: BringUpEvent { identity: live, reached: SlotServing }) { + BringUpAdvanced { phase: SlotServing } => true + _ => false + } + let skip = match advance_bring_up(live: live, at: VmmStarted, event: BringUpEvent { identity: live, reached: RunnerListening }) { + BringUpRefusedOutOfOrder { from: VmmStarted, to: RunnerListening } => true + _ => false + } + let other = match advance_bring_up(live: live, at: AttemptPrepared, event: BringUpEvent { identity: foreign, reached: VmmStarted }) { + BringUpRefusedForeignIncarnation => true + _ => false + } + steps && skip && other + } + } + } +} + +// AN ADMISSION FOR ONE CELL CANNOT START AN IDENTITY BOUND TO ANOTHER, even at the same generation, +// and not by either start arm: the launch and the unattributed quarantine both require the join. +test fn an_admission_for_one_cell_does_not_start_an_identity_of_another() -> Bool { + match identity(generation: 1, invocation: "inv-a") { + Absent => false + Present { value: id } => { + let clear = match controller_start(admission: CellIncarnationAdmitted { cell: other_cell, generation: 1 }, ground: GroundClear, identity: id) { + StartBindingRefused { binding: CellBindingRefusedCell { admitted: _, identity_cell: _ } } => true + _ => false + } + let occupied = match controller_start(admission: CellIncarnationAdmitted { cell: other_cell, generation: 1 }, ground: GroundOccupied, identity: id) { + StartBindingRefused { binding: CellBindingRefusedCell { admitted: _, identity_cell: _ } } => true + _ => false + } + let own = match controller_start(admission: CellIncarnationAdmitted { cell: cell, generation: 1 }, ground: GroundClear, identity: id) { + StartAttempt { bound: _, record: _ } => true + _ => false + } + clear && occupied && own + } + } +} + +// HOST GRAIN IS A PROPERTY OF THE STORE: a duplicate record for ANOTHER cell, or a settled record whose +// readiness names a different cell than its key, withdraws the host for this cell too -- whose own +// record reads Ready and would otherwise admit. +test fn a_defect_in_another_cells_records_withdraws_this_cell() -> Bool { + let mine = CellSettled { cell: cell, generation: 0, readiness: CellReady { cell: cell } } + let theirs = CellSettled { cell: other_cell, generation: 3, readiness: CellReady { cell: other_cell } } + let duplicate = match cell_incarnation_admission(store: StoreRead { ownership: StoreRootOwned, records: [mine, theirs, theirs] }, cell: cell, allocation_generation: 1) { + HostWithdrawn { withdrawal: HostStoreAmbiguous { cell: c } } => (c as String) == (other_cell as String) + _ => false + } + let incoherent = match cell_incarnation_admission( + store: StoreRead { ownership: StoreRootOwned, records: [mine, CellSettled { cell: other_cell, generation: 3, readiness: CellReady { cell: cell } }] }, + cell: cell, + allocation_generation: 1, + ) { + HostWithdrawn { withdrawal: HostStoreRecordIncoherent { record_cell: _, named_cell: _ } } => true + _ => false + } + let sound = match cell_incarnation_admission(store: StoreRead { ownership: StoreRootOwned, records: [mine, theirs] }, cell: cell, allocation_generation: 1) { + CellIncarnationAdmitted { cell: _, generation: _ } => true + _ => false + } + duplicate && incoherent && sound +} + +// A RECOVERY RECORD IS BOUND TO ITS CELL AT READ: an in-flight record keyed for this cell but carrying +// an attempt built on another slot is an unsound store, never a recovery -- recovering it would tear +// down and settle the other cell's attempt under this cell's key. +test fn a_recovery_record_carrying_another_cells_attempt_never_recovers() -> Bool { + match identity_on(slot: other_slot, generation: 1, invocation: "inv-b") { + Absent => false + Present { value: foreign } => + match identity(generation: 2, invocation: "inv-next") { + Absent => false + Present { value: next } => { + let admission = cell_incarnation_admission( + store: StoreRead { ownership: StoreRootOwned, records: [CellAttemptInFlight { cell: cell, generation: 1, attempt: in_flight(id: foreign) }] }, + cell: cell, + allocation_generation: 2, + ) + let incoherent = match admission { + HostWithdrawn { withdrawal: HostStoreRecordIncoherent { record_cell: rc, named_cell: nc } } => + (rc as String) == (cell as String) && (nc as String) == (other_cell as String) + _ => false + } + let no_recovery = match controller_start(admission: admission, ground: GroundClear, identity: next) { + StartRecovery { bound: _, trigger: _ } => false + _ => true + } + incoherent && no_recovery + } + } + } +} + +// TEARDOWN EVIDENCE FOR ONE ATTEMPT CANNOT SETTLE ANOTHER. A clean readback of cell A's attempt +// presented for cell B's is refused at the join, and so is a clean readback of this cell's attempt +// taken under a different controller incarnation; only the attempt's own readback binds. +test fn a_clean_readback_of_one_attempt_cannot_settle_another() -> Bool { + match identity(generation: 1, invocation: "inv-a") { + Absent => false + Present { value: a } => + match identity_on(slot: other_slot, generation: 1, invocation: "inv-a") { + Absent => false + Present { value: b } => + match identity(generation: 1, invocation: "inv-other") { + Absent => false + Present { value: a_other_incarnation } => + match bound_of(id: b) { + Absent => false + Present { value: bound_b } => + match bound_of(id: a) { + Absent => false + Present { value: bound_a } => { + let clean = clean_host(stop: StoppedGracefully, cgroup: CgroupSubtreeEmpty) + let cross_cell = match teardown_binding(bound: bound_b, id: a, facts: clean) { + TeardownReadbackForeignSubject { subject: _, expected: _, observed: _ } => true + _ => false + } + let cross_incarnation = match teardown_binding(bound: bound_a, id: a_other_incarnation, facts: clean) { + TeardownReadbackForeignSubject { subject: SubjectInvocation, expected: _, observed: _ } => true + _ => false + } + let own = match teardown_binding(bound: bound_a, id: a, facts: clean) { + TeardownReadbackBound { readback: _ } => true + _ => false + } + cross_cell && cross_incarnation && own + } + } + } + } + } + } +} + +// AN IN-FLIGHT RECORD IS NOT OVERWRITTEN BY ANYTHING BUT ITS OWN SETTLEMENT (review 68576). A clean +// readback of a later generation's attempt, and an unattributed-residue quarantine, both refuse over +// "cleanup owed"; the lost attempt's own settlement at its generation is accepted. +test fn an_in_flight_record_is_discharged_only_by_its_own_attempts_settlement() -> Bool { + match identity(generation: 1, invocation: "inv-lost") { + Absent => false + Present { value: lost } => + match identity(generation: 2, invocation: "inv-later") { + Absent => false + Present { value: later } => { + let owed = [CellAttemptInFlight { cell: cell, generation: 1, attempt: in_flight(id: lost) }] + let clean = clean_host(stop: StoppedGracefully, cgroup: CgroupSubtreeEmpty) + let later_refused = match settle(id: later, trigger: StopRequested, facts: clean) { + Present { value: st } => + match apply_cell_readiness_write(records: owed, write: st.record) { + WriteRefusedRecoveryOwed { cell: _, in_flight_generation: 1, in_flight_attempt: _ } => true + _ => false + } + Absent => false + } + let residue_refused = match apply_cell_readiness_write(records: owed, write: WriteUnattributedResidue { cell: cell, generation: 2 }) { + WriteRefusedRecoveryOwed { cell: _, in_flight_generation: 1, in_flight_attempt: _ } => true + _ => false + } + let own_accepted = match settle(id: lost, trigger: ControllerLost, facts: clean) { + Present { value: st } => + match apply_cell_readiness_write(records: owed, write: st.record) { + WriteAccepted { records: _ } => true + _ => false + } + Absent => false + } + later_refused && residue_refused && own_accepted + } + } + } +} + +// THE SLOT NETWORK READBACK IS JOINED BY SLOT LIKE EVERY OTHER SUBJECT (side-chat ruling on #11670). +// A quiet readback taken for another slot cannot settle this attempt, even though every other subject +// in the bundle is this attempt's; and the attempt's own quiet readback still binds. +test fn a_slot_network_readback_for_another_slot_cannot_settle_this_attempt() -> Bool { + match identity(generation: 1, invocation: "inv-a") { + Absent => false + Present { value: id } => + match bound_of(id: id) { + Absent => false + Present { value: b } => + match network_readback(slot: other_slot, readings: quiet_readings(slot: other_slot)) { + Absent => false + Present { value: foreign } => + match quiet_network() { + Absent => false + Present { value: own } => { + let refused = match attempt_teardown_readback( + bound: b, + observed: observed_for(id: id, facts: clean_host_with(stop: StoppedGracefully, cgroup: CgroupSubtreeEmpty, network: foreign)), + ) { + TeardownReadbackForeignSubject { subject: SubjectSlotNetwork, expected: _, observed: _ } => true + _ => false + } + let bound_own = match attempt_teardown_readback( + bound: b, + observed: observed_for(id: id, facts: clean_host_with(stop: StoppedGracefully, cgroup: CgroupSubtreeEmpty, network: own)), + ) { + TeardownReadbackBound { readback: _ } => true + _ => false + } + refused && bound_own + } + } + } + } + } +} diff --git a/dag/test/claim/runner/runner_microvm_witness_test.dag b/dag/test/claim/runner/runner_microvm_witness_test.dag index a1001b24b06..dfdc3c9fc2c 100644 --- a/dag/test/claim/runner/runner_microvm_witness_test.dag +++ b/dag/test/claim/runner/runner_microvm_witness_test.dag @@ -10,6 +10,15 @@ import product.fabric.isolation { } import extdeps.systemd.unit_file { ExitTypeMain, ExitTypeCgroup, KillModeControlGroup, KillModeProcess } import gunbc.runner_unit { RunnerUnitLifecycleIntent } +import gunbc.build_cache_instance { RunnerSlotIdentity, runner_slot_instance_name } +import gunbc.fleet_intent_network { operator_host_srv1 } +import gunbc.runner_microvm_attempt { MicroVmAttemptAccepted, microvm_attempt } +import product.fabric.sanitation { CellId, CellReady, CellQuarantined, FactNotObserved, CgroupEmpty } +import gunbc.runner_microvm_cell_readiness { + CellIncarnationAdmission, CellReadinessStoreRead, StoreRead, StoreUnreadable, StoreRootOwned, + CellSettled, CellAttemptInFlight, CellQuarantinedAt, HostStoreUnreadable, cell_incarnation_admission, + InFlightAttempt, +} import extdeps.virtualization.firecracker { firecracker_vcpu_range_v1_16_1, FirecrackerMachineConfig, @@ -49,6 +58,9 @@ import gunbc.runner_microvm { RunnerMicroVmRefusedMalformedVm, RunnerMicroVmRefusedEnvelopeDisagreement, RunnerMicroVmRefusedEnvelopeUnresolved, + RunnerMicroVmRefusedHostWithdrawn, + RunnerMicroVmRefusedCellWithdrawn, + RunnerMicroVmRecoveryRequired, gunbc_runner_microvm_declared_size, RunnerMicroVmShape, RunnerMicroVmShapeResolution, @@ -130,6 +142,9 @@ fn admission_is_orphan_refusal(a: RunnerMicroVmAdmission) -> Bool { RunnerMicroVmRefusedMalformedVm { reason: _ } => false RunnerMicroVmRefusedEnvelopeDisagreement { reason: _ } => false RunnerMicroVmRefusedEnvelopeUnresolved { reason: _ } => false + RunnerMicroVmRefusedHostWithdrawn { withdrawal: _ } => false + RunnerMicroVmRefusedCellWithdrawn { cell: _, withdrawal: _ } => false + RunnerMicroVmRecoveryRequired { bound: _ } => false } } @@ -141,6 +156,9 @@ fn admission_is_credential_refusal(a: RunnerMicroVmAdmission) -> Bool { RunnerMicroVmRefusedMalformedVm { reason: _ } => false RunnerMicroVmRefusedEnvelopeDisagreement { reason: _ } => false RunnerMicroVmRefusedEnvelopeUnresolved { reason: _ } => false + RunnerMicroVmRefusedHostWithdrawn { withdrawal: _ } => false + RunnerMicroVmRefusedCellWithdrawn { cell: _, withdrawal: _ } => false + RunnerMicroVmRecoveryRequired { bound: _ } => false } } @@ -152,6 +170,9 @@ fn admission_is_envelope_refusal(a: RunnerMicroVmAdmission) -> Bool { RunnerMicroVmRefusedSharedCredential { reason: _ } => false RunnerMicroVmRefusedMalformedVm { reason: _ } => false RunnerMicroVmRefusedEnvelopeUnresolved { reason: _ } => false + RunnerMicroVmRefusedHostWithdrawn { withdrawal: _ } => false + RunnerMicroVmRefusedCellWithdrawn { cell: _, withdrawal: _ } => false + RunnerMicroVmRecoveryRequired { bound: _ } => false } } @@ -168,6 +189,9 @@ fn admission_is_admitted(a: RunnerMicroVmAdmission) -> Bool { RunnerMicroVmRefusedMalformedVm { reason: _ } => false RunnerMicroVmRefusedEnvelopeDisagreement { reason: _ } => false RunnerMicroVmRefusedEnvelopeUnresolved { reason: _ } => false + RunnerMicroVmRefusedHostWithdrawn { withdrawal: _ } => false + RunnerMicroVmRefusedCellWithdrawn { cell: _, withdrawal: _ } => false + RunnerMicroVmRecoveryRequired { bound: _ } => false } } @@ -188,6 +212,9 @@ fn admission_refuses_naming_the_missing_reserve(a: RunnerMicroVmAdmission) -> Bo RunnerMicroVmRefusedSharedCredential { reason: _ } => false RunnerMicroVmRefusedMalformedVm { reason: _ } => false RunnerMicroVmRefusedEnvelopeDisagreement { reason: _ } => false + RunnerMicroVmRefusedHostWithdrawn { withdrawal: _ } => false + RunnerMicroVmRefusedCellWithdrawn { cell: _, withdrawal: _ } => false + RunnerMicroVmRecoveryRequired { bound: _ } => false } } @@ -199,6 +226,9 @@ fn admission_is_malformed_refusal(a: RunnerMicroVmAdmission) -> Bool { RunnerMicroVmRefusedSharedCredential { reason: _ } => false RunnerMicroVmRefusedEnvelopeDisagreement { reason: _ } => false RunnerMicroVmRefusedEnvelopeUnresolved { reason: _ } => false + RunnerMicroVmRefusedHostWithdrawn { withdrawal: _ } => false + RunnerMicroVmRefusedCellWithdrawn { cell: _, withdrawal: _ } => false + RunnerMicroVmRecoveryRequired { bound: _ } => false } } @@ -229,6 +259,7 @@ data exittype_cgroup_lifecycle_intent: RunnerUnitLifecycleIntent = RunnerUnitLif test fn orphanable_unit_refuses_the_microvm_migration() -> Bool { admission_is_orphan_refusal( a: runner_microvm_admission( + cell: witness_admitted_cell(), topology: VmmUnderLifecycleController, intent: deployed_lifecycle_intent, main_exits_when_incarnation_ends: true, @@ -244,6 +275,7 @@ test fn orphanable_unit_refuses_the_microvm_migration() -> Bool { test fn exittype_cgroup_unit_refuses_the_microvm_migration() -> Bool { admission_is_orphan_refusal( a: runner_microvm_admission( + cell: witness_admitted_cell(), topology: VmmUnderLifecycleController, intent: exittype_cgroup_lifecycle_intent, main_exits_when_incarnation_ends: true, @@ -259,6 +291,7 @@ test fn exittype_cgroup_unit_refuses_the_microvm_migration() -> Bool { test fn main_exit_teardown_admits_the_same_microvm() -> Bool { admission_is_admitted( a: runner_microvm_admission( + cell: witness_admitted_cell(), topology: VmmUnderLifecycleController, intent: repaired_lifecycle_intent, main_exits_when_incarnation_ends: true, @@ -276,6 +309,7 @@ test fn main_exit_teardown_admits_the_same_microvm() -> Bool { test fn shared_slot_directory_credential_is_refused() -> Bool { admission_is_credential_refusal( a: runner_microvm_admission( + cell: witness_admitted_cell(), topology: VmmUnderLifecycleController, intent: repaired_lifecycle_intent, main_exits_when_incarnation_ends: true, @@ -301,6 +335,7 @@ fn two_root_config() -> FirecrackerVmConfig { test fn two_root_devices_is_a_malformed_vm() -> Bool { admission_is_malformed_refusal( a: runner_microvm_admission( + cell: witness_admitted_cell(), topology: VmmUnderLifecycleController, intent: repaired_lifecycle_intent, main_exits_when_incarnation_ends: true, @@ -336,6 +371,7 @@ test fn microvm_provides_a_dedicated_kernel_and_the_current_slot_does_not() -> B test fn direct_exec_vmm_is_admitted_under_the_same_orphanable_intent() -> Bool { admission_is_admitted( a: runner_microvm_admission( + cell: witness_admitted_cell(), topology: VmmIsMainProcess, intent: deployed_lifecycle_intent, main_exits_when_incarnation_ends: true, @@ -352,6 +388,7 @@ test fn direct_exec_vmm_is_admitted_under_the_same_orphanable_intent() -> Bool { test fn topology_is_what_decides_and_it_decides_both_ways() -> Bool { admission_is_admitted( a: runner_microvm_admission( + cell: witness_admitted_cell(), topology: VmmIsMainProcess, intent: deployed_lifecycle_intent, main_exits_when_incarnation_ends: true, @@ -361,6 +398,7 @@ test fn topology_is_what_decides_and_it_decides_both_ways() -> Bool { ), ) && admission_is_orphan_refusal( a: runner_microvm_admission( + cell: witness_admitted_cell(), topology: VmmUnderLifecycleController, intent: deployed_lifecycle_intent, main_exits_when_incarnation_ends: true, @@ -376,6 +414,7 @@ test fn topology_is_what_decides_and_it_decides_both_ways() -> Bool { test fn direct_exec_still_refuses_the_shared_slot_credential() -> Bool { admission_is_credential_refusal( a: runner_microvm_admission( + cell: witness_admitted_cell(), topology: VmmIsMainProcess, intent: deployed_lifecycle_intent, main_exits_when_incarnation_ends: true, @@ -455,6 +494,7 @@ data witness_unmodeled_reserve: RealizationReserve = ReserveUnmodeled { test fn the_same_guest_is_refused_under_the_production_reserve() -> Bool { admission_refuses_naming_the_missing_reserve( a: runner_microvm_admission( + cell: witness_admitted_cell(), topology: VmmUnderLifecycleController, intent: repaired_lifecycle_intent, main_exits_when_incarnation_ends: true, @@ -484,6 +524,7 @@ fn config_with_machine(vcpus: Int, mib: Int) -> FirecrackerVmConfig { fn admission_of_machine(vcpus: Int, mib: Int) -> RunnerMicroVmAdmission { runner_microvm_admission( + cell: witness_admitted_cell(), topology: VmmUnderLifecycleController, intent: repaired_lifecycle_intent, main_exits_when_incarnation_ends: true, @@ -1244,3 +1285,103 @@ test fn a_guest_without_a_tap_carries_no_interface_and_one_with_a_tap_does() -> test fn the_cell_core_count_is_a_positive_policy() -> Bool { hardware_thread_count_value(t: gunbc_runner_cores_per_slot()) > 0 } + +// THE CELL ADMISSION EVERY OTHER CONTROL HERE RUNS UNDER, OBTAINED THROUGH THE REAL JOIN rather than +// constructed: a store holding a settled Ready at generation 0, asked for allocation generation 1. +fn witness_store(cell: String, readiness_ready: Bool) -> CellReadinessStoreRead { + StoreRead { + ownership: StoreRootOwned, + records: [ + CellSettled { + cell: cell as CellId, + generation: 0, + readiness: if readiness_ready { + CellReady { cell: cell as CellId } + } else { + CellQuarantined { cell: cell as CellId, unproven: [FactNotObserved { fact: CgroupEmpty }] } + }, + }, + ], + } +} + +fn witness_admitted_cell() -> CellIncarnationAdmission { + cell_incarnation_admission(store: witness_store(cell: "srv1-01", readiness_ready: true), cell: "srv1-01" as CellId, allocation_generation: 1) +} + +// A QUARANTINED CELL REFUSES AN OTHERWISE ADMISSIBLE VM, AND REFUSES WITH THE CELL'S CAUSE. The +// VM, intent and reserve are exactly those of the admitted controls, so the only thing this varies +// is the readiness the admission consumes -- the frontier #11662 declared here, now closed. +test fn a_quarantined_cell_refuses_an_otherwise_admissible_microvm() -> Bool { + let quarantined = runner_microvm_admission( + cell: cell_incarnation_admission(store: witness_store(cell: "srv1-01", readiness_ready: false), cell: "srv1-01" as CellId, allocation_generation: 1), + topology: VmmUnderLifecycleController, + intent: repaired_lifecycle_intent, + main_exits_when_incarnation_ends: true, + transport: JitConfigOnReadOnlyDrive { drive_id: "jitcfg" }, + config: mvp_sized_config(), + reserve: witness_reserve, + ) + let refused_with_cause = match quarantined { + RunnerMicroVmRefusedCellWithdrawn { cell: _, withdrawal: CellQuarantinedAt { generation: 0, unproven: _ } } => true + _ => false + } + refused_with_cause + && admission_is_admitted(a: runner_microvm_admission( + cell: witness_admitted_cell(), + topology: VmmUnderLifecycleController, + intent: repaired_lifecycle_intent, + main_exits_when_incarnation_ends: true, + transport: JitConfigOnReadOnlyDrive { drive_id: "jitcfg" }, + config: mvp_sized_config(), + reserve: witness_reserve, + )) +} + +// THE THREE NON-ADMITTING ARMS STAY DISTINCT THROUGH THE ADMISSION (review 68119): an unreadable +// store is a HOST refusal, an in-flight record is RECOVERY REQUIRED, and neither is the quarantine arm +// above. A collapse into one refusal would still pass the quarantine witness and fail this one. +test fn host_withdrawal_and_recovery_required_are_not_a_cell_refusal() -> Bool { + let host = match runner_microvm_admission( + cell: cell_incarnation_admission(store: StoreUnreadable { reason: "EACCES" as NonEmptyStr }, cell: "srv1-01" as CellId, allocation_generation: 1), + topology: VmmUnderLifecycleController, + intent: repaired_lifecycle_intent, + main_exits_when_incarnation_ends: true, + transport: JitConfigOnReadOnlyDrive { drive_id: "jitcfg" }, + config: mvp_sized_config(), + reserve: witness_reserve, + ) { + RunnerMicroVmRefusedHostWithdrawn { withdrawal: HostStoreUnreadable { reason: _ } } => true + _ => false + } + let lost_slot = RunnerSlotIdentity { host: operator_host_srv1, slot_index: 1 } + let lost_cell = runner_slot_instance_name(slot: lost_slot) as CellId + let recovery = match microvm_attempt(slot: lost_slot, attempt_id: "lost-0") { + MicroVmAttemptAccepted { attempt: lost } => + match runner_microvm_admission( + cell: cell_incarnation_admission( + store: StoreRead { + ownership: StoreRootOwned, + records: [CellAttemptInFlight { + cell: lost_cell, + generation: 0, + attempt: InFlightAttempt { attempt: lost, invocation_id: "inv-lost" as NonEmptyStr, jit_registration_id: "reg-lost" as NonEmptyStr }, + }], + }, + cell: lost_cell, + allocation_generation: 1, + ), + topology: VmmUnderLifecycleController, + intent: repaired_lifecycle_intent, + main_exits_when_incarnation_ends: true, + transport: JitConfigOnReadOnlyDrive { drive_id: "jitcfg" }, + config: mvp_sized_config(), + reserve: witness_reserve, + ) { + RunnerMicroVmRecoveryRequired { bound: _ } => true + _ => false + } + _ => false + } + host && recovery +}