Skip to content
Closed
268 changes: 268 additions & 0 deletions dag/gunbc/floor_memory_demand.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,268 @@
module gunbc.floor_memory_demand

import std.types { Bool, Int, NonEmptyStr, String }
import std.nat { Nat }
import std.measure { ByteSize, byte_size, byte_size_count }
import std.checked_arithmetic { nat_magnitude }
import extdeps.linux.cgroup_v2_memory {
CgroupMemoryLimitValue,
CgroupMemoryLimited,
CgroupMemoryUnlimited,
CgroupMemoryLimitUnparseable,
parse_cgroup_memory_limit,
}

// WHAT THIS MODULE IS FOR, AND WHY IT IS NOT A SECOND HOME FOR A NUMBER.
//
// A peak RSS or cgroup charge read from a run that was HELD measures what the process was
// ALLOWED, not what it needs. `gunbc.runner_slot_allocation` states the reading directly -- a
// peak equal to the throttle line is "the censored lower bound ... the workload being held, not
// the workload being measured" -- and then, on 2026-09-12, recorded two disagreeing figures for
// one run and said in as many words that it did not know which cgroup level each named.
//
// This module makes that ambiguity unwritable rather than re-describing it. A demand figure may
// not travel without its standing: whether anything held the workload, and whether the number is
// a demand or a floor under one. THE JUDGMENT IS DERIVED FROM THE KERNEL'S OWN COUNTERS, never
// authored beside them.
//
// SUBJECT: the measured PROCESS (or its declared process subtree), not any function inside it.
// That distinction is load-bearing and is why the reading is taken by a SUPERVISOR from outside.
// An in-process observer -- a Drop guard, an exit hook, a final log line -- covers ordinary
// returns and unwinding panics and NOTHING ELSE. It does not run on `panic = abort`, on
// `process::abort`, on `process::exit`, or on SIGKILL, and Rust's allocation-error handler
// normally ABORTS rather than unwinds. So allocation failure and the OOM kill -- the two
// terminations a memory instrument most exists to report -- are exactly the ones no in-process
// observer can report on. The kernel maintains `memory.peak` and `memory.events` regardless, and
// a supervisor that outlived the child can still read them, so the supervisor's post-mortem read
// is the load-bearing evidence and any in-process emission is a convenience beside it.

// HOW THE MEASURED PROCESS ENDED, observed by the supervisor from OUTSIDE it (a wait status, or
// the service manager's own record). This is an INDEPENDENT AXIS from whether the reading was
// censored: a run can terminate cleanly and still have been throttled the whole way, and a run
// can be killed without ever having been throttled. Folding them into one enum would lose
// exactly the pair of facts the operator needs to tell "it fits" from "it was held".
// THE THIRD ARM IS REACHED BY THE WITNESS AND NOT BY TODAY'S PRODUCER, WHICH IS STATED RATHER THAN
// hidden: the supervisor waits on its own child, so a lost termination currently refuses the whole
// invocation before any qualification is built. The arm is kept because the fail-closed reading it
// encodes -- not knowing how a process ended is NOT evidence that it ended well -- is a property of
// the judgment rather than of one producer, and a supervisor that ever reports a termination it
// could not observe (an adopted child, a detached run, a receipt read from elsewhere) must land
// here rather than be silently read as a clean exit. Its discriminating red is
// `an_unobserved_termination_is_not_a_demand_holds`.
type SupervisedTermination
= TerminationExited { code: Int }
| TerminationSignalled { signal: Int }
| TerminationUnobserved { cause: NonEmptyStr }

// The cumulative counters from `memory.events`, read AFTER the child is gone. `oom_kills` is the
// kernel's own statement that it killed something in this cgroup; it is not inferred from the
// wait status, because the two can disagree and the disagreement is informative.
type CgroupMemoryEvents {
high_events: Nat,
max_events: Nat,
oom_kills: Nat,
}

