Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
3e3b72c
Compute admission reserves observed host memory atomically, not a cou…
Sep 21, 2026
9bf00d7
The meminfo parse resolves each field by the lookup that proves it pr…
Sep 21, 2026
047bb3e
Three defects the first real run on srv1 found, and the controls for …
Sep 21, 2026
dd240f0
Body-position annotations refused by gunbc compile; move them to modu…
Sep 21, 2026
725d9c5
Four design defects: the double promise, the instance-keyed pool, the…
Sep 21, 2026
9172cf7
Quiescence is observed, obligations are per attempt, and the admissio…
Sep 21, 2026
5ee0cce
PR 1 rescoped to admission+pool: conservative release, declared disch…
Sep 21, 2026
773825c
The empty-ControlGroup release arm, the discarded host record, and tw…
Sep 21, 2026
73c570f
A completed wait never overrides a live cgroup; an uncertain completi…
Sep 21, 2026
1248df9
The bound termination policy is a fold a control can read, not a sent…
Sep 21, 2026
f5344b2
Merge remote-tracking branch 'origin/main' into session/bold-lynx-559
Sep 21, 2026
c901fc0
The release predicate is exactly four cases; a lost record reaches a …
Sep 21, 2026
1c670b8
The receipt stays parseable: the host-record fact gets its own file b…
Sep 21, 2026
bf58075
SeatRequest carries its dimension; the strip moves to where the pool …
Sep 21, 2026
afb46eb
The attached arm carried the loss it had just built into a discard
Sep 21, 2026
2700b01
File the partition-identity class the PoolAcquired argument would hav…
Sep 21, 2026
d5fc09b
WIP: unit peak producer, typed grant-exceeded ending, per-class grant…
Sep 21, 2026
f054978
Record the peak-route decision: display contract chosen on the tradeo…
Sep 21, 2026
72b8100
Merge main (#11962 landed) into the grants branch
Sep 22, 2026
4659691
Review 69829: one authority for the exceedance path, class-grain zero…
Sep 22, 2026
6a53f39
Bind the peak reader to an invocation that can print a peak, and name…
Sep 22, 2026
c88e690
An absence carries its cause, so three absence claims can no longer p…
Sep 22, 2026
030d9b6
One claim per absence cause, so a red names which cause collapsed
Sep 22, 2026
023912f
Roster the class, and correct two mint annotations that still claimed…
Sep 22, 2026
59b9772
A rung demotion has a population, not a site -- filed on the row that…
Sep 22, 2026
2079465
The summary format is version-keyed, so an unread major refuses inste…
Sep 22, 2026
7cf660c
The refusal names its own remedy, and a claim proves it reaches the c…
Sep 22, 2026
511b20b
Name the base case of the grounding recursion as the base case
Sep 22, 2026
a8809fa
Annotations at module-item grain: the floor's parse phase is a gate m…
Sep 22, 2026
920f7a5
Two blocking defects: an unclassifiable ending is not a failure, and …
Sep 22, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
383 changes: 381 additions & 2 deletions dag/extdeps/systemd/systemd_run.dag

Large diffs are not rendered by default.

24 changes: 14 additions & 10 deletions dag/gunbc/compute/host_capacity.dag
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,7 @@ fn compute_memory_partition(host: NonEmptyStr) -> 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 {
fn compute_capacity_subject(instance: HostDashboardInstance, request: Kibibyte) -> ComputeSubjectResolution {
match dashboard_instance_for_host(host: instance.host_identity as String) {
DashboardInstanceHostUnknown { host: h } => ComputeSubjectHostUnresolved { host: h as NonEmptyStr }
DashboardInstanceForHost { instance: host_instance } =>
Expand All @@ -114,7 +114,7 @@ fn compute_capacity_subject(instance: HostDashboardInstance) -> ComputeSubjectRe
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),
request: request,
},
}
}
Expand Down Expand Up @@ -182,11 +182,13 @@ fn compute_memory_appropriation(instance: HostDashboardInstance) -> Kibibyte {
// 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 {
// THE CEILING IS WHAT A CLASS RESERVES WHEN IT HAS NO GRANT, and it is no longer what every request
// reserves. The per-work-class amount (a claims run does not need a release build's ceiling) is
// gunbc.compute.work_class_grant work_class_grant, which resolves to THIS figure for any class
// without enough samples on the provider's own route -- the fail-closed arm, which over-reserves
// and never under-reserves. A request's amount is therefore supplied to compute_reserve rather than
// read here; this function only names the ceiling the grant falls back to and never exceeds.
fn compute_memory_ceiling(instance: HostDashboardInstance) -> Kibibyte {
kibibyte_from_byte_size_floor(b: instance.dispatch_worker_memory_max)
}

Expand Down Expand Up @@ -270,8 +272,8 @@ 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) {
fn compute_reserve(instance: HostDashboardInstance, reference: NonEmptyStr, term_seconds: Nat, request: Kibibyte) -> ComputeReservation {
match compute_capacity_subject(instance: instance, request: request) {
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)
Expand Down Expand Up @@ -443,8 +445,10 @@ type ComputeCapacityStanding
= ComputeCapacityStandingRead { committed: Kibibyte, ceiling: Kibibyte, headroom: Kibibyte, observed_available: Kibibyte, observed_total: Kibibyte }
| ComputeCapacityStandingUnread { detail: String }

// THE STANDING IS A FACT ABOUT THE POOL, NOT ABOUT ANY REQUEST, so it reads the subject at the
// ceiling: no field of the standing fold consults the subject's request.
fn compute_capacity_standing(instance: HostDashboardInstance) -> ComputeCapacityStanding {
match compute_capacity_subject(instance: instance) {
match compute_capacity_subject(instance: instance, request: compute_memory_ceiling(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)
}
Expand Down
225 changes: 225 additions & 0 deletions dag/gunbc/compute/work_class_grant.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,225 @@
module gunbc.compute.work_class_grant

import std.types { String, Bool, Int, List, NonEmptyStr, EpochSecs }
import std.nat { Nat }
import std.measure { Kibibyte, kibibyte, kibibyte_count, byte_size_count }
import gunbc.compute.work_request { WorkOperation, BuildGunbcBinaries, CompileEntry, RunClaims, CargoProfile, cargo_profile_wire, work_operation_canonical }
import extdeps.systemd.systemd_run {
SystemdRunWaitSummary, SystemdMemoryPeakReading, MemoryPeakRead, MemoryPeakUnparseable, MemoryPeakNotReported, systemd_formatted_bytes_upper,
MemoryPeakFormatNotGrounded, summary_format_standing_wire,
SummaryAbsence, summary_absence_wire,
}

// A WORK REQUEST RESERVES AN AMOUNT PER CLASS, AND THE AMOUNT IS A GRANT WITH ITS OBSERVATIONS
// ATTACHED (operator ruling 2026-09-21: do not raise a global ceiling; size a job's reservation per
// class from that class's measured peak, admitted against observed host memory).
//
// THE GRANT IS ALSO THE CAP. gunbc.compute.host_capacity makes the reserved amount and the unit's
// MemoryMax one figure, so a grant sized at a measured peak would also KILL the first run that
// exceeds it. A peak is a SAMPLE, not a bound. That is why a grant is peak plus headroom, why the
// headroom is a named policy budget rather than a picked multiplier, and why exceeding a grant is a
// typed, counted ending (gunbc.compute.work_provider_local compute_grant_exceeded_record) rather
// than an OOM that renders as the work having failed.
//
// WHAT THIS CHANGE DOES AND DOES NOT DELIVER. It builds the producer (the unit's peak, read from
// the launcher's own summary), the typed ending, the per-class counter and this resolution. It
// ships NO grant rows: no class has a peak measured on the provider's own route yet, so every class
// resolves to the ceiling and no reserved amount moves. The relief is the next change, the one that
// adds rows from the samples this one starts recording.

// THE CLASS GRAIN IS A CLAIM, STATED SO IT CAN BE WRONG. A class is the operation kind, split by
// cargo profile for builds. A compile's peak depends heavily on WHICH entry it compiles (the
// v2.compiler.compile closure is far above a single witness module), so two compiles of one class
// can differ by an order of magnitude. A grant over that grain is sampled, not derived, which is
// exactly the residual gunbc.recurring_failure_mode a_sampled_grant_is_discovered_below_worst_case
// rosters -- and the counted GrantExceeded ending is what reports a class whose grain is too coarse.
type WorkClass
= WorkClassBuild { profile: CargoProfile }
| WorkClassCompile
| WorkClassClaims

fn work_class_of(op: WorkOperation) -> WorkClass {
match op {
BuildGunbcBinaries { profile, bins: _ } => WorkClassBuild { profile: profile }
CompileEntry { entry: _ } => WorkClassCompile
RunClaims { entry: _, functions: _, hermetic: _ } => WorkClassClaims
}
}

fn work_class_wire(c: WorkClass) -> String {
match c {
WorkClassBuild { profile } => join(["build-", cargo_profile_wire(p: profile)], "")
WorkClassCompile => "compile"
WorkClassClaims => "claims"
}
}

// ONE SAMPLE: one attempt of one work identity on one host, and the UPPER BOUND of the peak the
// unit's manager reported (extdeps.systemd.systemd_run systemd_formatted_bytes_upper -- the printed
// figure is truncated, so its lower reading would size a grant below the peak that produced it).
// The operation's canonical text says what ran, so "over what" is carried, not remembered.
type WorkClassPeakSample {
work_identity: NonEmptyStr
operation: NonEmptyStr
host: NonEmptyStr
observed_at: EpochSecs
peak_upper: Kibibyte
}

// THE SAMPLE PRODUCER: the launcher's summary to a typed sample (review 69829 -- the upper bound was
// computed and then written only as prose). The byte upper bound is rounded UP to kibibytes, the
// direction a capacity reading may round. A summary with no peak, an unparseable peak or an
// unreadable clock takes NO sample and says which; it never takes a zero.
fn work_class_summary_peak_upper(summary: SystemdRunWaitSummary) -> Kibibyte? {
match summary.memory_peak {
MemoryPeakRead { peak: b } => Present { value: kibibyte(count: (byte_size_count(b: systemd_formatted_bytes_upper(b: b)) + 1023) / 1024) }
MemoryPeakUnparseable { text: _ } => none
MemoryPeakNotReported { absence: _ } => none
MemoryPeakFormatNotGrounded { standing: _ } => none
}
}

type WorkClassPeakSampleReading
= PeakSampleTaken { class: WorkClass, sample: WorkClassPeakSample }
| PeakSampleNotTaken { reason: String }

fn work_class_peak_sample(summary: SystemdRunWaitSummary, work_identity: String, op: WorkOperation, host: String, observed_at: EpochSecs?) -> WorkClassPeakSampleReading {
match work_class_summary_peak_upper(summary: summary) {
Absent => PeakSampleNotTaken { reason: match summary.memory_peak {
MemoryPeakUnparseable { text } => join(["the Memory peak line did not parse: ", text], "")
MemoryPeakNotReported { absence } => summary_absence_wire(a: absence)
MemoryPeakFormatNotGrounded { standing } => summary_format_standing_wire(s: standing)
MemoryPeakRead { peak: _ } => "the peak was read but produced no upper bound"
} }
Present { value: upper } =>
match observed_at {
Absent => PeakSampleNotTaken { reason: "the clock could not be read as epoch seconds" }
Present { value: at } =>
if work_identity == "" || host == "" {
PeakSampleNotTaken { reason: "the attempt carries no work identity or host" }
} else {
PeakSampleTaken { class: work_class_of(op: op), sample: WorkClassPeakSample {
work_identity: work_identity as NonEmptyStr,
operation: work_operation_canonical(op: op) as NonEmptyStr,
host: host as NonEmptyStr,
observed_at: at,
peak_upper: upper,
} }
}
}
}
}

fn work_class_peak_sample_wire(r: WorkClassPeakSampleReading) -> String {
match r {
PeakSampleTaken { class, sample } =>
join(["class=", work_class_wire(c: class), " identity=", sample.work_identity as String, " host=", sample.host as String,
" observed_at=", to_string(value: sample.observed_at), " peak_upper_kib=", to_string(value: kibibyte_count(k: sample.peak_upper)),
" operation=", sample.operation as String], "")
PeakSampleNotTaken { reason } => join(["NOT TAKEN (", reason, ")"], "")
}
}

// THE ROW: a policy budget grounded in observations. The headroom is the OPERATOR'S figure and is
// cited as such; what makes it admissible (DESIGN 5) is that it is FALSIFIABLE -- a non-zero
// GrantExceeded count for this class (compute_grant_exceeded_count) means the grant is wrong and
// the row is re-derived. A budget nobody can prove wrong is a guess; this one carries its counter.
type WorkClassGrantRow {
class: WorkClass
samples: List<WorkClassPeakSample>
headroom: Kibibyte
headroom_authority: NonEmptyStr
}

// ONE OBSERVATION IS NOT A PEAK (operator ruling, 2026-09-21), so the smallest sample set a grant
// may be sized from is two. Below that the class reserves the ceiling and says how many it has.
data work_class_minimum_samples: Int = 2

// THE ROWS. Empty in this change, deliberately and not as a placeholder: a row lands with samples
// taken on the provider's route (the per-attempt record compute_run_and_settle writes), and none
// exist yet. neat-boar-16's 9.7 GB peak for the v2.compiler.compile closure is a real observation
// but was not taken under a provider unit, so it is cited in the next change's evidence and does
// not size a row here.
data work_class_grant_rows: List<WorkClassGrantRow> = []

type WorkClassCeilingReason
= ClassUnmeasured
| ClassTooFewSamples { samples: Int }
| ClassRowsAmbiguous { rows: Int }
| ClassRetryAfterGrantExceeded { exceeded: Kibibyte }
| ClassSizedAtOrAboveCeiling { samples: Int, sized: Kibibyte }

// EVERY ARM NAMES ITS CLASS AND ITS EVIDENCE COUNT. The ceiling arm is the fail-closed one and it
// is the only arm this change's rows reach; it must stay reachable, so "no row" and "too few
// samples" are both ceiling, never a default amount.
type WorkClassGrant
= GrantAtCeiling { class: WorkClass, amount: Kibibyte, reason: WorkClassCeilingReason }
| GrantSized { class: WorkClass, amount: Kibibyte, samples: Int, peak_upper: Kibibyte, headroom: Kibibyte, headroom_authority: NonEmptyStr }

fn work_class_grant_amount(g: WorkClassGrant) -> Kibibyte {
match g {
GrantAtCeiling { class: _, amount, reason: _ } => amount
GrantSized { class: _, amount, samples: _, peak_upper: _, headroom: _, headroom_authority: _ } => amount
}
}

fn work_class_grant_is_ceiling(g: WorkClassGrant) -> Bool {
match g {
GrantAtCeiling { class: _, amount: _, reason: _ } => true
GrantSized { class: _, amount: _, samples: _, peak_upper: _, headroom: _, headroom_authority: _ } => false
}
}

fn work_class_grant_wire(g: WorkClassGrant) -> String {
match g {
GrantAtCeiling { class, amount, reason } =>
join(["class ", work_class_wire(c: class), " reserves the ceiling ", to_string(value: kibibyte_count(k: amount)), " KiB (",
match reason {
ClassUnmeasured => "no grant row"
ClassTooFewSamples { samples } => join([to_string(value: samples), " sample(s), fewer than ", to_string(value: work_class_minimum_samples)], "")
ClassRetryAfterGrantExceeded { exceeded } => join(["this attempt's grant of ", to_string(value: kibibyte_count(k: exceeded)), " KiB was exceeded, so it is retried at the ceiling"], "")
ClassRowsAmbiguous { rows } => join([to_string(value: rows), " grant rows name this class, so none of them decides"], "")
ClassSizedAtOrAboveCeiling { samples, sized } => join(["sized ", to_string(value: kibibyte_count(k: sized)), " KiB from ", to_string(value: samples), " samples, not below the ceiling"], "")
}, ")"], "")
GrantSized { class, amount, samples, peak_upper, headroom, headroom_authority } =>
join(["class ", work_class_wire(c: class), " reserves ", to_string(value: kibibyte_count(k: amount)), " KiB = peak ",
to_string(value: kibibyte_count(k: peak_upper)), " KiB over ", to_string(value: samples), " samples + headroom ",
to_string(value: kibibyte_count(k: headroom)), " KiB (", headroom_authority as String, ")"], "")
}
}

fn work_class_rows_for(rows: List<WorkClassGrantRow>, class: WorkClass) -> List<WorkClassGrantRow> {
filter(rows, r => work_class_wire(c: r.class) == work_class_wire(c: class))
}

fn work_class_samples_peak(samples: List<WorkClassPeakSample>) -> Nat {
fold(samples, init: kibibyte_count(k: kibibyte(count: 0)), f: (acc, s) => if kibibyte_count(k: s.peak_upper) > acc { kibibyte_count(k: s.peak_upper) } else { acc })
}

// THE RESOLUTION, taking the rows and the ceiling as values so every arm is exercisable with a
// supplied row while production passes work_class_grant_rows. A class with more than one row is
// refused to the ceiling rather than resolved by position: two rows for one class are two
// authorities for one fact, and picking one would be the silent choice DESIGN 3 forbids.
fn work_class_grant(class: WorkClass, rows: List<WorkClassGrantRow>, ceiling: Kibibyte) -> WorkClassGrant {
match work_class_rows_for(rows: rows, class: class) {
Empty {} => GrantAtCeiling { class: class, amount: ceiling, reason: ClassUnmeasured }
Cons { head: row, tail: more } =>
match more {
Cons { head: _, tail: _ } => GrantAtCeiling { class: class, amount: ceiling, reason: ClassRowsAmbiguous { rows: length(work_class_rows_for(rows: rows, class: class)) } }
Empty {} => {
let n = length(row.samples)
if n < work_class_minimum_samples {
GrantAtCeiling { class: class, amount: ceiling, reason: ClassTooFewSamples { samples: n } }
} else {
let peak = work_class_samples_peak(samples: row.samples)
let sized = kibibyte(count: peak + kibibyte_count(k: row.headroom))
if kibibyte_count(k: sized) >= kibibyte_count(k: ceiling) {
GrantAtCeiling { class: class, amount: ceiling, reason: ClassSizedAtOrAboveCeiling { samples: n, sized: sized } }
} else {
GrantSized { class: class, amount: sized, samples: n, peak_upper: kibibyte(count: peak), headroom: row.headroom, headroom_authority: row.headroom_authority }
}
}
}
}
}
}
Loading