diff --git a/dag/gunbc/auth/privileged_effect_census.dag b/dag/gunbc/auth/privileged_effect_census.dag index db8742b465c..76aee5df7d9 100644 --- a/dag/gunbc/auth/privileged_effect_census.dag +++ b/dag/gunbc/auth/privileged_effect_census.dag @@ -245,7 +245,7 @@ fn accessor_grant(subject: NonEmptyStr) -> PrivilegedEffect { data mtcollins1_operator_ruling: StandingDestructiveAuthorization = StandingDestructiveAuthorization { ruling_text: "the fleet-converge mtcollins1_boot and host_reset_return modes, dispatched from gunb-ai/gunbc main under their workload identity, may attach media to, set the boot device of, power-cycle and capture the console of Mt. Collins unit 1 on every dispatch with no per-run or standing approval, provided each run first takes the unit's maintenance hold. Operator chat rulings 2026-09-23 ('we technically don't even need my approval - would you mind getting rid of that step or making WIF just trust this workflow') and 2026-09-25 ('no I don't want that - can you just remove that check asap')" as NonEmptyStr, effect_subject: "mtcollins1 destructive controller effect: BMC virtual-media attach, one-shot boot-device set, power cycle and SOL capture" as NonEmptyStr, - interlock: decl_ref(module_path: "gunbc.machine_intake_mtcollins1_maintenance_hold", decl_name: "mtcollins1_unit_hold_key"), + interlock: decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "UnitHoldProof"), } data mtcollins1_operator_ruling_roots: List = [ @@ -353,14 +353,14 @@ data privileged_effect_interlocks: List = [ PrivilegedEffectInterlock { site: site(module_path: "gunbc.machine_intake_mtcollins1_boot_run", decl_name: "mtcollins1_boot_wet"), hold: mtcollins1_operator_ruling.interlock, - refusal: site(module_path: "gunbc.machine_intake_mtcollins1_maintenance_hold", decl_name: "unit_hold_acquire"), + refusal: site(module_path: "gunbc.managed_host_unit_hold", decl_name: "unit_hold_acquire"), premise: "the boot takes the unit's one durable exclusive hold before any BMC write and refuses FileHoldOccupied naming the holder" as NonEmptyStr, hold_owning_roots: mtcollins1_hold_owning_roots, }, PrivilegedEffectInterlock { site: site(module_path: "gunbc.host_reset_return_run", decl_name: "host_reset_return_wet"), hold: mtcollins1_operator_ruling.interlock, - refusal: site(module_path: "gunbc.machine_intake_mtcollins1_maintenance_hold", decl_name: "unit_hold_acquire"), + refusal: site(module_path: "gunbc.managed_host_unit_hold", decl_name: "unit_hold_acquire"), premise: "host reset-return takes the same unit hold before it sets the boot device or power-cycles the unit" as NonEmptyStr, hold_owning_roots: mtcollins1_hold_owning_roots, }, diff --git a/dag/gunbc/durable_exclusive_hold_file_store.dag b/dag/gunbc/durable_exclusive_hold_file_store.dag index 7063c99497d..706722dc49f 100644 --- a/dag/gunbc/durable_exclusive_hold_file_store.dag +++ b/dag/gunbc/durable_exclusive_hold_file_store.dag @@ -348,7 +348,7 @@ fn file_hold_recovery_assess( released_by: DurableHoldReleaseRef, ) -> FileHoldRecoveryAssessment admit_callers: [ - decl_ref(module_path: "gunbc.machine_intake_mtcollins1_maintenance_hold", decl_name: "unit_hold_recover_dead_holder"), + decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "unit_hold_recover_dead_holder"), ] { match durable_hold_recovery_assess(observed: observe_file_hold(root: root, key: slot_key), report: report) { diff --git a/dag/gunbc/fleet/fleet_converge_workflow.dag b/dag/gunbc/fleet/fleet_converge_workflow.dag index 92e6265b103..bfc19162b9b 100644 --- a/dag/gunbc/fleet/fleet_converge_workflow.dag +++ b/dag/gunbc/fleet/fleet_converge_workflow.dag @@ -110,7 +110,11 @@ import gunbc.fleet_workflow_steps { } import gunbc.runner_spec_from_offer { gunbc_ci_runner_spec } import gunbc.host_reset_return_run { host_reset_dispatch_mode_env } -import gunbc.machine_intake_mtcollins1_maintenance_hold { mtcollins1_unit_hold_store_host } +import gunbc.managed_host_unit_hold { + UnitHoldHostAdmission, UnitHoldHostAdmitted, UnitHoldHostNotManaged, UnitHoldHostNotRequired, + unit_hold_admission_for, unit_hold_host_admission_refusal, +} +import gunbc.fleet_intent_network { operator_host_mtcollins1 } import gunbc.auth.gcp_iam_converge_federation { gcp_iam_converge_environment, gcp_iam_observe_wif_provider_resource } import gunbc.auth.gcp_iam_converge { iam_observe_service_account, iam_converge_service_account, iam_converge_token_lifetime } import gunbc.auth.gcp_iam_converge_run { gcp_iam_converge_step_timeout_minutes, iam_converge_token_env, gcp_iam_converge_approved_output } @@ -3750,13 +3754,44 @@ fn fleet_converge_boot_federation_admitted() -> Bool { // mtcollins1_boot_admit_executor) refuses such a dispatch with a typed reason before the WIF token // or the fleet key exist; the wet entry re-runs the same fold. data fleet_converge_mtcollins1_boot_job_if: String = fleet_converge_mtcollins1_boot_step_if -data fleet_converge_mtcollins1_boot_concurrency_group: String = join([fleet_host_mutation_group_prefix, mtcollins1_unit_hold_store_host as String], "") +data fleet_converge_mtcollins1_boot_concurrency_group: String = join([fleet_host_mutation_group_prefix, fleet_converge_mtcollins1_boot_store_host()], "") + +// THE STORE HOST IS READ OFF THE UNIT'S MANAGED ROW, through the hold admission +// (gunbc.managed_host_unit_hold unit_hold_admission_for): the row's hold decision names where its +// store lives, and this job is pinned there. A unit that is not a managed host, or whose row declares +// no hold, has no store host, and there is no label to fall back to: the reading below carries the +// refusal in place of a host, and fleet_converge_yml_after_reset_assignment refuses to emit any yaml +// while it stands, so the refusal text never reaches a runs-on. +data fleet_converge_mtcollins1_boot_hold_admission: UnitHoldHostAdmission = unit_hold_admission_for(host: operator_host_mtcollins1 as NonEmptyStr) + +fn fleet_converge_mtcollins1_boot_store_host_refusal() -> String? { + match unit_hold_host_admission_refusal(admission: fleet_converge_mtcollins1_boot_hold_admission) { + Absent => none + Present { value: r } => + Present { value: join(["REFUSED gunbc.fleet_converge_workflow: the mtcollins1 boot job runs on its unit hold's store host, and ", r as String, ". No workflow yaml was emitted."], "") } + } +} + +fn fleet_converge_mtcollins1_boot_store_host() -> String { + match fleet_converge_mtcollins1_boot_hold_admission { + UnitHoldHostAdmitted { subject: s } => s.store_host as String + UnitHoldHostNotManaged { host: _ } => fleet_converge_mtcollins1_boot_store_host_unread() + UnitHoldHostNotRequired { host: _ } => fleet_converge_mtcollins1_boot_store_host_unread() + } +} + +fn fleet_converge_mtcollins1_boot_store_host_unread() -> String { + match fleet_converge_mtcollins1_boot_store_host_refusal() { + Present { value: r } => r + Absent => "REFUSED gunbc.fleet_converge_workflow: the mtcollins1 unit hold admission is unclassified. No workflow yaml was emitted." + } +} // THE BOOT JOB'S RUNNER AND STEPS ARE THEIR OWN PRODUCERS for the same reason as the credential // prelude below: which runner holds the credentials, and which bytes the steps fetch and execute, are // facts a witness reads, and reading them here costs those parts rather than the whole job's. fn fleet_converge_mtcollins1_boot_runner() -> RunnerSpec { - SelfHosted { labels: ["self-hosted", "linux", "arm64", mtcollins1_unit_hold_store_host as String] } + SelfHosted { labels: ["self-hosted", "linux", "arm64", fleet_converge_mtcollins1_boot_store_host()] } } // The two rendered credential scripts -- the fleet key step and the boot step -- are the job's @@ -4564,6 +4599,13 @@ fn fleet_converge_yml_after_toolchain_admission() -> FleetConvergeYamlGeneration } fn fleet_converge_yml_after_reset_assignment() -> FleetConvergeYamlGenerationOutcome { + match fleet_converge_mtcollins1_boot_store_host_refusal() { + Present { value: r } => FleetConvergeYamlGenerationRefused { reason: r } + Absent => fleet_converge_yml_after_unit_hold_admission() + } +} + +fn fleet_converge_yml_after_unit_hold_admission() -> FleetConvergeYamlGenerationOutcome { if fleet_converge_build_job_capability_closure_holds() { match checked_job_timeout_minutes(computed: gunbc_ci_fleet_job_backstop_timeout_minutes()) { JobTimeoutExceedsCeiling { minutes: _, ceiling: _ } => diff --git a/dag/gunbc/host/host_maintenance_hold_reason.dag b/dag/gunbc/host/host_maintenance_hold_reason.dag new file mode 100644 index 00000000000..78ffd610bef --- /dev/null +++ b/dag/gunbc/host/host_maintenance_hold_reason.dag @@ -0,0 +1,20 @@ +module gunbc.host_maintenance_hold_reason + +import std.types { NonEmptyStr } +import product.placement_supply { host_identity_eq } +import gunbc.fleet_intent_network { operator_host_mtcollins1 } +import gunbc.managed_host { ManagedHost } + +// THE VARIABLE AN OPERATOR NAMES THEIR MAINTENANCE REASON THROUGH IS MAINTENANCE POLICY, not a fact +// about the host, so it lives beside the maintenance operation rather than on gunbc.managed_host +// ManagedHost, and this is its one authority: gunbc.managed_host_unit_hold admit_maintenance_hold_in +// reads it to admit a host to the operator's take and release. Mt. Collins unit 1's variable keeps +// the name operators already export. A host with no row here has no maintenance entry, however its +// hold is declared: the admission refuses it instead of deriving a variable name from its label. +fn maintenance_hold_reason_env(host: ManagedHost) -> NonEmptyStr? { + if host_identity_eq(a: host.host, b: operator_host_mtcollins1) { + Present { value: "GUNBC_MTCOLLINS1_MAINTENANCE_REASON" as NonEmptyStr } + } else { + none + } +} diff --git a/dag/gunbc/host/host_reset_return_run.dag b/dag/gunbc/host/host_reset_return_run.dag index 42048fb8136..f60e03d7290 100644 --- a/dag/gunbc/host/host_reset_return_run.dag +++ b/dag/gunbc/host/host_reset_return_run.dag @@ -1,8 +1,8 @@ module gunbc.host_reset_return_run -import gunbc.machine_intake_mtcollins1_maintenance_hold { +import gunbc.managed_host_unit_hold { UnitHoldProof, UnitHeld, UnitHoldRefused, unit_hold_acquire, unit_hold_release, unit_hold_proof_refusal, - unit_hold_store_root, host_reset_owner, + host_reset_owner, admit_unit_hold_subject, UnitHoldSubjectAdmitted, UnitHoldNotRequired, } import std.decl_ref { decl_ref } import std.types { Bool, EpochMs, Int, List, NonEmptyStr, String } @@ -80,7 +80,6 @@ import gunbc.host_reset_return { subject_for_observer, } import gunbc.host_reset_subject_roster { AdmittedResetSubject, reset_observer_peer_roster, reset_subject_for, reset_subject_roster } -import gunbc.managed_host { ResetNoUnitHold, ResetUnitHoldRequired } import gunbc.machine_intake_oob_boot_handoff { oob_boot_handoff, BootControlIssued, @@ -393,13 +392,13 @@ data host_reset_down_watch_samples: Nat = 120 data host_reset_back_watch_samples: Nat = 200 fn reset_unit_hold_gate(candidate: AdmittedResetSubject, proof: UnitHoldProof?) -> NonEmptyStr? { - match candidate.binding.host.unit_hold { - ResetNoUnitHold => none - ResetUnitHoldRequired { key: k, store_host: _ } => + match admit_unit_hold_subject(host: candidate.binding.host) { + UnitHoldNotRequired { host: _ } => none + UnitHoldSubjectAdmitted { subject: _ } => match proof { Absent => Present { value: join(["subject ", candidate.binding.host.host as String, " is hold-gated and no unit hold proof was presented; no controller write was attempted"], "") as NonEmptyStr } Present { value: p } => - match unit_hold_proof_refusal(proof: p, key: k, label: "host reset-return") { + match unit_hold_proof_refusal(proof: p, host: candidate.binding.host.host, label: "host reset-return") { Present { value: why } => Present { value: why as NonEmptyStr } Absent => none } @@ -478,7 +477,7 @@ fn host_reset_return_attempt( } // A HOLD-GATED SUBJECT IS NOT WRITTEN WITHOUT A PROOF FOR ITS SLOT, and the proof exists only if the -// entry's live acquire committed (gunbc.machine_intake_mtcollins1_maintenance_hold UnitHoldProof). +// entry's live acquire committed (gunbc.managed_host_unit_hold UnitHoldProof). fn host_reset_return_issue_and_watch( proof: UnitHoldProof?, candidate: AdmittedResetSubject, @@ -688,21 +687,21 @@ fn host_reset_return_wet() -> ProcessExit remedy: "the assigned subject has no roster row carrying its controller evidence", ) Present { value: candidate } => - match candidate.binding.host.unit_hold { - ResetNoUnitHold => + match admit_unit_hold_subject(host: candidate.binding.host) { + UnitHoldNotRequired { host: _ } => host_reset_return_attempt_exit(proof: none, candidate: candidate, observer: observer, subject: subject, route: route, password_file: password_file_raw as NonEmptyStr) - ResetUnitHoldRequired { key: k, store_host: h } => - if (observer as String) != (h as String) { + UnitHoldSubjectAdmitted { subject: held } => + if (observer as String) != (held.store_host as String) { host_reset_return_preflight_exit( - refusal: UnitHoldStoreNotOnObserver { subject: subject, observer: observer, store_host: h }, + refusal: UnitHoldStoreNotOnObserver { subject: subject, observer: observer, store_host: held.store_host }, remedy: "the subject's maintenance hold lives on the store host; a reset observed from anywhere else would take a hold in a store the operator never sees", ) } else { - match unit_hold_acquire(root: unit_hold_store_root, key: k, owner: host_reset_owner(attempt: host_reset_return_attempt_label(observer: observer, subject: subject))) { + match unit_hold_acquire(subject: held, owner: host_reset_owner(attempt: host_reset_return_attempt_label(observer: observer, subject: subject))) { UnitHoldRefused { reason: r } => host_reset_return_preflight_exit( refusal: UnitHeldForMaintenance { subject: subject, reason: r }, - remedy: "the unit is held (maintenance or another run); nothing was written to its controller", + remedy: "the unit hold was not acquired: it is held (maintenance or another run), or this runner was not observed on the hold store's host; nothing was written to its controller", ) UnitHeld { proof: p } => unit_hold_release( diff --git a/dag/gunbc/host/managed_host.dag b/dag/gunbc/host/managed_host.dag index b25fa755877..f30fe85e566 100644 --- a/dag/gunbc/host/managed_host.dag +++ b/dag/gunbc/host/managed_host.dag @@ -7,10 +7,9 @@ import extdeps.bmc.endpoint { BmcControllerEndpoint } import extdeps.bmc.access_profile { BmcAccessObservation, BmcAccessObservationStanding, BmcAccessObserved, BmcAccessUnobserved } import extdeps.bmc.capability { BmcFirmwareReleaseCapabilityRow } import gunbc.machine_intake_bmc_secure { BmcSecureRefusalCause, BmcSecureRefused, BmcSecureStanding, BmcSecured } -import gunbc.fleet_intent_network { operator_host_mtcollins1 } +import gunbc.fleet_intent_network { operator_host_mtcollins1, operator_host_srv1 } import gunbc.machine_intake_mtcollins1_access_observation { mtcollins1_access_standing, mtcollins1_capability_row } import gunbc.machine_intake_mtcollins1_bmc_secure_observation { mtcollins1_bmc_secure_standing } -import gunbc.machine_intake_mtcollins1_maintenance_hold { mtcollins1_unit_hold_key, mtcollins1_unit_hold_store_host } // A HOST THIS FLEET DRIVES THROUGH ITS BASEBOARD CONTROLLER, and the one record a host-generic // procedure takes instead of a unit's constants (docs/plans/managed-host-untangle.md, cut 0). It is @@ -37,9 +36,10 @@ type ManagedHost sole_constructor { } // WHETHER DRIVING THIS HOST MUST TAKE ITS MAINTENANCE HOLD FIRST, and on which host the hold store -// lives. Mt. Collins unit 1 is serviced by hand (gunbc.machine_intake_mtcollins1_maintenance_hold), -// so a power cycle of it is gated by the same slot the boot takes; a write may only run where that -// store is, or it would acquire a hold in an empty store the operator never sees. +// lives. Mt. Collins unit 1 is serviced by hand, so a power cycle of it is gated by the same slot the +// boot takes; a write may only run where that store is, or it would acquire a hold in an empty store +// the operator never sees. This decision is the row's; gunbc.managed_host_unit_hold admits a host to +// the hold procedure from it and is the only reader that turns it into a slot. type ResetUnitHold = ResetUnitHoldRequired { key: NonEmptyStr, store_host: NonEmptyStr } | ResetNoUnitHold @@ -93,7 +93,7 @@ fn managed_hosts() -> List { access: mtcollins1_access_standing, capability_row: mtcollins1_capability_row, secure: secure, - unit_hold: ResetUnitHoldRequired { key: mtcollins1_unit_hold_key, store_host: mtcollins1_unit_hold_store_host }, + unit_hold: ResetUnitHoldRequired { key: operator_host_mtcollins1 as NonEmptyStr, store_host: operator_host_srv1 as NonEmptyStr }, }, ] } @@ -113,6 +113,9 @@ fn managed_host_fixture( admit_callers: [ decl_ref(module_path: "test.claim.managed_host_witness", decl_name: "w_a_secured_account_beside_another_controllers_access_is_not_bound_or_rostered"), decl_ref(module_path: "test.claim.managed_host_witness", decl_name: "w_a_capable_host_with_no_reset_selection_is_absent_from_the_roster"), + decl_ref(module_path: "test.claim.managed_host_unit_hold_witness", decl_name: "w_a_managed_host_with_no_unit_hold_is_refused_and_has_no_store"), + decl_ref(module_path: "test.claim.managed_host_unit_hold_witness", decl_name: "w_a_held_host_with_no_reason_variable_is_refused_for_maintenance"), + decl_ref(module_path: "test.claim.managed_host_unit_hold_witness", decl_name: "w_a_store_host_with_no_allocated_hostname_refuses_the_executor"), decl_ref(module_path: "test.claim.managed_host_boot_federation_witness", decl_name: "w_a_bound_host_with_no_boot_policy_is_unprovisioned"), ] { diff --git a/dag/gunbc/machine_intake/mtcollins1_maintenance_hold.dag b/dag/gunbc/host/managed_host_unit_hold.dag similarity index 58% rename from dag/gunbc/machine_intake/mtcollins1_maintenance_hold.dag rename to dag/gunbc/host/managed_host_unit_hold.dag index c66a1a9d4cd..bf69248e7cc 100644 --- a/dag/gunbc/machine_intake/mtcollins1_maintenance_hold.dag +++ b/dag/gunbc/host/managed_host_unit_hold.dag @@ -1,4 +1,4 @@ -module gunbc.machine_intake_mtcollins1_maintenance_hold +module gunbc.managed_host_unit_hold import std.types { Bool, Int, List, NonEmptyStr, String } import std.process { ProcessExit, ExitSuccess, ExitFailure, exit_failure } @@ -17,6 +17,7 @@ import std.durable_exclusive_hold { import std.nat { Nat } import std.checked_arithmetic { checked_int_to_nat } import std.algebra { trim } +import std.list { distinct_by_key } import gunbc.build_cache_instance { ProcessIdentity, process_identity_eq } import gunbc.command_runner { run_shell_command_capture } import extdeps.exec.command { LocalExec } @@ -40,18 +41,23 @@ import gunbc.durable_exclusive_hold_file_store { } import gunbc.actions_run_binding { actions_variable_trimmed } import std.decl_ref { decl_ref } -import gunbc.fleet_intent_network { operator_host_srv1, operator_host_mtcollins1 } +import product.placement_supply { HostIdentity, host_identity_eq } +import gunbc.managed_host { ManagedHost, ResetNoUnitHold, ResetUnitHoldRequired, managed_hosts } +import gunbc.host_maintenance_hold_reason { maintenance_hold_reason_env } +import extdeps.tools.hostname +import gunbc.hostname_allocation { canonical_hostname_for_fleet_slot } // ── THE INTERLOCK THE PER-RUN APPROVAL WAS PROVIDING WITHOUT SAYING SO ──────────────────────── // -// Until 2026-09-23 every Mt. Collins boot waited for one operator tap, and the operator tapped only +// Until 2026-09-23 every boot of a hand-serviced unit waited for one operator tap, and the operator tapped only // when nobody had hands in the chassis. That consent carried two facts: "this effect may run" and // "the unit is not under maintenance right now". The operator ruling of 2026-09-23 retired the // first (the boot is a recurring automated effect; gunbc.auth.privileged_effect_census derives the // federated pattern for it). The second is a physical-safety fact about the unit, not about who may // authorize, so it does not dissolve with the approval stage: a boot that power-cycles a unit whose // DIMMs are being reseated is the harm. It is carried here as ONE std.durable_exclusive_hold slot -// per unit, keyed by the machine name the signed subject already uses. +// per unit, keyed by the key its gunbc.managed_host ManagedHost row declares (unit_hold). Nothing here +// names a unit: which hosts have a hold, under which key and on which store host, is read off the row. // // ONE SLOT, TWO KINDS OF HOLDER, AND THAT IS THE POINT. The operator takes the slot for // maintenance; the boot run takes the SAME slot before any BMC actuation and frees it after. So @@ -66,11 +72,174 @@ import gunbc.fleet_intent_network { operator_host_srv1, operator_host_mtcollins1 data unit_hold_store_root: NonEmptyStr = "/var/lib/gunbc/unit-holds" as NonEmptyStr -data mtcollins1_unit_hold_key: NonEmptyStr = operator_host_mtcollins1 as NonEmptyStr +// ── THE ADMISSION: WHICH HOSTS HAVE A HOLD AT ALL ───────────────────────────────────────────── +// Taking, releasing or checking a unit hold is an operation on a managed host, and its policy is the +// row's own unit_hold decision. A host whose row says ResetNoUnitHold has no slot, and a label that +// names no row of managed_hosts() is not a host this fleet drives; both are typed refusals, and no +// arm falls back to a key spelled from the label. AdmittedUnitHoldSubject is sole_constructor and +// admit_unit_hold_subject is its only mint, so every acquire, release and proof check below is fed a +// key and a store host that came from a ManagedHost row and from nowhere else. +type AdmittedUnitHoldSubject sole_constructor { + host: ManagedHost + key: NonEmptyStr + store_host: NonEmptyStr +} + +type UnitHoldAdmission + = UnitHoldSubjectAdmitted { subject: AdmittedUnitHoldSubject } + | UnitHoldNotRequired { host: HostIdentity } + +fn admit_unit_hold_subject(host: ManagedHost) -> UnitHoldAdmission { + match host.unit_hold { + ResetUnitHoldRequired { key: k, store_host: s } => + UnitHoldSubjectAdmitted { subject: AdmittedUnitHoldSubject { host: host, key: k, store_host: s } } + ResetNoUnitHold => UnitHoldNotRequired { host: host.host } + } +} + +// THE SAME ADMISSION FOR A LABEL, over the rows it is given so the refusals have something to refuse: +// a caller that knows only a host's name (an operator's argument, a unit procedure's own identity) +// reaches the row here and nowhere else. +type UnitHoldHostAdmission + = UnitHoldHostAdmitted { subject: AdmittedUnitHoldSubject } + | UnitHoldHostNotManaged { host: NonEmptyStr } + | UnitHoldHostNotRequired { host: HostIdentity } -// The host the store lives on: the srv1 runner, where the boot job is pinned and where the operator -// takes maintenance holds. Every hold-owning root of this unit runs there. -data mtcollins1_unit_hold_store_host: NonEmptyStr = operator_host_srv1 as NonEmptyStr +fn unit_hold_admission_in(hosts: List, host: NonEmptyStr) -> UnitHoldHostAdmission { + fold( + hosts, + init: UnitHoldHostNotManaged { host: host }, + f: (acc, h) => match acc { + UnitHoldHostAdmitted { subject: _ } => acc + UnitHoldHostNotRequired { host: _ } => acc + UnitHoldHostNotManaged { host: _ } => + if (h.host as String) == (host as String) { + match admit_unit_hold_subject(host: h) { + UnitHoldSubjectAdmitted { subject: s } => UnitHoldHostAdmitted { subject: s } + UnitHoldNotRequired { host: x } => UnitHoldHostNotRequired { host: x } + } + } else { + acc + } + }, + ) +} + +fn unit_hold_admission_for(host: NonEmptyStr) -> UnitHoldHostAdmission { + unit_hold_admission_in(hosts: managed_hosts(), host: host) +} + +// Absent means the host was admitted; the text is what a refused caller prints. +fn unit_hold_host_admission_refusal(admission: UnitHoldHostAdmission) -> NonEmptyStr? { + match admission { + UnitHoldHostAdmitted { subject: _ } => none + UnitHoldHostNotManaged { host: h } => + Present { value: join(["'", h as String, "' is not a managed host (gunbc.managed_host managed_hosts has no row for it), so it has no unit hold; nothing was taken, released or written"], "") as NonEmptyStr } + UnitHoldHostNotRequired { host: h } => + Present { value: join(["managed host '", h as String, "' declares no unit hold (ResetNoUnitHold), so there is no hold slot for it; nothing was taken, released or written"], "") as NonEmptyStr } + } +} + +// THE HOSTS A HOLD STORE MUST EXIST ON: every store host some managed host's hold names, each once, +// in row order. gunbc.runner_host_grants provisions the store root on exactly these. The named hosts +// are gathered by prepending and reversed once, and std.list distinct_by_key removes repeats through +// its keyed map, so neither step copies an accumulator or scans one per row. +fn unit_hold_named_store_hosts_reversed(hosts: List) -> List { + fold( + hosts, + init: [], + f: (acc, h) => match admit_unit_hold_subject(host: h) { + UnitHoldNotRequired { host: _ } => acc + UnitHoldSubjectAdmitted { subject: s } => concat([s.store_host], acc) + }, + ) +} + +fn unit_hold_store_hosts_of(hosts: List) -> List { + distinct_by_key(xs: reverse(unit_hold_named_store_hosts_reversed(hosts: hosts)), key: fn(h) { h as String }) +} + +fn unit_hold_store_hosts() -> List { + unit_hold_store_hosts_of(hosts: managed_hosts()) +} + +// ── THE STORE IS A LOCAL DIRECTORY, SO THE PROCESS MUST BE ON THE STORE HOST ─────────────────── +// unit_hold_store_root is a path on whatever machine runs this code. An admitted subject names the +// host its store lives on, and a take, release or acquire run anywhere else would succeed against that +// other machine's empty directory while the real store stayed free: an interlock held where nobody +// looks. So every store effect below is fed a UnitHoldStoreExecutor, and that carrier exists only +// when THIS PROCESS OBSERVED its own short hostname (os.Hostname.ReadShort) and it equals the +// hostname gunbc.hostname_allocation allocates to the subject's store host -- the same two +// authorities gunbc.host_reset_return_run observer_self_corroboration reads to establish which +// machine a run is on. A label a caller supplies is not that observation, so there is no parameter +// for one: unit_hold_store_executor performs the read itself. A store host with no allocated +// hostname, and a hostname that cannot be read, refuse; neither is treated as a match. +type UnitHoldStoreExecutorDecision + = UnitHoldExecutorIsStoreHost { observed: NonEmptyStr } + | UnitHoldExecutorElsewhere { observed: NonEmptyStr, store_host: NonEmptyStr, allocated: NonEmptyStr } + | UnitHoldStoreHostUnallocated { store_host: NonEmptyStr } + | UnitHoldExecutorUnread { store_host: NonEmptyStr } + +// THE DECISION IS A PURE FOLD OVER A SUPPLIED READING, so a witness can show both sides of it; it +// returns a decision and never the carrier. Absent means the hostname could not be read. +fn unit_hold_store_executor_decision(subject: AdmittedUnitHoldSubject, observed: String?) -> UnitHoldStoreExecutorDecision { + match canonical_hostname_for_fleet_slot(fleet_slot: subject.store_host as HostIdentity) { + Absent => UnitHoldStoreHostUnallocated { store_host: subject.store_host } + Present { value: allocated } => + match observed { + Absent => UnitHoldExecutorUnread { store_host: subject.store_host } + Present { value: raw } => + if trim(s: raw) == "" { + UnitHoldExecutorUnread { store_host: subject.store_host } + } else if trim(s: raw) == (allocated as String) { + UnitHoldExecutorIsStoreHost { observed: trim(s: raw) as NonEmptyStr } + } else { + UnitHoldExecutorElsewhere { observed: trim(s: raw) as NonEmptyStr, store_host: subject.store_host, allocated: allocated as String as NonEmptyStr } + } + } + } +} + +fn unit_hold_store_executor_refusal(key: NonEmptyStr, decision: UnitHoldStoreExecutorDecision) -> NonEmptyStr? { + match decision { + UnitHoldExecutorIsStoreHost { observed: _ } => none + UnitHoldExecutorElsewhere { observed: o, store_host: h, allocated: a } => + Present { value: join(["the unit hold store for '", key as String, "' is on '", h as String, "' (hostname '", a as String, "'), and this process observes its own host as '", o as String, "'; a hold taken or released here would act on a store nobody reads; nothing was read or written"], "") as NonEmptyStr } + UnitHoldStoreHostUnallocated { store_host: h } => + Present { value: join(["the unit hold store for '", key as String, "' is on '", h as String, "', which has no hostname allocated in gunbc.hostname_allocation, so this process cannot establish that it runs there; nothing was read or written"], "") as NonEmptyStr } + UnitHoldExecutorUnread { store_host: h } => + Present { value: join(["the unit hold store for '", key as String, "' is on '", h as String, "', and this process could not read its own short hostname, so it cannot establish that it runs there; nothing was read or written"], "") as NonEmptyStr } + } +} + +type UnitHoldStoreExecutor sole_constructor { + subject: AdmittedUnitHoldSubject + observed_hostname: NonEmptyStr +} + +type UnitHoldStoreExecutorStanding + = UnitHoldOnStoreHost { executor: UnitHoldStoreExecutor } + | UnitHoldNotOnStoreHost { reason: NonEmptyStr } + +// THE ONE MINT OF THE EXECUTOR CARRIER, and it reads the hostname itself. +fn unit_hold_store_executor(subject: AdmittedUnitHoldSubject) -> UnitHoldStoreExecutorStanding { + let read = os.Hostname.ReadShort() + let observed = if read.success { Present { value: read.value } } else { none } + let decision = unit_hold_store_executor_decision(subject: subject, observed: observed) + match decision { + UnitHoldExecutorIsStoreHost { observed: o } => UnitHoldOnStoreHost { executor: UnitHoldStoreExecutor { subject: subject, observed_hostname: o } } + UnitHoldExecutorElsewhere { observed: _, store_host: _, allocated: _ } => unit_hold_not_on_store_host(key: subject.key, decision: decision) + UnitHoldStoreHostUnallocated { store_host: _ } => unit_hold_not_on_store_host(key: subject.key, decision: decision) + UnitHoldExecutorUnread { store_host: _ } => unit_hold_not_on_store_host(key: subject.key, decision: decision) + } +} + +fn unit_hold_not_on_store_host(key: NonEmptyStr, decision: UnitHoldStoreExecutorDecision) -> UnitHoldStoreExecutorStanding { + match unit_hold_store_executor_refusal(key: key, decision: decision) { + Present { value: r } => UnitHoldNotOnStoreHost { reason: r } + Absent => UnitHoldNotOnStoreHost { reason: "unit hold store executor decision unclassified; nothing was read or written" as NonEmptyStr } + } +} // WHO HOLDS THE UNIT IS A DECLARED SUM (review 70459), each kind carrying its detail. The durable // owner string is RENDERED from it and DECODED back to it here, in one place: nothing else builds an @@ -96,9 +265,9 @@ type UnitHoldOwner fn unit_hold_owner_tag(o: UnitHoldOwner) -> String { match o { OperatorMaintenance { reason: _ } => "operator-maintenance:" - BootRun { run_id: _, process: _, pid_namespace: _ } => "mtcollins1-boot:" + BootRun { run_id: _, process: _, pid_namespace: _ } => "boot-run:" HostResetReturn { attempt: _ } => "host-reset-return:" - KvmObserverProbe { run_id: _, process: _, pid_namespace: _ } => "mtcollins1-kvm-observer:" + KvmObserverProbe { run_id: _, process: _, pid_namespace: _ } => "kvm-observer:" } } @@ -166,9 +335,9 @@ fn unit_hold_owner_ref(o: UnitHoldOwner) -> DurableHoldOwnerRef { fn unit_hold_owner_label(o: UnitHoldOwner) -> String { match o { OperatorMaintenance { reason: r } => concat("operator maintenance: ", r as String) - BootRun { run_id: r, process: p, pid_namespace: _ } => join(["the mtcollins1 boot run ", r as String, " (process ", to_string(p.pid), " on boot ", p.boot_id as String, ")"], "") + BootRun { run_id: r, process: p, pid_namespace: _ } => join(["the boot run ", r as String, " (process ", to_string(p.pid), " on boot ", p.boot_id as String, ")"], "") HostResetReturn { attempt: a } => concat("host reset-return attempt ", a as String) - KvmObserverProbe { run_id: r, process: p, pid_namespace: _ } => join(["the mtcollins1 KVM observer probe run ", r as String, " (process ", to_string(p.pid), " on boot ", p.boot_id as String, ")"], "") + KvmObserverProbe { run_id: r, process: p, pid_namespace: _ } => join(["the KVM observer probe run ", r as String, " (process ", to_string(p.pid), " on boot ", p.boot_id as String, ")"], "") } } @@ -233,8 +402,6 @@ fn host_reset_owner(attempt: NonEmptyStr) -> DurableHoldOwnerRef { } // The operator names why they hold the unit; the reason is the owner, so a refused boot prints it. -data mtcollins1_maintenance_reason_env: NonEmptyStr = "GUNBC_MTCOLLINS1_MAINTENANCE_REASON" - fn operator_maintenance_owner(reason: NonEmptyStr) -> DurableHoldOwnerRef { unit_hold_owner_ref(o: OperatorMaintenance { reason: reason }) } @@ -250,11 +417,12 @@ fn boot_run_owner(run_id: NonEmptyStr, process: ProcessIdentity, pid_namespace: // arm of unit_hold_minted, admitted only to unit_hold_acquire and fed only that call's own live // compare-and-set outcomes. A supplied or authored // acquire outcome therefore cannot become a proof: the pure refusal fold below reads outcomes, and -// it returns text, never a proof. test.claim.machine_intake.mtcollins1_maintenance_hold_witness_test -// enrolls test.probe.unit_hold_proof_forged_probe, where a forged proof is refused at the literal. +// it returns text, never a proof. The proof carries the admitted subject it was acquired for, so what +// it proves -- this host's slot is held -- is read from the row that admitted it. +// test.claim.machine_intake.mtcollins1_unit_hold_forged_probe_witness_test enrolls +// test.probe.unit_hold_proof_forged_probe, where a forged proof is refused at the literal. type UnitHoldProof sole_constructor { - root: NonEmptyStr - key: NonEmptyStr + subject: AdmittedUnitHoldSubject owner: DurableHoldOwnerRef generation: CasGeneration } @@ -282,8 +450,8 @@ fn unit_hold_refusal(outcome: FileHoldAcquireOutcome) -> NonEmptyStr? { } // ── WHETHER A HOLDING PROCESS STILL RUNS, OBSERVED ───────────────────────────────────────────── -// The store and every holder that can be recovered run on one host (mtcollins1_unit_hold_store_host; -// the boot admission refuses any other), so the holder's process is observable through this host's +// The store and every holder that can be recovered run on one host (the admitted subject's +// store_host; each hold-owning root refuses any other), so the holder's process is observable through this host's // procfs. Three reads decide it, each typed by the host's own error kind: // - /proc/sys/kernel/random/boot_id differs from the holder's boot -> the host rebooted since, so // every process of that boot is gone: OBSERVED DEAD; @@ -479,7 +647,7 @@ fn recovery_refusal_text(key: NonEmptyStr, r: DurableHoldRecoveryRefusal) -> Non fn unit_hold_recover_dead_holder(root: NonEmptyStr, key: NonEmptyStr, holder: DurableHoldOwnerRef, generation: CasGeneration) -> DeadHolderRecovery admit_callers: [ - decl_ref(module_path: "gunbc.machine_intake_mtcollins1_maintenance_hold", decl_name: "unit_hold_acquire"), + decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "unit_hold_acquire_on_store_host"), ] { let report = holder_report(holder: holder, generation: generation) @@ -498,14 +666,14 @@ fn unit_hold_recover_dead_holder(root: NonEmptyStr, key: NonEmptyStr, holder: Du // The proof is built here, from an outcome only unit_hold_acquire's own live acquires produce: the // admission is what keeps a supplied FileHoldAcquired from becoming a proof. -fn unit_hold_minted(root: NonEmptyStr, key: NonEmptyStr, outcome: FileHoldAcquireOutcome) -> UnitHoldAcquisition +fn unit_hold_minted(subject: AdmittedUnitHoldSubject, outcome: FileHoldAcquireOutcome) -> UnitHoldAcquisition admit_callers: [ - decl_ref(module_path: "gunbc.machine_intake_mtcollins1_maintenance_hold", decl_name: "unit_hold_acquire"), + decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "unit_hold_acquire_on_store_host"), ] { match outcome { FileHoldAcquired { slot_key: _, owner: o, generation: g } => - UnitHeld { proof: UnitHoldProof { root: root, key: key, owner: o, generation: g } } + UnitHeld { proof: UnitHoldProof { subject: subject, owner: o, generation: g } } FileHoldOccupied { slot_key: _, holder: _, generation: _ } => unit_hold_not_acquired(outcome: outcome) FileHoldAcquireLost { slot_key: _ } => unit_hold_not_acquired(outcome: outcome) FileHoldAcquireStoreUnavailable { slot_key: _, cause: _ } => unit_hold_not_acquired(outcome: outcome) @@ -526,57 +694,91 @@ fn unit_hold_not_acquired(outcome: FileHoldAcquireOutcome) -> UnitHoldAcquisitio // further question -- is its holder observed dead? -- and only an observed-dead holder's hold is freed, // after which this caller acquires once more like any acquirer. There is no loop: a slot taken by // someone else in between refuses as occupied, naming them. -fn unit_hold_acquire(root: NonEmptyStr, key: NonEmptyStr, owner: DurableHoldOwnerRef) -> UnitHoldAcquisition +fn unit_hold_acquire(subject: AdmittedUnitHoldSubject, owner: DurableHoldOwnerRef) -> UnitHoldAcquisition admit_callers: [ - decl_ref(module_path: "gunbc.machine_intake_mtcollins1_maintenance_hold", decl_name: "mtcollins1_boot_acquire_unit_hold"), + decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "boot_run_acquire_unit_hold"), decl_ref(module_path: "gunbc.host_reset_return_run", decl_name: "host_reset_return_wet"), - decl_ref(module_path: "gunbc.machine_intake_mtcollins1_maintenance_hold", decl_name: "mtcollins1_kvm_observer_acquire_unit_hold"), + decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "kvm_observer_acquire_unit_hold"), ] { - let outcome = file_hold_acquire(root: root, slot_key: key, requested_owner: owner) + match unit_hold_store_executor(subject: subject) { + UnitHoldNotOnStoreHost { reason: r } => UnitHoldRefused { reason: join([r as String, "; controller untouched"], "") as NonEmptyStr } + UnitHoldOnStoreHost { executor: e } => unit_hold_acquire_on_store_host(executor: e, owner: owner) + } +} + +// The store effect itself, reachable only with the executor carrier and only from the mint above. +fn unit_hold_acquire_on_store_host(executor: UnitHoldStoreExecutor, owner: DurableHoldOwnerRef) -> UnitHoldAcquisition + admit_callers: [ + decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "unit_hold_acquire"), + ] +{ + let subject = executor.subject + let outcome = file_hold_acquire(root: unit_hold_store_root, slot_key: subject.key, requested_owner: owner) match outcome { FileHoldOccupied { slot_key: _, holder: h, generation: g } => - match unit_hold_recover_dead_holder(root: root, key: key, holder: h, generation: g) { + match unit_hold_recover_dead_holder(root: unit_hold_store_root, key: subject.key, holder: h, generation: g) { DeadHolderNotRecovered { reason: r } => UnitHoldRefused { reason: r } DeadHolderRecovered { dead_holder: _, evidence: _ } => - unit_hold_minted(root: root, key: key, outcome: file_hold_acquire(root: root, slot_key: key, requested_owner: owner)) + unit_hold_minted(subject: subject, outcome: file_hold_acquire(root: unit_hold_store_root, slot_key: subject.key, requested_owner: owner)) } - _ => unit_hold_minted(root: root, key: key, outcome: outcome) + FileHoldAcquired { slot_key: _, owner: _, generation: _ } => unit_hold_minted(subject: subject, outcome: outcome) + FileHoldAcquireLost { slot_key: _ } => unit_hold_minted(subject: subject, outcome: outcome) + FileHoldAcquireStoreUnavailable { slot_key: _, cause: _ } => unit_hold_minted(subject: subject, outcome: outcome) + FileHoldSlotUndecodable { slot_key: _, generation: _, detail: _ } => unit_hold_minted(subject: subject, outcome: outcome) + FileHoldKeyNotSlotAddressable { slot_key: _ } => unit_hold_minted(subject: subject, outcome: outcome) } } -fn unit_hold_proof_key(proof: UnitHoldProof) -> NonEmptyStr { - proof.key -} - -fn mtcollins1_boot_acquire_unit_hold(run_id: NonEmptyStr) -> UnitHoldAcquisition +// A HOLD-OWNING RUN NAMES THE HOST IT DRIVES, AND THE ADMISSION IS HERE. The boot and the KVM probe +// know their unit by its HostIdentity; the label is admitted against the managed rows before anything +// touches the store, and a host that is not managed, or has no hold, refuses with that cause. The +// acquire itself takes only the admitted subject. +fn boot_run_acquire_unit_hold(host: HostIdentity, run_id: NonEmptyStr) -> UnitHoldAcquisition admit_callers: [ decl_ref(module_path: "gunbc.machine_intake_mtcollins1_boot_run", decl_name: "mtcollins1_boot_under_live_unit_hold"), ] { - match self_process_identity() { - SelfUnidentified { cause: c } => - UnitHoldRefused { reason: join(["this boot cannot name its own process (", c as String, "), and a hold it could never be shown dead in would lock the unit out if it died; controller untouched"], "") as NonEmptyStr } - SelfIdentified { process: p, pid_namespace: n } => - unit_hold_acquire(root: unit_hold_store_root, key: mtcollins1_unit_hold_key, owner: boot_run_owner(run_id: run_id, process: p, pid_namespace: n)) + match unit_hold_admission_for(host: host as NonEmptyStr) { + UnitHoldHostNotManaged { host: h } => unit_hold_not_admitted(admission: UnitHoldHostNotManaged { host: h }) + UnitHoldHostNotRequired { host: h } => unit_hold_not_admitted(admission: UnitHoldHostNotRequired { host: h }) + UnitHoldHostAdmitted { subject: subject } => + match self_process_identity() { + SelfUnidentified { cause: c } => + UnitHoldRefused { reason: join(["this boot cannot name its own process (", c as String, "), and a hold it could never be shown dead in would lock the unit out if it died; controller untouched"], "") as NonEmptyStr } + SelfIdentified { process: p, pid_namespace: n } => + unit_hold_acquire(subject: subject, owner: boot_run_owner(run_id: run_id, process: p, pid_namespace: n)) + } } } -// THE KVM OBSERVER PROBE TAKES THE SAME SLOT (gunbc.machine_intake_mtcollins1_kvm_observer_observe). +fn unit_hold_not_admitted(admission: UnitHoldHostAdmission) -> UnitHoldAcquisition { + match unit_hold_host_admission_refusal(admission: admission) { + Present { value: r } => UnitHoldRefused { reason: join([r as String, "; controller untouched"], "") as NonEmptyStr } + Absent => UnitHoldRefused { reason: "unit hold admission unclassified; controller untouched" as NonEmptyStr } + } +} + +// THE KVM OBSERVER PROBE TAKES THE SAME SLOT (a unit's KVM observer probe, e.g. gunbc.machine_intake_mtcollins1_kvm_observer_observe). // It writes nothing to the controller, but it takes the BMC's one KVM viewer seat, and the boot takes // that seat under this hold and REFUSES its handoff when the seat is busy -- so a probe that did not // hold the unit could make a concurrent boot refuse, and an operator's maintenance would see a viewer // nobody accounted for. Holding the unit makes the probe, the boot and maintenance exclude each other. -fn mtcollins1_kvm_observer_acquire_unit_hold(run_id: NonEmptyStr) -> UnitHoldAcquisition +fn kvm_observer_acquire_unit_hold(host: HostIdentity, run_id: NonEmptyStr) -> UnitHoldAcquisition admit_callers: [ decl_ref(module_path: "gunbc.machine_intake_mtcollins1_kvm_observer_observe", decl_name: "mtcollins1_kvm_observer_observe_wet"), ] { - match self_process_identity() { - SelfUnidentified { cause: c } => - UnitHoldRefused { reason: join(["this probe cannot name its own process (", c as String, "), and a hold it could never be shown dead in would lock the unit out if it died; controller untouched"], "") as NonEmptyStr } - SelfIdentified { process: p, pid_namespace: n } => - unit_hold_acquire(root: unit_hold_store_root, key: mtcollins1_unit_hold_key, owner: unit_hold_owner_ref(o: KvmObserverProbe { run_id: run_id, process: p, pid_namespace: n })) + match unit_hold_admission_for(host: host as NonEmptyStr) { + UnitHoldHostNotManaged { host: h } => unit_hold_not_admitted(admission: UnitHoldHostNotManaged { host: h }) + UnitHoldHostNotRequired { host: h } => unit_hold_not_admitted(admission: UnitHoldHostNotRequired { host: h }) + UnitHoldHostAdmitted { subject: subject } => + match self_process_identity() { + SelfUnidentified { cause: c } => + UnitHoldRefused { reason: join(["this probe cannot name its own process (", c as String, "), and a hold it could never be shown dead in would lock the unit out if it died; controller untouched"], "") as NonEmptyStr } + SelfIdentified { process: p, pid_namespace: n } => + unit_hold_acquire(subject: subject, owner: unit_hold_owner_ref(o: KvmObserverProbe { run_id: run_id, process: p, pid_namespace: n })) + } } } @@ -654,23 +856,47 @@ fn probe_hold_release_outcome_text(o: ProbeHoldReleaseOutcome) -> String { } } -fn mtcollins1_kvm_observer_release_unit_hold(run_id: NonEmptyStr) -> ProbeHoldReleaseOutcome +fn kvm_observer_release_unit_hold(host: HostIdentity, run_id: NonEmptyStr) -> ProbeHoldReleaseOutcome admit_callers: [ decl_ref(module_path: "gunbc.machine_intake_mtcollins1_kvm_observer_observe", decl_name: "mtcollins1_kvm_observer_release_wet"), ] { - match probe_hold_release_decision(observed: observe_file_hold(root: unit_hold_store_root, key: mtcollins1_unit_hold_key), run_id: run_id) { + match unit_hold_admission_for(host: host as NonEmptyStr) { + UnitHoldHostNotManaged { host: h } => kvm_observer_release_not_admitted(admission: UnitHoldHostNotManaged { host: h }) + UnitHoldHostNotRequired { host: h } => kvm_observer_release_not_admitted(admission: UnitHoldHostNotRequired { host: h }) + UnitHoldHostAdmitted { subject: subject } => + match unit_hold_store_executor(subject: subject) { + UnitHoldNotOnStoreHost { reason: r } => ProbeHoldUnreleased { cause: r as String } + UnitHoldOnStoreHost { executor: e } => kvm_observer_release_on_store_host(executor: e, run_id: run_id) + } + } +} + +fn kvm_observer_release_on_store_host(executor: UnitHoldStoreExecutor, run_id: NonEmptyStr) -> ProbeHoldReleaseOutcome + admit_callers: [ + decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "kvm_observer_release_unit_hold"), + ] +{ + let key = executor.subject.key + match probe_hold_release_decision(observed: observe_file_hold(root: unit_hold_store_root, key: key), run_id: run_id) { ProbeHoldFreeNoop => ProbeHoldAlreadyFree ProbeHoldForeignNoop { holder: h } => ProbeHoldNotOurs { holder: h } ProbeHoldUnobservable { cause: c } => ProbeHoldUnreleased { cause: c } ProbeHoldReleaseAt { owner: o, generation: g } => - match file_hold_release_assess(root: unit_hold_store_root, slot_key: mtcollins1_unit_hold_key, owner: o, acquired_generation: g, released_by: concat("mtcollins1-kvm-observer-always-release:", run_id as String) as DurableHoldReleaseRef) { + match file_hold_release_assess(root: unit_hold_store_root, slot_key: key, owner: o, acquired_generation: g, released_by: concat("kvm-observer-always-release:", run_id as String) as DurableHoldReleaseRef) { FileHoldReleaseNotEligible { slot_key: _, refusal: r } => probe_hold_release_refused(refusal: r) FileHoldReleasePlanned { plan: p } => probe_hold_release_committed(outcome: file_hold_release_commit(plan: p)) } } } +fn kvm_observer_release_not_admitted(admission: UnitHoldHostAdmission) -> ProbeHoldReleaseOutcome { + match unit_hold_host_admission_refusal(admission: admission) { + Present { value: r } => ProbeHoldUnreleased { cause: r as String } + Absent => ProbeHoldUnreleased { cause: "unit hold admission unclassified" } + } +} + // THE RELEASE CONSUMES THE PROOF AND KEEPS THE STEP'S OWN OUTCOME, saying when the hold was left: a // run that actuated and then failed to free the unit has still actuated, and an operator reading a // bare success would not know the next run will refuse on a stale holder. @@ -679,7 +905,7 @@ type UnitHoldReleaseOutcome | UnitHoldLeftHeld { cause: NonEmptyStr } fn unit_hold_release_outcome(proof: UnitHoldProof) -> UnitHoldReleaseOutcome { - match file_hold_release_assess(root: proof.root, slot_key: proof.key, owner: proof.owner, acquired_generation: proof.generation, released_by: proof.owner as String as DurableHoldReleaseRef) { + match file_hold_release_assess(root: unit_hold_store_root, slot_key: proof.subject.key, owner: proof.owner, acquired_generation: proof.generation, released_by: proof.owner as String as DurableHoldReleaseRef) { FileHoldReleaseNotEligible { slot_key: _, refusal: _ } => UnitHoldLeftHeld { cause: "the slot no longer showed this run's hold" as NonEmptyStr } FileHoldReleasePlanned { plan: p } => match file_hold_release_commit(plan: p) { @@ -695,69 +921,175 @@ fn unit_hold_release(proof: UnitHoldProof, outcome: ProcessExit) -> ProcessExit match unit_hold_release_outcome(proof: proof) { UnitHoldReleasedCleanly => outcome UnitHoldLeftHeld { cause: c } => - exit_failure(reason: join(["unit hold ", proof.key as String, " left held (", c as String, "); step outcome was: ", match outcome { + exit_failure(reason: join(["unit hold ", proof.subject.key as String, " left held (", c as String, "); step outcome was: ", match outcome { ExitSuccess => "success" ExitFailure { code: _, reason: r } => concat("failure: ", r) }], "")) } } -// A BMC WRITE PATH ASKS THIS BEFORE ITS FIRST REQUEST: the proof must be for this unit's slot. A -// proof for another unit is still a proof, so the key is compared rather than assumed. -fn unit_hold_proof_refusal(proof: UnitHoldProof, key: NonEmptyStr, label: String) -> String? { - if (proof.key as String) == (key as String) { +// A BMC WRITE PATH ASKS THIS BEFORE ITS FIRST REQUEST: the proof must be for the host it is about to +// write to. A proof for another host is still a proof, so the host its subject was admitted from is +// compared rather than assumed. +fn unit_hold_proof_refusal(proof: UnitHoldProof, host: HostIdentity, label: String) -> String? { + if host_identity_eq(a: proof.subject.host.host, b: host) { none } else { - Present { value: join([label, ": unit hold proof is for '", proof.key as String, "', not '", key as String, "'; controller untouched"], "") } + Present { value: join([label, ": unit hold proof is for '", proof.subject.host.host as String, "', not '", host as String, "'; controller untouched"], "") } + } +} + +// ── The operator's side: two entries run in the operator's own session on the store host ─────── +// MAINTENANCE IS ITS OWN OPERATION WITH ITS OWN POLICY: beside the host's hold decision, the operator +// names why the unit is held, through the variable gunbc.host_maintenance_hold_reason declares for +// that host. A host with a hold and no declared reason variable is refused rather than given a +// default name. AdmittedMaintenanceHold is sole_constructor and admit_maintenance_hold_in its only +// mint, so the take and the release below act only on a host that passed both -- and, like every +// other store effect here, only from a process observed on the store host (UnitHoldStoreExecutor). +type AdmittedMaintenanceHold sole_constructor { + subject: AdmittedUnitHoldSubject + reason_env: NonEmptyStr +} + +type MaintenanceHoldAdmission + = MaintenanceHoldAdmitted { hold: AdmittedMaintenanceHold } + | MaintenanceHoldHostRefused { admission: UnitHoldHostAdmission } + | MaintenanceHoldNoReasonVariable { host: HostIdentity } + +fn admit_maintenance_hold_in(hosts: List, host: NonEmptyStr) -> MaintenanceHoldAdmission { + match unit_hold_admission_in(hosts: hosts, host: host) { + UnitHoldHostNotManaged { host: h } => MaintenanceHoldHostRefused { admission: UnitHoldHostNotManaged { host: h } } + UnitHoldHostNotRequired { host: h } => MaintenanceHoldHostRefused { admission: UnitHoldHostNotRequired { host: h } } + UnitHoldHostAdmitted { subject: s } => + match maintenance_hold_reason_env(host: s.host) { + Absent => MaintenanceHoldNoReasonVariable { host: s.host.host } + Present { value: env } => MaintenanceHoldAdmitted { hold: AdmittedMaintenanceHold { subject: s, reason_env: env } } + } } } -// ── The operator's side: two entries run in the operator's own session on the runner host ────── -fn mtcollins1_maintenance_hold_take() -> ProcessExit { - let reason = actions_variable_trimmed(name: mtcollins1_maintenance_reason_env) - if reason == "" { - return exit_failure(reason: concat(mtcollins1_maintenance_reason_env as String, " is unset; a maintenance hold names why the unit is held")) +fn maintenance_hold_admission_refusal(admission: MaintenanceHoldAdmission) -> String { + match admission { + MaintenanceHoldAdmitted { hold: _ } => "" + MaintenanceHoldHostRefused { admission: a } => + match unit_hold_host_admission_refusal(admission: a) { + Present { value: r } => concat("maintenance hold: ", r as String) + Absent => "maintenance hold: unit hold admission unclassified" + } + MaintenanceHoldNoReasonVariable { host: h } => + join(["maintenance hold: managed host '", h as String, "' has a unit hold but gunbc.host_maintenance_hold_reason declares no reason variable for it; nothing was taken or released"], "") } - match file_hold_acquire(root: unit_hold_store_root, slot_key: mtcollins1_unit_hold_key, requested_owner: operator_maintenance_owner(reason: reason as NonEmptyStr)) { - FileHoldAcquired { slot_key: _, owner: _, generation: _ } => ExitSuccess - FileHoldOccupied { slot_key: _, holder: h, generation: _ } => - exit_failure(reason: concat("mtcollins1 maintenance hold: unit already held by ", h as String)) - FileHoldAcquireLost { slot_key: _ } => exit_failure(reason: "mtcollins1 maintenance hold: lost the race; re-run") - FileHoldAcquireStoreUnavailable { slot_key: _, cause: _ } => exit_failure(reason: "mtcollins1 maintenance hold: store unavailable; the unit is NOT held") - FileHoldSlotUndecodable { slot_key: _, generation: _, detail: d } => exit_failure(reason: concat("mtcollins1 maintenance hold: slot undecodable: ", d as String)) - FileHoldKeyNotSlotAddressable { slot_key: _ } => exit_failure(reason: "mtcollins1 maintenance hold: key not slot-addressable") +} + +// THE HOST IS THE ENTRY'S ARGUMENT (`gunbc run ... --function maintenance_hold_take --arg host=