// THIS IS THE JUDGMENT'S OWN REFUSAL VOCABULARY, AND ITS SCOPE IS DELIBERATELY NARROW.
//
// An earlier revision of this type listed four arms -- an absent directory, an unreadable file, an
// unparseable value, and a supervisor that did not own the cgroup -- as though it were the roster
// of every way a qualification can fail. It is not, and pretending otherwise forked the vocabulary
// in both directions at once: three of those arms had no constructor anywhere (a check whose
// forbidden state cannot be expressed is a decoration, DESIGN section 4b), while the producer
// carried five real causes -- no cgroup with a readable peak, child not spawned, child not waited,
// measurement cgroup shared, peak dominated by prior history -- that this type had never heard of.
// Every refusal the instrument actually emits came from the set this module did not model.
//
// THE TWO POPULATIONS ARE DIFFERENT SUBJECTS AND NOW SAY SO. A supervisor's refusals happen BEFORE
// there is anything to judge: no cgroup, no child, no attributable counter. They never produce a
// qualification at all -- they terminate the invocation with no observation. What reaches THIS
// fold is a complete set of readings, so the only way it can refuse is that a reading it was
// handed cannot be interpreted. One arm, because there is exactly one such way.
//
// The consequence worth stating: a caller may NOT read `DemandUnreadable` as "every possible
// failure is covered here". It covers the judgment's own domain, and the supervisor's refusals are
// a separate, earlier population that this module deliberately does not enumerate -- modelling
// them here would put the producer's vocabulary in a second home (DESIGN section 3).
type DemandReadRefusalCause
= CgroupValueUnparseable { file: NonEmptyStr, body: String }

// THE THREE ARMS AN OPERATOR READS, and they are three because two of the pairings are the ones
// that have actually caused harm here.
//
// `DemandObserved` is the only arm whose peak may be cited as a DEMAND. `DemandBounded` carries a
// peak that is a LOWER BOUND on demand -- the workload wanted at least this much and we cannot say
// how much more -- and it covers both ways that happens, because the consequence for a consumer is
// identical: the number may not be used to size anything downward. Which way it happened is
// carried in the fields rather than in a fourth arm, so a consumer asking "may I treat this as a
// demand?" gets a two-valued answer and a consumer asking "why not?" still gets the cause.
//
// `DemandUnreadable` is separate from both and must never render like either.
//
// WHAT `DemandObserved` DOES NOT SAY, because the gap is easy to cross by accident: it says
// NOTHING HELD THE MEMORY. It does not say the workload was COMPLETE. A run that refused half its
// witnesses and exited early was not throttled, so it qualifies here, and its peak is still a
// truthful statement about what that run demanded -- but it is not a statement about what a
// complete run would demand. Workload completeness is the caller's subject and is carried by the
// caller's own verdict, never inferred from this one.
type FloorMemoryQualification
= DemandObserved {
peak: ByteSize,
limit_max: CgroupMemoryLimitValue,
limit_high: CgroupMemoryLimitValue,
events: CgroupMemoryEvents,
termination: SupervisedTermination,
}
| DemandBounded {
peak_lower_bound: ByteSize,
limit_max: CgroupMemoryLimitValue,
limit_high: CgroupMemoryLimitValue,
events: CgroupMemoryEvents,
termination: SupervisedTermination,
}
| DemandUnreadable { cause: DemandReadRefusalCause }

// A LIMIT THAT IS ABSENT CANNOT HOLD ANYTHING, and an unparseable one cannot be reasoned about at
// all. `CgroupMemoryUnlimited` is the `high=max` case that makes an uncensored measurement
// possible in the first place, so it must read as "this line did not bind" rather than as a very
// large number.
fn peak_reached_limit(peak: ByteSize, limit: CgroupMemoryLimitValue) -> Bool {
match limit {
CgroupMemoryLimited { bytes: b } => byte_size_count(b: peak) >= byte_size_count(b: b)
CgroupMemoryUnlimited => false
CgroupMemoryLimitUnparseable { body: _ } => false
}
}

fn any_events(events: CgroupMemoryEvents) -> Bool {
events.high_events > 0 || events.max_events > 0 || events.oom_kills > 0
}

// A TERMINATION THAT WAS NOT AN ORDINARY EXIT WITHHELD THE REST OF THE WORKLOAD, so whatever the
// peak reached, the process had not finished wanting memory. An UNOBSERVED termination counts the
// same way and deliberately so: not knowing how a process ended is not evidence that it ended
// well, and the fail-closed reading of an unobserved end is that the figure is a lower bound.
fn termination_withheld_completion(termination: SupervisedTermination) -> Bool {
match termination {
TerminationExited { code: _ } => false
TerminationSignalled { signal: _ } => true
TerminationUnobserved { cause: _ } => true
}
}

