diff --git a/dag/extdeps/linux/proc_meminfo.dag b/dag/extdeps/linux/proc_meminfo.dag index f52806502d4..f513ff3e962 100644 --- a/dag/extdeps/linux/proc_meminfo.dag +++ b/dag/extdeps/linux/proc_meminfo.dag @@ -1,8 +1,9 @@ module extdeps.linux.proc_meminfo -import std.types { NonEmptyStr } +import std.types { NonEmptyStr, String, Bool, Int } import std.types { List } -import std.measure { Kibibyte } +import std.measure { Kibibyte, kibibyte } +import std.algebra { trim } import extdeps.external_authority { ExternalAuthority } import extdeps.uri { Uri, Https } @@ -38,3 +39,157 @@ data meminfo_field_names: List = [ "SwapTotal", "SwapFree", ] + +// READING THE FILE'S TEXT BACK INTO THE SHAPE ABOVE. proc.5 describes /proc/meminfo as one metric +// per line, `Name:` followed by a decimal count and, for every field this module names, the unit +// `kB` -- which proc.5 spells in kilobytes and the kernel emits in KIBIBYTES, so the field type is +// Kibibyte and not a kilobyte. The parse lives here because this module owns the file's shape; the +// transport that produces the text is extdeps.linux.procfs, one of N (DESIGN 3). +// +// A MISSING FIELD IS ITS OWN ARM AND NEVER A ZERO. A host whose kernel does not publish +// MemAvailable (pre-3.14) would otherwise read as a host with no memory available, which is the +// state-space conflation an admission decision cannot survive: zero headroom and unknown headroom +// have opposite remedies, and only one of them is a refusal. +type MeminfoRead + = MeminfoParsed { meminfo: ProcMeminfo } + | MeminfoFieldAbsent { field: NonEmptyStr } + +// THE UNIT IS THE DISCRIMINATOR AND IT IS PRESENT IN THE TEXT, so throwing it away and minting a +// Kibibyte for every line is the one thing this fold must not do (review 69784). +// +// /proc/meminfo IS NOT UNIFORMLY kB. Most lines are `Name: N kB`, and four on every Linux host -- +// HugePages_Total, HugePages_Free, HugePages_Rsvd, HugePages_Surp -- are `Name: N` with NO unit, +// because they are counts of PAGES. Reading a page count as a kibibyte value is wrong by the huge +// page size, 2048x at the usual 2 MiB, and nothing in the resulting type says so: a MemoryMetric +// carrying 0 pages and a MemoryMetric carrying 0 KiB are indistinguishable, and one carrying 3 +// pages claims 3 KiB. That is DESIGN 5's fabricated plausible output in the small -- syntactically +// fine, semantically not the quantity it claims -- and DESIGN 3's instruction for extdeps is to +// model what the API actually returns rather than what would be convenient. +// +// SO A LINE BECOMES A MemoryMetric ONLY IF IT SAYS kB. The third token is required and compared, +// not discarded. A line without it is not a memory measure and has no business in a +// List; excluding it is the type being honest rather than data being lost. +// +// WHAT THIS MEANS FOR all_metrics, said because the name overpromises on its own: it is the +// kB-DENOMINATED metrics, not every line of the file. The unitless lines are unmodelled here and +// would need their own carrier -- a page count is a different quantity, not a memory one -- which +// is a row to add when a consumer exists (DESIGN 3c) rather than a field to fake now. +data meminfo_kibibyte_unit: String = "kB" + +fn meminfo_line_metric(line: String) -> MemoryMetric? { + let tokens = filter(split(s: line, delimiter: " "), t => trim(s: t) != "") + if count(tokens) != 3 { + none + } else { + match first(tokens) { + Absent => none + Present { value: head } => + if !ends_with(s: head, suffix: ":") { + none + } else { + let key = substring(s: head, start: 0, end: length(head) - 1) + match first(tokens |> skip(n: 1)) { + Absent => none + Present { value: raw } => + match first(tokens |> skip(n: 2)) { + Absent => none + Present { value: unit } => + if trim(s: unit) != meminfo_kibibyte_unit { + none + } else { + match parse_int(s: trim(s: raw)) { + Absent => none + Present { value: n } => + if key == "" || n < 0 { none } else { Present { value: MemoryMetric { key: key as NonEmptyStr, value: kibibyte(count: n) } } } + } + } + } + } + } + } + } +} + +fn meminfo_metrics(text: String) -> List { + fold(split(s: text, delimiter: "\n"), init: [], f: (acc, line) => + match meminfo_line_metric(line: line) { + Absent => acc + Present { value: m } => concat(acc, [m]) + }) +} + +fn meminfo_metric_named(metrics: List, name: NonEmptyStr) -> Kibibyte? { + match first(filter(metrics, m => (m.key as String) == (name as String))) { + Absent => none + Present { value: m } => Present { value: m.value } + } +} + +// EVERY NAMED FIELD IS RESOLVED BY THE SAME LOOKUP THAT PROVES IT PRESENT, and that is the whole +// shape of this fold rather than a stylistic preference. +// +// IT WAS WRITTEN THE OTHER WAY FIRST AND THE OTHER WAY WAS WRONG (review 69561 on gunbc#11962). A +// presence pass walked meminfo_field_names and refused the first name it could not find; the record +// was then built from a SECOND spelling of those names, each one falling back to +// `kibibyte(count: 0)` on an absence the presence pass had supposedly ruled out. Two lists for one +// concept is DESIGN 3's nicknaming, and here the fork was load-bearing rather than cosmetic: the +// zero's unreachability was an invariant maintained AT A DISTANCE between the roster and the record, +// so renaming or dropping a roster entry made mem_total and mem_available read 0 KiB -- which a +// compute admission (gunbc.compute.host_capacity compute_reserve_on) turns into a permanent +// below-floor or appropriation-exceeds-total refusal ATTRIBUTED TO THE MACHINE rather than to the +// parse. A fabricated plausible output (DESIGN 5) behind a guard that looked like a wall. +// +// So the guard is deleted rather than strengthened. Each field is matched once, its absence names +// ITSELF, and its value is the one the match just bound: `meminfo_required` and its zero are gone, +// and the fabricated reading has no constructor left to be written in (DESIGN 4b, structurally +// impossible rather than validated). meminfo_field_names is consequently NOT this fold's authority +// and no longer claims to be -- it is the roster of fields this module models, read by consumers +// that want the names; what this parse demands is exactly what ProcMeminfo has fields for, which is +// a fact the record already carries and cannot drift from itself. +// +// The nesting is flat in meaning and deep in shape on purpose: there is no total lookup over seven +// independent optionals that does not either lose which one was missing or introduce a positional +// list, and a positional list would be the same fork one representation over. +fn parse_proc_meminfo(text: String) -> MeminfoRead { + let metrics = meminfo_metrics(text: text) + match meminfo_metric_named(metrics: metrics, name: "MemTotal" as NonEmptyStr) { + Absent => MeminfoFieldAbsent { field: "MemTotal" as NonEmptyStr } + Present { value: mem_total } => + match meminfo_metric_named(metrics: metrics, name: "MemFree" as NonEmptyStr) { + Absent => MeminfoFieldAbsent { field: "MemFree" as NonEmptyStr } + Present { value: mem_free } => + match meminfo_metric_named(metrics: metrics, name: "MemAvailable" as NonEmptyStr) { + Absent => MeminfoFieldAbsent { field: "MemAvailable" as NonEmptyStr } + Present { value: mem_available } => + match meminfo_metric_named(metrics: metrics, name: "Buffers" as NonEmptyStr) { + Absent => MeminfoFieldAbsent { field: "Buffers" as NonEmptyStr } + Present { value: buffers } => + match meminfo_metric_named(metrics: metrics, name: "Cached" as NonEmptyStr) { + Absent => MeminfoFieldAbsent { field: "Cached" as NonEmptyStr } + Present { value: cached } => + match meminfo_metric_named(metrics: metrics, name: "SwapTotal" as NonEmptyStr) { + Absent => MeminfoFieldAbsent { field: "SwapTotal" as NonEmptyStr } + Present { value: swap_total } => + match meminfo_metric_named(metrics: metrics, name: "SwapFree" as NonEmptyStr) { + Absent => MeminfoFieldAbsent { field: "SwapFree" as NonEmptyStr } + Present { value: swap_free } => + MeminfoParsed { + meminfo: ProcMeminfo { + mem_total: mem_total, + mem_free: mem_free, + mem_available: mem_available, + buffers: buffers, + cached: cached, + swap_total: swap_total, + swap_free: swap_free, + all_metrics: metrics, + }, + } + } + } + } + } + } + } + } +} diff --git a/dag/extdeps/linux/procfs.dag b/dag/extdeps/linux/procfs.dag index 7e2721ffc88..7fd793e0995 100644 --- a/dag/extdeps/linux/procfs.dag +++ b/dag/extdeps/linux/procfs.dag @@ -87,9 +87,11 @@ data procfs_paths_read_by_this_repository: List = [ // operation with a shell transport, so gunbc.host_operation_exec can carry it over whichever // transport the caller holds (DESIGN 3: the transport is a realization bound to this shape, never // a fact about procfs). `cat` is the whole realization: procfs files are read-once text and the -// kernel synthesizes them on open, so there is nothing to seek, follow or lock. Three operations -// and not one generic ReadFile, so that the operation's identity says which file it reads and an -// argv over an arbitrary path cannot be materialized from this service. +// kernel synthesizes them on open, so there is nothing to seek, follow or lock. ONE OPERATION PER +// FILE and not one generic ReadFile, so that the operation's identity says which file it reads and +// an argv over an arbitrary path cannot be materialized from this service. ReadMeminfo serves the +// host memory capacity and live availability a compute admission reads before it reserves +// (gunbc.compute.host_capacity). service linux.Procfs { operation ReadStat { input {} @@ -108,6 +110,23 @@ service linux.Procfs { } } + operation ReadMeminfo { + input {} + output { + value: String from "stdout" + success: Bool from "exit_success" + } + readonly + transport shell { argv: ["cat", "/proc/meminfo"] } + exit { + 0 => Unit + nonzero => String "/proc/meminfo read failed" + } + mock_response { + 0 => { value: "MemTotal: 16777216 kB\nMemFree: 1048576 kB\nMemAvailable: 8388608 kB\nBuffers: 65536 kB\nCached: 4194304 kB\nSwapTotal: 0 kB\nSwapFree: 0 kB\n", success: true } "hermetic linux.Procfs.ReadMeminfo" + } + } + operation ReadPidStat { input { pid: NonEmptyStr } output { diff --git a/dag/gunbc/ci/ci_layer_roots.dag b/dag/gunbc/ci/ci_layer_roots.dag index e932f3fbbaa..448b54f0df7 100644 --- a/dag/gunbc/ci/ci_layer_roots.dag +++ b/dag/gunbc/ci/ci_layer_roots.dag @@ -1026,6 +1026,11 @@ data witness_exclusion_frontier: List = [ classification: LocalRepoWetLane, reason: excl_local_repo_wet_tempdir_write_reason, dissolution: excl_local_repo_wet_dissolve}, + WitnessExclusionRow { + pattern: "host_capacity_wet_witness_test.dag", + classification: LocalRepoWetLane, + reason: excl_local_repo_wet_tempdir_write_reason, + dissolution: excl_local_repo_wet_dissolve}, WitnessExclusionRow { pattern: "review_sheet_legacy_declaration_wet_witness_test.dag", classification: LocalRepoWetLane, diff --git a/dag/gunbc/compute/host_capacity.dag b/dag/gunbc/compute/host_capacity.dag new file mode 100644 index 00000000000..a4dbfb0a8a7 --- /dev/null +++ b/dag/gunbc/compute/host_capacity.dag @@ -0,0 +1,511 @@ +module gunbc.compute.host_capacity + +import std.types { String, Bool, Int, NonEmptyStr, EpochSecs } +import std.nat { Nat } +import std.measure { Measure, Memory, Kibi, Kibibyte, kibibyte, kibibyte_count, kibibyte_from_byte_size_floor, ByteSize, byte_size_count } +import extdeps.linux.procfs +import extdeps.linux.proc_meminfo { MeminfoRead, MeminfoParsed, MeminfoFieldAbsent, parse_proc_meminfo } +import product.capacity.pool { Pool, pool_of, NoReplenishment, PoolReading, PoolRead, PoolReadingRefused, pool_reading_at } +import product.capacity.event_chain { PartitionId } +import product.capacity.pool_events { SeatRequest, PoolReleased, pool_full_wire } +import product.capacity.lease { LeasePolicy, LeaseGrant, QuiescenceRequired } +import gunbc.fabric_storage_client { FabricStorageBinding, FabricStorageLocalFiles } +import gunbc.fabric_storage_file_store { fabric_storage_file_root, fabric_storage_file_root_ensure, FabricStorageRootStanding, FabricStorageRootReady, FabricStorageRootRefused } +import gunbc.fabric_event_log { + SeatAcquisition, SeatGranted, SeatFull, SeatContended, SeatAcquireRefused, SeatStoreRefused, + fabric_seat_acquire, seat_acquisition_wire, + SeatStandingObservation, SeatRoomObserved, SeatFullObserved, SeatStandingUnobserved, SeatStandingStoreRefused, fabric_seat_observe, + SeatRelease, SeatReleased, SeatNotHeld, SeatReleaseContended, SeatReleaseRefused, fabric_seat_release, seat_release_wire, + PoolEventAppend, PoolEventAppended, PoolEventContended, PoolEventAppendRefused, fabric_pool_event_append, pool_event_append_wire, +} +import gunbc.fabric_event_log_host { now_epoch_seconds } +import gunbc.roadmap_dashboard_instance { + HostDashboardInstance, dashboard_instance_compute_root, + DashboardInstanceByHost, DashboardInstanceForHost, DashboardInstanceHostUnknown, dashboard_instance_for_host, +} + +// THE HOST'S COMPUTE MEMORY IS A POOL, AND A WORK REQUEST TAKES A SEAT IN IT BEFORE IT RUNS. +// +// gunbc.compute.work_provider_local admitted work by COUNTING LEASE FILES against a policy budget +// of two (compute_cold_build_cap): list the lease directory, compare the count, then create a lease +// for THIS identity. Two things were wrong with that and only the second is about arithmetic. +// +// FIRST, IT WAS NOT ATOMIC. The list and the create are two operations on different names, and the +// create excludes only a second producer of the SAME identity. Two requests with DIFFERENT +// identities both read one lease in flight, both compared 1 < 2, and both created their own lease: +// the cap admitted three. O_EXCL cannot close that, because the thing being over-committed is not a +// name -- it is a quantity, and no exclusive create of any path excludes a quantity. +// +// SECOND, A COUNT IS NOT A CAPACITY. Two producers on a 125 GiB host and two on a 502 GiB host are +// the same policy applied to hosts that differ by a factor of four, and a class that needs a +// gibibyte is charged the same as a release build. What the host actually has is memory, so what is +// reserved is memory -- and the ceiling is compared against a READING of the host rather than +// assumed. +// +// WHAT THIS IS NOT A SECOND AUTHORITY FOR. product.capacity.pool owns the appropriation, the +// encumbrance, the term and the release law; product.capacity.pool_events owns the transitions; +// gunbc.fabric_event_log owns the linearization -- one compare-and-set per append against the +// partition's head, which is what makes the reservation atomic across competing requests rather +// than merely checked. This module declares WHICH pool (the host's compute appropriation), WHERE it +// is linearized (this host, not the fleet), and joins it to the observation. It coins no capacity +// vocabulary of its own. + +// ── WHERE THE LEDGER LIVES, AND WHY NOT THE FLEET'S ──────────────────────────────────────────── +// +// gunbc.fabric_storage_placement places the fabric DB on ONE host and every other host reaches it +// over its served endpoint, which is correct for a fact the FLEET contends on -- an upstream's rate +// limit is metered on the credential, so every host must linearize against one partition. +// +// A HOST'S OWN MEMORY IS NOT SUCH A FACT. The contenders for it are all local, and routing their +// reservation through another machine would mean a local build refusing because a remote host was +// unreachable -- a fail-open in the other direction, since the refusal would not be about capacity +// at all. So the store is the SAME realization (gunbc.fabric_storage_file_store, whose exclusive +// create supplies the linearization) rooted under this host's own compute root. The partition names +// the host so a ledger copied between machines does not silently answer for the wrong one. +// THE SUBJECT OF A RESERVATION: which ledger, which partition, how much the pool appropriates and +// how much this request takes. It is separated from the instance deliberately, and not only to be +// testable: everything below is arithmetic and transaction over these four facts, while reading +// them off a HostDashboardInstance is a JOIN with the deployment's authority. Fusing the two would +// have made every reservation carry a whole deployment record in order to add two numbers, and +// would have left no seam at which the transaction can be exercised on a host other than the one +// the deployment describes. +type ComputeCapacitySubject { + root: NonEmptyStr + partition: PartitionId + appropriation: Kibibyte + request: Kibibyte +} + +// THE POOL IS A HOST'S, AND KEYING IT BY THE INSTANCE WAS A MIS-KEYING (side-chat review of +// gunbc#11962 at dd240f0d, 2026-09-21). srv1 declares TWO dashboard instances -- srv1-live and +// srv1-lab -- with different ids and different instance roots, and the memory they would spend is +// ONE machine's. An instance-keyed partition gives each of them its own appropriation and its own +// ledger, so two pools each promise the same bytes and neither can see the other: the exclusion the +// compare-and-set provides is perfect and is about the wrong subject. +// +// So both halves are keyed by the HOST. The partition names the host identity, and the ledger is +// rooted under the instance THAT HOST resolves to -- gunbc.roadmap_dashboard_instance +// dashboard_instance_for_host, the same host-to-instance authority the fabric event log already +// uses to decide where a host's log lives. Two instances on one host therefore resolve to one +// partition at one root, which is the single host-scoped authority this fact needs; inventing a new +// host-scoped path would have been a second one. +// +// A HOST THAT AUTHORITY CANNOT RESOLVE RESERVES NOTHING. It is not defaulted to the calling +// instance: that is exactly the fork this fix removes, re-entering through a fallback. +type ComputeSubjectResolution + = ComputeSubjectResolved { subject: ComputeCapacitySubject } + | ComputeSubjectHostUnresolved { host: NonEmptyStr } + +fn compute_capacity_root(host_instance: HostDashboardInstance) -> NonEmptyStr { + join([dashboard_instance_compute_root(instance: host_instance) as String, "/capacity"], "") as NonEmptyStr +} + +fn compute_memory_partition(host: NonEmptyStr) -> PartitionId { + join(["compute-memory-", host as String], "") as PartitionId +} + +// THE JOIN WITH THE DEPLOYMENT, and the only function in this module that knows what an instance is. +fn compute_capacity_subject(instance: HostDashboardInstance) -> ComputeSubjectResolution { + match dashboard_instance_for_host(host: instance.host_identity as String) { + DashboardInstanceHostUnknown { host: h } => ComputeSubjectHostUnresolved { host: h as NonEmptyStr } + DashboardInstanceForHost { instance: host_instance } => + ComputeSubjectResolved { + subject: ComputeCapacitySubject { + root: compute_capacity_root(host_instance: host_instance), + partition: compute_memory_partition(host: instance.host_identity), + appropriation: compute_memory_appropriation(instance: host_instance), + request: compute_request_memory(instance: instance), + }, + } + } +} + +fn compute_capacity_store(subject: ComputeCapacitySubject) -> FabricStorageBinding { + FabricStorageLocalFiles { root: fabric_storage_file_root(root: subject.root) } +} + +fn compute_capacity_store_ensure(subject: ComputeCapacitySubject) -> FabricStorageRootStanding { + fabric_storage_file_root_ensure(root: fabric_storage_file_root(root: subject.root)) +} + +// ── WHAT THE HOST HAS, READ RATHER THAN SPELLED ──────────────────────────────────────────────── +// +// TWO FIGURES AND THEY ANSWER DIFFERENT QUESTIONS. MemTotal is the machine's installed memory and +// does not move, which is what a ledger needs: an appropriation whose ceiling changed between two +// folds would make the same chain of events add up differently each time it was read. MemAvailable +// is what is free RIGHT NOW including everything outside this pool -- the runner slices, the +// sessions, the page cache the kernel can hand back -- and it is a LIVE FLOOR, not a ceiling. +// +// Both are needed and neither substitutes for the other. The pool alone would admit work while +// another tenant had eaten the machine; MemAvailable alone would admit work whose own ledger says +// the memory is already promised, because memory a reservation holds but has not yet touched is +// still available to read. +type HostMemoryObservation + = HostMemoryObserved { total: Kibibyte, available: Kibibyte } + | HostMemoryUnobserved { detail: String } + +fn observe_host_memory() -> HostMemoryObservation { + let read = linux.Procfs.ReadMeminfo() + if !read.success { + HostMemoryUnobserved { detail: "/proc/meminfo could not be read on this host" } + } else { + match parse_proc_meminfo(text: read.value) { + MeminfoFieldAbsent { field: f } => HostMemoryUnobserved { detail: join(["/proc/meminfo carries no readable ", f as String, " line"], "") } + MeminfoParsed { meminfo: m } => HostMemoryObserved { total: m.mem_total, available: m.mem_available } + } + } +} + +// ── THE APPROPRIATION, AND WHAT IT REPLACES ──────────────────────────────────────────────────── +// +// THE SHARE OF THE HOST THIS PROVIDER MAY COMMIT, denominated in the bytes the old count was +// implicitly worth: compute_cold_build_cap was two producers, and each producer runs under the +// instance's worker memory ceiling, so two ceilings is EXACTLY the memory the deleted row admitted. +// Nothing is widened by this change and a class that needs less than a ceiling now admits more +// requests than a count ever could. +// +// DECLARED FRONTIER (DESIGN 3c), STATED BECAUSE IT IS THE HONEST LIMIT OF THIS ROW: charging this +// appropriation against the host's OTHER commitments -- the runner slice, the sessions slice, the +// fixed overhead -- is gunbc.ci_runner_placement's conservation wall, and this appropriation is +// DECLARED rather than derived from it. What keeps that from being fail-open is the pair of +// observations below: an appropriation larger than the machine refuses outright, and a request is +// refused when the machine's live availability cannot back it whatever the ledger says. +data compute_pool_slots: Nat = 2 + +fn compute_memory_appropriation(instance: HostDashboardInstance) -> Kibibyte { + kibibyte(count: kibibyte_count(k: kibibyte_from_byte_size_floor(b: instance.dispatch_worker_memory_max)) * compute_pool_slots) +} + +// THE UNIT'S CEILING IS THE RESERVED AMOUNT, and that identity is the whole point rather than a +// convenience. A reservation of X that caps the unit at Y is arithmetic about a number nothing +// enforces: if Y > X the pool's total is a fiction, and if Y < X the pool refuses work the host +// could have run. So one figure serves both, and it is the instance's worker memory ceiling -- +// the existing safety limit, unchanged and now also the thing being counted. +// +// DECLARED FRONTIER: a per-work-class amount (a claims run does not need a release build's +// ceiling) needs per-class peak measurements, which the consumption reading this change starts +// recording is the first producer of. Until those exist every class reserves the ceiling, which +// over-reserves and never under-reserves. +fn compute_request_memory(instance: HostDashboardInstance) -> Kibibyte { + kibibyte_from_byte_size_floor(b: instance.dispatch_worker_memory_max) +} + +// A COMPUTE SEAT IS QUIESCENCE-REQUIRED AND THAT IS THE SAFE ARM, NOT A LIMITATION. A running cargo +// cannot be told its lease lapsed -- there is no fence a compute unit honours -- so a term that runs +// out frees nothing, and product.capacity.pool holds the encumbrance until the seat is RELEASED. +// A worker that dies wedges its own share rather than silently handing it to the next arrival, +// which is the only direction that cannot oversubscribe a machine. Recovering a wedged seat is an +// explicit release naming why, which is the same entry completion and cancellation take. +fn compute_lease_policy(term_seconds: Nat) -> LeasePolicy { + LeasePolicy { maximum_duration_seconds: term_seconds, release_law: QuiescenceRequired } +} + +// THE BACKING RELATION, AND IT IS THE WHOLE REASON THE TWO OBSERVATIONS ARE NOT INDEPENDENT CHECKS. +// +// The first revision compared the pool's committed total against the appropriation in one place and +// the machine's live availability against ONE request in another. Both checks passed and the pair +// still double-promised (side-chat review of gunbc#11962 at dd240f0d, 2026-09-21): with a 52 GiB +// appropriation, 30 GiB available and two 26 GiB requests, each request sees 26 <= 30 and each fits +// the appropriation, so BOTH admit -- because neither sees the other's granted-but-not-yet-consumed +// memory. The compare-and-set was doing its job perfectly on a question that was missing a term. +// +// The fix is not a third check. The pool already computes the committed total INSIDE the linearized +// fold, so the machine's reading belongs in the SAME comparison: the ceiling this attempt is +// adjudicated against is the smaller of the declared appropriation and what the host says is free. +// Then "everything this pool has promised, plus what I am asking for, must fit in what the machine +// actually has" is one predicate evaluated in one CAS'd step, and the second 26 GiB request is +// refused as a full pool because 26 + 26 > 30. +// +// WHAT THIS ADMITS AGAINST IS AN ESTIMATE, AND IT IS NOT A NO-OOM GUARANTEE. MemAvailable is the +// kernel's own ESTIMATE of what a new workload could obtain without swapping, it moves between the +// reading and the grant, and nothing here constrains the processes outside this pool. So the claim +// this relation supports is "this pool does not knowingly promise more than the machine reported", +// which is a real property and is strictly weaker than "no admitted workload will be OOM-killed". +// The unit's own MemoryMax is what bounds a single workload; this is what stops the POOL from +// over-promising. Conflating the two would be the rung inflation DESIGN 4b forbids. +// +// WORST-CASE-SOUND, AND CONSERVATIVE, AND SAYING SO. MemAvailable already excludes whatever the +// pool's outstanding grants have actually touched, so a grant that is fully resident is counted +// twice -- once in the machine's reading and once in the committed total. That errs toward refusing +// work the host could have run, which is the direction a safety admission must err in when the term +// it needs is unobserved. The exact relation needs the RESIDENT share of outstanding grants, which +// is observable -- each grant runs in a named transient unit with its own cgroup -- and is not +// observed here. DECLARED FRONTIER (DESIGN 3c), trigger: a per-host read of the compute units' +// current usage, whose first consumer is this fold; until it lands the conservative bound stands +// and the cost is stated rather than hidden. +// +// A CEILING THAT MOVES BETWEEN ATTEMPTS IS SAFE BY CONSTRUCTION HERE, which is why this is a ceiling +// and not a pre-check. product.capacity.pool ruled that replay does not adjudicate the ceiling -- +// an event's admission happened when it was written -- so a dip in availability cannot make a +// historical acquire refuse the fold and poison the partition. It makes the pool over-committed, +// which refuses new acquires until it drains. That is the correct consequence of a reduction. +fn compute_backing_ceiling(subject: ComputeCapacitySubject, available: Kibibyte) -> Kibibyte { + if kibibyte_count(k: available) < kibibyte_count(k: subject.appropriation) { available } else { subject.appropriation } +} + +fn compute_memory_root_pool(subject: ComputeCapacitySubject, ceiling: Kibibyte) -> Pool { + pool_of( + identity: subject.partition as String as NonEmptyStr, + ceiling: ceiling, + replenishment: NoReplenishment, + release_law: QuiescenceRequired, + ) +} + +// ── THE RESERVATION ──────────────────────────────────────────────────────────────────────────── +// +// EVERY ARM IS TYPED AND NONE OF THEM WIDENS. Insufficient capacity is ComputeCapacityFull and says +// so; a machine whose live availability cannot back the request is ComputeHostBelowFloor and is a +// DIFFERENT fact with a different remedy (wait, or find out who else is on the host); an +// unobservable host reserves nothing at all rather than reserving against a guess. +type ComputeReservation + = ComputeReserved { grant: LeaseGrant, partition: PartitionId, amount: Kibibyte, store: FabricStorageBinding } + | ComputeCapacityFull { wire: String } + | ComputeHostBelowFloor { requested: Kibibyte, available: Kibibyte } + | ComputeReservationRefused { detail: String } + +data compute_seat_attempts: Nat = 3 +data compute_partition_read_budget: Nat = 4096 + +// THE APPROPRIATION IS CHECKED AGAINST THE MACHINE BEFORE ANY SEAT IS TAKEN. A host too small for +// the declared share is a configuration error that would otherwise present as an OOM kill during a +// build, which is the same information arriving hours later and destructively. +fn compute_reserve(instance: HostDashboardInstance, reference: NonEmptyStr, term_seconds: Nat) -> ComputeReservation { + match compute_capacity_subject(instance: instance) { + ComputeSubjectHostUnresolved { host: h } => + ComputeReservationRefused { detail: join(["no dashboard instance is declared for host ", h as String, ", so this host has no compute capacity authority to reserve against"], "") } + ComputeSubjectResolved { subject: subject } => compute_reserve_on(subject: subject, reference: reference, term_seconds: term_seconds) + } +} + +// THE DECISION TAKES THE OBSERVATION AS A VALUE, AND THE DOOR ABOVE TAKES THE READING. +// +// It used to read /proc/meminfo itself, which made the admission arithmetic untestable except +// against whatever the host happened to be doing: the headroom control had to DERIVE its fixture +// from the live reading, and a fixture derived from the thing under test is not a fixture. It was +// wrong in both directions -- on a lightly loaded host the derived appropriation exceeded MemTotal +// and the cell refused before reaching the comparison it existed to make, and on a busy one it +// passed for reasons unrelated to the relation (side-chat review of gunbc#11962 at 725d9c58). +// +// So the boundary is here: this fold decides admission from a supplied observation, and +// compute_reserve supplies the real one. DESIGN 3's pairing obligation is discharged by an +// inhabitance claim that observe_host_memory really produces a well-formed reading of this machine, +// and by the srv1 receipts, where the whole path runs for real. +fn compute_reserve_on(subject: ComputeCapacitySubject, reference: NonEmptyStr, term_seconds: Nat) -> ComputeReservation { + match observe_host_memory() { + HostMemoryUnobserved { detail: d } => ComputeReservationRefused { detail: join(["the host's memory could not be observed, so nothing was reserved: ", d], "") } + HostMemoryObserved { total: total, available: available } => + compute_reserve_against(subject: subject, reference: reference, term_seconds: term_seconds, total: total, available: available) + } +} + +fn compute_reserve_against( + subject: ComputeCapacitySubject, + reference: NonEmptyStr, + term_seconds: Nat, + total: Kibibyte, + available: Kibibyte, +) -> ComputeReservation { + if kibibyte_count(k: subject.appropriation) > kibibyte_count(k: total) { + ComputeReservationRefused { + detail: join([ + "the compute appropriation is ", to_string(value: kibibyte_count(k: subject.appropriation)), + " KiB and this host has ", to_string(value: kibibyte_count(k: total)), + " KiB installed, so the share was never backed by the machine", + ], ""), + } + } else if kibibyte_count(k: available) < kibibyte_count(k: subject.request) { + ComputeHostBelowFloor { requested: subject.request, available: available } + } else { + match compute_capacity_store_ensure(subject: subject) { + FabricStorageRootRefused { area: a, detail: d } => ComputeReservationRefused { detail: join(["the capacity ledger could not be prepared at ", a, ": ", d], "") } + FabricStorageRootReady => + match now_epoch_seconds() { + Absent => ComputeReservationRefused { detail: "the clock could not be read as epoch seconds" } + Present { value: now } => compute_seat(subject: subject, reference: reference, now: now, term_seconds: term_seconds, ceiling: compute_backing_ceiling(subject: subject, available: available)) + } + } + } +} + +// A REFUSED ACQUIRE IS NOT AUTOMATICALLY A FULL POOL. The carrier renders every pool refusal into +// SeatFull, so the reason survives only in the wire; a DuplicateReference reported as capacity sent +// an operator looking for a busy host while srv1 had 400 GiB free (2026-09-21). The marker is read +// from the authority that writes it (product.capacity.pool_events pool_full_wire), never re-spelled +// here, and anything else is a ledger refusal with its text carried through. +fn compute_seat(subject: ComputeCapacitySubject, reference: NonEmptyStr, now: EpochSecs, term_seconds: Nat, ceiling: Kibibyte) -> ComputeReservation { + let store = compute_capacity_store(subject: subject) + match fabric_seat_acquire( + store: store, + partition: subject.partition, + root: compute_memory_root_pool(subject: subject, ceiling: ceiling), + actor: reference, + request: SeatRequest { reference: reference, amount: subject.request, at: now, term_seconds: term_seconds }, + policy: compute_lease_policy(term_seconds: term_seconds), + attempts: compute_seat_attempts, + budget: compute_partition_read_budget, + ) { + SeatGranted { grant: g, generation: _, attempts_used: _ } => ComputeReserved { grant: g, partition: subject.partition, amount: subject.request, store: store } + SeatFull { wire: w, attempts_used: n } => + if starts_with(s: w, prefix: pool_full_wire) { + ComputeCapacityFull { wire: join([w, " (attempt ", to_string(value: n), ")"], "") } + } else { + ComputeReservationRefused { detail: join(["the capacity ledger refused the acquire: ", w, " (attempt ", to_string(value: n), ")"], "") } + } + other => ComputeReservationRefused { detail: seat_acquisition_wire(a: other) } + } +} + +// ── THE RELEASE, WHICH IS THE ONLY WAY CAPACITY COMES BACK ───────────────────────────────────── +// +// COMPLETION AND CANCELLATION ARE THE SAME TRANSITION WITH DIFFERENT REASONS, which is why the +// reason is carried rather than encoded in two functions: the pool does not care why a holder +// stopped, and a caller that had to choose between two spellings would eventually pick the wrong +// one on the path it exercises least -- which is always the cancellation path. +// +// A RELEASE THAT DID NOT LAND IS NOT A RELEASE. The append is retried against a moving head and +// exhaustion is its own arm; nothing here reports a return of capacity it did not observe. +type ComputeRelease + = ComputeReleased { partition: PartitionId, reference: NonEmptyStr, reason: NonEmptyStr } + | ComputeReleaseRefused { detail: String } + +fn compute_release(reservation: ComputeReservation, reason: NonEmptyStr) -> ComputeRelease { + match reservation { + ComputeCapacityFull { wire: w } => ComputeReleaseRefused { detail: join(["nothing to release: ", w], "") } + ComputeHostBelowFloor { requested: _, available: _ } => ComputeReleaseRefused { detail: "nothing to release: the host was below its live memory floor" } + ComputeReservationRefused { detail: d } => ComputeReleaseRefused { detail: join(["nothing to release: ", d], "") } + ComputeReserved { grant: g, partition: p, amount: _, store: store } => + compute_release_on(store: store, partition: p, appropriation: kibibyte(count: 0), reference: g.reference, reason: reason) + } +} + +// THE ONE RELEASE PATH, CHECKED. It reads, folds, PROPOSES the release against the folded pool and +// appends only what the pool admits -- the mirror of the acquire. That check is load-bearing rather +// than defensive: a reference the pool is not holding, appended anyway, would not fail at the +// append; it would fail at every later READ, when the fold hits UnknownEncumbrance and refuses the +// WHOLE partition. +// +// THE OPERATOR'S RECOVERY DOOR IS NOT HERE, and its absence is declared rather than implied. The +// discharge of a seat whose release did not land needs a termination decision bound to the unit, an +// attempt-to-unit binding that cannot release another attempt's live reservation, and a settled +// state a retry consumes -- see gunbc.recurring_failure_mode +// a_held_compute_seat_has_no_in_corpus_discharge, whose trigger names that capability. Shipping a +// recovery route with any of those missing would FREE SEATS THAT SHOULD NOT BE FREED, which is +// worse than not having one: without it every failure here keeps the charge and the host merely +// under-admits. +// +// THE APPROPRIATION PASSED HERE IS NOT LOAD-BEARING AND THE ZERO IS NOT A FABRICATED READING. product.capacity.pool +// ruled that replay never adjudicates the ceiling, so a release is decided by whether the ledger +// HOLDS the reference and by nothing about capacity; a reservation released from its own provider +// carries no subject to read an appropriation from, and inventing one for it would be a number with +// no consequence. Where a subject is at hand it is passed; where none is, zero is passed, and zero +// cannot admit anything -- which is the right direction for a value nothing should be deciding on. +fn compute_release_on( + store: FabricStorageBinding, + partition: PartitionId, + appropriation: Kibibyte, + reference: NonEmptyStr, + reason: NonEmptyStr, +) -> ComputeRelease { + match now_epoch_seconds() { + Absent => ComputeReleaseRefused { detail: "the clock could not be read as epoch seconds" } + Present { value: now } => + match fabric_seat_release( + store: store, + partition: partition, + root: pool_of( + identity: partition as String as NonEmptyStr, + ceiling: appropriation, + replenishment: NoReplenishment, + release_law: QuiescenceRequired, + ), + reference: reference, + reason: reason, + at: now, + attempts: compute_seat_attempts, + budget: compute_partition_read_budget, + ) { + SeatReleased { reference: r, id: _ } => ComputeReleased { partition: partition, reference: r, reason: reason } + other => ComputeReleaseRefused { detail: seat_release_wire(r: other) } + } + } +} + +// ── WHAT THE HOST IS CARRYING, WITHOUT TAKING FROM IT ────────────────────────────────────────── +// +// THE AGGREGATE READING A RECEIPT CARRIES: what the ledger says is committed on this host, beside +// what the machine says is free. The two are independent measurements of one quantity and a +// receipt that carried only the first would be a ledger agreeing with itself (DESIGN 5: a +// measurement copied from the same tree is not an oracle). Their DISAGREEMENT is the signal -- +// committed far above the machine's own shortfall means the pool is over-reserving each class, and +// the reverse means work is running outside the pool. +type ComputeCapacityStanding + = ComputeCapacityStandingRead { committed: Kibibyte, ceiling: Kibibyte, headroom: Kibibyte, observed_available: Kibibyte, observed_total: Kibibyte } + | ComputeCapacityStandingUnread { detail: String } + +fn compute_capacity_standing(instance: HostDashboardInstance) -> ComputeCapacityStanding { + match compute_capacity_subject(instance: instance) { + ComputeSubjectHostUnresolved { host: h } => ComputeCapacityStandingUnread { detail: join(["no dashboard instance is declared for host ", h as String], "") } + ComputeSubjectResolved { subject: subject } => compute_capacity_standing_on(subject: subject) + } +} + +fn compute_capacity_standing_on(subject: ComputeCapacitySubject) -> ComputeCapacityStanding { + match observe_host_memory() { + HostMemoryUnobserved { detail: d } => ComputeCapacityStandingUnread { detail: d } + HostMemoryObserved { total: total, available: available } => + match now_epoch_seconds() { + Absent => ComputeCapacityStandingUnread { detail: "the clock could not be read as epoch seconds" } + Present { value: now } => + match fabric_seat_observe( + store: compute_capacity_store(subject: subject), + partition: subject.partition, + root: compute_memory_root_pool(subject: subject, ceiling: subject.appropriation), + at: now, + budget: compute_partition_read_budget, + ) { + SeatRoomObserved { headroom: h, generation: _ } => + ComputeCapacityStandingRead { + committed: kibibyte(count: kibibyte_count(k: subject.appropriation) - kibibyte_count(k: h)), + ceiling: subject.appropriation, + headroom: h, + observed_available: available, + observed_total: total, + } + SeatFullObserved { generation: _ } => + ComputeCapacityStandingRead { + committed: subject.appropriation, + ceiling: subject.appropriation, + headroom: kibibyte(count: 0), + observed_available: available, + observed_total: total, + } + SeatStandingUnobserved { step: s, reason: why } => ComputeCapacityStandingUnread { detail: join(["the capacity ledger could not be read at ", s, ": ", why], "") } + SeatStandingStoreRefused { cause: _ } => ComputeCapacityStandingUnread { detail: "the capacity ledger refused the read" } + } + } + } +} + +fn compute_reservation_wire(r: ComputeReservation) -> String { + match r { + ComputeReserved { grant: g, partition: p, amount: a, store: _ } => + join(["reserved ", to_string(value: kibibyte_count(k: a)), " KiB on ", p as String, " as ", g.reference as String, " fence=", g.fence.grant as String, " expires_at=", to_string(value: g.expires_at)], "") + ComputeCapacityFull { wire: w } => join(["capacity full: ", w], "") + ComputeHostBelowFloor { requested: rq, available: av } => + join(["host below floor: ", to_string(value: kibibyte_count(k: rq)), " KiB requested, ", to_string(value: kibibyte_count(k: av)), " KiB available"], "") + ComputeReservationRefused { detail: d } => join(["refused: ", d], "") + } +} + +fn compute_capacity_standing_wire(s: ComputeCapacityStanding) -> String { + match s { + ComputeCapacityStandingRead { committed: c, ceiling: cl, headroom: h, observed_available: av, observed_total: tt } => + join([ + "committed ", to_string(value: kibibyte_count(k: c)), " KiB of ", to_string(value: kibibyte_count(k: cl)), + " KiB (headroom ", to_string(value: kibibyte_count(k: h)), " KiB); host reports ", to_string(value: kibibyte_count(k: av)), + " KiB available of ", to_string(value: kibibyte_count(k: tt)), " KiB installed", + ], "") + ComputeCapacityStandingUnread { detail: d } => join(["unread: ", d], "") + } +} diff --git a/dag/gunbc/compute/test_run.dag b/dag/gunbc/compute/test_run.dag index 3711f1b1f6e..4ad563fe459 100644 --- a/dag/gunbc/compute/test_run.dag +++ b/dag/gunbc/compute/test_run.dag @@ -19,6 +19,7 @@ import gunbc.roadmap_execution_contract { GitWorkspaceCapability } import gunbc.compute.work_request { WorkOperation, RunClaims, CompileEntry } import gunbc.compute.work_provider_local { ProvideResult, ProvideFresh, ProvideAttached, compute_provide, provide_result_succeeded, provide_result_ending, provide_result_identity, provide_result_document, + HostRecordStatus, HostRecordWritten, HostRecordLost, provide_result_host_record, host_record_wire, host_record_was_written, compute_write_host_record_note, } import gunbc.compute.test_selection { SelectedFile, select_witness_files, classify_witness_module, planned_functions_joined, @@ -86,7 +87,7 @@ fn show_file(instance: HostDashboardInstance, worktree: String, commit: String, // One selected module's result in the report. type ModuleRun - = ModuleRan { label: String, module_path: String, planned: List, declined: List, ending: String, identity: String, document: String } + = ModuleRan { label: String, module_path: String, planned: List, declined: List, ending: String, identity: String, document: String, host_record: String } | ModuleAllDeclined { label: String, module_path: String, declined: List } | ModuleUnreadable { label: String, path: String, reason: String } | ModuleNotAWitness { label: String, path: String, reason: String } @@ -105,15 +106,22 @@ fn run_selected_module(instance: HostDashboardInstance, worktree: String, commit ModuleRan { label: render_label(l: label), module_path: module_path, planned: planned, declined: declined, ending: provide_result_ending(r: result), identity: provide_result_identity(r: result), document: provide_result_document(r: result), + host_record: host_record_wire(h: provide_result_host_record(r: result)), } } } } } +// A HOST-RECORD LOSS COUNTS AGAINST THE MODULE'S VERDICT, and that is the point of carrying it this +// far. The worker CLIs are where a compute result stops being a value and becomes an exit code, so a +// loss that reaches here and is not counted is a loss nobody ever hears about: the dependent request +// dropped it at one seam (compute_provide_dependent) and these two consumers dropped it at the next +// (side-chat review at f5344b28). The work's own ending is still reported verbatim in the receipt -- +// what changes is only whether the run is called clean. fn module_run_succeeded(r: ModuleRun) -> Bool { match r { - ModuleRan { label: _, module_path: _, planned: _, declined: _, ending, identity: _, document: _ } => ending == "succeeded" + ModuleRan { label: _, module_path: _, planned: _, declined: _, ending, identity: _, document: _, host_record: record } => ending == "succeeded" && record == "" ModuleAllDeclined { label: _, module_path: _, declined: _ } => true ModuleUnreadable { label: _, path: _, reason: _ } => false ModuleNotAWitness { label: _, path: _, reason: _ } => true @@ -129,7 +137,7 @@ fn standing_json(s: WitnessStanding) -> JsonValue { fn module_run_json(r: ModuleRun) -> JsonValue { match r { - ModuleRan { label, module_path, planned, declined, ending, identity, document: _ } => + ModuleRan { label, module_path, planned, declined, ending, identity, document: _, host_record: record } => json_object(members: [ json_kv(key: "label", value: json_string(s: label)), json_kv(key: "module", value: json_string(s: module_path)), @@ -137,6 +145,7 @@ fn module_run_json(r: ModuleRun) -> JsonValue { json_kv(key: "declined", value: json_array(elements: map(declined, standing_json))), json_kv(key: "ending", value: json_string(s: ending)), json_kv(key: "identity", value: json_string(s: identity)), + json_kv(key: "host_record", value: json_string(s: record)), ]) ModuleAllDeclined { label, module_path, declined } => json_object(members: [ @@ -164,7 +173,7 @@ fn test_run_report_json(r: TestRunReport) -> JsonValue { json_kv(key: "pattern", value: json_string(s: pattern)), json_kv(key: "snapshot_commit", value: json_string(s: commit)), json_kv(key: "selected", value: json_int(n: count(modules))), - json_kv(key: "succeeded", value: json_int(n: count(filter(modules, m => match m { ModuleRan { label: _, module_path: _, planned: _, declined: _, ending, identity: _, document: _ } => ending == "succeeded" _ => false })))), + json_kv(key: "succeeded", value: json_int(n: count(filter(modules, m => match m { ModuleRan { label: _, module_path: _, planned: _, declined: _, ending, identity: _, document: _, host_record: record } => ending == "succeeded" && record == "" _ => false })))), json_kv(key: "not_succeeded", value: json_int(n: count(filter(modules, m => !module_run_succeeded(r: m))))), json_kv(key: "modules", value: json_array(elements: map(modules, module_run_json))), ]) @@ -264,9 +273,13 @@ fn compile_entry_cli(repo_root: String, worktree: String, entry: String, receipt SnapshotRefused { step, detail } => ExitFailure { code: 2, reason: join(["gunbc compile: snapshot refused at ", step, ": ", detail], "") } SnapshotResolved { commit } => { let result = compute_provide(instance: instance, commit: commit, op: CompileEntry { entry: entry as FilePath }) + let record = provide_result_host_record(r: result) let receipt = Filesystem.Write(path: receipt_path, content: provide_result_document(r: result)) + let record_note = compute_write_host_record_note(receipt_path: receipt_path, record: record) if !receipt.success { ExitFailure { code: 2, reason: join(["gunbc compile: receipt could not be written to ", receipt_path, ": ", receipt.error, "; outcome was ", provide_result_document(r: result)], "") } + } else if !host_record_was_written(h: record) { + ExitFailure { code: 1, reason: join(["gunbc compile: the work ended ", provide_result_ending(r: result), " and its stored record is authoritative, but ", host_record_wire(h: record), "; ", record_note], "") } } else if provide_result_succeeded(r: result) { ExitSuccess } else { diff --git a/dag/gunbc/compute/work_provider_local.dag b/dag/gunbc/compute/work_provider_local.dag index fb1eea1c1eb..13ca10a3a44 100644 --- a/dag/gunbc/compute/work_provider_local.dag +++ b/dag/gunbc/compute/work_provider_local.dag @@ -7,9 +7,15 @@ import std.measure { byte_size_count } import extdeps.filesystem.filesystem_io { Filesystem } import gunbc.output_policy { OutcomeIsData } import extdeps.gunbc +import extdeps.shell import extdeps.git { shape_git_worktree_add_detached_argv } import extdeps.git.object_store { GitObjectId, git_object_id_from_untagged_hex, git_object_id_wire_hex } import extdeps.systemd.systemd_run { systemd_run_user_wait_arguments, systemd_run_property } +import extdeps.systemd.systemctl +import extdeps.linux.cgroup_v2 { + cgroup_v2_mount_point, cgroup_v2_events_path, + CgroupEventsDecoding, CgroupEventsDecoded, CgroupEventsUnparseable, decode_cgroup_events_populated, +} import extdeps.cache.sccache { sccache_installed_binary_path } import gunbc.clock_read { clock_now_probed_at_or_unknown } import gunbc.roadmap_dashboard_instance { @@ -20,30 +26,39 @@ import gunbc.roadmap_dispatch_actuator { dispatch_capability_program } import gunbc.roadmap_execution_contract { ExecutionCapability, GitWorkspaceCapability, CargoCapability, RustcCapability, AttemptStateDirectoryCapability, } +import std.measure { Kibibyte, kibibyte_count, kibibyte_to_byte_size } +import gunbc.compute.host_capacity { + ComputeReservation, ComputeReserved, ComputeCapacityFull, ComputeHostBelowFloor, ComputeReservationRefused, + ComputeRelease, ComputeReleased, ComputeReleaseRefused, compute_reserve, compute_release, compute_reservation_wire, + ComputeCapacityStanding, ComputeCapacityStandingRead, ComputeCapacityStandingUnread, compute_capacity_standing, compute_capacity_standing_wire, +} import gunbc.compute.work_request { WorkSubject, ExactTree, WorkOperation, BuildGunbcBinaries, CompileEntry, RunClaims, CargoProfile, CargoRelease, CargoDebug, WorkToolchainIdentity, work_identity, work_identity_hex, work_default_build, work_declared_outputs, DeclaredOutput, WorkOutputRoot, CheckoutRoot, TargetRoot, WorkOutput, WorkOutcome, WorkSucceeded, WorkFailed, WorkRefusedByInfrastructure, WorkCancelled, WorkOutputMismatch, - WorkInfrastructureRefusal, ProducerInFlight, HostAtColdBuildCap, CheckoutUnavailable, StoreUnavailable, + WorkInfrastructureRefusal, ProducerInFlight, HostComputeCapacityFull, HostBelowMemoryFloor, ComputeCapacityLedgerUnavailable, + CheckoutUnavailable, StoreUnavailable, ToolchainUnobserved, DependencyNotSucceeded, SubjectUnresolved, work_outcome_wire, work_outcome_ending, StoredOutcomeRead, StoredOutcomeFound, StoredOutcomeUnreadable, stored_outcome_decode, stored_outcome_is_success, } // THE LOCAL PROVIDER: one of N behind the exact work contract, serving the host it runs on. It is a // realization and knows nothing the contract does not: it resolves the subject, observes the -// toolchain, takes a lease, checks the commit out, runs the operation inside a transient user unit -// with a memory bound, returns declared outputs by content into a store, and writes the outcome -// beside them. A second caller with the same identity attaches to the stored outcome and runs +// toolchain, takes a producer lease, RESERVES THE MEMORY THE WORK WILL USE out of the host's +// compute pool, checks the commit out, runs the operation inside a transient user unit capped at +// exactly that reservation, returns declared outputs by content into a store, writes the outcome +// beside them, and releases the reservation on every ending. A second caller with the same identity attaches to the stored outcome and runs // nothing (compute-deduplication-and-admission's first slice: two callers, one build). Placement // across the fabric is the next slice; this provider's boundary is the host. -// HOW MANY COLD BUILDS THIS HOST CARRIES AT ONCE. A policy budget, not a measurement: each producer -// runs under the instance's worker memory ceiling, and two of them fit beside the serve and belt -// units on the smaller build host (srv2, 125 GiB) without the page-cache eviction that hung srv1 in -// August. The dedup row's red control is that a caller refused for capacity is told so and counted; -// it is, as HostAtColdBuildCap. -data compute_cold_build_cap: Int = 2 +// HOW LONG A COMPUTE RESERVATION DECLARES IT WILL HOLD. Two hours covers the cold release build +// this provider's heaviest class runs, and it is a DECLARATION rather than a deadline anything +// enforces: the pool's release law for a compute seat is quiescence-required +// (gunbc.compute.host_capacity), so a term that runs out frees nothing and the seat comes back only +// by an explicit release. Saying so here rather than leaving the reader to infer a reclaim that +// does not happen. +data compute_reservation_term_seconds: Int = 7200 type ComputeLayout { root: String @@ -56,6 +71,7 @@ type ComputeLayout { target_dir: String log_path: String outcome_path: String + consumption_path: String } fn compute_layout(instance: HostDashboardInstance, identity_hex: String) -> ComputeLayout { @@ -72,6 +88,7 @@ fn compute_layout(instance: HostDashboardInstance, identity_hex: String) -> Comp target_dir: join([root, "/target"], ""), log_path: join([work_dir, "/log"], ""), outcome_path: join([work_dir, "/outcome.json"], ""), + consumption_path: join([work_dir, "/consumption"], ""), } } @@ -134,40 +151,97 @@ fn compute_ensure_dir(instance: HostDashboardInstance, path: String) -> Bool { } } -fn compute_count_lines(text: String) -> Int { - count(filter(text.split(sep: "\n"), l => trim(s: l) != "")) -} - // What a provide returns: a fresh run's outcome, or an attachment to a stored one (no run). +// THE WORK'S RESULT AND THIS HOST'S RECORD ARE TWO FACTS AND ARE RETURNED AS TWO. +// +// They were fused twice, in opposite directions, and both were wrong. First a successful run whose +// release failed handed the caller a REFUSAL while outcome.json said it succeeded -- so the caller +// and the next attacher read different contracts. Then the repair for a lost host record did the +// same thing again: it published the real outcome and synthesized a WorkRefusedByInfrastructure for +// the caller (side-chat review at 773825cf). The stored document is what a later caller attaches +// to, so a returned outcome that differs from it is a disagreement no wording can fix. +// +// So the outcome carried here is ALWAYS the outcome that was stored, and whether this host managed +// to record its own side facts rides beside it. Both consumers get the same contract about the +// work; only this caller learns that the host lost its record, which is the only consumer that +// could act on it anyway. +type HostRecordStatus + = HostRecordWritten + | HostRecordLost { detail: String } + type ProvideResult - = ProvideFresh { outcome: WorkOutcome, document: String } - | ProvideAttached { identity: String, ending: String, document: String } + = ProvideFresh { outcome: WorkOutcome, document: String, host_record: HostRecordStatus } + | ProvideAttached { identity: String, ending: String, document: String, host_record: HostRecordStatus } + +fn provide_result_host_record(r: ProvideResult) -> HostRecordStatus { + match r { + ProvideFresh { outcome: _, document: _, host_record: h } => h + ProvideAttached { identity: _, ending: _, document: _, host_record: h } => h + } +} + +fn host_record_wire(h: HostRecordStatus) -> String { + match h { + HostRecordWritten => "" + HostRecordLost { detail: d } => join(["; HOST RECORD LOST: ", d], "") + } +} + +// JOINING TWO HOST-RECORD FACTS: a loss anywhere in the chain is a loss the caller must hear about, +// so the arms accumulate rather than the later one winning. Both details are kept because they name +// different identities and an operator needs each one. +fn host_record_join(a: HostRecordStatus, b: HostRecordStatus) -> HostRecordStatus { + match a { + HostRecordWritten => b + HostRecordLost { detail: da } => + match b { + HostRecordWritten => HostRecordLost { detail: da } + HostRecordLost { detail: db } => HostRecordLost { detail: join([da, "; and ", db], "") } + } + } +} + +fn provide_result_with_host_record(r: ProvideResult, carried: HostRecordStatus) -> ProvideResult { + match r { + ProvideFresh { outcome: o, document: d, host_record: h } => + ProvideFresh { outcome: o, document: d, host_record: host_record_join(a: carried, b: h) } + ProvideAttached { identity: i, ending: e, document: d, host_record: h } => + ProvideAttached { identity: i, ending: e, document: d, host_record: host_record_join(a: carried, b: h) } + } +} + +fn host_record_was_written(h: HostRecordStatus) -> Bool { + match h { + HostRecordWritten => true + HostRecordLost { detail: _ } => false + } +} fn provide_result_succeeded(r: ProvideResult) -> Bool { match r { - ProvideFresh { outcome, document: _ } => work_outcome_ending(o: outcome) == "succeeded" - ProvideAttached { identity: _, ending, document: _ } => ending == "succeeded" + ProvideFresh { outcome, document: _, host_record: _ } => work_outcome_ending(o: outcome) == "succeeded" + ProvideAttached { identity: _, ending, document: _, host_record: _ } => ending == "succeeded" } } fn provide_result_identity(r: ProvideResult) -> String { match r { - ProvideFresh { outcome, document: _ } => gunbc.compute.work_request.work_outcome_identity(o: outcome) - ProvideAttached { identity, ending: _, document: _ } => identity + ProvideFresh { outcome, document: _, host_record: _ } => gunbc.compute.work_request.work_outcome_identity(o: outcome) + ProvideAttached { identity, ending: _, document: _, host_record: _ } => identity } } fn provide_result_ending(r: ProvideResult) -> String { match r { - ProvideFresh { outcome, document: _ } => work_outcome_ending(o: outcome) - ProvideAttached { identity: _, ending, document: _ } => ending + ProvideFresh { outcome, document: _, host_record: _ } => work_outcome_ending(o: outcome) + ProvideAttached { identity: _, ending, document: _, host_record: _ } => ending } } fn provide_result_document(r: ProvideResult) -> String { match r { - ProvideFresh { outcome: _, document } => document - ProvideAttached { identity: _, ending: _, document } => document + ProvideFresh { outcome: _, document, host_record: _ } => document + ProvideAttached { identity: _, ending: _, document, host_record: _ } => document } } @@ -199,9 +273,40 @@ fn compute_unit_name(identity_hex: String) -> NonEmptyStr { join(["gunbc-compute-", identity_hex], "") as NonEmptyStr } -// Run the operation as a transient user unit and wait for it: the unit carries the memory ceiling, -// the checkout as working directory, the shared per-host target directory and the sccache wrapper. -fn compute_run_unit(instance: HostDashboardInstance, layout: ComputeLayout, identity_hex: String, argv: List) -> ComputeExec { +// THE TERMINATION POLICY IS BOUND, NOT INHERITED, and that is what makes a successful wait mean +// anything about the cgroup. `systemd-run --wait` returns when the MAIN process exits; under +// KillMode=process or none a forked child survives in the unit's cgroup and goes on using the +// memory this seat is accounting for. control-group is systemd's default, but a default is not a +// declaration -- a drop-in or a future default could change it, and this provider would keep +// treating a completed wait as an empty cgroup (side-chat review at 773825cf). Binding it makes the +// policy a fact of the invocation. +// +// IT IS BOUND *AND* THE EVIDENCE IS STILL REQUIRED, IN BOTH DIRECTIONS. A positive populated=1 is +// never discarded in favour of a completed wait; and an UNREADABLE population is not licensed by one +// either. A bound policy says what systemd WILL do, the cgroup says what IS true, and "I could not +// look" is not the second (side-chat review at f5344b28). Completion confirms a release only beside +// a positively empty cgroup -- or, short-circuiting all of this, a manager that has no record of +// the unit at all. +data compute_kill_mode_property: String = "KillMode" +data compute_kill_mode_value: String = "control-group" + +// THE PROPERTIES ARE A FOLD SO THE BOUND POLICY IS CHECKABLE. A termination policy that is only +// asserted in prose is exactly the thing the release decision must not trust, and the whole point +// of binding it is that the decision leans on it -- so the invocation's properties are produced +// where a control can read them rather than spelled inline at the call. +fn compute_unit_properties(layout: ComputeLayout, granted: Kibibyte) -> List { + [ + systemd_run_property(name: "MemoryMax", value: to_string(value: byte_size_count(b: kibibyte_to_byte_size(k: granted)))), + systemd_run_property(name: compute_kill_mode_property, value: compute_kill_mode_value), + systemd_run_property(name: "WorkingDirectory", value: layout.checkout), + ] +} + +// Run the operation as a transient user unit and wait for it: the unit carries THE MEMORY THE POOL +// GRANTED -- not a ceiling read independently from the instance, which would let the reservation and +// the enforcement drift apart -- the checkout as working directory, the shared per-host target +// directory and the sccache wrapper. +fn compute_run_unit(instance: HostDashboardInstance, layout: ComputeLayout, identity_hex: String, argv: List, granted: Kibibyte) -> ComputeExec { let systemd_run = match instance.toolchain.systemd_run { Present { value: p } => p as String Absent => "" } if systemd_run == "" { ComputeExecFailed { exit_code: 127, stdout: "", stderr: "this instance's toolchain declares no systemd-run; the local provider runs only under systemd" } @@ -211,10 +316,7 @@ fn compute_run_unit(instance: HostDashboardInstance, layout: ComputeLayout, iden workdir: layout.checkout, args: systemd_run_user_wait_arguments( unit: compute_unit_name(identity_hex: identity_hex), - properties: [ - systemd_run_property(name: "MemoryMax", value: to_string(value: byte_size_count(b: instance.dispatch_worker_memory_max))), - systemd_run_property(name: "WorkingDirectory", value: layout.checkout), - ], + properties: compute_unit_properties(layout: layout, granted: granted), setenv_bindings: [ join(["CARGO_TARGET_DIR=", layout.target_dir], ""), join(["RUSTC_WRAPPER=", sccache_installed_binary_path], ""), @@ -225,6 +327,197 @@ fn compute_run_unit(instance: HostDashboardInstance, layout: ComputeLayout, iden } } +// ── WHETHER THE ATTEMPT HAS ENDED AND ITS UNIT IS GONE ──────────────────────────────────────── +// +// THE RELEASE LAW SAID "QUIESCENCE REQUIRED" AND NOTHING OBSERVED QUIESCENCE. compute_release ran +// on whatever compute_run_leased returned, and that is the exit of `systemd-run --wait`, which is +// NOT the unit: systemd-run is a launcher, the transient service is owned by the manager, and a +// launcher killed or disconnected yields a failure WHILE THE UNIT KEEPS RUNNING. +// +// TWO EARLIER SHAPES OF THIS FOLD WERE WRONG, AND BOTH WERE WRONG IN THE SAME DIRECTION -- they +// found a way to say "gone" from evidence that does not establish it. +// +// ActiveState ALONE (first shape): `failed` coexists with live processes while a unit's stop +// reaches its SIGKILL timeout, and an empty ActiveState is the manager declining to answer. +// +// AN EMPTY ControlGroup (second shape, side-chat review at 5ee0cce): it was read as observed +// termination without reading any cgroup at all, and it is not. systemd realizes the cgroup AT +// SPAWN, so an empty ControlGroup equally describes a unit whose start is still PENDING -- which +// makes a whole unbacked launch reachable: reserve, the start is pending, the launcher is lost +// while this driver lives on, settlement sees the empty property, releases, and THEN the job +// starts against memory nobody holds. An empty required property is now never promoted to a +// conclusion; it is UNAVAILABLE, like every other absence of evidence. +// +// SO CAPACITY IS FREED ON TWO FACTS AND NO OTHERS, both of which establish that the attempt ENDED +// rather than that it looks quiet: +// +// THE ATTEMPT COMPLETED. `systemd-run --wait` returned success, which it does only after the +// unit it started ran to completion. A lost launcher does not return success, and a pending job +// has not returned at all. +// +// THE MANAGER HAS NO RECORD OF THE UNIT. LoadState=not-found is the wire value this corpus reads +// positively, and a transient --wait unit reaches it once it has run and been collected. +// +// A REALIZED CGROUP REPORTING populated 0 IS THE THIRD, AND IT IS EVIDENCE RATHER THAN A GUESS, +// which is why it survives where the empty property did not: the cgroup exists only from spawn +// onward, so a NON-EMPTY ControlGroup whose cgroup reports no processes cannot be a pending start. +// It spawned, and everything in it exited. +// +// EVERYTHING ELSE KEEPS THE CHARGE: populated, an unreadable manager, an unreadable cgroup, an +// undecodable body, a property that came back empty. "I could not establish it" is what a lost +// launcher, a pending job and a broken bus all look like, and reading any of them as permission to +// take the memory back is the absorbing fallback DESIGN 5 forbids. +type UnitTermination + = UnitAttemptCompleted { detail: String } + | UnitAbsentAuthoritatively { detail: String } + | UnitPopulated { detail: String } + | UnitTerminationUnavailable { detail: String } + +data unit_load_state_property: NonEmptyStr = "LoadState" as NonEmptyStr +data unit_control_group_property: NonEmptyStr = "ControlGroup" as NonEmptyStr +data unit_load_state_absent_wire: String = "not-found" + +// ONE PROPERTY READ, AS READ. success is the query's, value is the manager's answer; the two are +// separate because a successful query that answers nothing is a different fact from a query that +// failed, and the fold below must be able to tell them apart without re-deriving either. +type UnitPropertyReading { + queried: Bool + value: String +} + +// THE RAW OBSERVATIONS THE DECISION IS MADE FROM, carried as a value so the decision is a fold over +// supplied readings rather than a fold over live service calls. That is what lets the controls +// drive the OBSERVATION-TO-DECISION boundary -- a failed query whose text looks like an answer, a +// property that came back empty, a pending start -- instead of only the variant-to-release mapping, +// which cannot see any of those (side-chat review at 5ee0cce). +type UnitObservations { + attempt_completed: Bool + load_state: UnitPropertyReading + control_group: UnitPropertyReading + events: UnitPropertyReading +} + +// A FAILED QUERY IS UNAVAILABLE WHATEVER IT PRINTED. systemctl writes diagnostics that read like +// answers -- "Failed to connect to bus", "not-found" inside a sentence -- so the exit status +// decides first and the text is never consulted on a failed query. +// WHAT THE POPULATION READING ESTABLISHES, AS ITS OWN THREE-VALUED FACT. It has to be separable +// from the decision because the decision now consults it TWICE -- once to refuse a release outright, +// and once to confirm one -- and "not positively populated" is not the same as "positively empty". +type UnitPopulation + = PopulationOccupied { detail: String } + | PopulationEmpty { detail: String } + | PopulationUnknown { detail: String } + +fn unit_population(o: UnitObservations) -> UnitPopulation { + if !o.control_group.queried { + PopulationUnknown { detail: "the control group could not be queried" } + } else if trim(s: o.control_group.value) == "" { + PopulationUnknown { detail: "the unit holds no control group, which is EITHER a unit that has finished OR a start that is still pending -- the cgroup is realized at spawn" } + } else if !o.events.queried { + PopulationUnknown { detail: join(["the cgroup events of ", trim(s: o.control_group.value), " could not be read"], "") } + } else { + match decode_cgroup_events_populated(body: o.events.value) { + CgroupEventsUnparseable { cause: c } => PopulationUnknown { detail: join(["the cgroup events of ", trim(s: o.control_group.value), " could not be decoded: ", c], "") } + CgroupEventsDecoded { populated: p } => + if p { + PopulationOccupied { detail: join(["processes remain in ", trim(s: o.control_group.value)], "") } + } else { + PopulationEmpty { detail: join([trim(s: o.control_group.value), " reports populated 0"], "") } + } + } + } +} + +// THE ORDER OF THESE TESTS IS THE SAFETY PROPERTY, and the previous order was the defect. Completion +// was checked FIRST and returned immediately, so {completed, populated 1} RELEASED -- a completed +// wait overriding the kernel telling us processes are still there. Contrary evidence now wins: +// a positive population refuses the release before anything else is considered, and is never +// discarded (side-chat review at 773825cf). +// +// AND A MOMENTARILY EMPTY CGROUP IS NOT TERMINAL ON ITS OWN. populated=0 with completion NOT +// established used to release; a realized cgroup can be empty between execs, and emptiness does not +// cover a pending job. So in this PR an uncertain completion KEEPS THE CHARGE, and the population +// reading serves only to CONFIRM a completion or to REFUSE one. Establishing termination without a +// completed attempt is the lifecycle capability's job, not this one's. +fn unit_termination_decide(o: UnitObservations) -> UnitTermination { + let population = unit_population(o: o) + match population { + PopulationOccupied { detail: d } => UnitPopulated { detail: d } + _ => + if o.load_state.queried && trim(s: o.load_state.value) == unit_load_state_absent_wire { + UnitAbsentAuthoritatively { detail: join(["LoadState=", unit_load_state_absent_wire, ", so the manager has no record of this unit"], "") } + } else if !o.attempt_completed { + UnitTerminationUnavailable { + detail: join([ + "the attempt did not complete, so its end is not established -- ", + match population { PopulationEmpty { detail: pd } => join([pd, ", but a realized cgroup can be empty between execs and emptiness does not cover a pending job"], "") PopulationUnknown { detail: pd } => pd PopulationOccupied { detail: pd } => pd }, + ], ""), + } + } else { + match population { + PopulationEmpty { detail: pd } => + UnitAttemptCompleted { + detail: join([ + "systemd-run --wait returned success under ", compute_kill_mode_property, "=", compute_kill_mode_value, + " and ", pd, + ], ""), + } + _ => + UnitTerminationUnavailable { + detail: join([ + "the attempt completed, but the population could not be read (", + match population { PopulationUnknown { detail: pd } => pd PopulationEmpty { detail: pd } => pd PopulationOccupied { detail: pd } => pd }, + ") -- a bound KillMode says what systemd WILL do, not what is true, so an unreadable cgroup establishes nothing even beside a completed wait", + ], ""), + } + } + } + } +} + +// THE USER MANAGER IS ASKED, NOT THE SYSTEM ONE. systemctl_show_load_state_argv exists and is +// system-scope; these are transient --user units, so asking the system manager would answer +// not-found for EVERY one of them -- a fabricated authoritative absence, the worst answer this fold +// can produce. The property goes through the user-scope show operation for that reason and no other. +// +// THE READS ARE TAKEN UNCONDITIONALLY AND THE FOLD DECIDES. Short-circuiting them here would put +// half the decision in this function and half in the fold, which is the split that let an empty +// property become a conclusion in the first place. +fn observe_unit_termination(identity_hex: String, attempt_completed: Bool) -> UnitTermination { + let unit = compute_unit_name(identity_hex: identity_hex) + let load = systemd.Systemctl.ShowUserProperty(unit: unit, property: unit_load_state_property) + let cg = systemd.Systemctl.ShowUserProperty(unit: unit, property: unit_control_group_property) + let events = if cg.success && trim(s: cg.value) != "" { + linux.CgroupV2.ReadEvents(events_path: cgroup_v2_events_path(cgroup_path: join([cgroup_v2_mount_point as String, trim(s: cg.value)], "") as NonEmptyStr)) + } else { + linux.CgroupV2.ReadEvents(events_path: cgroup_v2_events_path(cgroup_path: cgroup_v2_mount_point)) + } + unit_termination_decide(o: UnitObservations { + attempt_completed: attempt_completed, + load_state: UnitPropertyReading { queried: load.success, value: load.value }, + control_group: UnitPropertyReading { queried: cg.success, value: cg.value }, + events: UnitPropertyReading { queried: events.success, value: events.value }, + }) +} + +fn unit_termination_frees_capacity(t: UnitTermination) -> Bool { + match t { + UnitAttemptCompleted { detail: _ } => true + UnitAbsentAuthoritatively { detail: _ } => true + UnitPopulated { detail: _ } => false + UnitTerminationUnavailable { detail: _ } => false + } +} + +fn unit_termination_wire(t: UnitTermination) -> String { + match t { + UnitAttemptCompleted { detail: d } => join(["attempt completed (", d, ")"], "") + UnitAbsentAuthoritatively { detail: d } => join(["absent (", d, ")"], "") + UnitPopulated { detail: d } => join(["STILL POPULATED (", d, "), so the seat stays charged"], "") + UnitTerminationUnavailable { detail: d } => join(["termination UNESTABLISHED (", d, "), so the seat stays charged"], "") + } +} + // Return declared outputs by content: hash each with git (a blob object id is a content identity // every subject already uses) and install it into the identity's store directory. An absent or // unreadable output is a mismatch, never a success with a hole. @@ -263,6 +556,253 @@ fn compute_basename(path: String) -> String { // makes the retry cheap; what must never happen is a caller attaching to a failure it did not ask for); refuse at the cap or behind a lease; take the lease; check out; // run; return outputs; write the outcome; release the lease. A refusal before the lease leaves no // state; a refusal after it leaves the lease released and the outcome written. +// SETTLING A RUN THAT HAS FINISHED, AND THE ONE RULE THAT GOVERNS IT: THE DURABLE RECORD AND THE +// CALLER MUST AGREE ABOUT WHAT HAPPENED. +// +// They did not. The outcome document was written unconditionally, so a run whose work SUCCEEDED but +// whose reservation failed to release wrote WorkSucceeded to outcome.json and handed its caller a +// WorkRefusedByInfrastructure -- and the next caller of that identity ATTACHED to the stored +// success, which is the contract behaving correctly on a record that had quietly become a lie about +// the infrastructure's state. The leaked seat then had no consumer that would ever look for it +// (side-chat review of gunbc#11962 at dd240f0d, 2026-09-21). +// +// THE RESOLUTION IS NOT TO SUPPRESS THE SUCCESS. The work really did succeed and its outputs really +// are in the store; deleting that fact would make every later caller rebuild and would be a second +// lie in the other direction. The run's ending and the infrastructure's unresolved obligation are +// TWO FACTS, so they are recorded as two: the obligation is written as its own durable file, and +// the outcome document carries the refusal the caller is given -- so a later caller attaches to +// EXACTLY what this caller was told, and neither of them attaches to a success whose reservation is +// still outstanding. The run's own ending is never lost: it is named in the obligation and in the +// refusal, and the outputs stay in the store under their content identity. +// +// THE SEAT STAYS HELD, AND THAT IS THE SAFE DIRECTION rather than an omission. The pool's release +// law for a compute seat is quiescence-required precisely because nothing here can prove a unit +// stopped using memory; a release that did not land leaves the capacity encumbered, so the host +// under-admits until the obligation is discharged rather than handing the same bytes to the next +// arrival. Discharging it is an explicit release naming why -- the same entry completion and +// cancellation take. +// THE PRODUCER LEASE IS DROPPED LAST, AND THE ORDER IS THE POINT. It used to be deleted before the +// outcome and the obligation were written, so a second producer could take the lease and start +// against a work directory whose record was still being published -- the exclusion held for the +// name and not for the publication it exists to protect. +// THE ATTEMPT'S OWN COMPLETION IS A SEPARATE FACT FROM THE WORK'S ENDING, and only the first one +// licenses a release. A WorkFailed says the unit exited nonzero OR that the launcher never got an +// answer; a successful `systemd-run --wait` says the unit ran to completion, which is the fact the +// termination decision needs. So the ending is what the caller is told and this is what the seat is +// decided on; they are not the same question and were conflated before. +fn compute_attempt_completed(outcome: WorkOutcome) -> Bool { + match outcome { + WorkSucceeded { identity: _, outputs: _, log_path: _ } => true + WorkOutputMismatch { identity: _, detail: _ } => true + WorkFailed { identity: _, exit_code: _, log_path: _ } => false + WorkRefusedByInfrastructure { identity: _, cause: _ } => false + WorkCancelled { identity: _ } => false + } +} + +fn compute_run_and_settle( + instance: HostDashboardInstance, + commit: String, + layout: ComputeLayout, + identity: String, + subject: WorkSubject, + op: WorkOperation, + dependency_store: String, + granted: Kibibyte, + reference: NonEmptyStr, + reservation: ComputeReservation, +) -> ProvideResult { + let outcome = compute_run_leased(instance: instance, commit: commit, layout: layout, identity: identity, op: op, dependency_store: dependency_store, granted: granted) + let standing = compute_capacity_standing(instance: instance) + let termination = observe_unit_termination(identity_hex: identity, attempt_completed: compute_attempt_completed(outcome: outcome)) + let returned = if unit_termination_frees_capacity(t: termination) { + compute_release(reservation: reservation, reason: join(["work ", work_outcome_ending(o: outcome), ", unit ", unit_termination_wire(t: termination)], "") as NonEmptyStr) + } else { + ComputeReleaseRefused { detail: join(["the seat was NOT released: ", unit_termination_wire(t: termination)], "") } + } + let settled = if compute_release_landed(r: returned) { + compute_settled_record(layout: layout, identity: identity, subject: subject, op: op, outcome: outcome) + } else { + compute_unreleased_record( + layout: layout, identity: identity, subject: subject, op: op, outcome: outcome, + reservation: reservation, returned: returned, reference: reference, termination: termination) + } + let dropped = Filesystem.Delete(path: layout.lease_path) + let measured = Filesystem.Write( + path: layout.consumption_path, + content: join([ + compute_capacity_standing_wire(s: standing), "\n", + "unit: ", unit_termination_wire(t: termination), "\n", + "reservation: ", compute_release_wire(r: returned), "\n", + if dropped.success { "" } else { compute_stale_lease_note(layout: layout, error: dropped.error) }, + ], "")) + if measured.success { + settled + } else { + compute_with_lost_host_record( + settled: settled, layout: layout, + dropped_ok: dropped.success, dropped_error: dropped.error, error: measured.error) + } +} + +// THE HOST RECORD IS THE ONLY DURABLE CARRIER OF THREE FACTS, so losing it is reported rather than +// discarded -- and reported BESIDE the work's result, not instead of it. +// +// TWO DEFECTS MET HERE. The arm read `if measured.success { settled } else { settled }`, so a failed +// write vanished by construction (review 69645); and the compound case was the sharp one, because +// the stale-lease note lives only in this file -- a lease that failed to drop AND a write that +// failed left an identity whose lease is permanently held with NO RECORD ANYWHERE. The repair then +// over-corrected: it synthesized a WorkRefusedByInfrastructure for the caller while outcome.json +// said the run had succeeded, which is the stored-record disagreement again, one layer along +// (side-chat review at 773825cf). +// +// So the outcome is untouched -- the caller reads exactly what the next attacher will read -- and +// the lost record rides as its own fact. The CLI turns that fact into a nonzero exit with both +// halves named, which is how a recording failure stays visible without becoming a verdict about +// work that really did run. +// +// AND IT GOES THROUGH THE ONE JOIN RATHER THAN MATCHING THE ARMS ITSELF. It matched them, and the +// ProvideAttached arm returned the status it was handed while DISCARDING the detail it had just +// built -- the exact vanish this function exists to prevent, one arm along, in the function whose +// annotation describes the vanish (review 69724). It was latent only because the single call site +// passes a fresh result, which is the kind of "safe today" that stops being true at the next call +// site. Two spellings of one join is the fork DESIGN 3 forbids, so there is now one: +// provide_result_with_host_record, which already handled both arms and accumulates rather than +// letting either side win. +fn compute_with_lost_host_record( + settled: ProvideResult, + layout: ComputeLayout, + dropped_ok: Bool, + dropped_error: String, + error: String, +) -> ProvideResult { + let detail = join([ + "this host's record at ", layout.consumption_path, " could not be written: ", error, + "; the consumption reading is lost, and ", + if dropped_ok { + "the producer lease was dropped, so nothing else is outstanding" + } else { + join(["THE PRODUCER LEASE AT ", layout.lease_path, " IS ALSO STILL HELD (", dropped_error, ") AND NOTHING NOW RECORDS THAT IT IS STALE: an operator must remove the name before this identity can be produced again"], "") + }, + ], "") + provide_result_with_host_record(r: settled, carried: HostRecordLost { detail: detail }) +} +// BLOCKER (7): ONE CONTRACT, AND THE CONTRACT IS THE STORED RECORD. This arm used to hand the +// caller a refusal while the outcome document already said the run had SUCCEEDED, and then state +// that the next request would refuse as ProducerInFlight -- three claims that cannot all be true, +// because the stored record is exactly what the next caller attaches to. So the stored record +// decides: a published success IS the result, the caller is told the same thing the next caller +// will read, and the stale lease is recorded as the operational fact it is rather than converted +// into a verdict about the work. An operator removes the name; nothing about the run changed. +// +// AND THE NOTE SAYS WHAT THE NAME ACTUALLY BLOCKS. It used to say the next request would refuse as +// ProducerInFlight, which contradicts the very contract this block establishes: a caller reaching a +// published SUCCESS attaches to it, and the attach is decided before the lease is consulted. The +// stale name only blocks a request that must PRODUCE again. +fn compute_stale_lease_note(layout: ComputeLayout, error: String) -> String { + join([ + "STALE PRODUCER LEASE: ", layout.lease_path, " could not be dropped: ", error, + "; the record for this identity is published at ", layout.outcome_path, " and is authoritative, ", + "and a caller reaching that record ATTACHES to it -- the attach is decided before this name is ", + "consulted. The stale name matters only to a request that must PRODUCE again, which it will ", + "refuse as ProducerInFlight until an operator removes it\n", + ], "") +} + +// THE ORDINARY ENDING: the reservation came back, so the record is the run's own ending and the +// caller is told the same thing. +fn compute_settled_record( + layout: ComputeLayout, + identity: String, + subject: WorkSubject, + op: WorkOperation, + outcome: WorkOutcome, +) -> ProvideResult { + let document = work_outcome_wire(o: outcome, subject: subject, op: op) + let written = Filesystem.Write(path: layout.outcome_path, content: document) + if written.success { + ProvideFresh { outcome: outcome, document: document, host_record: HostRecordWritten } + } else { + compute_fresh( + outcome: WorkRefusedByInfrastructure { + identity: identity, + cause: StoreUnavailable { + detail: join([ + "the work ended ", work_outcome_ending(o: outcome), + " and its reservation was released, but the record could not be completed -- outcome written: ", + written.error, + ], ""), + }, + }, + subject: subject, op: op) + } +} + +// THE ENDING WITH AN OUTSTANDING OBLIGATION: one document, written once, given to this caller and +// read by the next one. +fn compute_unreleased_record( + layout: ComputeLayout, + identity: String, + subject: WorkSubject, + op: WorkOperation, + outcome: WorkOutcome, + reservation: ComputeReservation, + returned: ComputeRelease, + reference: NonEmptyStr, + termination: UnitTermination, +) -> ProvideResult { + let cause = ComputeCapacityLedgerUnavailable { + detail: join([ + "the seat for ", reference as String, " is STILL CHARGED and this provider has no way to discharge it: ", + unit_termination_wire(t: termination), ". ", compute_release_wire(r: returned), + ". The work itself ended ", work_outcome_ending(o: outcome), + " and any declared outputs are in the store. ", compute_stuck_reservation_remedy, + ], ""), + } + let document = work_outcome_wire(o: WorkRefusedByInfrastructure { identity: identity, cause: cause }, subject: subject, op: op) + let written = Filesystem.Write(path: layout.outcome_path, content: document) + if written.success { + ProvideFresh { outcome: WorkRefusedByInfrastructure { identity: identity, cause: cause }, document: document, host_record: HostRecordWritten } + } else { + compute_fresh(outcome: WorkRefusedByInfrastructure { identity: identity, cause: cause }, subject: subject, op: op) + } +} + +// THE REMEDY SENTENCE FOR A SEAT THIS PROVIDER CANNOT GIVE BACK, and it is a declared absence +// rather than a route claimed in prose. No discharge existed on main -- there were no reservations +// at all, only a count of lease files -- so this is not a rung that dropped; it is a failure mode +// this change makes reachable for the first time, rostered as +// gunbc.recurring_failure_mode a_held_compute_seat_has_no_in_corpus_discharge, whose trigger names +// the capability that closes it. +// +// WHAT KEEPS IT FAIL-CLOSED MEANWHILE: every arm that cannot prove the unit is gone keeps the +// charge, so the host UNDER-admits. Nothing is over-promised; the pool simply shrinks until an +// operator clears the partition by hand. That is the direction a capacity ledger must fail in. +data compute_stuck_reservation_remedy: String = "There is NO safe discharge for this seat while this host is admitting work: clearing the capacity partition by hand under live admission removes the record the admission arithmetic is computed from, so the next requests would be admitted against memory this one still holds -- trading a host that under-admits for one that over-promises. The discharge is the compute lifecycle capability (gunbc.recurring_failure_mode a_held_compute_seat_has_no_in_corpus_discharge). Any manual intervention before then requires compute admission STOPPED on this host and every gunbc-compute unit PROVEN gone, in that order. Until then this host under-admits, which is the fail-closed direction and is not an incident." + +// THE ORDER THE TWO HOLDS ARE TAKEN IN// THE ORDER THE TWO HOLDS ARE TAKEN IN, and they are two facts rather than one. The producer lease +// excludes a SECOND PRODUCER OF THIS IDENTITY and is a NAME, so an exclusive create settles it; the +// reservation is a QUANTITY on the host, and no exclusive create of any name settles that. The +// lease is taken first because a request that then loses on capacity releases a name it holds +// rather than memory it may never use, and a name is the cheaper of the two to undo. +// +// THE WORK RUNS UNDER THE GRANT: the transient unit's MemoryMax is the amount the pool reserved, so +// the ledger's arithmetic IS the enforcement rather than a parallel description of it. +// +// AGGREGATE CONSUMPTION IS READ WHILE THE GRANT IS STILL HELD, which is the only instant at which +// the ledger's committed total and the machine's own availability describe the same population; +// after the release the reservation is gone from one side and the memory may not yet be gone from +// the other. +// +// COMPLETION AND CANCELLATION RELEASE THE SAME WAY. Every ending of compute_run_leased -- succeeded, +// failed, output-mismatch, refused by infrastructure -- reaches the release, so there is no ending +// on which the seat stays held. +// +// THE COMMENTS ABOVE USED TO SIT INSIDE THIS FUNCTION'S BODY, and the first real compile of this +// module on srv1 (2026-09-21) is what moved them: DESIGN 4c admits standalone leading blocks +// attached to MODULE-SCOPE declarations only, and the interpreter route this provider's witnesses +// run on tolerates a body-position block that `gunbc compile` refuses outright -- 14 blocking +// errors on a module every witness had reported green. fn compute_provide_leaf( instance: HostDashboardInstance, commit: String, @@ -277,37 +817,94 @@ fn compute_provide_leaf( let attached = if stored.success { stored_outcome_decode(text: stored.content) } else { StoredOutcomeUnreadable { reason: "no stored outcome" } } if stored_outcome_is_success(r: attached) { match attached { - StoredOutcomeFound { ending, identity: stored_identity, document } => ProvideAttached { identity: stored_identity, ending: ending, document: document } + StoredOutcomeFound { ending, identity: stored_identity, document } => ProvideAttached { identity: stored_identity, ending: ending, document: document, host_record: HostRecordWritten } StoredOutcomeUnreadable { reason } => compute_fresh(outcome: WorkRefusedByInfrastructure { identity: identity, cause: StoreUnavailable { detail: reason } }, subject: subject, op: op) } } else if !(compute_ensure_dir(instance: instance, path: layout.work_dir) && compute_ensure_dir(instance: instance, path: layout.leases_dir) && compute_ensure_dir(instance: instance, path: layout.store_dir) && compute_ensure_dir(instance: instance, path: layout.target_dir)) { compute_fresh(outcome: WorkRefusedByInfrastructure { identity: identity, cause: StoreUnavailable { detail: join(["could not create the compute directories under ", layout.root], "") } }, subject: subject, op: op) } else { - let leases = Filesystem.List(path: layout.leases_dir) - let in_flight = if leases.success { compute_count_lines(text: leases.entries) } else { 0 } - if in_flight >= compute_cold_build_cap { - compute_fresh(outcome: WorkRefusedByInfrastructure { identity: identity, cause: HostAtColdBuildCap { in_flight: in_flight, cap: compute_cold_build_cap } }, subject: subject, op: op) + let lease = Filesystem.WriteCreateNew(path: layout.lease_path, content: join([commit, " ", clock_now_probed_at_or_unknown() as String, "\n"], "")) + if !lease.success { + compute_fresh(outcome: WorkRefusedByInfrastructure { identity: identity, cause: ProducerInFlight { lease_path: layout.lease_path } }, subject: subject, op: op) } else { - let lease = Filesystem.WriteCreateNew(path: layout.lease_path, content: join([commit, " ", clock_now_probed_at_or_unknown() as String, "\n"], "")) - if !lease.success { - compute_fresh(outcome: WorkRefusedByInfrastructure { identity: identity, cause: ProducerInFlight { lease_path: layout.lease_path } }, subject: subject, op: op) - } else { - let outcome = compute_run_leased(instance: instance, commit: commit, layout: layout, identity: identity, op: op, dependency_store: dependency_store) - let document = work_outcome_wire(o: outcome, subject: subject, op: op) - let written = Filesystem.Write(path: layout.outcome_path, content: document) - let released = Filesystem.Delete(path: layout.lease_path) - if written.success && released.success { - ProvideFresh { outcome: outcome, document: document } - } else { - compute_fresh(outcome: WorkRefusedByInfrastructure { identity: identity, cause: StoreUnavailable { detail: join(["outcome written: ", if written.success { "yes" } else { written.error }, "; lease released: ", if released.success { "yes" } else { released.error }], "") } }, subject: subject, op: op) - } + let reference = compute_reservation_reference(identity: identity) + let reservation = compute_reserve(instance: instance, reference: reference, term_seconds: compute_reservation_term_seconds) + match reservation { + ComputeCapacityFull { wire: w } => + compute_refused_unreserved(instance: instance, identity: identity, subject: subject, op: op, layout: layout, cause: HostComputeCapacityFull { wire: w }) + ComputeHostBelowFloor { requested: rq, available: av } => + compute_refused_unreserved(instance: instance, identity: identity, subject: subject, op: op, layout: layout, cause: HostBelowMemoryFloor { requested: rq, available: av }) + ComputeReservationRefused { detail: d } => + compute_refused_unreserved(instance: instance, identity: identity, subject: subject, op: op, layout: layout, cause: ComputeCapacityLedgerUnavailable { detail: d }) + ComputeReserved { grant: _, partition: _, amount: granted, store: _ } => + compute_run_and_settle( + instance: instance, commit: commit, layout: layout, identity: identity, subject: subject, op: op, + dependency_store: dependency_store, granted: granted, reference: reference, reservation: reservation) } } } } + +// THE CONSUMPTION READING IS ITS OWN FILE AND MUST NOT JOIN THE OUTCOME DOCUMENT. It was appended +// to outcome.json first, and the first real run on srv1 (2026-09-21) is what said why that is +// wrong: the stored outcome is PARSED by the attach path (stored_outcome_decode), so a line +// appended after the JSON made every later caller of a SUCCEEDED identity read +// StoredOutcomeUnreadable and rebuild -- the contract's "two callers, one build" silently dead, and +// the provider's own dependent request refusing on a dependency that had in fact succeeded. A +// realization's measurement does not get to change the shape of the contract's document. + +// THE RESERVATION REFERENCE NAMES AN ATTEMPT, NOT A WORK IDENTITY, and the first real run on srv1 +// (2026-09-21) is what forced the distinction. The identity is stable by construction -- that is its +// whole job -- so using it as the encumbrance reference meant the SECOND request for the same +// identity hit the ledger's DuplicateReference refusal and was reported as a capacity refusal on a +// host with 400 GiB free. The pool's reference is the name of one HOLD, and two holds of one +// identity at different times are two holds; the identity stays in the receipt, where it belongs. +fn compute_reservation_reference(identity: String) -> NonEmptyStr { + join([identity, "@", clock_now_probed_at_or_unknown() as String], "") as NonEmptyStr +} + +// A REQUEST REFUSED FOR CAPACITY HOLDS NOTHING. The producer lease is dropped on the way out, so a +// host that is full does not accumulate names that would refuse the next attempt for the wrong +// reason -- a capacity refusal reported as a producer already in flight is the state conflation +// this provider's refusal vocabulary exists to prevent. +fn compute_refused_unreserved( + instance: HostDashboardInstance, + identity: String, + subject: WorkSubject, + op: WorkOperation, + layout: ComputeLayout, + cause: WorkInfrastructureRefusal, +) -> ProvideResult { + let dropped = Filesystem.Delete(path: layout.lease_path) + if dropped.success { + compute_fresh(outcome: WorkRefusedByInfrastructure { identity: identity, cause: cause }, subject: subject, op: op) + } else { + compute_fresh( + outcome: WorkRefusedByInfrastructure { + identity: identity, + cause: StoreUnavailable { detail: join(["a capacity refusal could not drop its producer lease at ", layout.lease_path, ": ", dropped.error], "") }, + }, + subject: subject, op: op) + } +} + +fn compute_release_landed(r: ComputeRelease) -> Bool { + match r { + ComputeReleased { partition: _, reference: _, reason: _ } => true + ComputeReleaseRefused { detail: _ } => false + } +} + +fn compute_release_wire(r: ComputeRelease) -> String { + match r { + ComputeReleased { partition: _, reference: ref_, reason: why } => join(["released ", ref_ as String, " (", why as String, ")"], "") + ComputeReleaseRefused { detail: d } => join(["NOT released: ", d], "") + } +} + fn compute_fresh(outcome: WorkOutcome, subject: WorkSubject, op: WorkOperation) -> ProvideResult { - ProvideFresh { outcome: outcome, document: work_outcome_wire(o: outcome, subject: subject, op: op) } + ProvideFresh { outcome: outcome, document: work_outcome_wire(o: outcome, subject: subject, op: op), host_record: HostRecordWritten } } fn compute_run_leased( @@ -317,6 +914,7 @@ fn compute_run_leased( identity: String, op: WorkOperation, dependency_store: String, + granted: Kibibyte, ) -> WorkOutcome { let existing = Filesystem.List(path: layout.checkout) let checkout = if existing.success { @@ -332,7 +930,7 @@ fn compute_run_leased( ComputeExecFailed { exit_code, stdout: _, stderr } => WorkRefusedByInfrastructure { identity: identity, cause: CheckoutUnavailable { detail: join(["git worktree add exited ", to_string(value: exit_code), ": ", stderr], "") } } ComputeExecOk { stdout: _, stderr: _ } => { - let run = compute_run_unit(instance: instance, layout: layout, identity_hex: identity, argv: compute_command_argv(instance: instance, layout: layout, op: op, dependency_store: dependency_store)) + let run = compute_run_unit(instance: instance, layout: layout, identity_hex: identity, argv: compute_command_argv(instance: instance, layout: layout, op: op, dependency_store: dependency_store), granted: granted) let log = Filesystem.Write(path: layout.log_path, content: match run { ComputeExecOk { stdout, stderr } => join([stdout, stderr], "") ComputeExecFailed { exit_code: _, stdout, stderr } => join([stdout, stderr], "") @@ -370,14 +968,23 @@ fn compute_provide(instance: HostDashboardInstance, commit: String, op: WorkOper } } +// THE DEPENDENCY'S LOST RECORD TRAVELS WITH THE RESULT, because the caller of a dependent request +// never sees the dependency's own result. Returning the second leaf's result alone silently dropped +// the fact that the BUILD failed to record its side facts -- the stuck lease or the lost consumption +// reading vanished at exactly the seam where nobody was left to report it (side-chat review at +// f5344b28). The work contract is untouched; only the host-record fact is joined. fn compute_provide_dependent(instance: HostDashboardInstance, commit: String, subject: WorkSubject, op: WorkOperation, toolchain: WorkToolchainIdentity) -> ProvideResult { let build = compute_provide_leaf(instance: instance, commit: commit, subject: subject, op: work_default_build(), toolchain: toolchain, dependency_store: "") if provide_result_succeeded(r: build) { let build_identity = provide_result_identity(r: build) - compute_provide_leaf(instance: instance, commit: commit, subject: subject, op: op, toolchain: toolchain, dependency_store: compute_layout(instance: instance, identity_hex: build_identity).store_dir) + provide_result_with_host_record( + r: compute_provide_leaf(instance: instance, commit: commit, subject: subject, op: op, toolchain: toolchain, dependency_store: compute_layout(instance: instance, identity_hex: build_identity).store_dir), + carried: provide_result_host_record(r: build)) } else { let identity = work_identity_hex(id: work_identity(subject: subject, op: op, toolchain: toolchain)) - compute_fresh(outcome: WorkRefusedByInfrastructure { identity: identity, cause: DependencyNotSucceeded { dependency_identity: provide_result_identity(r: build), ending: provide_result_ending(r: build) } }, subject: subject, op: op) + provide_result_with_host_record( + r: compute_fresh(outcome: WorkRefusedByInfrastructure { identity: identity, cause: DependencyNotSucceeded { dependency_identity: provide_result_identity(r: build), ending: provide_result_ending(r: build) } }, subject: subject, op: op), + carried: provide_result_host_record(r: build)) } } @@ -405,9 +1012,20 @@ fn compute_request_cli(repo_root: String, commit: String, operation: String, ent Absent => ExitFailure { code: 2, reason: join(["compute: operation must be build, compile or claims (compile and claims need entry; claims needs functions and hermetic=true|false); got ", operation], "") } Present { value: op } => { let result = compute_provide(instance: instance, commit: commit, op: op) - let receipt = Filesystem.Write(path: receipt_path, content: provide_result_document(r: result)) + let record = provide_result_host_record(r: result) + let receipt = Filesystem.Write(path: receipt_path, content: join([provide_result_document(r: result), "\n"], "")) + let record_note = compute_write_host_record_note(receipt_path: receipt_path, record: record) if !receipt.success { ExitFailure { code: 2, reason: join(["compute: receipt could not be written to ", receipt_path, ": ", receipt.error, "; outcome was ", provide_result_document(r: result)], "") } + } else if !host_record_was_written(h: record) { + ExitFailure { + code: 1, + reason: join([ + "compute: the work ended ", provide_result_ending(r: result), + " and its record at the store is authoritative -- a later request for this identity reads exactly that -- but ", + host_record_wire(h: record), "; ", record_note, + ], ""), + } } else if provide_result_succeeded(r: result) { ExitSuccess } else { @@ -418,6 +1036,26 @@ fn compute_request_cli(repo_root: String, commit: String, operation: String, ent } } +// THE RECEIPT STAYS THE DOCUMENT, AND THE HOST-RECORD FACT GETS ITS OWN FILE BESIDE IT. +// +// The first version of this appended the host-record sentence to the receipt, and the srv1 +// fault-injection run is what caught it: the receipt stopped being parseable JSON, so a consumer +// reading it back got "Extra data" instead of an outcome. That is the SAME defect as the +// consumption line once appended to outcome.json, committed a second time one file along -- a +// realization's side fact changing the shape of a document some consumer parses. The rule has to be +// the same in both places: a document a consumer parses carries exactly what its contract says, and +// everything else lives beside it. +fn compute_write_host_record_note(receipt_path: String, record: HostRecordStatus) -> String { + match record { + HostRecordWritten => "no host-record note was needed" + HostRecordLost { detail: d } => { + let path = join([receipt_path, ".host-record"], "") + let written = Filesystem.Write(path: path, content: join([d, "\n"], "")) + if written.success { join(["the loss is recorded at ", path], "") } else { join(["and the note could not be written to ", path, " either: ", written.error], "") } + } + } +} + fn compute_parse_operation(operation: String, entry: String, functions: String, hermetic: String) -> WorkOperation? { if operation == "build" { Present { value: work_default_build() } diff --git a/dag/gunbc/compute/work_request.dag b/dag/gunbc/compute/work_request.dag index 53af4e64651..16883a0830b 100644 --- a/dag/gunbc/compute/work_request.dag +++ b/dag/gunbc/compute/work_request.dag @@ -1,6 +1,7 @@ module gunbc.compute.work_request import std.types { String, Bool, Int, List, NonEmptyStr, FilePath } +import std.measure { Kibibyte, kibibyte_count } import std.content_hash { Fnv1a64Structural, content_hash_atom, content_hash_tagged_structural } import extdeps.git.object_store { GitObjectId, git_object_id_wire_hex } import extdeps.languages.json.emit { @@ -134,12 +135,30 @@ type WorkOutcome | WorkOutputMismatch { identity: String, detail: String } // Infrastructure refusals are typed and counted, never a widen: a producer already holds the lease -// (the caller attaches later, it does not start a second build), the host is at its cold-build cap, -// the checkout or the store could not be prepared, or a dependency of this operation (the build the -// compile consumes) did not succeed. +// (the caller attaches later, it does not start a second build), the host cannot back the memory +// this class reserves, the checkout or the store could not be prepared, or a dependency of this +// operation (the build the compile consumes) did not succeed. +// +// THE MEMORY ARMS CARRY Kibibyte, NOT Int FIELDS NAMED _kib. A unit in a field NAME on a bare Int +// is the unit modeled twice -- once in the name and once in the " KiB" this module then renders -- +// and modeled nowhere the compiler can see. The producer already had it right +// (gunbc.compute.host_capacity ComputeHostBelowFloor carries Kibibyte) and the provider was calling +// kibibyte_count to STRIP the carrier on the way in, which is the tell (review 69624). The deleted +// arm this replaced, HostAtColdBuildCap { in_flight, cap }, was a dimensionless COUNT, so Int was +// right there and is not right here. +// +// THREE CAPACITY ARMS WHERE THERE USED TO BE ONE COUNT. HostAtColdBuildCap { in_flight, cap } is +// DELETED, and its disposition is that the fact it reported -- this host is already carrying as +// much as it may -- is now HostComputeCapacityFull, measured in the memory the pool actually +// appropriates rather than in producers. The other two are facts the count could not express at +// all and that a caller must not confuse with it: the machine's LIVE availability being below what +// this class needs is somebody else's memory, not this pool's commitments, and an unreadable +// ledger is a store repair. One arm for three remedies is the conflation DESIGN 5 forbids. type WorkInfrastructureRefusal = ProducerInFlight { lease_path: String } - | HostAtColdBuildCap { in_flight: Int, cap: Int } + | HostComputeCapacityFull { wire: String } + | HostBelowMemoryFloor { requested: Kibibyte, available: Kibibyte } + | ComputeCapacityLedgerUnavailable { detail: String } | CheckoutUnavailable { detail: String } | StoreUnavailable { detail: String } | ToolchainUnobserved { detail: String } @@ -169,7 +188,9 @@ fn work_outcome_ending(o: WorkOutcome) -> String { fn work_refusal_detail(r: WorkInfrastructureRefusal) -> String { match r { ProducerInFlight { lease_path } => join(["a producer already holds the lease at ", lease_path, "; attach later, do not start a second one"], "") - HostAtColdBuildCap { in_flight, cap } => join([to_string(value: in_flight), " producers in flight on this host, cap ", to_string(value: cap)], "") + HostComputeCapacityFull { wire } => join(["this host's compute memory pool has no room for another reservation: ", wire], "") + HostBelowMemoryFloor { requested, available } => join(["this class reserves ", to_string(value: kibibyte_count(k: requested)), " KiB and the host reports only ", to_string(value: kibibyte_count(k: available)), " KiB available, so the reservation would not have been backed by the machine"], "") + ComputeCapacityLedgerUnavailable { detail } => join(["the host's compute capacity ledger could not be transacted: ", detail], "") CheckoutUnavailable { detail } => join(["checkout unavailable: ", detail], "") StoreUnavailable { detail } => join(["store unavailable: ", detail], "") ToolchainUnobserved { detail } => join(["toolchain unobserved: ", detail], "") diff --git a/dag/gunbc/fabric/fabric_event_log.dag b/dag/gunbc/fabric/fabric_event_log.dag index 5225efab78a..877a4368837 100644 --- a/dag/gunbc/fabric/fabric_event_log.dag +++ b/dag/gunbc/fabric/fabric_event_log.dag @@ -2,7 +2,7 @@ module gunbc.fabric_event_log import std.types { String, Bool, Int, NonEmptyStr, List, EpochSecs } import std.nat { Nat, nat_range_inclusive } -import std.measure { Count, One } +import std.measure { Count, One, Measure } import product.placement_supply { HostIdentity } import std.process { ProcessExit, ExitSuccess, exit_failure } import std.fabric_storage { @@ -16,7 +16,7 @@ import std.fabric_storage { import gunbc.fabric_storage_placement { fabric_storage_placement, FabricStoragePlaced, FabricStorageUnplaced } import gunbc.fabric_storage_client { FabricStorageBinding, fabric_storage_binding_for, fabric_storage_head, fabric_storage_put, fabric_storage_advance, fabric_storage_closure } import gunbc.fabric_storage_file_store { fabric_storage_file_root, fabric_storage_file_root_ensure, FabricStorageRootReady, FabricStorageRootRefused } -import product.capacity.pool { Pool, PoolReading, PoolRead, PoolReadingRefused, pool_reading_at } +import product.capacity.pool { Pool, PoolReading, PoolRead, PoolReadingRefused, pool_reading_at, PoolOutcome, PoolAdvanced, PoolRefused, pool_release, pool_refusal_wire } import product.capacity.event_chain { PartitionId, EventId, ChainEvent, ChainEnvelope, HeadExpectation, HeadAbsent, HeadAt, head_expectation_eq, event_parent_expectation, AppendDecision, AppendAdmitted, AppendStale, ChainWalk, ChainWalked, ChainIncomplete, ChainBudgetExhausted, chain_from_head, @@ -25,6 +25,7 @@ import product.capacity.event_chain { import product.capacity.pool_events { PoolEvent, pool_event_wire_text, pool_event_decode, PoolFold, PoolFolded, PoolFoldRefused, pool_fold, SeatRequest, SeatProposal, SeatProposed, SeatRefused, propose_acquire, grant_from_admission, + PoolReleased, } import product.capacity.lease { LeasePolicy, LeaseGrant, release_law_eq, release_law_wire } @@ -243,13 +244,20 @@ type SeatAttemptState { // and take a reading. Every step is the one seat_attempt already runs, which is what keeps this a // second QUESTION rather than a second authority -- there is no separate notion here of what a seat // is or when a pool is full. -type SeatStandingObservation - = SeatRoomObserved { headroom: Nat, generation: Nat } +// THE HEADROOM CARRIES ITS DIMENSION, AND THIS PR IS WHY IT HAS TO. A bare Nat was legitimate while +// this fold was fixed at Pool: seats are dimensionless and the field meant seats. The +// generalization to Pool above made the same field mean KiB for a memory pool and seats for a +// seat pool, with nothing in the type to say which -- so the unit moved into the consumer's head and +// into rendered strings, which is the unit modeled twice and checked nowhere (review 69624). The +// earliest unjustified boundary is this declaration, not its consumers, and it is one this change +// moved itself (DESIGN 6b). +type SeatStandingObservation + = SeatRoomObserved { headroom: Measure, generation: Nat } | SeatFullObserved { generation: Nat } | SeatStandingUnobserved { step: String, reason: String } | SeatStandingStoreRefused { cause: EventLogRefusal } -fn fabric_seat_observe(store: FabricStorageBinding, partition: PartitionId, root: Pool, at: EpochSecs, budget: Nat) -> SeatStandingObservation { +fn fabric_seat_observe(store: FabricStorageBinding, partition: PartitionId, root: Pool, at: EpochSecs, budget: Nat) -> SeatStandingObservation { match event_log_read_partition(store: store, partition: partition, budget: budget) { PartitionReadRefused { cause: c } => SeatStandingStoreRefused { cause: c } PartitionReadOk { head: _, walk: walk } => @@ -267,7 +275,7 @@ fn fabric_seat_observe(store: FabricStorageBinding, partition: PartitionId, root PoolReadingRefused { at: t, anchor: a } => SeatStandingUnobserved { step: "reading", reason: join(["instant ", to_string(t), " precedes the pool anchor ", to_string(a)], "") } PoolRead { committed: _, ceiling: _, headroom: h, over_committed: _ } => - if h.count > 0 { SeatRoomObserved { headroom: h.count, generation: g } } + if h.count > 0 { SeatRoomObserved { headroom: h, generation: g } } else { SeatFullObserved { generation: g } } } } @@ -275,7 +283,7 @@ fn fabric_seat_observe(store: FabricStorageBinding, partition: PartitionId, root } } -fn seat_attempt(store: FabricStorageBinding, partition: PartitionId, root: Pool, actor: NonEmptyStr, request: SeatRequest, policy: LeasePolicy, budget: Nat, attempt: Nat) -> SeatAcquisition? { +fn seat_attempt(store: FabricStorageBinding, partition: PartitionId, root: Pool, actor: NonEmptyStr, request: SeatRequest, policy: LeasePolicy, budget: Nat, attempt: Nat) -> SeatAcquisition? { match event_log_read_partition(store: store, partition: partition, budget: budget) { PartitionReadRefused { cause: c } => Present { value: SeatStoreRefused { cause: c, attempts_used: attempt } } PartitionReadOk { head: head, walk: walk } => @@ -313,7 +321,7 @@ fn seat_attempt(store: FabricStorageBinding, partition: PartitionId, root: Pool< // and the drift is invisible because each side is internally consistent. A mismatch is refused before // anything is appended rather than resolved in favour of either side: neither is authoritative over // the other, and picking one silently would be the same fail-open in a different costume. -fn fabric_seat_acquire(store: FabricStorageBinding, partition: PartitionId, root: Pool, actor: NonEmptyStr, request: SeatRequest, policy: LeasePolicy, attempts: Nat, budget: Nat) -> SeatAcquisition { +fn fabric_seat_acquire(store: FabricStorageBinding, partition: PartitionId, root: Pool, actor: NonEmptyStr, request: SeatRequest, policy: LeasePolicy, attempts: Nat, budget: Nat) -> SeatAcquisition { if !release_law_eq(left: root.release_law, right: policy.release_law) { SeatAcquireRefused { step: "release-law", @@ -337,6 +345,164 @@ fn fabric_seat_acquire(store: FabricStorageBinding, partition: PartitionId, root } } +// APPENDING A POOL EVENT THAT IS NOT AN ACQUISITION -- a settlement or a release -- against the +// partition's current head, re-observing and retrying while the head moves under it. +// +// WHY IT IS HERE AND NOT AT EACH CALLER. Acquisition already lived here because it has to fold the +// pool to decide; settlement and release decide nothing, so each caller wrote its own +// observe/append/retry loop and gunbc.fabric_quota had the only copy. A second consumer +// (gunbc.compute.host_capacity, releasing a compute reservation) would have made it two spellings +// of one transaction, free to disagree about how many times a contended head is retried -- so the +// loop moves to the carrier that owns partition appends and both consumers call it. +// +// A RELEASE THAT LOSES ITS RACE IS RETRIED, NEVER ASSUMED. Nothing here reports a success it did +// not observe: exhausting the attempts is its own arm, and a caller holding it still holds the +// reservation. +type PoolEventAppend + = PoolEventAppended { id: EventId } + | PoolEventContended { attempts: Nat } + | PoolEventAppendRefused { detail: String } + +type PoolEventAttemptState { + done: PoolEventAppend? +} + +fn pool_event_append_attempt(store: FabricStorageBinding, partition: PartitionId, actor: NonEmptyStr, at: EpochSecs, payload: PoolEvent) -> PoolEventAppend? { + match event_log_observe_head(store: store, partition: partition) { + HeadObservationRefused { cause: c } => Present { value: PoolEventAppendRefused { detail: event_log_refusal_wire(cause: c) } } + HeadObserved { head: head } => + match event_log_append( + store: store, + partition: partition, + event: ChainEvent { + partition: partition, + parent: match head { HeadAbsent => none HeadAt { id: h } => Present { value: h } }, + recorded_at: at, + actor: actor, + payload: payload, + }, + expected: head, + ) { + EventAppended { id: h } => Present { value: PoolEventAppended { id: h } } + EventAppendStale { expected: _, observed: _ } => none + EventAppendRefused { cause: c } => Present { value: PoolEventAppendRefused { detail: event_log_refusal_wire(cause: c) } } + } + } +} + +fn fabric_pool_event_append(store: FabricStorageBinding, partition: PartitionId, actor: NonEmptyStr, at: EpochSecs, payload: PoolEvent, attempts: Nat) -> PoolEventAppend { + let st = fold(nat_range_inclusive(lo: 1, hi: attempts), init: PoolEventAttemptState { done: none }, f: (acc, _i) => + match acc.done { + Present { value: _ } => acc + Absent => PoolEventAttemptState { done: pool_event_append_attempt(store: store, partition: partition, actor: actor, at: at, payload: payload) } + }) + match st.done { + Present { value: d } => d + Absent => PoolEventContended { attempts: attempts } + } +} + +fn pool_event_append_wire(a: PoolEventAppend) -> String { + match a { + PoolEventAppended { id: h } => join(["appended ", h as String], "") + PoolEventContended { attempts: n } => join(["contended after ", to_string(n), " attempts"], "") + PoolEventAppendRefused { detail: d } => join(["refused ", d], "") + } +} + +// RELEASING A SEAT, AND IT IS CHECKED AGAINST THE FOLDED POOL BEFORE ANYTHING IS APPENDED. +// +// fabric_pool_event_append is unchecked by construction -- it writes the event a caller hands it -- +// which is correct for a settlement whose amount the caller already knows and WRONG for a release, +// because a release names a reference the ledger may not be holding. An unheld reference appended +// anyway does not fail at the append: it fails at the next READ, when pool_fold reaches the event, +// gets UnknownEncumbrance, and answers PoolFoldRefused for the WHOLE PARTITION. One mistyped +// reference in a recovery command would make a host's capacity ledger permanently unreadable, and +// the damage would surface at an unrelated caller's next acquire. +// +// So this is the mirror of fabric_seat_acquire and not of the settlement helper: read the partition, +// fold it, PROPOSE the release against the folded pool, and append only what the pool admits. A +// reference the pool is not holding is a typed refusal that writes nothing. +// +// ITS CONSUMER IS gunbc.compute.host_capacity compute_release_on, which every compute settlement +// reaches when a run ends and its unit is proven gone. Under QuiescenceRequired a term never frees +// capacity, so an explicit release is the ONLY way a seat comes back. +// +// AN OPERATOR-FACING RECOVERY DOOR IS NOT AMONG ITS CONSUMERS, and this annotation said it was +// until review 69645 caught the citation naming two symbols that do not exist -- they were removed +// when the compute lifecycle was split out, and the comment was not. A citation that does not +// resolve is a citation defect (DESIGN 3), and worse here because host_capacity's own annotation +// states the opposite. Discharging a seat whose release did not land is the capability named by +// gunbc.recurring_failure_mode a_held_compute_seat_has_no_in_corpus_discharge; when it lands it +// will reach this same function, which is why the check below is built to serve a caller that did +// not take the reservation. +type SeatRelease + = SeatReleased { reference: NonEmptyStr, id: EventId } + | SeatNotHeld { reference: NonEmptyStr, wire: String } + | SeatReleaseContended { attempts: Nat } + | SeatReleaseRefused { step: String, reason: String } + +type SeatReleaseState { + done: SeatRelease? +} + +fn seat_release_attempt(store: FabricStorageBinding, partition: PartitionId, root: Pool, reference: NonEmptyStr, reason: NonEmptyStr, at: EpochSecs, budget: Nat) -> SeatRelease? { + match event_log_read_partition(store: store, partition: partition, budget: budget) { + PartitionReadRefused { cause: c } => Present { value: SeatReleaseRefused { step: "store", reason: event_log_refusal_wire(cause: c) } } + PartitionReadOk { head: head, walk: walk } => + match walk { + ChainIncomplete { missing: m, newest_first_so_far: _ } => Present { value: SeatReleaseRefused { step: "chain", reason: join(["partition chain is missing event ", m as String], "") } } + ChainBudgetExhausted { at: a } => Present { value: SeatReleaseRefused { step: "chain", reason: join(["partition chain exceeded the read budget at ", a as String], "") } } + ChainWalked { oldest_first: xs } => + match pool_fold(root: root, oldest_first: xs) { + PoolFoldRefused { at_event: e, wire: w } => Present { value: SeatReleaseRefused { step: "fold", reason: join(["event ", e as String, " refused: ", w], "") } } + PoolFolded { pool: p, generation: _ } => + match pool_release(pool: p, reference: reference, reason: reason, at: at) { + PoolRefused { refusal: r } => Present { value: SeatNotHeld { reference: reference, wire: pool_refusal_wire(r: r) } } + PoolAdvanced { pool: _ } => + match event_log_append( + store: store, + partition: partition, + event: ChainEvent { + partition: partition, + parent: match head { HeadAbsent => none HeadAt { id: h } => Present { value: h } }, + recorded_at: at, + actor: reference, + payload: PoolReleased { reference: reference, reason: reason }, + }, + expected: head, + ) { + EventAppended { id: h } => Present { value: SeatReleased { reference: reference, id: h } } + EventAppendStale { expected: _, observed: _ } => none + EventAppendRefused { cause: c } => Present { value: SeatReleaseRefused { step: "store", reason: event_log_refusal_wire(cause: c) } } + } + } + } + } + } +} + +fn fabric_seat_release(store: FabricStorageBinding, partition: PartitionId, root: Pool, reference: NonEmptyStr, reason: NonEmptyStr, at: EpochSecs, attempts: Nat, budget: Nat) -> SeatRelease { + let st = fold(nat_range_inclusive(lo: 1, hi: attempts), init: SeatReleaseState { done: none }, f: (acc, _i) => + match acc.done { + Present { value: _ } => acc + Absent => SeatReleaseState { done: seat_release_attempt(store: store, partition: partition, root: root, reference: reference, reason: reason, at: at, budget: budget) } + }) + match st.done { + Present { value: d } => d + Absent => SeatReleaseContended { attempts: attempts } + } +} + +fn seat_release_wire(r: SeatRelease) -> String { + match r { + SeatReleased { reference: ref_, id: h } => join(["released ", ref_ as String, " at ", h as String], "") + SeatNotHeld { reference: ref_, wire: w } => join(["the pool is not holding ", ref_ as String, ": ", w], "") + SeatReleaseContended { attempts: n } => join(["contended after ", to_string(n), " attempts"], "") + SeatReleaseRefused { step: s, reason: why } => join(["refused at ", s, ": ", why], "") + } +} + fn seat_acquisition_wire(a: SeatAcquisition) -> String { match a { SeatGranted { grant: g, generation: gen, attempts_used: n } => join(["granted ", g.reference as String, " fence=", g.fence.grant as String, "@", to_string(gen), " expires_at=", to_string(g.expires_at), " attempt=", to_string(n)], "") diff --git a/dag/gunbc/fabric/fabric_quota.dag b/dag/gunbc/fabric/fabric_quota.dag index 5fa0f3429a8..870172d2f17 100644 --- a/dag/gunbc/fabric/fabric_quota.dag +++ b/dag/gunbc/fabric/fabric_quota.dag @@ -1,20 +1,18 @@ module gunbc.fabric_quota import std.types { String, Bool, Int, NonEmptyStr, List, EpochSecs } -import std.nat { Nat, nat_range_inclusive } -import std.measure { Measure, Count, One } +import std.nat { Nat } +import std.measure { Measure } import extdeps.api_rate_limit { UpstreamRateLimit, upstream_rate_limit_key } import product.capacity.quota { quota_partition, quota_root_pool } -import product.capacity.event_chain { PartitionId, HeadExpectation, HeadAbsent, HeadAt, ChainEvent } -import product.capacity.pool_events { PoolEvent, PoolSettled, SeatRequest } +import product.capacity.event_chain { PartitionId } +import product.capacity.pool_events { PoolSettled, SeatRequest } import product.capacity.lease { LeasePolicy, LeaseGrant, FencedResource } import gunbc.fabric_event_log_host { HostEventLogStore, HostStoreResolved, HostStoreRefused, event_log_store_for_host, now_epoch_seconds } import gunbc.fabric_storage_client { FabricStorageBinding } import gunbc.fabric_event_log { - event_log_refusal_wire, - HeadObservation, HeadObserved, HeadObservationRefused, event_log_observe_head, - EventAppend, EventAppended, EventAppendStale, EventAppendRefused, event_log_append, SeatAcquisition, SeatGranted, SeatFull, SeatContended, SeatAcquireRefused, fabric_seat_acquire, seat_acquisition_wire, + PoolEventAppend, PoolEventAppended, PoolEventContended, PoolEventAppendRefused, fabric_pool_event_append, pool_event_append_wire, } // A CALLER LEASES UPSTREAM QUOTA BEFORE IT SPENDS IT. The lease holds the calls it is about to @@ -45,7 +43,7 @@ fn fabric_quota_lease(short_hostname: String, limit: UpstreamRateLimit, amount: let partition = quota_partition(limit: limit) match fabric_seat_acquire( store: store, partition: partition, root: quota_root_pool(limit: limit), actor: actor, - request: SeatRequest { reference: join([actor as String, "@", to_string(now)], "") as NonEmptyStr, amount: amount, at: now, term_seconds: term_seconds }, + request: SeatRequest { reference: join([actor as String, "@", to_string(now)], "") as NonEmptyStr, amount: Measure { count: amount }, at: now, term_seconds: term_seconds }, policy: quota_policy(term_seconds: term_seconds), attempts: 3, budget: 4096, ) { SeatGranted { grant: g, generation: _, attempts_used: _ } => QuotaLeased { grant: g, partition: partition, store: store } @@ -61,46 +59,26 @@ type QuotaSettle = QuotaSettled { partition: PartitionId, actual: Nat } | QuotaSettleRefused { detail: String } -type SettleFold { - done: QuotaSettle? -} - -fn settle_attempt(lease: QuotaLease, actual: Nat, now: EpochSecs) -> QuotaSettle? { +// SETTLEMENT IS ONE PARTITION APPEND, and the observe/append/retry loop it needs is the carrier's +// (gunbc.fabric_event_log fabric_pool_event_append), not a second copy here. It used to be a copy: +// this module held the only one until a compute reservation needed to release, at which point the +// loop would have existed twice and been free to disagree with itself about a contended head. +fn fabric_quota_settle(lease: QuotaLease, actual: Nat) -> QuotaSettle { match lease { - QuotaFull { wire: w } => Present { value: QuotaSettleRefused { detail: join(["nothing to settle: ", w], "") } } - QuotaLeaseRefused { detail: d } => Present { value: QuotaSettleRefused { detail: join(["nothing to settle: ", d], "") } } + QuotaFull { wire: w } => QuotaSettleRefused { detail: join(["nothing to settle: ", w], "") } + QuotaLeaseRefused { detail: d } => QuotaSettleRefused { detail: join(["nothing to settle: ", d], "") } QuotaLeased { grant: g, partition: p, store: store } => - match event_log_observe_head(store: store, partition: p) { - HeadObservationRefused { cause: c } => Present { value: QuotaSettleRefused { detail: event_log_refusal_wire(cause: c) } } - HeadObserved { head: head } => { - let event = ChainEvent { - partition: p, - parent: match head { HeadAbsent => none HeadAt { id: h } => Present { value: h } }, - recorded_at: now, - actor: g.reference, - payload: PoolSettled { reference: g.reference, actual: actual }, - } - match event_log_append(store: store, partition: p, event: event, expected: head) { - EventAppended { id: _ } => Present { value: QuotaSettled { partition: p, actual: actual } } - EventAppendStale { expected: _, observed: _ } => none - EventAppendRefused { cause: c } => Present { value: QuotaSettleRefused { detail: event_log_refusal_wire(cause: c) } } + match now_epoch_seconds() { + Absent => QuotaSettleRefused { detail: "the clock could not be read as epoch seconds" } + Present { value: now } => + match fabric_pool_event_append( + store: store, partition: p, actor: g.reference, at: now, + payload: PoolSettled { reference: g.reference, actual: actual }, attempts: 3, + ) { + PoolEventAppended { id: _ } => QuotaSettled { partition: p, actual: actual } + other => QuotaSettleRefused { detail: pool_event_append_wire(a: other) } } - } - } - } -} - -fn fabric_quota_settle(lease: QuotaLease, actual: Nat) -> QuotaSettle { - match now_epoch_seconds() { - Absent => QuotaSettleRefused { detail: "the clock could not be read as epoch seconds" } - Present { value: now } => { - let st = fold(nat_range_inclusive(lo: 1, hi: 3), init: SettleFold { done: none }, f: (acc, _i) => - match acc.done { Present { value: _ } => acc Absent => SettleFold { done: settle_attempt(lease: lease, actual: actual, now: now) } }) - match st.done { - Present { value: r } => r - Absent => QuotaSettleRefused { detail: "settlement contended three times" } } - } } } diff --git a/dag/gunbc/harness/harness_guidance.dag b/dag/gunbc/harness/harness_guidance.dag index 563571b4166..599e907dabb 100644 --- a/dag/gunbc/harness/harness_guidance.dag +++ b/dag/gunbc/harness/harness_guidance.dag @@ -157,7 +157,7 @@ fn harness_worker_guidance_at(worktree: String, test_command: String, test_recei grounded(premise: TestProcessIs { command: test_command, receipt_path: test_receipt_path }, module_path: "gunbc.compute.test_run", decl_name: "test_pattern_cli"), grounded(premise: CapabilityWithheld { capability: BuildOrTestOutsideTheProcess }, - module_path: "gunbc.compute.work_provider_local", decl_name: "compute_cold_build_cap"), + module_path: "gunbc.compute.host_capacity", decl_name: "compute_reserve"), ]) } diff --git a/dag/gunbc/harness/harness_seat.dag b/dag/gunbc/harness/harness_seat.dag index 4b6de567bae..dd4c79fc6cf 100644 --- a/dag/gunbc/harness/harness_seat.dag +++ b/dag/gunbc/harness/harness_seat.dag @@ -3,7 +3,7 @@ module gunbc.harness.harness_seat import product.placement_supply { HostIdentity } import std.types { String, Bool, Int, NonEmptyStr, List, EpochSecs } import std.nat { Nat, nat_range_inclusive, nat_min } -import std.measure { Measure, Count, One, money_amount_micro, second } +import std.measure { Measure, Count, One, money_amount_micro, second, measure_count } import gunbc.spark.fabric_switch_observed { FabricGroup, FabricGroupA, FabricGroupB, fabric_group_wire, fabric_group_hosts } import gunbc.serving.serving_enrollment { ServingRoute, ServingRouteResolved, ServingRouteUnresolved, ServingRouteEndpoint, @@ -334,7 +334,7 @@ fn harness_class_held(route: ServingRoute, class: ServingCoTenancyClass, store: } SeatFullObserved { generation: _ } => ClassSeatsHeld { held: ceiling } SeatRoomObserved { headroom: h, generation: _ } => - ClassSeatsHeld { held: ceiling - nat_min(a: h, b: ceiling) } + ClassSeatsHeld { held: ceiling - nat_min(a: measure_count(h), b: ceiling) } } } } @@ -1225,7 +1225,7 @@ fn harness_acquire_under_authority(candidate: HarnessCandidate, class: ServingCo HeadObserved { head: h } => { let request = SeatRequest { reference: harness_seat_reference(attempt: attempt, offer_key: candidate.key, now: now, round: round, head: harness_head_word(head: h)), - amount: 1, + amount: Measure { count: 1 }, at: now, term_seconds: policy.maximum_duration_seconds, } diff --git a/dag/gunbc/instruments/fabric_event_log_probe.dag b/dag/gunbc/instruments/fabric_event_log_probe.dag index a6fb6382359..b8cb28f25a6 100644 --- a/dag/gunbc/instruments/fabric_event_log_probe.dag +++ b/dag/gunbc/instruments/fabric_event_log_probe.dag @@ -91,14 +91,14 @@ fn fabric_event_log_probe_step(store: FabricStorageBinding, partition: Partition ChainBudgetExhausted { at: _ } => 6 ChainWalked { oldest_first: xs } => if !(length(xs) == 2 && (match first(xs) { Present { value: x } => (x.id as String) == (first_id as String) Absent => false })) { 6 } else { - match fabric_seat_acquire(store: store, partition: partition, root: probe_root_pool(), actor: probe_actor(), request: SeatRequest { reference: "turn-a" as NonEmptyStr, amount: 1, at: 2000, term_seconds: 300 }, policy: probe_policy(), attempts: 3, budget: 16) { + match fabric_seat_acquire(store: store, partition: partition, root: probe_root_pool(), actor: probe_actor(), request: SeatRequest { reference: "turn-a" as NonEmptyStr, amount: Measure { count: 1 }, at: 2000, term_seconds: 300 }, policy: probe_policy(), attempts: 3, budget: 16) { SeatFull { wire: _, attempts_used: _ } => 7 SeatContended { attempts: _ } => 7 SeatAcquireRefused { step: _, reason: _, attempts_used: _ } => 7 SeatStoreRefused { cause: _, attempts_used: _ } => 7 SeatGranted { grant: ga, generation: gen_a, attempts_used: _ } => if !(gen_a == 3 && ga.expires_at == 2300) { 7 } else { - match fabric_seat_acquire(store: store, partition: partition, root: probe_root_pool(), actor: probe_actor(), request: SeatRequest { reference: "turn-b" as NonEmptyStr, amount: 1, at: 2001, term_seconds: 300 }, policy: probe_policy(), attempts: 3, budget: 16) { + match fabric_seat_acquire(store: store, partition: partition, root: probe_root_pool(), actor: probe_actor(), request: SeatRequest { reference: "turn-b" as NonEmptyStr, amount: Measure { count: 1 }, at: 2001, term_seconds: 300 }, policy: probe_policy(), attempts: 3, budget: 16) { SeatGranted { grant: _, generation: _, attempts_used: _ } => 8 SeatContended { attempts: _ } => 8 SeatAcquireRefused { step: _, reason: _, attempts_used: _ } => 8 @@ -109,7 +109,7 @@ fn fabric_event_log_probe_step(store: FabricStorageBinding, partition: Partition EventAppendRefused { cause: _ } => 9 EventAppendStale { expected: _, observed: _ } => 9 EventAppended { id: _ } => - match fabric_seat_acquire(store: store, partition: partition, root: probe_root_pool(), actor: probe_actor(), request: SeatRequest { reference: "turn-c" as NonEmptyStr, amount: 1, at: 2003, term_seconds: 300 }, policy: probe_policy(), attempts: 3, budget: 16) { + match fabric_seat_acquire(store: store, partition: partition, root: probe_root_pool(), actor: probe_actor(), request: SeatRequest { reference: "turn-c" as NonEmptyStr, amount: Measure { count: 1 }, at: 2003, term_seconds: 300 }, policy: probe_policy(), attempts: 3, budget: 16) { SeatGranted { grant: _, generation: gen_c, attempts_used: _ } => if gen_c == 5 { 0 } else { 9 } SeatFull { wire: _, attempts_used: _ } => 9 SeatContended { attempts: _ } => 9 diff --git a/dag/gunbc/instruments/fabric_seat_probe.dag b/dag/gunbc/instruments/fabric_seat_probe.dag index 041fd8bbfc1..e010e35be4c 100644 --- a/dag/gunbc/instruments/fabric_seat_probe.dag +++ b/dag/gunbc/instruments/fabric_seat_probe.dag @@ -93,7 +93,7 @@ fn fabric_seat_collision_probe(endpoint: NonEmptyStr, partition: NonEmptyStr, re partition: (partition as String) as PartitionId, root: pool, actor: join(["collision-probe:", short], "") as NonEmptyStr, - request: SeatRequest { reference: join([short, "@", to_string(now)], "") as NonEmptyStr, amount: 1, at: now, term_seconds: 120 }, + request: SeatRequest { reference: join([short, "@", to_string(now)], "") as NonEmptyStr, amount: Measure { count: 1 }, at: now, term_seconds: 120 }, policy: LeasePolicy { maximum_duration_seconds: 120, release_law: QuiescenceRequired }, attempts: 3, budget: 256, @@ -154,7 +154,7 @@ fn fabric_seat_collision_probe_from(endpoint: NonEmptyStr, partition: NonEmptySt match harness_now_epoch() { Absent => exit_failure(reason: "collision-at: clock unreadable") Present { value: now } => - match propose_acquire(pool: folded, generation: g, head: head, partition: pid, actor: actor, request: SeatRequest { reference: join([short, "@", to_string(now)], "") as NonEmptyStr, amount: 1, at: now, term_seconds: 120 }) { + match propose_acquire(pool: folded, generation: g, head: head, partition: pid, actor: actor, request: SeatRequest { reference: join([short, "@", to_string(now)], "") as NonEmptyStr, amount: Measure { count: 1 }, at: now, term_seconds: 120 }) { SeatRefused { wire: w } => { let w1 = Filesystem.Write(path: receipt as String, content: join(["host=", short, " proposal refused before the race: ", w, "\n"], "")) ExitSuccess @@ -169,7 +169,7 @@ fn fabric_seat_collision_probe_from(endpoint: NonEmptyStr, partition: NonEmptySt } EventAppendStale { expected: _, observed: _ } => { let after = fabric_seat_acquire(store: store, partition: pid, root: pool, actor: actor, - request: SeatRequest { reference: join([short, "@", to_string(now), "-retry"], "") as NonEmptyStr, amount: 1, at: now, term_seconds: 120 }, + request: SeatRequest { reference: join([short, "@", to_string(now), "-retry"], "") as NonEmptyStr, amount: Measure { count: 1 }, at: now, term_seconds: 120 }, policy: LeasePolicy { maximum_duration_seconds: 120, release_law: QuiescenceRequired }, attempts: 3, budget: 256) let w3 = Filesystem.Write(path: receipt as String, content: join(["host=", short, " STALE on first push, then ", seat_acquisition_wire(a: after), "\n"], "")) ExitSuccess diff --git a/dag/gunbc/product/capacity/pool_events.dag b/dag/gunbc/product/capacity/pool_events.dag index a7c765f7c2c..13ca830929a 100644 --- a/dag/gunbc/product/capacity/pool_events.dag +++ b/dag/gunbc/product/capacity/pool_events.dag @@ -2,7 +2,7 @@ module product.capacity.pool_events import std.types { String, Bool, Int, NonEmptyStr, List, EpochSecs } import std.nat { Nat } -import std.measure { Measure } +import std.measure { Measure, measure_count } import extdeps.languages.json.emit { JsonValue, JsonKeyValue, json_kv, json_string, json_int } import product.capacity.event_json { chain_event_wire_text, chain_event_decode, member_nonempty, member_nat } import product.capacity.pool { @@ -175,9 +175,27 @@ fn pool_fold(root: Pool, oldest_first: List // event with the head it was decided against. The carrier performs the compare-and-set; a stale // answer sends the caller back through this function with the new head. A full pool is a typed // refusal, never a queue. -type SeatRequest { +// THE REQUESTED AMOUNT CARRIES ITS DIMENSION, and this is the same repair SeatStandingObservation +// took for the same reason. A bare Nat was right while every pool reachable through this fold was +// Pool: seats are dimensionless and the field meant seats. Generalizing the carrier to +// Pool made the same field mean KiB for a memory pool and seats for a seat pool, with nothing +// in the type to say which -- so gunbc.compute.host_capacity had to call kibibyte_count to STRIP its +// Kibibyte on the way in, which is precisely the tell this change diagnoses one boundary over +// (review 69724 on gunbc#11962). +// +// WHERE THE STRIP LEGITIMATELY HAPPENS IS HERE, one layer down, and the difference is not cosmetic: +// propose_acquire holds the POOL, so the pool's own type parameters prove the request's dimension +// matches the appropriation it is being adjudicated against. A consumer stripping the carrier is +// asserting that match; this fold checks it. +// +// THE PERSISTED EVENT KEEPS A BARE Nat AND THAT IS NOT THE SAME DEFECT. PoolAcquired is a WIRE +// RECORD: its dimension is the partition's, and it is restored at both ends from the pool's own +// parameters -- minted here from a Measure the pool typed, and re-minted at replay by +// pool_apply_event into the Pool being folded. A JSON integer carrying a magnitude whose unit +// the surrounding type fixes is a serialization, not a second model of the unit. +type SeatRequest { reference: NonEmptyStr - amount: Nat + amount: Measure at: EpochSecs term_seconds: Nat } @@ -186,19 +204,35 @@ type SeatProposal = SeatProposed { event: ChainEvent, expected_head: HeadExpectation } | SeatRefused { wire: String } +// THE ONE SPELLING OF "THE POOL HAD NO ROOM", named because a consumer has to be able to tell that +// refusal from every other reason an acquire can be refused and the wire is currently the only place +// the distinction survives. SeatRefused carries a rendered string for all of them, so a consumer +// that wants "full" versus "the ledger said no" reads THIS row rather than authoring a second +// literal of its own (DESIGN 3). The reason it matters is measured: gunbc.compute.host_capacity +// mapped every SeatRefused onto a capacity refusal, and a DuplicateReference -- a ledger fact with +// nothing to do with capacity -- was reported to an operator as a full pool on a host with 400 GiB +// free (srv1, 2026-09-21). +// +// THE HONEST FIX IS A TYPED ARM AND IT IS NOT THIS. SeatRefused / SeatFull should carry the +// distinction in their constructors instead of in rendered text; that widens +// gunbc.fabric_event_log.SeatAcquisition and every existing match on SeatFull, so it is its own +// change. DECLARED FRONTIER (DESIGN 3c), trigger: the next consumer that needs a third +// classification, or the first one that must branch on a refusal this row cannot name. +data pool_full_wire: String = "pool-full" + fn seat_refusal_wire(r: PoolRefusal) -> String { match r { LedgerRefusal { refusal: lr } => match lr { - ExceedsAppropriation { requested: _, committed: _, ceiling: _ } => "pool-full" + ExceedsAppropriation { requested: _, committed: _, ceiling: _ } => pool_full_wire _ => pool_refusal_wire(r: r) } _ => pool_refusal_wire(r: r) } } -fn propose_acquire(pool: Pool, generation: Nat, head: HeadExpectation, partition: PartitionId, actor: NonEmptyStr, request: SeatRequest) -> SeatProposal { - match pool_acquire(pool: pool, reference: request.reference, amount: Measure { count: request.amount }, at: request.at, term_seconds: request.term_seconds) { +fn propose_acquire(pool: Pool, generation: Nat, head: HeadExpectation, partition: PartitionId, actor: NonEmptyStr, request: SeatRequest) -> SeatProposal { + match pool_acquire(pool: pool, reference: request.reference, amount: request.amount, at: request.at, term_seconds: request.term_seconds) { PoolRefused { refusal: r } => SeatRefused { wire: seat_refusal_wire(r: r) } PoolAdvanced { pool: _ } => SeatProposed { event: ChainEvent { @@ -206,7 +240,7 @@ fn propose_acquire(pool: Pool, generation: Nat, head: HeadExpectatio parent: match head { HeadAbsent => none HeadAt { id: h } => Present { value: h } }, recorded_at: request.at, actor: actor, - payload: PoolAcquired { reference: request.reference, amount: request.amount, term_seconds: request.term_seconds }, + payload: PoolAcquired { reference: request.reference, amount: measure_count(request.amount), term_seconds: request.term_seconds }, }, expected_head: head, } @@ -215,7 +249,7 @@ fn propose_acquire(pool: Pool, generation: Nat, head: HeadExpectatio // THE GRANT IS MINTED FROM THE ADMISSION, never from the proposal: a proposal that lost the // compare-and-set mints nothing. -fn grant_from_admission(request: SeatRequest, admission: AppendDecision, policy: LeasePolicy) -> LeaseGrant? { +fn grant_from_admission(request: SeatRequest, admission: AppendDecision, policy: LeasePolicy) -> LeaseGrant? { match admission { AppendStale { expected: _, observed: _ } => none AppendAdmitted { new_head: h, generation: g } => diff --git a/dag/gunbc/recurring_failure_mode/a_held_compute_seat_has_no_in_corpus_discharge.dag b/dag/gunbc/recurring_failure_mode/a_held_compute_seat_has_no_in_corpus_discharge.dag new file mode 100644 index 00000000000..7abfa38c7ee --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/a_held_compute_seat_has_no_in_corpus_discharge.dag @@ -0,0 +1,36 @@ +module gunbc.recurring_failure_mode.a_held_compute_seat_has_no_in_corpus_discharge + +import std.types { NonEmptyStr } +import std.decl_ref { DeclarationRef, decl_ref } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data a_held_compute_seat_has_no_in_corpus_discharge: RecurringFailureMode = RecurringFailureMode { + identity: "a_held_compute_seat_has_no_in_corpus_discharge" as NonEmptyStr, + + receipts: [ + "INVALID STATE: a quantitative reservation is taken under a release law that never lapses, and the only path that returns it is the settlement of the run that took it. When that settlement cannot prove the unit is gone -- or cannot append at all -- the encumbrance stays Held and NO DECLARATION IN THE CORPUS CAN DISCHARGE IT. HARM: the host's compute pool shrinks by one grant per occurrence and never grows back; at gunbc.compute.host_capacity compute_pool_slots = 2, two occurrences consume the whole appropriation, after which every request is refused for capacity on a host with its memory free.", + + "THIS IS A NEW CLASS RATHER THAN A DECLARED RUNG DROP, and the distinction is the one DESIGN 4b(3) turns on: a drop is a rung that FELL. Before gunbc#11962 this host admitted work by counting lease files (gunbc.compute.work_provider_local compute_cold_build_cap, deleted), so there were no reservations at all and nothing to discharge. The state becomes reachable for the first time with the pool, so it is filed here and not in gunbc.rung_drop.", + + "WHY THE RESERVATION IS NOT SIMPLY FREED ON DOUBT, which is the repair that suggests itself and is the wrong one: the pool's release law for a compute seat is QuiescenceRequired precisely because nothing can prove a systemd transient unit stopped using memory from outside it. Freeing a seat whose cargo is still resident hands its memory to the next arrival on top of a live build. Every arm that cannot prove termination therefore keeps the charge, so this class's harm is UNDER-admission -- the fail-closed direction -- and its opposite would be over-admission on a shared host.", + + "SPECIMEN, EXECUTED ON srv1 (2026-09-21, gunbc#11962): a real release build was started under a grant of 27262976 KiB and the gunbc driver was SIGKILLed mid-run. The unit stayed active, the partition carried the acquire and no release, and the producer lease stayed held -- the commitment correctly stayed charged, and nothing in the corpus could return it.", + + "THERE IS NO SAFE MANUAL DISCHARGE UNDER LIVE ADMISSION, and saying so is part of the row rather than a caveat on it. Clearing the capacity partition by hand while this host is admitting work removes the very record the admission arithmetic folds, so the next requests are admitted against memory the stuck grant still holds -- trading a host that under-admits for one that over-promises, which is the direction this whole change exists to prevent. Any manual intervention requires compute admission STOPPED on the host and every gunbc-compute unit PROVEN gone, in that order.", + + "RUNG FOUND AT: mitigatable. The state is reachable, its harm is bounded to one host's compute appropriation, it is visible in the outcome document and in the partition, and it never over-promises.", + + "CEILING: mechanically preventable. A discharge route exists to be built -- the evidence needed is a termination decision bound to the unit plus a settled lifecycle state that a retry consumes -- so this is not a class that must stay a ratchet.", + + "NEXT-RUNG TRIGGER, NAMING THE CAPABILITY AND NOT AN ARTIFACT: the compute reservation LIFECYCLE capability -- a discharge that (a) decides termination from authoritative absence or an observed-empty cgroup rather than from a state word, (b) binds the attempt and its unit from the authoritative attempt record so releasing one cannot release another's live reservation, (c) coordinates with a pending producer so a release cannot race a launch that has not happened yet, and (d) produces a settled state a retry consumes, with history kept. Until a discharge with all four properties is consumed by a real caller, this row stands.", + + "CONSUMPTION: the derived gunbc.recurring_failure_mode.roster recurring_failure_mode_roster includes this per-class declaration, and gunbc.compute.work_provider_local compute_stuck_reservation_remedy carries the remedy sentence into the refusal a caller actually receives.", + ], + + evidence: [ + decl_ref(module_path: "gunbc.compute.work_provider_local", decl_name: "compute_stuck_reservation_remedy"), + decl_ref(module_path: "gunbc.compute.work_provider_local", decl_name: "unit_termination_frees_capacity"), + decl_ref(module_path: "gunbc.compute.host_capacity", decl_name: "compute_release"), + decl_ref(module_path: "test.claim.compute.work_request_witness_test", decl_name: "only_proven_absence_or_an_ended_cgroup_frees_a_seat"), + ], +} diff --git a/dag/gunbc/recurring_failure_mode/a_pool_partition_does_not_declare_its_quantity.dag b/dag/gunbc/recurring_failure_mode/a_pool_partition_does_not_declare_its_quantity.dag new file mode 100644 index 00000000000..138a4b7c99c --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/a_pool_partition_does_not_declare_its_quantity.dag @@ -0,0 +1,34 @@ +module gunbc.recurring_failure_mode.a_pool_partition_does_not_declare_its_quantity + +import std.types { NonEmptyStr } +import std.decl_ref { DeclarationRef, decl_ref } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data a_pool_partition_does_not_declare_its_quantity: RecurringFailureMode = RecurringFailureMode { + identity: "a_pool_partition_does_not_declare_its_quantity" as NonEmptyStr, + + receipts: [ + "INVALID STATE: a persisted capacity partition carries magnitudes and does not declare the QUANTITY they are denominated in. product.capacity.pool_events pool_apply_event mints every replayed amount into the Q and S OF THE POOL BEING FOLDED, and the wire has nothing to disagree with -- so a partition written by a seat pool and replayed by a memory pool reinterprets 1 seat as 1 KiB, and a memory partition replayed by a seat pool reinterprets 27262976 KiB as 27262976 seats. HARM: an admission decision computed against a committed total that means something else; the numbers are arithmetically consistent and semantically unrelated, so nothing refuses and nothing looks wrong.", + + "THE CLASS BECAME REACHABLE WHEN THE POOL BECAME POLYMORPHIC. gunbc#11962 generalized gunbc.fabric_event_log fabric_seat_acquire and fabric_seat_observe from Pool to Pool so a host memory pool could use the same linearization as the seat pools. Before that every partition reachable through that fold was denominated in seats, the question could not be asked, and the answer could not be wrong. The generalization is what made two quantities share one carrier.", + + "WHY TYPING THE WIRE FIELD IS NOT THE REPAIR, ruled 2026-09-21 and recorded here because the wrong repair is the attractive one. Making PoolAcquired.amount a Measure looks like the fix and buys nothing: the DECODER would still mint the caller-requested Q and S, because there is nothing on the wire to disagree with. The RED would not be authorable anywhere a check could run, which DESIGN 4b names as worse than absent -- a decoration that gets cited as coverage. The admission boundary, where the hazard WAS reachable, is closed separately and by construction: SeatRequest must match Pool at propose_acquire, so a seat count can no longer be charged against a memory pool at the door.", + + "WHAT IS NOT CLAIMED: that this has occurred. The two partition namers in the corpus are disjoint by construction today -- product.capacity.quota quota_partition prefixes `quota-` over an upstream rate-limit key and gunbc.compute.host_capacity compute_memory_partition prefixes `compute-memory-` over a host identity -- so no name collides and no fold has been observed reading the wrong one. The class is filed because the DISCIPLINE preventing it is a naming convention held by two authors, not a fact the substrate checks.", + + "RUNG FOUND AT: mitigatable, and only by that convention. Nothing refuses a cross-quantity fold; what prevents it is that the two producers happen to choose non-overlapping prefixes and that each consumer happens to pass the pool it built the partition name from.", + + "CEILING: structurally guaranteed. A partition identity that BINDS the quantity it is denominated in, checked where the fold is assembled, makes the mismatched pairing refuse rather than reinterpret -- the root pool and the partition are already supplied together at every call site, so the join exists and is simply not made.", + + "NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: partition identity binds the pool quantity, so assembling a fold from a partition and a root pool whose quantities disagree is a typed refusal rather than a silent reinterpretation. It is deliberately NOT `carry Measure through the codec` -- that artifact could land in full while this class stayed exactly as dead, which is the grain mismatch DESIGN 4b(3) warns about between a loss sentence and its trigger.", + + "CONSUMPTION: the derived gunbc.recurring_failure_mode.roster recurring_failure_mode_roster includes this per-class declaration.", + ], + + evidence: [ + decl_ref(module_path: "product.capacity.pool_events", decl_name: "pool_apply_event"), + decl_ref(module_path: "product.capacity.pool_events", decl_name: "pool_event_decode"), + decl_ref(module_path: "product.capacity.quota", decl_name: "quota_partition"), + decl_ref(module_path: "gunbc.compute.host_capacity", decl_name: "compute_memory_partition"), + ], +} diff --git a/dag/std/measure.dag b/dag/std/measure.dag index 46b181dc4d5..29df7c94796 100644 --- a/dag/std/measure.dag +++ b/dag/std/measure.dag @@ -329,6 +329,16 @@ fn kibibyte_to_byte_size(k: Kibibyte) -> ByteSize { byte_size(count: kibibyte_count(k) * kibi_factor()) } +// THE INVERSE OF kibibyte_to_byte_size, FLOORING. A byte count that is not a whole number of +// kibibytes has no exact kibibyte reading, and the floor is the only rounding a CAPACITY may take: +// rounding up would report a ceiling the host does not have, and a reservation admitted against it +// would be admitted against memory that is not there. Named _floor for the same reason +// measure_scale_fraction_floor is -- the direction is part of what the caller is asking for, not an +// implementation detail it may discover later. +fn kibibyte_from_byte_size_floor(b: ByteSize) -> Kibibyte { + kibibyte(count: byte_size_count(b: b) / kibi_factor()) +} + fn mebibyte_to_byte_size(m: Mebibyte) -> ByteSize { byte_size(count: mebibyte_count(m) * mebibyte_scale_factor_bytes()) } diff --git a/dag/test/claim/capacity_lease_chain_witness_test.dag b/dag/test/claim/capacity_lease_chain_witness_test.dag index 825874a4632..50b263bff49 100644 --- a/dag/test/claim/capacity_lease_chain_witness_test.dag +++ b/dag/test/claim/capacity_lease_chain_witness_test.dag @@ -90,9 +90,9 @@ test fn two_writers_from_one_head_produce_one_admission_one_stale_and_then_a_ful PoolFoldRefused { at_event: _, wire: _ } => false PoolFolded { pool: p, generation: g } => { let a = propose_acquire(pool: p, generation: g, head: head, partition: w_partition(), actor: "srv1-harness" as NonEmptyStr, - request: SeatRequest { reference: "srv1-turn-7" as NonEmptyStr, amount: 1, at: 1100, term_seconds: 300 }) + request: SeatRequest { reference: "srv1-turn-7" as NonEmptyStr, amount: Measure { count: 1 }, at: 1100, term_seconds: 300 }) let b = propose_acquire(pool: p, generation: g, head: head, partition: w_partition(), actor: "srv2-harness" as NonEmptyStr, - request: SeatRequest { reference: "srv2-turn-3" as NonEmptyStr, amount: 1, at: 1100, term_seconds: 300 }) + request: SeatRequest { reference: "srv2-turn-3" as NonEmptyStr, amount: Measure { count: 1 }, at: 1100, term_seconds: 300 }) match a { SeatRefused { wire: _ } => false SeatProposed { event: ea, expected_head: xa } => @@ -109,7 +109,7 @@ test fn two_writers_from_one_head_produce_one_admission_one_stale_and_then_a_ful PoolFolded { pool: p2, generation: g2 } => g2 == 2 && w_headroom(p: p2, at: 1100) == 0 && (match propose_acquire(pool: p2, generation: g2, head: HeadAt { id: w_id(s: "e2") }, partition: w_partition(), actor: "srv2-harness" as NonEmptyStr, - request: SeatRequest { reference: "srv2-turn-3" as NonEmptyStr, amount: 1, at: 1101, term_seconds: 300 }) { + request: SeatRequest { reference: "srv2-turn-3" as NonEmptyStr, amount: Measure { count: 1 }, at: 1101, term_seconds: 300 }) { SeatRefused { wire: w } => w == "pool-full" SeatProposed { event: _, expected_head: _ } => false }) @@ -147,7 +147,7 @@ test fn the_fence_rejects_obsolete_and_foreign_grants_and_expiry_frees_only_unde // THE GRANT IS MINTED FROM THE ADMISSION, never from the proposal: its fence is the admitted event // and generation, and its deadline is the declared policy applied at the grant instant. test fn a_grant_carries_the_admitted_event_as_its_fence_and_the_declared_deadline() -> Bool { - let req = SeatRequest { reference: "srv1-turn-7" as NonEmptyStr, amount: 1, at: 1100, term_seconds: 300 } + let req = SeatRequest { reference: "srv1-turn-7" as NonEmptyStr, amount: Measure { count: 1 }, at: 1100, term_seconds: 300 } match grant_from_admission(request: req, admission: AppendAdmitted { new_head: w_id(s: "e2"), generation: 2 }, policy: w_policy()) { Absent => false Present { value: g } => @@ -212,7 +212,7 @@ test fn an_over_committed_pool_still_refuses_a_new_acquire() -> Bool { PoolFolded { pool: p, generation: g } => match propose_acquire(pool: p, generation: g, head: HeadAt { id: w_id(s: "o4") }, partition: w_partition(), actor: "srv1-harness" as NonEmptyStr, - request: SeatRequest { reference: "seat-5" as NonEmptyStr, amount: 1, at: 1100, term_seconds: 300 }) { + request: SeatRequest { reference: "seat-5" as NonEmptyStr, amount: Measure { count: 1 }, at: 1100, term_seconds: 300 }) { SeatProposed { event: _, expected_head: _ } => false SeatRefused { wire: w } => w == "pool-full" } @@ -311,7 +311,7 @@ test fn a_lapsed_quiescence_required_partition_still_refuses_the_next_seat() -> PoolFolded { pool: p, generation: g } => match propose_acquire(pool: p, generation: g, head: HeadAt { id: w_id(s: "l2") }, partition: w_partition(), actor: "srv1-harness" as NonEmptyStr, - request: SeatRequest { reference: "seat-arriving" as NonEmptyStr, amount: 1, at: 2001, term_seconds: 300 }) { + request: SeatRequest { reference: "seat-arriving" as NonEmptyStr, amount: Measure { count: 1 }, at: 2001, term_seconds: 300 }) { SeatProposed { event: _, expected_head: _ } => false SeatRefused { wire: w } => w == "pool-full" } diff --git a/dag/test/claim/compute/host_capacity_wet_witness_test.dag b/dag/test/claim/compute/host_capacity_wet_witness_test.dag new file mode 100644 index 00000000000..490ef641cd8 --- /dev/null +++ b/dag/test/claim/compute/host_capacity_wet_witness_test.dag @@ -0,0 +1,231 @@ +module test.claim.compute.host_capacity_wet_witness + +import extdeps.shell +import std.types { Bool, Int, NonEmptyStr, String } +import std.measure { Kibibyte, kibibyte, kibibyte_count } +import std.algebra { trim } +import product.capacity.event_chain { PartitionId } +import gunbc.roadmap_dashboard_instance { srv1_live_dashboard_instance, srv1_lab_dashboard_instance, dashboard_instance_compute_root } +import gunbc.compute.host_capacity { + ComputeCapacitySubject, ComputeSubjectResolution, ComputeSubjectResolved, ComputeSubjectHostUnresolved, + compute_capacity_subject, compute_capacity_root, compute_memory_partition, + HostMemoryObservation, HostMemoryObserved, HostMemoryUnobserved, observe_host_memory, + ComputeReservation, ComputeReserved, ComputeCapacityFull, ComputeHostBelowFloor, ComputeReservationRefused, + compute_reserve_on, compute_reserve_against, compute_release, ComputeRelease, ComputeReleased, ComputeReleaseRefused, + ComputeCapacityStanding, ComputeCapacityStandingRead, ComputeCapacityStandingUnread, compute_capacity_standing_on, +} + +// WET CONTROLS FOR THE HOST'S COMPUTE MEMORY POOL. Every reservation below is a real append to a +// real event log on a real temporary directory, decided against a real reading of this machine's +// /proc/meminfo. Nothing here is a fixture standing in for the store: the linearization being +// asserted is the one gunbc.compute.work_provider_local runs. +// +// THE SUBJECT IS SUPPLIED AND THE JOIN THAT PRODUCES ONE IS ASSERTED SEPARATELY (DESIGN 3, the +// pairing obligation): a ComputeCapacitySubject is four values, and deriving it here would mean +// standing up a whole deployment record to exercise arithmetic that does not depend on one. The +// inhabitance claim is the_deployment_join_roots_the_ledger_under_the_instance_compute_root below, +// which runs the real producer. + +data one_gibibyte_in_kibibytes: Int = 1048576 + +fn fresh_root() -> String { + shell.Mktemp.DirWithTemplate(template: "/tmp/gunbc_compute_capacity.XXXXXX").path +} + +fn subject_at(root: String, appropriation_kib: Int, request_kib: Int) -> ComputeCapacitySubject { + ComputeCapacitySubject { + root: join([trim(s: root), "/capacity"], "") as NonEmptyStr, + partition: "compute-memory-wet-witness" as PartitionId, + appropriation: kibibyte(count: appropriation_kib), + request: kibibyte(count: request_kib), + } +} + +fn reserved_amount(r: ComputeReservation) -> Int { + match r { + ComputeReserved { grant: _, partition: _, amount: a, store: _ } => kibibyte_count(k: a) + ComputeCapacityFull { wire: _ } => 0 + ComputeHostBelowFloor { requested: _, available: _ } => 0 + ComputeReservationRefused { detail: _ } => 0 + } +} + +fn is_capacity_full(r: ComputeReservation) -> Bool { + match r { + ComputeCapacityFull { wire: w } => string_contains(s: w, pattern: "pool-full") + ComputeReserved { grant: _, partition: _, amount: _, store: _ } => false + ComputeHostBelowFloor { requested: _, available: _ } => false + ComputeReservationRefused { detail: _ } => false + } +} + +fn is_ledger_refusal(r: ComputeReservation) -> Bool { + match r { + ComputeReservationRefused { detail: d } => string_contains(s: d, pattern: "the capacity ledger refused the acquire") + ComputeReserved { grant: _, partition: _, amount: _, store: _ } => false + ComputeCapacityFull { wire: _ } => false + ComputeHostBelowFloor { requested: _, available: _ } => false + } +} + +fn released(r: ComputeRelease) -> Bool { + match r { + ComputeReleased { partition: _, reference: _, reason: _ } => true + ComputeReleaseRefused { detail: _ } => false + } +} + +fn standing_committed(s: ComputeCapacityStanding) -> Int { + match s { + ComputeCapacityStandingRead { committed: c, ceiling: _, headroom: _, observed_available: _, observed_total: _ } => kibibyte_count(k: c) + ComputeCapacityStandingUnread { detail: _ } => 0 - 1 + } +} + +// THE CONTROL THIS WHOLE CHANGE EXISTS FOR, AND IT IS RED UNDER THE THING IT REPLACED. A pool of two +// gibibytes admits two one-gibibyte reservations and REFUSES THE THIRD; the deleted admission -- +// count the lease directory, compare, then create -- admitted the third whenever the two lease +// files belonged to different identities, because a count of names excludes no quantity. Then the +// release returns exactly what it held and the next request is admitted again, which is the other +// half: capacity that never comes back is a wall, not a pool. +// +// MUTATION CONTROL: raise the appropriation above the sum of the three requests and the third +// reservation is admitted, so this cell goes red for the reason it names rather than for any +// property of the store. +test fn competing_reservations_cannot_over_reserve_and_a_release_returns_the_capacity() -> Bool { + let subject = subject_at(root: fresh_root(), appropriation_kib: one_gibibyte_in_kibibytes * 2, request_kib: one_gibibyte_in_kibibytes) + let first = compute_reserve_on(subject: subject, reference: "wet-first" as NonEmptyStr, term_seconds: 60) + let second = compute_reserve_on(subject: subject, reference: "wet-second" as NonEmptyStr, term_seconds: 60) + let full = compute_reserve_on(subject: subject, reference: "wet-third" as NonEmptyStr, term_seconds: 60) + let at_capacity = compute_capacity_standing_on(subject: subject) + let back = compute_release(reservation: first, reason: "witness completion" as NonEmptyStr) + let after_release = compute_capacity_standing_on(subject: subject) + let readmitted = compute_reserve_on(subject: subject, reference: "wet-fourth" as NonEmptyStr, term_seconds: 60) + reserved_amount(r: first) == one_gibibyte_in_kibibytes + && reserved_amount(r: second) == one_gibibyte_in_kibibytes + && is_capacity_full(r: full) + && standing_committed(s: at_capacity) == one_gibibyte_in_kibibytes * 2 + && released(r: back) + && standing_committed(s: after_release) == one_gibibyte_in_kibibytes + && reserved_amount(r: readmitted) == one_gibibyte_in_kibibytes +} + +// A RESERVATION THE MACHINE CANNOT BACK IS REFUSED BEFORE THE LEDGER IS TOUCHED, and it is a +// DIFFERENT refusal from a full pool: the pool's own commitments are irrelevant here (this ledger is +// empty), and the remedy is to find out what else is on the host rather than to wait for a seat. +// The request is the machine's own installed memory, which is strictly above what it reports +// available on any host that is running anything at all -- including the one running this witness. +test fn a_request_the_machine_cannot_back_refuses_below_the_live_floor() -> Bool { + let total = kibibyte(count: 64 * one_gibibyte_in_kibibytes) + let available = kibibyte(count: 4 * one_gibibyte_in_kibibytes) + let subject = subject_at(root: fresh_root(), appropriation_kib: 52 * one_gibibyte_in_kibibytes, request_kib: 26 * one_gibibyte_in_kibibytes) + match compute_reserve_against(subject: subject, reference: "wet-floor" as NonEmptyStr, term_seconds: 60, total: total, available: available) { + ComputeHostBelowFloor { requested: rq, available: av } => + kibibyte_count(k: rq) == 26 * one_gibibyte_in_kibibytes && kibibyte_count(k: av) == 4 * one_gibibyte_in_kibibytes + ComputeReserved { grant: _, partition: _, amount: _, store: _ } => false + ComputeCapacityFull { wire: _ } => false + ComputeReservationRefused { detail: _ } => false + } +} + +// AN APPROPRIATION LARGER THAN THE MACHINE IS A CONFIGURATION ERROR AND SAYS SO, rather than +// presenting hours later as a build the kernel killed. It is refused ahead of the floor check, +// because a share that was never backed is wrong whatever this instant's availability happens to be. +test fn an_appropriation_larger_than_the_machine_refuses_rather_than_admitting() -> Bool { + let total = kibibyte(count: 64 * one_gibibyte_in_kibibytes) + let subject = subject_at(root: fresh_root(), appropriation_kib: 64 * one_gibibyte_in_kibibytes + 1, request_kib: one_gibibyte_in_kibibytes) + match compute_reserve_against(subject: subject, reference: "wet-oversized" as NonEmptyStr, term_seconds: 60, total: total, available: total) { + ComputeReservationRefused { detail: d } => string_contains(s: d, pattern: "never backed by the machine") + ComputeReserved { grant: _, partition: _, amount: _, store: _ } => false + ComputeCapacityFull { wire: _ } => false + ComputeHostBelowFloor { requested: _, available: _ } => false + } +} + +// THE INHABITANCE CLAIM FOR EVERY SUPPLIED SUBJECT ABOVE (DESIGN 3). The real producer is the +// deployment join, and what it must establish is the ROUTE and not only the shape: the ledger a +// live instance reserves against is rooted under THAT INSTANCE'S compute root, and its partition +// names that instance, so two instances on one machine cannot silently transact on one pool. +test fn two_instances_on_one_host_resolve_to_one_pool_at_one_root() -> Bool { + let live = srv1_live_dashboard_instance() + let lab = srv1_lab_dashboard_instance() + match compute_capacity_subject(instance: live) { + ComputeSubjectHostUnresolved { host: _ } => false + ComputeSubjectResolved { subject: a } => + match compute_capacity_subject(instance: lab) { + ComputeSubjectHostUnresolved { host: _ } => false + ComputeSubjectResolved { subject: b } => + (live.instance_id as String) != (lab.instance_id as String) + && (live.instance_root as String) != (lab.instance_root as String) + && (live.host_identity as String) == (lab.host_identity as String) + && (a.partition as String) == (b.partition as String) + && (a.root as String) == (b.root as String) + && string_contains(s: a.partition as String, pattern: live.host_identity as String) + && !string_contains(s: a.partition as String, pattern: lab.instance_id as String) + && (a.root as String) == join([dashboard_instance_compute_root(instance: live) as String, "/capacity"], "") + && kibibyte_count(k: a.appropriation) == kibibyte_count(k: a.request) * 2 + && kibibyte_count(k: a.request) > 0 + } + } +} + + +// A LEDGER REFUSAL IS NOT A CAPACITY REFUSAL, and this cell exists because the two were conflated in +// production and the conflation was only visible on a real host. The reservation reference names one +// HOLD; re-using it is a DuplicateReference from the encumbrance ledger, which the seat carrier +// renders into the same SeatFull arm a genuinely exhausted pool reaches. Reported as capacity, it +// sent a reader looking for a busy machine while srv1 had 400 GiB free (2026-09-21) -- and the +// provider's own dependent request refused on a dependency that had succeeded. +// +// The pool here has room for BOTH requests, so nothing about capacity can explain the second +// answer: if this cell ever reports ComputeCapacityFull again, the conflation is back. +test fn a_reused_reference_is_a_ledger_refusal_and_never_reported_as_a_full_pool() -> Bool { + let subject = subject_at(root: fresh_root(), appropriation_kib: one_gibibyte_in_kibibytes * 4, request_kib: one_gibibyte_in_kibibytes) + let first = compute_reserve_on(subject: subject, reference: "wet-same-reference" as NonEmptyStr, term_seconds: 60) + let again = compute_reserve_on(subject: subject, reference: "wet-same-reference" as NonEmptyStr, term_seconds: 60) + let other = compute_reserve_on(subject: subject, reference: "wet-other-reference" as NonEmptyStr, term_seconds: 60) + reserved_amount(r: first) == one_gibibyte_in_kibibytes + && is_ledger_refusal(r: again) + && !is_capacity_full(r: again) + && reserved_amount(r: other) == one_gibibyte_in_kibibytes +} + +// THE DOUBLE PROMISE, AND IT IS THE CELL THE COMPARE-AND-SET COULD NOT SUPPLY. Two requests whose +// SUM exceeds what the machine says is free, against a pool whose declared appropriation is large +// enough for both: the first admits, and the second must be refused because the pool's committed +// total and the host's own reading are adjudicated in ONE step. Before that, each request compared +// itself alone against the reading, both passed, and both fit the appropriation -- so both admitted +// and the host was promised memory it does not have. The linearization was never the defect. +// +// The appropriation here is deliberately FOUR requests wide, so nothing about the declared share +// can explain the refusal; only the machine's reading can. The backing ceiling is derived from the +// live observation, so the fixture states the relation rather than a number: it asks for slightly +// more than half of what the host reports free, twice. +test fn two_requests_summing_past_the_observed_headroom_cannot_both_admit() -> Bool { + let total = kibibyte(count: 64 * one_gibibyte_in_kibibytes) + let available = kibibyte(count: 30 * one_gibibyte_in_kibibytes) + let subject = subject_at(root: fresh_root(), appropriation_kib: 52 * one_gibibyte_in_kibibytes, request_kib: 26 * one_gibibyte_in_kibibytes) + let first = compute_reserve_against(subject: subject, reference: "wet-headroom-a" as NonEmptyStr, term_seconds: 60, total: total, available: available) + let second = compute_reserve_against(subject: subject, reference: "wet-headroom-b" as NonEmptyStr, term_seconds: 60, total: total, available: available) + kibibyte_count(k: subject.request) <= kibibyte_count(k: available) + && kibibyte_count(k: subject.request) * 2 > kibibyte_count(k: available) + && kibibyte_count(k: subject.appropriation) >= kibibyte_count(k: subject.request) * 2 + && kibibyte_count(k: subject.appropriation) <= kibibyte_count(k: total) + && reserved_amount(r: first) == kibibyte_count(k: subject.request) + && is_capacity_full(r: second) +} + +// THE PAIRING OBLIGATION FOR EVERY SUPPLIED OBSERVATION ABOVE (DESIGN 3): the real producer emits a +// reading of THIS machine, and it is a reading rather than a shape -- installed memory is positive, +// availability does not exceed it, and the two are not the same number on a host that is running +// anything. A fixture cannot establish that and the supplied cells do not claim to. +test fn the_real_observation_reads_this_machine() -> Bool { + match observe_host_memory() { + HostMemoryUnobserved { detail: _ } => false + HostMemoryObserved { total: total, available: available } => + kibibyte_count(k: total) > 0 + && kibibyte_count(k: available) > 0 + && kibibyte_count(k: available) < kibibyte_count(k: total) + } +} + diff --git a/dag/test/claim/compute/work_request_witness_test.dag b/dag/test/claim/compute/work_request_witness_test.dag index 6d57f7a0a71..c641d411fed 100644 --- a/dag/test/claim/compute/work_request_witness_test.dag +++ b/dag/test/claim/compute/work_request_witness_test.dag @@ -2,11 +2,23 @@ module test.claim.compute.work_request_witness_test import std.types { String, Bool, Int, List, NonEmptyStr, FilePath } import extdeps.git.object_store { GitObjectId, git_object_id_from_untagged_hex } +import gunbc.compute.work_provider_local { + UnitTermination, UnitAttemptCompleted, UnitAbsentAuthoritatively, UnitPopulated, UnitTerminationUnavailable, + UnitPropertyReading, UnitObservations, unit_termination_decide, + unit_termination_frees_capacity, unit_termination_wire, compute_attempt_completed, + ProvideResult, ProvideFresh, ProvideAttached, HostRecordStatus, HostRecordWritten, HostRecordLost, + provide_result_host_record, provide_result_ending, provide_result_document, host_record_was_written, host_record_wire, + compute_with_lost_host_record, provide_result_with_host_record, host_record_join, + ComputeLayout, compute_layout, compute_unit_properties, + compute_kill_mode_property, compute_kill_mode_value, +} +import std.measure { kibibyte } +import gunbc.roadmap_dashboard_instance { srv1_live_dashboard_instance } import gunbc.compute.work_request { WorkSubject, ExactTree, WorkOperation, BuildGunbcBinaries, CompileEntry, RunClaims, CargoRelease, CargoDebug, WorkToolchainIdentity, work_identity, work_identity_hex, work_default_build, work_declared_outputs, DeclaredOutput, WorkOutputRoot, CheckoutRoot, TargetRoot, - WorkOutput, WorkOutcome, WorkSucceeded, WorkFailed, WorkRefusedByInfrastructure, HostAtColdBuildCap, + WorkOutput, WorkOutcome, WorkSucceeded, WorkFailed, WorkRefusedByInfrastructure, HostComputeCapacityFull, work_outcome_wire, stored_outcome_decode, StoredOutcomeFound, StoredOutcomeUnreadable, stored_outcome_is_success, } @@ -64,13 +76,166 @@ test fn the_stored_outcome_round_trips_and_a_broken_one_is_unreadable() -> Bool let subject = tree(hex: tree_a) let ok = work_outcome_wire(o: WorkSucceeded { identity: "abc", outputs: [WorkOutput { declared: "target/release/gunbc", blob: "deadbeef", store_path: "/s/gunbc" }], log_path: "/l" }, subject: subject, op: work_default_build()) let failed = work_outcome_wire(o: WorkFailed { identity: "abc", exit_code: 101, log_path: "/l" }, subject: subject, op: work_default_build()) - let refused = work_outcome_wire(o: WorkRefusedByInfrastructure { identity: "abc", cause: HostAtColdBuildCap { in_flight: 2, cap: 2 } }, subject: subject, op: work_default_build()) + let refused = work_outcome_wire(o: WorkRefusedByInfrastructure { identity: "abc", cause: HostComputeCapacityFull { wire: "pool-full (attempt 1)" } }, subject: subject, op: work_default_build()) (match stored_outcome_decode(text: ok) { StoredOutcomeFound { ending, identity, document: _ } => ending == "succeeded" && identity == "abc" StoredOutcomeUnreadable { reason: _ } => false }) && stored_outcome_is_success(r: stored_outcome_decode(text: ok)) && !stored_outcome_is_success(r: stored_outcome_decode(text: failed)) && (match stored_outcome_decode(text: refused) { StoredOutcomeFound { ending, identity: _, document: _ } => ending == "refused_by_infrastructure" StoredOutcomeUnreadable { reason: _ } => false }) - && string_contains(s: refused, pattern: "cap 2") + && string_contains(s: refused, pattern: "pool-full") && string_contains(s: ok, pattern: "\"blob\": \"deadbeef\"") && (match stored_outcome_decode(text: "{\"identity\": \"abc\"}") { StoredOutcomeUnreadable { reason: _ } => true StoredOutcomeFound { ending: _, identity: _, document: _ } => false }) && (match stored_outcome_decode(text: "not json") { StoredOutcomeUnreadable { reason: _ } => true StoredOutcomeFound { ending: _, identity: _, document: _ } => false }) } + +// THE CONTROLS SIT AT THE OBSERVATION-TO-DECISION BOUNDARY, not at the variant-to-release mapping, +// because the mapping cannot see the defects that actually occurred: a failed query whose TEXT +// looks like an answer, a property that came back EMPTY, and a start that is still PENDING all +// arrive as readings and are wrong only in how they are read (side-chat review at 5ee0cce). +// +// THE PREDICATE IS EXACTLY FOUR WORDS LONG AND EVERY OTHER READING KEEPS THE CHARGE: occupied +// keeps; authoritative absence releases; completed AND POSITIVELY EMPTY releases; everything else +// keeps. The revision before this one read "not occupied AND (absent OR completed)", so +// completed + UNKNOWN released -- and this cell ASSERTED that, which is the worse half: a control +// that pins the defect is not a control (side-chat verdict at f5344b28). A bound KillMode says what +// systemd WILL do; it is not a reading of what is true, and an unreadable cgroup establishes +// nothing beside a completed wait. +// +// A COMPLETED WAIT NEVER OVERRIDES A POSITIVE POPULATION, which is the row the previous revision +// got backwards: completion was tested FIRST and returned immediately, so {completed, populated 1} +// RELEASED -- a launcher's success overriding the kernel saying processes are still there. Under +// KillMode=process or none a forked child outlives the main process exactly like that. Contrary +// evidence wins now, and a positive populated=1 is never discarded. +// +// AND A MOMENTARILY EMPTY CGROUP IS NOT TERMINAL ON ITS OWN: populated=0 WITHOUT an established +// completion used to release, and a realized cgroup can be empty between execs. Uncertain +// completion keeps the charge. +// +// THE PENDING-START ROW IS THE ONE THIS CELL EXISTS FOR. An empty ControlGroup was read as observed +// termination, and it equally describes a unit whose start has not spawned yet -- systemd realizes +// the cgroup AT SPAWN. That made a whole unbacked launch reachable: reserve, start pending, the +// LAUNCHER lost while this driver lives on, settlement sees the empty property, releases, and the +// job then starts against memory nobody holds. It must establish nothing. +fn reading(queried: Bool, value: String) -> UnitPropertyReading { + UnitPropertyReading { queried: queried, value: value } +} + +fn decided(done: Bool, load: UnitPropertyReading, cg: UnitPropertyReading, ev: UnitPropertyReading) -> UnitTermination { + unit_termination_decide(o: UnitObservations { attempt_completed: done, load_state: load, control_group: cg, events: ev }) +} + +test fn only_proven_absence_or_an_ended_cgroup_frees_a_seat() -> Bool { + let no_events = reading(queried: false, value: "") + let unread = reading(queried: false, value: "") + let completed_empty = decided(done: true, load: reading(queried: true, value: "loaded"), cg: reading(queried: true, value: "/x"), ev: reading(queried: true, value: "populated 0\n")) + let completed_populated = decided(done: true, load: reading(queried: true, value: "loaded"), cg: reading(queried: true, value: "/x"), ev: reading(queried: true, value: "populated 1\n")) + let completed_unknown = decided(done: true, load: reading(queried: true, value: "loaded"), cg: reading(queried: true, value: ""), ev: no_events) + let absent = decided(done: false, load: reading(queried: true, value: "not-found"), cg: unread, ev: no_events) + let misleading = decided(done: false, load: reading(queried: false, value: "Failed to connect to bus: not-found"), cg: unread, ev: no_events) + let empty_load = decided(done: false, load: reading(queried: true, value: ""), cg: reading(queried: true, value: "/x"), ev: reading(queried: true, value: "populated 0\n")) + let pending = decided(done: false, load: reading(queried: true, value: "loaded"), cg: reading(queried: true, value: ""), ev: no_events) + let empty_no_completion = decided(done: false, load: reading(queried: true, value: "loaded"), cg: reading(queried: true, value: "/x"), ev: reading(queried: true, value: "populated 0\n")) + let populated_no_completion = decided(done: false, load: reading(queried: true, value: "loaded"), cg: reading(queried: true, value: "/x"), ev: reading(queried: true, value: "populated 1\n")) + let undecodable = decided(done: false, load: reading(queried: true, value: "loaded"), cg: reading(queried: true, value: "/x"), ev: reading(queried: true, value: "garbage\n")) + unit_termination_frees_capacity(t: completed_empty) + && unit_termination_frees_capacity(t: absent) + && !unit_termination_frees_capacity(t: completed_unknown) + && !unit_termination_frees_capacity(t: completed_populated) + && !unit_termination_frees_capacity(t: empty_no_completion) + && !unit_termination_frees_capacity(t: populated_no_completion) + && !unit_termination_frees_capacity(t: misleading) + && !unit_termination_frees_capacity(t: empty_load) + && !unit_termination_frees_capacity(t: pending) + && !unit_termination_frees_capacity(t: undecodable) + && string_contains(s: unit_termination_wire(t: completed_populated), pattern: "STILL POPULATED") + && string_contains(s: unit_termination_wire(t: completed_unknown), pattern: "establishes nothing even beside a completed wait") + && string_contains(s: unit_termination_wire(t: empty_no_completion), pattern: "did not complete") + && string_contains(s: unit_termination_wire(t: pending), pattern: "pending") + && string_contains(s: unit_termination_wire(t: misleading), pattern: "UNESTABLISHED") +} + +// A COMPLETED ATTEMPT RELEASES, AND AN ATTEMPT THAT DID NOT COMPLETE DOES NOT RELEASE ON ITS OWN. +// The work's ENDING and the attempt's COMPLETION are different questions: a WorkFailed says the +// unit exited nonzero OR that the launcher never got an answer, and only the second is a lost +// launcher. The ending is what the caller is told; completion is what the seat is decided on. +test fn the_attempt_completion_fact_is_not_the_works_ending() -> Bool { + compute_attempt_completed(outcome: WorkSucceeded { identity: "a", outputs: [], log_path: "/l" }) + && compute_attempt_completed(outcome: WorkOutputMismatch { identity: "a", detail: "d" }) + && !compute_attempt_completed(outcome: WorkFailed { identity: "a", exit_code: 1, log_path: "/l" }) + && !compute_attempt_completed(outcome: WorkCancelled { identity: "a" }) + && !compute_attempt_completed(outcome: WorkRefusedByInfrastructure { identity: "a", cause: HostComputeCapacityFull { wire: "pool-full" } }) +} + +// AN ATTACHED RESULT CARRIES THE LOSS TOO, which is the arm that used to throw it away. The only +// call site passes a FRESH result, so the discard was latent -- and "latent" is the kind of safe +// that stops being true at the next call site, in the very function whose annotation is about a +// fact vanishing (review 69724). Both arms are driven here. +// +// THE STORED RECORD AND THE RETURNED OUTCOME AGREE, WHATEVER HAPPENED TO THIS HOST'S OWN RECORD. +// The fusion was made twice in opposite directions -- a refusal handed to the caller over a stored +// success, then a synthesized refusal over a published outcome -- and both times the next attacher +// read something different from the caller. Losing the host record now changes the host_record +// fact and NOTHING about the work, so re-requesting the identity yields the same ending the first +// caller was told; what the first caller additionally gets is the recording failure, which is the +// only consumer that could act on it. +test fn a_lost_host_record_changes_no_contract_the_next_caller_reads() -> Bool { + let succeeded = WorkSucceeded { identity: "abc", outputs: [], log_path: "/l" } + let document = work_outcome_wire(o: succeeded, subject: tree(hex: tree_a), op: work_default_build()) + let settled = ProvideFresh { outcome: succeeded, document: document, host_record: HostRecordWritten } + let attached = ProvideAttached { identity: "abc", ending: "succeeded", document: document, host_record: HostRecordWritten } + let layout = compute_layout(instance: srv1_live_dashboard_instance(), identity_hex: "abc") + let lost = compute_with_lost_host_record(settled: settled, layout: layout, dropped_ok: false, dropped_error: "EBUSY", error: "ENOSPC") + let lost_attached = compute_with_lost_host_record(settled: attached, layout: layout, dropped_ok: false, dropped_error: "EBUSY", error: "ENOSPC") + provide_result_ending(r: lost) == provide_result_ending(r: settled) + && provide_result_document(r: lost) == provide_result_document(r: settled) + && provide_result_ending(r: lost) == "succeeded" + && host_record_was_written(h: provide_result_host_record(r: settled)) + && !host_record_was_written(h: provide_result_host_record(r: lost)) + && string_contains(s: host_record_wire(h: provide_result_host_record(r: lost)), pattern: "STILL HELD") + && provide_result_ending(r: lost_attached) == "succeeded" + && provide_result_document(r: lost_attached) == document + && !host_record_was_written(h: provide_result_host_record(r: lost_attached)) + && string_contains(s: host_record_wire(h: provide_result_host_record(r: lost_attached)), pattern: "STILL HELD") +} + +// THIS CHECKS INVOCATION WIRING, NOT A RUNTIME POLICY READBACK, and the distinction is the whole +// honesty of the cell. It reads the argv this provider CONSTRUCTS and establishes that the +// KillMode word is in it. It does NOT establish what systemd applied: a drop-in, a manager that +// rejected the property, or a unit started by some other path are all outside what any fold over +// our own argv can see. That is precisely why the release predicate does not lean on the binding -- +// completion must still be confirmed by a positively empty cgroup, and this row only ensures we are +// not ALSO shipping an invocation that opts into the dangerous mode. +test fn the_unit_binds_the_termination_policy_the_release_decision_relies_on() -> Bool { + let props = compute_unit_properties( + layout: compute_layout(instance: srv1_live_dashboard_instance(), identity_hex: "abc"), + granted: kibibyte(count: 1048576)) + contains(props, join([compute_kill_mode_property, "=", compute_kill_mode_value], "")) + && compute_kill_mode_value == "control-group" + && count(filter(props, p => starts_with(s: p, prefix: "MemoryMax="))) == 1 +} + +// A LOSS ANYWHERE IN THE CHAIN REACHES A TERMINAL CONSUMER, which is the property three separate +// seams were erasing: compute_provide_dependent returned only the child's result, so a BUILD that +// lost its record followed by a successful dependent reported clean; and compile_entry_cli and +// run_selected_module both read only the work's ending (side-chat verdict at f5344b28). +// +// The join is what carries it, and it accumulates rather than letting the later arm win -- both +// details are kept because they name different identities and an operator needs each. The work +// contract is untouched by all of this: the ending and the document are exactly what was stored. +test fn a_lost_record_on_a_dependency_survives_a_successful_dependent() -> Bool { + let succeeded = WorkSucceeded { identity: "child", outputs: [], log_path: "/l" } + let document = work_outcome_wire(o: succeeded, subject: tree(hex: tree_a), op: work_default_build()) + let clean_child = ProvideFresh { outcome: succeeded, document: document, host_record: HostRecordWritten } + let attached_child = ProvideAttached { identity: "child", ending: "succeeded", document: document, host_record: HostRecordWritten } + let build_lost = HostRecordLost { detail: "the build's lease is still held" } + let carried_fresh = provide_result_with_host_record(r: clean_child, carried: build_lost) + let carried_attached = provide_result_with_host_record(r: attached_child, carried: build_lost) + let both_lost = host_record_join(a: build_lost, b: HostRecordLost { detail: "and the dependent lost its reading" }) + !host_record_was_written(h: provide_result_host_record(r: carried_fresh)) + && !host_record_was_written(h: provide_result_host_record(r: carried_attached)) + && provide_result_ending(r: carried_fresh) == "succeeded" + && provide_result_document(r: carried_fresh) == document + && provide_result_ending(r: carried_attached) == "succeeded" + && host_record_was_written(h: provide_result_host_record(r: clean_child)) + && string_contains(s: host_record_wire(h: both_lost), pattern: "still held") + && string_contains(s: host_record_wire(h: both_lost), pattern: "lost its reading") +} diff --git a/dag/test/claim/os_proc_meminfo_witness_test.dag b/dag/test/claim/os_proc_meminfo_witness_test.dag index eb6c7b69ebb..cee634e8adc 100644 --- a/dag/test/claim/os_proc_meminfo_witness_test.dag +++ b/dag/test/claim/os_proc_meminfo_witness_test.dag @@ -24,3 +24,89 @@ test fn proc_meminfo_witnesses() -> Bool { && measure_count(m: info.mem_available) <= measure_count(m: info.mem_total) && measure_count(m: metric.value) > 0 } + +// THE PARSE, AND THE TWO THINGS IT MUST NOT DO. A field the kernel did not publish may not read as +// a zero (a host with no MemAvailable line would otherwise present as a host with no memory +// available, and an admission would refuse forever for the wrong reason), and a line whose value is +// not a decimal count may not contribute a metric. Both are asserted against the same text with one +// line changed, so the assertion discriminates the parse rather than the fixture. +// +// TWO DIFFERENT NON-kB SHAPES, BECAUSE THEY ARE CAUGHT BY TWO DIFFERENT PARTS OF THE FOLD AND ONE +// OF THEM HAS NO OTHER WITNESS. A UNITLESS line (`HugePages_Total: 0`) is excluded by the arity +// requirement; a line with the WRONG unit (`SomeFutureField: 64 MB`) is excluded only by the unit +// COMPARISON, and nothing in /proc/meminfo authors that shape today -- so without the fixture the +// comparison would be a permanently green decoration (DESIGN 4b: ask whether the RED is authorable +// before writing the check, and a fixture is where it is authorable). Found by mutating the +// comparison away and watching this cell stay GREEN. +// +// THE UNITLESS LINE IS EXCLUDED, AND THE PREVIOUS REVISION OF THIS CELL ASSERTED THE OPPOSITE. It +// required count(all_metrics) == 8 against a fixture whose eighth line is `HugePages_Total: 0` -- +// so it pinned the defect it should have caught, which is the second time in this change a control +// of mine locked in the behaviour it existed to refuse (review 69784). A MemoryMetric carrying a +// page count is wrong by the huge page size and indistinguishable in the type from a real reading; +// the seven kB-denominated lines are admitted and the unitless one is not. +// +// EVERY FIELD CARRIES A DISTINCT VALUE AND EVERY FIELD IS ASSERTED, because with seven lookups +// written by hand a name paired with the WRONG field is the one defect the absence arms cannot +// catch. And a field missing from the MIDDLE of the file names itself: that arm used to be +// unreachable only by an invariant held between two lists, and is now unreachable by construction +// -- there is no fallback left that could answer 0 KiB for it (review 69561 on gunbc#11962). +test fn parsing_meminfo_reads_the_named_fields_and_refuses_a_missing_one() -> Bool { + let text = "MemTotal: 16777216 kB\nMemFree: 1048576 kB\nMemAvailable: 8388608 kB\nBuffers: 65536 kB\nCached: 4194304 kB\nSwapTotal: 2097152 kB\nSwapFree: 524288 kB\nHugePages_Total: 0\n" + let without_available = "MemTotal: 16777216 kB\nMemFree: 1048576 kB\nBuffers: 65536 kB\nCached: 4194304 kB\nSwapTotal: 0 kB\nSwapFree: 0 kB\n" + let unparseable = "MemTotal: 16777216 kB\nMemFree: 1048576 kB\nMemAvailable: not-a-number kB\nBuffers: 65536 kB\nCached: 4194304 kB\nSwapTotal: 0 kB\nSwapFree: 0 kB\n" + (match parse_proc_meminfo(text: text) { + MeminfoParsed { meminfo: m } => + kibibyte_count(k: m.mem_total) == 16777216 + && kibibyte_count(k: m.mem_free) == 1048576 + && kibibyte_count(k: m.mem_available) == 8388608 + && kibibyte_count(k: m.buffers) == 65536 + && kibibyte_count(k: m.cached) == 4194304 + && kibibyte_count(k: m.swap_total) == 2097152 + && kibibyte_count(k: m.swap_free) == 524288 + && count(m.all_metrics) == 7 + MeminfoFieldAbsent { field: _ } => false + }) + && (match parse_proc_meminfo(text: without_available) { + MeminfoFieldAbsent { field: f } => (f as String) == "MemAvailable" + MeminfoParsed { meminfo: _ } => false + }) + && (match parse_proc_meminfo(text: unparseable) { + MeminfoFieldAbsent { field: f } => (f as String) == "MemAvailable" + MeminfoParsed { meminfo: _ } => false + }) + && (match parse_proc_meminfo(text: "") { + MeminfoFieldAbsent { field: f } => (f as String) == "MemTotal" + MeminfoParsed { meminfo: _ } => false + }) + && (match parse_proc_meminfo(text: text) { + MeminfoParsed { meminfo: m } => + count(filter(m.all_metrics, x => (x.key as String) == "HugePages_Total")) == 0 + && count(filter(m.all_metrics, x => (x.key as String) == "SwapFree")) == 1 + MeminfoFieldAbsent { field: _ } => false + }) + && (match parse_proc_meminfo(text: join([ + "MemTotal: 16777216 kB\n", "MemFree: 1048576 kB\n", "MemAvailable: 8388608 kB\n", + "Buffers: 65536 kB\n", "Cached: 4194304 kB\n", "SwapTotal: 2097152 kB\n", + "SwapFree: 524288 kB\n", "SomeFutureField: 64 MB\n", + ], "")) { + MeminfoParsed { meminfo: m } => + count(m.all_metrics) == 7 && count(filter(m.all_metrics, x => (x.key as String) == "SomeFutureField")) == 0 + MeminfoFieldAbsent { field: _ } => false + }) + && (match parse_proc_meminfo(text: join([ + "MemTotal: 16777216 kB\n", "MemFree: 1048576 kB\n", "MemAvailable: 8388608 kB\n", + "Buffers: 65536 kB\n", "Cached: 4194304 kB\n", "SwapTotal: 2097152 kB\n", + "SwapFree: 524288\n", + ], "")) { + MeminfoFieldAbsent { field: f } => (f as String) == "SwapFree" + MeminfoParsed { meminfo: _ } => false + }) + && (match parse_proc_meminfo(text: join([ + "MemTotal: 16777216 kB\n", "MemFree: 1048576 kB\n", "MemAvailable: 8388608 kB\n", + "Buffers: 65536 kB\n", "Cached: 4194304 kB\n", "SwapFree: 524288 kB\n", + ], "")) { + MeminfoFieldAbsent { field: f } => (f as String) == "SwapTotal" + MeminfoParsed { meminfo: _ } => false + }) +} diff --git a/dag/test/claim/spark/pair_serving_d0_real_execution_witness_test.dag b/dag/test/claim/spark/pair_serving_d0_real_execution_witness_test.dag index 928326e3974..00aea13fd0c 100644 --- a/dag/test/claim/spark/pair_serving_d0_real_execution_witness_test.dag +++ b/dag/test/claim/spark/pair_serving_d0_real_execution_witness_test.dag @@ -3,7 +3,7 @@ module test.claim.spark.pair_serving_d0_real_execution import std.logic { Bool } import std.types { String, NonEmptyStr, FilePath, List, Int } import v2.std.optional { Present, Absent } -import std.measure { second } +import std.measure { second, measure_count, Measure } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import extdeps.shell import std.content_hash { ContentHash, Sha256Hash, sha256_hex_digest, compare_content_hash, ContentHashEqual, ContentHashDifferent, ContentHashCrossFamilyIncomparable, serialize_content_hash, content_hash_equal } @@ -383,14 +383,14 @@ test fn a_seat_granted_after_the_suspension_landed_is_released_by_real_execution AuthorityTransitionAppended { id: _, generation: g1, next: _ } => g1 == 1 _ => false }) - && (match fabric_seat_acquire(store: store, partition: partition, root: root, actor: "witness" as NonEmptyStr, request: SeatRequest { reference: "witness-seat-1" as NonEmptyStr, amount: 1, at: 1001, term_seconds: 300 }, policy: policy, attempts: 3, budget: 64) { + && (match fabric_seat_acquire(store: store, partition: partition, root: root, actor: "witness" as NonEmptyStr, request: SeatRequest { reference: "witness-seat-1" as NonEmptyStr, amount: Measure { count: 1 }, at: 1001, term_seconds: 300 }, policy: policy, attempts: 3, budget: 64) { SeatGranted { grant: g, generation: _, attempts_used: _ } => (match harness_seat_after_grant_authority(store: store, group: FabricGroupA, partition: partition, ceiling: ceiling, grant: g, now: 1001) { SeatReleasedAuthorityMoved { cause: _ } => true _ => false }) && (match fabric_seat_observe(store: store, partition: partition, root: root, at: 1002, budget: 64) { - SeatRoomObserved { headroom: room, generation: _ } => room == ceiling + SeatRoomObserved { headroom: room, generation: _ } => measure_count(room) == ceiling _ => false }) _ => false diff --git a/src/v2/workflow/local_repo_wet_terminal.dag b/src/v2/workflow/local_repo_wet_terminal.dag index 801f00984ae..c59f66e7174 100644 --- a/src/v2/workflow/local_repo_wet_terminal.dag +++ b/src/v2/workflow/local_repo_wet_terminal.dag @@ -244,6 +244,48 @@ fn local_repo_wet_requirement(candidate: String) -> WetEvidenceRequirement { // probe failed without output rather than running its payload. fn local_repo_wet_schedule() -> List { [ + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.host_capacity_wet_witness", function: "the_real_observation_reads_this_machine" }, + entry: "dag/test/claim/compute/host_capacity_wet_witness_test.dag", + function: "the_real_observation_reads_this_machine", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.host_capacity_wet_witness", function: "two_requests_summing_past_the_observed_headroom_cannot_both_admit" }, + entry: "dag/test/claim/compute/host_capacity_wet_witness_test.dag", + function: "two_requests_summing_past_the_observed_headroom_cannot_both_admit", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.host_capacity_wet_witness", function: "a_reused_reference_is_a_ledger_refusal_and_never_reported_as_a_full_pool" }, + entry: "dag/test/claim/compute/host_capacity_wet_witness_test.dag", + function: "a_reused_reference_is_a_ledger_refusal_and_never_reported_as_a_full_pool", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.host_capacity_wet_witness", function: "competing_reservations_cannot_over_reserve_and_a_release_returns_the_capacity" }, + entry: "dag/test/claim/compute/host_capacity_wet_witness_test.dag", + function: "competing_reservations_cannot_over_reserve_and_a_release_returns_the_capacity", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.host_capacity_wet_witness", function: "a_request_the_machine_cannot_back_refuses_below_the_live_floor" }, + entry: "dag/test/claim/compute/host_capacity_wet_witness_test.dag", + function: "a_request_the_machine_cannot_back_refuses_below_the_live_floor", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.host_capacity_wet_witness", function: "an_appropriation_larger_than_the_machine_refuses_rather_than_admitting" }, + entry: "dag/test/claim/compute/host_capacity_wet_witness_test.dag", + function: "an_appropriation_larger_than_the_machine_refuses_rather_than_admitting", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.compute.host_capacity_wet_witness", function: "two_instances_on_one_host_resolve_to_one_pool_at_one_root" }, + entry: "dag/test/claim/compute/host_capacity_wet_witness_test.dag", + function: "two_instances_on_one_host_resolve_to_one_pool_at_one_root", + expectation: ExpectedToHold {} + }, WetScheduledClaim { identity: WitnessIdentity { module_path: "test.claim.effect_plan_bash_materialize_real_execution_witness", function: "effect_plan_bash_two_declared_operations_execute" }, entry: "dag/test/claim/effect_plan_bash_materialize_real_execution_witness_test.dag",