Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
2 changes: 1 addition & 1 deletion dag/gunbc/actions_run_binding.dag
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ import gunbc.running_release_identity { release_revision_text_valid }
// downstream join compares bindings rather than trusting a workflow input. The expected revision is
// an INDEPENDENT input (RLM_EXPECTED_REVISION, a workflow_dispatch input the operator types), so
// `run_revision == expected` is a comparison of two origins and can fail; deriving both from the
// checkout would compare git to itself (gunbc.live_rust_observation live_rust_observation_note).
// checkout would compare git to itself (gunbc.live_rust_observation LiveRustObservationRequest).
// Every absence is its own typed arm: outside Actions the variables are legitimately unset, and a
// run must refuse to mint a receipt it cannot bind rather than mint one bound to nothing.
type ActionsRunBinding {
Expand Down
4 changes: 2 additions & 2 deletions dag/gunbc/host/memory_stall_refusal.dag
Original file line number Diff line number Diff line change
Expand Up @@ -20,9 +20,9 @@ data memory_stall_refusal_authority_disposition: Disposition = Terminal {
reason: "Single authority for the STALL half of the memory governor: the decision that a resolve which is thrashing -- spending its wall time refaulting its own evicted pages rather than computing -- must stop the line with a typed refusal instead of holding indefinitely. The budget half (what bound to admit against) is gunbc.host_budget_source; the capacity half (how many typed modules the cache may hold) is gunbc.typed_module_cache_capacity; this module owns what happens when both of those were satisfied and the run still cannot make progress, which is the state neither of them can see: the budget was readable and admitted, the cap was derived and enforced, and the machine underneath cannot actually deliver the budget the operator declared."
}

data memory_stall_observed_receipt_note: String = "THE MEASURED STALL THIS MODULE REFUSES, so the thresholds below face a real specimen rather than a thought experiment. 2026-08-30, default BuildBuddy remote-execution VM (7276 MiB total, 6 CPUs, swap 0, no procfs PSI, no cgroup memory controller files at any depth), GUNBC_MEMORY_BUDGET_BYTES=7000000000: four whole-closure gunbc runs (invocations 0cf5e9cb-f09e-47b6-a953-9bb4528ea9ec, e11bc9bf-61a8-432f-b596-e1d74efc5b55, ecd54e06-8b02-48c6-9f63-95e912c9edff, 33d93219-793c-40fe-a2c1-84f64d0fb743, measured by session loyal-raven-297) ran 2 to 4.5 hours without completing and without printing a further line, while the same census completes in about 10 minutes on a 20 GB runner. The budget was READABLE (env override) and ADMITTED; the machine simply cannot hold the working set beside its own page cache, and with swap disabled the kernel's only recourse is evicting file-backed pages -- including the binary's own text -- which the process immediately refaults. Wall time is consumed by disk reads the process never asked for; memory.current never crosses a kill line; no signal any existing arm reads ever fires. The run is not slow, it is a treadmill.\n\nWHY NO EXISTING ARM COVERS IT. gunbc.host_budget_source refuses an UNREADABLE budget -- this budget was readable. gunbc.whole_corpus_compile_admission refuses a whole-root subject below measured demand -- these were Entry subjects, deliberately outside that arm (whole_corpus_compile_scope_note reserves the gap). gunbc.typed_module_cache_capacity bounds the typed cache -- the thrash is at PAGE grain underneath the allocator, invisible to entry counts. And the deleted AIMD controller's PSI arm could not run here even if it survived: the VM synthesizes no /proc/pressure files at all (measured, same day)."
data memory_stall_observed_receipt_note: String = "THE MEASURED STALL THIS MODULE REFUSES, so the thresholds below face a real specimen rather than a thought experiment. 2026-08-30, default BuildBuddy remote-execution VM (7276 MiB total, 6 CPUs, swap 0, no procfs PSI, no cgroup memory controller files at any depth), GUNBC_MEMORY_BUDGET_BYTES=7000000000: four whole-closure gunbc runs (invocations 0cf5e9cb-f09e-47b6-a953-9bb4528ea9ec, e11bc9bf-61a8-432f-b596-e1d74efc5b55, ecd54e06-8b02-48c6-9f63-95e912c9edff, 33d93219-793c-40fe-a2c1-84f64d0fb743, measured by session loyal-raven-297) ran 2 to 4.5 hours without completing and without printing a further line, while the same census completes in about 10 minutes on a 20 GB runner. The budget was READABLE (env override) and ADMITTED; the machine simply cannot hold the working set beside its own page cache, and with swap disabled the kernel's only recourse is evicting file-backed pages -- including the binary's own text -- which the process immediately refaults. Wall time is consumed by disk reads the process never asked for; memory.current never crosses a kill line; no signal any existing arm reads ever fires. The run is not slow, it is a treadmill.\n\nWHY NO EXISTING ARM COVERS IT. gunbc.host_budget_source refuses an UNREADABLE budget -- this budget was readable. gunbc.whole_corpus_compile_admission refuses a whole-root subject below measured demand -- these were Entry subjects, deliberately outside that arm (whole_corpus_compile_measured_peak_demand's annotation reserves the gap). gunbc.typed_module_cache_capacity bounds the typed cache -- the thrash is at PAGE grain underneath the allocator, invisible to entry counts. And the deleted AIMD controller's PSI arm could not run here even if it survived: the VM synthesizes no /proc/pressure files at all (measured, same day)."

data memory_stall_signal_choice_note: String = "WHY THE SIGNAL IS THE PROCESS'S OWN MAJOR-FAULT COUNTER AND NOTHING HOST-SHARED. majflt in /proc/self/stat (proc.5 field 12) counts the times THIS process had to read one of its own pages back from disk: it is the kernel's record of eviction-and-readmission at the grain the kernel actually evicts, observed about this process alone. A warm, healthy process sustains approximately zero major faults after its inputs are first read, whatever its size and however slow its arithmetic -- so a slow-but-progressing resolve and a thrashing one, which no wall-clock bound can tell apart, are cleanly separated by this counter: the first accumulates wall with majflt flat, the second accumulates majflt in the thousands per second. That is also why the verdict below carries NO elapsed-time arm: time appears only as the denominator of a rate, never as a refusal condition, because a timeout labelled pressure-detection would refuse exactly the honest slow case this signal exists to admit.\n\nWHAT WAS REJECTED. /proc/meminfo MemAvailable is a fact about the MACHINE and is precisely the absorbing substitution gunbc.host_budget_source deleted (host_budget_unreadable_cgroup_receipt_note); reusing it here as a trigger would re-open that arm one layer up. PSI (/proc/pressure/memory) is the kernel's own stall accounting and would be preferable where it exists, but the VM this class was measured on does not synthesize it (no /proc/pressure, no cgroup controllers -- measured 2026-08-30), so an arm keyed on PSI is permanently green exactly where the harm lives. The typed-module cache's eviction/readmission counters are the governor's own bookkeeping and ARE carried in the refusal so the operator can see whether the cache was implicated, but they do not gate: recompute-on-miss across entries is designed-in cost, and no measured stall has yet implicated it (the observed specimens thrash below the allocator, at page grain). If a measured stall ever shows the cache readmitting the same module unboundedly, the threshold for that axis is added HERE with its receipt, not improvised at a call site."
data memory_stall_signal_choice_note: String = "WHY THE SIGNAL IS THE PROCESS'S OWN MAJOR-FAULT COUNTER AND NOTHING HOST-SHARED. majflt in /proc/self/stat (proc.5 field 12) counts the times THIS process had to read one of its own pages back from disk: it is the kernel's record of eviction-and-readmission at the grain the kernel actually evicts, observed about this process alone. A warm, healthy process sustains approximately zero major faults after its inputs are first read, whatever its size and however slow its arithmetic -- so a slow-but-progressing resolve and a thrashing one, which no wall-clock bound can tell apart, are cleanly separated by this counter: the first accumulates wall with majflt flat, the second accumulates majflt in the thousands per second. That is also why the verdict below carries NO elapsed-time arm: time appears only as the denominator of a rate, never as a refusal condition, because a timeout labelled pressure-detection would refuse exactly the honest slow case this signal exists to admit.\n\nWHAT WAS REJECTED. /proc/meminfo MemAvailable is a fact about the MACHINE and is precisely the absorbing substitution gunbc.host_budget_source deleted (host_budget_source_seed_mirror_disposition's annotation); reusing it here as a trigger would re-open that arm one layer up. PSI (/proc/pressure/memory) is the kernel's own stall accounting and would be preferable where it exists, but the VM this class was measured on does not synthesize it (no /proc/pressure, no cgroup controllers -- measured 2026-08-30), so an arm keyed on PSI is permanently green exactly where the harm lives. The typed-module cache's eviction/readmission counters are the governor's own bookkeeping and ARE carried in the refusal so the operator can see whether the cache was implicated, but they do not gate: recompute-on-miss across entries is designed-in cost, and no measured stall has yet implicated it (the observed specimens thrash below the allocator, at page grain). If a measured stall ever shows the cache readmitting the same module unboundedly, the threshold for that axis is added HERE with its receipt, not improvised at a call site."

data memory_stall_admitted_under_pressure_receipt_note: String = "THE MEASURED CONTROL THAT FORCED THE CPU CONJUNCT, found by this refusal's own first execution rather than by reasoning. On the first CI run carrying a rate-only form of this verdict (gunbc PR #9755, run 33319823294, required-witnesses-floor, srv3 actions-runner slice, budget 15 GiB from cgroup memory.high), the arm fired at 12431 major faults/minute sustained over a 788-second window -- one 13-minute typecheck of std.constructors under the slice's memory.high reclaim throttle. That configuration is not a treadmill: the same floor completes green on main on the same runners day after day. A resolve can sustain hundreds of refaults per second under a reclaim throttle and still be spending most of its wall COMPUTING -- which is exactly the slow-but-progressing state this module is forbidden to refuse. Rate alone cannot separate the two; what separates them is where the wall goes. A progressing run under pressure still burns CPU between faults; the treadmill's defining property is that its CPU share of wall is near zero, because the process sits in disk wait re-reading its own text. So the refusal is a CONJUNCTION: the fault rate above its line AND the process's own CPU share of the window below its floor. Both halves are the process observing itself; neither is host-shared; neither is a timeout."

Expand Down
2 changes: 1 addition & 1 deletion dag/gunbc/roadmap/roadmap_launch_deployment_cli.dag
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,7 @@ fn rlm_workflow_file_path() -> String {
//
// THE PRINCIPAL IS OBSERVED, NOT ASSUMED. Footprint, provider and dispatch preflights are only
// meaningful as the belt's effective service principal (gunbc.roadmap_belt_actuate
// belt_footprint_admission_note), so the receipt run records `whoami` and the join refuses when it
// BeltFootprintRoot), so the receipt run records `whoami` and the join refuses when it
// is not the emitted ServiceUser. If srv1's runner principal is not that user, the wet run produces
// an Incomplete receipt naming `principal`, and the repair is a modeled execution-as-principal
// step, not a relaxation here.
Expand Down
16 changes: 8 additions & 8 deletions dag/gunbc/rung_drop.dag
Original file line number Diff line number Diff line change
Expand Up @@ -145,15 +145,15 @@ data rung_drop_roster: List<RungDrop> = [
fabric_evidence_gating,
]

// THE DERIVATION THE PROJECTION USES, so "standing today" has one authority and not two.
fn rung_drop_is_standing(drop: RungDrop) -> Bool {
match drop.standing {
// THE DERIVATION THE PROJECTION USES, so "standing today" has one authority and not two. The
// standing arm is read AT THE ONE SITE THAT CONSUMES IT rather than through a reusable
// RungDropStanding -> Bool accessor: a named predicate beside a coproduct is a second, weaker
// spelling of the variant the row already carries, and every later caller reaches for the Bool
// instead of the arm it came from.
fn standing_rung_drops() -> List<RungDrop> {
filter(rung_drop_roster, d => match d.standing {
Standing => true
Retired { trigger_fired: _ } => false
}
}

fn standing_rung_drops() -> List<RungDrop> {
filter(rung_drop_roster, d => rung_drop_is_standing(d))
})
}

2 changes: 1 addition & 1 deletion dag/gunbc/stage0_partition_rebuild_scope.dag
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ import gunbc.stage0_partition_package_graph {
// PACKAGES those changed mirrors force the next-pass compiler to rebuild. The two are different
// questions over different graphs -- one over .dag module references, one over cargo packages --
// and the second is the larger of the two costs on every measured host
// (gunbc.regen_round_cost regen_round_cost_shape_note).
// (gunbc.regen_round_cost regen_affected_set_disposition).
//
// THE CLAIM IS NOT "ONE MIRROR, ONE CRATE". A foundation edit legitimately rebuilds several
// downstream packages; the guarantee is that an UNRELATED package stays uncompiled, and that
Expand Down
2 changes: 1 addition & 1 deletion dag/test/claim/host/host_budget_source_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,7 @@ data all_kernels: List<KernelFamily> = [Linux, Darwin, WindowsNt, LinuxGuestOnWi
//
// The arm went away for a different reason than this note: capping a host-shared reading at one
// fleet's declared slot line was a substitution, not a bound (gunbc.host_budget_source
// host_budget_unreadable_cgroup_receipt_note). The lesson survives the arm, which is why this row
// host_budget_source_seed_mirror_disposition). The lesson survives the arm, which is why this row
// does — a fixture derived from the tree under test is inert whatever it is measuring.

data all_sources: List<HostBudgetSource> = [
Expand Down
11 changes: 8 additions & 3 deletions dag/test/claim/rung_drop_standing_partition_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ module test.claim.rung_drop_standing_partition_witness_test
import gunbc.rung_drop {
rung_drop_roster,
standing_rung_drops,
rung_drop_is_standing,
cited_symbol_census,
}

// THE DEFECT THIS WITNESS EXISTS FOR, stated as the state that must stay unwritable: DESIGN.md's
Expand Down Expand Up @@ -32,7 +32,12 @@ import gunbc.rung_drop {
// witness closes the projection fork -- one authority for the standing list -- and leaves the
// prose-to-field agreement as the honest open residue.

// THE JOIN IS ON IDENTITY, NOT ON A RE-DERIVED PREDICATE. Asking each row "are you standing?" a
// second time here would test this file's copy of the arm rather than the projection's, and it
// would need the coproduct -> Bool accessor gunbc.rung_drop deliberately does not carry. So the
// witness names the retired row and asks where it appears: absent from the derived list, present
// exactly once in the roster it was retired in place within.
test fn standing_list_excludes_every_retired_drop() -> Bool {
length(xs: filter(standing_rung_drops(), d => !rung_drop_is_standing(d))) == 0
&& length(xs: filter(rung_drop_roster, d => !rung_drop_is_standing(d))) > 0
length(xs: filter(map(standing_rung_drops(), d => d.identity), i => i == cited_symbol_census.identity)) == 0
&& length(xs: filter(map(rung_drop_roster, d => d.identity), i => i == cited_symbol_census.identity)) == 1
}
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ import gunbc.whole_corpus_compile_admission {

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

data witness_subject_note: String = "BOTH ARMS STAND ON INDEPENDENTLY MEASURED MACHINES, which is what makes the pair fail for a reason worth knowing in either direction rather than restating its own input.\n\nThe REFUSING budget is the one the BuildBuddy remote-execution runner actually answered with on invocation 13cf8d2e-173a-42d2-9a56-101bb3332740, the run that was SIGKILLed at exit 137. It is not chosen to make the assertion true: it is recovered from the cap=1675 line that run printed, by inverting the integer division cli_run performs.\n\nTHE SOURCE ON THAT FIXTURE MOVED AND THE BUDGET DID NOT. It was BudgetSourceMemAvailable, the arm that produced the doomed number in the first place; that arm is deleted (gunbc.host_budget_source host_budget_unreadable_cgroup_receipt_note) because a reading about the MACHINE is not a bound on the slot, and a runner in that state now resolves to HostBudgetUnreadable and refuses before this arm is reached. What this row judges is the QUANTITY, so the fixture is now carried on BudgetSourceEnvOverride — which is precisely the shape an operator on that runner produces today, and it makes the arm say something sharper than it did: even a 4.9 GiB budget DECLARED by an operator is refused against the measured demand.\n\nThe ADMITTING budget is gunbc.runner_slot_allocation's declared per-slot memory.high, READ FROM THAT AUTHORITY rather than retyped here. Retyping it would have been the exact defect this PR's own threshold note argues against, and it has a live specimen one module over: host_budget_source_witness_test built its expectation from the seed mirror value retyped, so it greened whichever way the mirror went (found by stern-heron-695, corrected in gunbc#8638). A fixture input is still an input, and one that silently tracks nothing is worse than one that fails. So a refusal that stopped firing would mean the measured doomed run had become admissible, and an admission that stopped holding would mean CI's own runner had been refused — two different regressions, each with its own arm here."
data witness_subject_note: String = "BOTH ARMS STAND ON INDEPENDENTLY MEASURED MACHINES, which is what makes the pair fail for a reason worth knowing in either direction rather than restating its own input.\n\nThe REFUSING budget is the one the BuildBuddy remote-execution runner actually answered with on invocation 13cf8d2e-173a-42d2-9a56-101bb3332740, the run that was SIGKILLed at exit 137. It is not chosen to make the assertion true: it is recovered from the cap=1675 line that run printed, by inverting the integer division cli_run performs.\n\nTHE SOURCE ON THAT FIXTURE MOVED AND THE BUDGET DID NOT. It was BudgetSourceMemAvailable, the arm that produced the doomed number in the first place; that arm is deleted (gunbc.host_budget_source host_budget_source_seed_mirror_disposition) because a reading about the MACHINE is not a bound on the slot, and a runner in that state now resolves to HostBudgetUnreadable and refuses before this arm is reached. What this row judges is the QUANTITY, so the fixture is now carried on BudgetSourceEnvOverride — which is precisely the shape an operator on that runner produces today, and it makes the arm say something sharper than it did: even a 4.9 GiB budget DECLARED by an operator is refused against the measured demand.\n\nThe ADMITTING budget is gunbc.runner_slot_allocation's declared per-slot memory.high, READ FROM THAT AUTHORITY rather than retyped here. Retyping it would have been the exact defect this PR's own threshold note argues against, and it has a live specimen one module over: host_budget_source_witness_test built its expectation from the seed mirror value retyped, so it greened whichever way the mirror went (found by stern-heron-695, corrected in gunbc#8638). A fixture input is still an input, and one that silently tracks nothing is worse than one that fails. So a refusal that stopped firing would mean the measured doomed run had become admissible, and an admission that stopped holding would mean CI's own runner had been refused — two different regressions, each with its own arm here."

fn observed_doomed_budget() -> HostBudgetResolution {
host_budget_resolved_observation(
Expand Down
2 changes: 1 addition & 1 deletion src/v1/stage0/src/memory_governor.rs
Original file line number Diff line number Diff line change
Expand Up @@ -694,7 +694,7 @@ pub fn host_budget_unreadable_reason() -> String {
admitting against the widest signal available: a host-shared reading is a number \
about the MACHINE, not about this slot, and admitting against one is the rc=137 \
SIGKILL this arm exists to prevent (BuildBuddy receipt 2026-08-30, \
gunbc.host_budget_source host_budget_unreadable_cgroup_receipt_note). The executor must \
gunbc.host_budget_source host_budget_source_seed_mirror_disposition). The executor must \
expose an enforceable limit; GUNBC_MEMORY_BUDGET_BYTES may only request a lower planning ceiling.",
std::env::consts::OS
)
Expand Down
Loading
Loading