// THE JUDGMENT. Every input is a kernel counter or a wait status; nothing here is authored.
//
// The order of the tests is the order of severity, and each one independently establishes that the
// peak is a lower bound rather than a demand:
// a kill -- the workload was stopped before it finished wanting memory;
// an event -- reclaim or the OOM killer acted, so the workload was held below what it asked for;
// a pin -- the peak sits AT a limit, which is the censored signature even when the counters
// have not yet ticked, and is what a throttled run looks like from the outside.
// Only a run that survived all three may be read as a demand.
fn qualify_floor_memory_demand(
peak: ByteSize,
limit_max: CgroupMemoryLimitValue,
limit_high: CgroupMemoryLimitValue,
events: CgroupMemoryEvents,
termination: SupervisedTermination,
) -> FloorMemoryQualification {
let killed = termination_withheld_completion(termination: termination)
let pinned =
peak_reached_limit(peak: peak, limit: limit_high)
|| peak_reached_limit(peak: peak, limit: limit_max)
if killed || any_events(events: events) || pinned {
DemandBounded {
peak_lower_bound: peak,
limit_max: limit_max,
limit_high: limit_high,
events: events,
termination: termination,
}
} else {
DemandObserved {
peak: peak,
limit_max: limit_max,
limit_high: limit_high,
events: events,
termination: termination,
}
}
}

// THE ONE QUESTION A SIZING CONSUMER MAY ASK, so that no consumer re-derives the judgment and
// gets a different answer (DESIGN section 3). A bounded or unreadable qualification is never a
// demand; only `DemandObserved` is.
fn qualification_is_a_demand(q: FloorMemoryQualification) -> Bool {
match q {
DemandObserved { peak: _, limit_max: _, limit_high: _, events: _, termination: _ } => true
DemandBounded { peak_lower_bound: _, limit_max: _, limit_high: _, events: _, termination: _ } => false
DemandUnreadable { cause: _ } => false
}
}

// THE HOST'S ENTRY POINT, TAKING ONLY PRIMITIVES.
//
// The supervisor reads bytes off `/sys/fs/cgroup` and knows nothing about what they mean; every
// interpretation — what "max" denotes, whether a negative body is a magnitude or a malformed
// read, and which combination makes a peak a lower bound — happens HERE, over the upstream
// authority's own parsers. A host that constructed `CgroupMemoryLimitValue` itself would be a
// second parser for a file `extdeps.linux.cgroup_v2_memory` already owns (DESIGN section 3).
//
// A NEGATIVE COUNT IS A MALFORMED READ, NOT A MAGNITUDE. `memory.peak` and the `memory.events`
// fields are documented as non-negative, so a leading minus means the read is wrong, and taking
// its absolute value would fabricate a plausible number from a broken one.
// 🟡 DISSOLVE-ON, AND THE ROW IS ANSWERED RATHER THAN WAVED THROUGH. The mechanical unit scan
// flags `peak_bytes: Int` below as a flat-scalar unit field, and two reviewers have now split on
// it -- review 68906 refuted it as a correct host-to-substrate primitive boundary, review 68936
// echoed it as unrefuted-by-the-diff. Both readings are fair, so the row gets a gate rather than
// an argument.
//
// WHY THE PARAMETER IS A PRIMITIVE TODAY: this is the seam where the seed hands bytes it read off
// /sys/fs/cgroup to the substrate, and the interpreter passes them as `Value::Int`. There is no
// `ByteSize` on the Rust side to pass -- constructing one would mean the HOST minting a
// `std.measure` carrier, which is the measure vocabulary living in a second home. The scalar does
// not propagate: it is lifted on the very next hop (`byte_size(count: nat_magnitude(...))`) and
// every field it reaches -- `DemandObserved.peak`, `DemandBounded.peak_lower_bound` -- is
// `ByteSize`. Nothing downstream of this function sees an `Int` byte count.
//
// DISSOLVES WHEN the host can hand a `std.measure` value across the boundary directly -- that is,
// when the interpreter's argument surface admits a constructed `ByteSize` rather than only
// primitives, so the lift happens at the reader that already knows the unit instead of one hop
// inside. At that point this signature takes `ByteSize`, `nat_magnitude` disappears from it, and
// the negative-count arm below moves to the reader. It is NOT dissolved by wrapping the literal at
// the call site in Rust, which would relocate the same primitive one frame outward.
fn qualify_floor_memory_from_readings(
peak_bytes: Int,
limit_max_body: String,
limit_high_body: String,
high_events: Int,
max_events: Int,
oom_kills: Int,
terminated_by_signal: Bool,
exit_code: Int,
) -> FloorMemoryQualification {
if peak_bytes < 0 || high_events < 0 || max_events < 0 || oom_kills < 0 {
DemandUnreadable {
cause: CgroupValueUnparseable {
file: "memory.peak/memory.events" as NonEmptyStr,
body: "a negative count: the kernel documents these as non-negative, so this read is malformed rather than small",
},
}
} else {
qualify_floor_memory_demand(
peak: byte_size(count: nat_magnitude(a: peak_bytes)),
limit_max: parse_cgroup_memory_limit(body: limit_max_body),
limit_high: parse_cgroup_memory_limit(body: limit_high_body),
events: CgroupMemoryEvents {
high_events: nat_magnitude(a: high_events),
max_events: nat_magnitude(a: max_events),
oom_kills: nat_magnitude(a: oom_kills),
},
termination: if terminated_by_signal {
TerminationSignalled { signal: exit_code }
} else {
TerminationExited { code: exit_code }
},
)
}
}
37 changes: 35 additions & 2 deletions dag/gunbc/instrument_targets.dag
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ import gunbc.target_binding {
BehavioralReceiptPlanProducer, BehavioralReceiptCensusProducer,
BehavioralReceiptSelftestProducer,
HeadsReadingDifferentialProducer,
FloorMemoryQualificationProducer,
CompileCleanDiagnosticCensusProducer,
EvaluationStoreAddressExactHeadProducer,
CompileCleanDiagnosticCensusStanding,
Expand Down Expand Up @@ -77,6 +78,17 @@ fn heads_reading_differential_label() -> Label {
}
}

// THE FLOOR'S MEMORY DEMAND, QUALIFIED. The subject is the required-floor PROCESS -- not any
// function inside it -- which is why the reading is taken by a supervisor from outside rather than
// by anything the floor itself emits. See `gunbc.floor_memory_demand` for why an in-process
// observer cannot report the two terminations that matter most.
fn floor_memory_qualification_label() -> Label {
Label {
package: instruments_package()
target: TargetName { name: "floor-memory-qualification" }
}
}

fn behavioral_receipt_plan_label() -> Label {
Label { package: instruments_package() target: TargetName { name: "behavioral-receipt-plan" } }
}
Expand Down Expand Up @@ -189,6 +201,18 @@ fn heads_reading_differential_target() -> BuildTarget {
}
}

// A `*_target()` HERE IS NOT NECESSARILY CONSUMED, AND ADDING ONE BY REFLEX IS THE TRAP. The two
// folds below are the live consumers: `instrument_targets()` folds LABELS and
// `instrument_bindings()` folds BINDINGS. NEITHER READS A `BuildTarget`, so a `*_target()` earns
// its place only if some other module reads it -- `self_host_target` does, and several siblings do
// not. That residue is a DESIGN section 3c dangling set, recorded rather than resolved because
// resolving it is a separate change.
//
// The population is deliberately NOT enumerated here: a hand-written list of which ones dangle
// goes stale the moment someone adds an instrument, which is the same positional-citation decay
// section 3 forbids. Check it instead -- a `*_target()` whose only occurrence in `dag/` is its own
// definition line has no consumer. The floor-memory row adds no `*_target()` for exactly this
// reason.
fn instrument_test_target(label: Label) -> BuildTarget {
BuildTarget { label: label kind: TestRule {} dependencies: [] }
}
Expand Down Expand Up @@ -284,6 +308,13 @@ fn primitive_egress_census_dag_binding() -> TargetBinding {
TargetBinding { target: primitive_egress_census_dag_label() producer: PrimitiveEgressCensusDagProducer {} }
}

fn floor_memory_qualification_binding() -> TargetBinding {
TargetBinding {
target: floor_memory_qualification_label()
producer: FloorMemoryQualificationProducer {}
}
}

fn primitive_egress_census_seed_binding() -> TargetBinding {
TargetBinding { target: primitive_egress_census_seed_label() producer: PrimitiveEgressCensusSeedProducer {} }
}
Expand Down Expand Up @@ -350,7 +381,8 @@ fn instrument_targets() -> List<Label> {
behavioral_receipt_census_label(), behavioral_receipt_selftest_label(),
compile_clean_diagnostic_census_label(), self_host_label(), v2_native_cli_label(),
evaluation_store_address_exact_head_label(), primitive_egress_census_label(),
primitive_egress_census_v2_label(), primitive_egress_census_dag_label(), primitive_egress_census_seed_label()
primitive_egress_census_v2_label(), primitive_egress_census_dag_label(),
primitive_egress_census_seed_label(), floor_memory_qualification_label()
]
}

Expand All @@ -360,7 +392,8 @@ fn instrument_bindings() -> List<TargetBinding> {
behavioral_receipt_census_binding(), behavioral_receipt_selftest_binding(),
compile_clean_diagnostic_census_binding(), self_host_binding(), v2_native_cli_binding(),
evaluation_store_address_exact_head_binding(), primitive_egress_census_binding(),
primitive_egress_census_v2_binding(), primitive_egress_census_dag_binding(), primitive_egress_census_seed_binding()
primitive_egress_census_v2_binding(), primitive_egress_census_dag_binding(),
primitive_egress_census_seed_binding(), floor_memory_qualification_binding()
]
}

Expand Down
Loading