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 docs/plans/budget-tree.md
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ A third measured field validates the cap is not a false-killer: **worst-observed

**Reservation-fit vs hard-guarantee (the valve is load-bearing).** `srv1_runs_fit_in_pool()` = `floor(pool / reservation)` = 3 is the *bin-packing* count — it assumes typical usage, so a correlated burst of rust-gate jobs each spiking to the ~30 GiB worst would over-commit (3 × 30 > 49.45 GiB pool). The *hard-guarantee* count `srv1_runs_hard_guaranteed()` = `floor(pool / hard_cap)` = 1 is the number that never over-commits even if every job hits the container cap. `1 ≤ 3` is witnessed. The gap is covered by the host-RSS valve (deep-otter's admission backstop) — i.e. the reservation-based R is **valve-backstopped, not a hard guarantee**, exactly as the dashboard session pool is. The actuator that *enforces* R by start/stopping runner services (B5's "GHA-runner-pool memory cap") is a live-fleet apply and stays **operator-fenced** (§5); until it lands deep-otter holds the runner count at R=3 by hand, and the convergence proof is that the hand-walked count already equals the derived R.

**Values — provenance.** typical/reservation ← **B4 (quick-lynx-78) verified** (`11592347648`, run 28003119550); worst-observed ← **deep-otter-528's srv2 cgroup `memory.peak` monitor** (`32434110464`); hard cap ← the measured container `memory.max`. The two-driver invariant (parent): the reservation side is driven by typical claim_executor batches (B4 measures it), the cap/worst side by rust-gate rustc *children* (only deep-otter's rust-gate-present monitor sees it; B4's no-rust-gate run under-reports it). NOTE: B4's #5619 dedup moves the *typical* self-RSS only ~0.57 GiB (8.7→8.1, NOT the earlier-retracted 8.7→4.2) and never touches the cap side. The margin is a single knob (`gunbc_ci_floor_runner_margin_num/den`, currently 6/5 = 20%) and applies to the **reservation only**.
**Values — provenance.** typical/reservation ← **B4 (quick-lynx-78) verified** (`11592347648`, run 28003119550); worst-observed ← **deep-otter-528's srv2 cgroup `memory.peak` monitor** (`32434110464`); hard cap ← the measured container `memory.max`. The two-driver invariant (parent): the reservation side is driven by typical claim_executor batches (B4 measures it), the cap/worst side by rust-gate rustc *children* (only deep-otter's rust-gate-present monitor sees it; B4's no-rust-gate run under-reports it). NOTE: B4's #5619 dedup moves the *typical* self-RSS only ~0.57 GiB (8.7→8.1, NOT the earlier-retracted 8.7→4.2) and never touches the cap side. NOTE 2: `gunbc_ci_floor_runner_margin_num/den` (6/5 = 20%) was documented here as applying to the reservation, but its only code consumer was `within_run_spawn_budget()` (RETIRED in #5831 — was computing the wrong budget for within-run spawn-width, not the reservation). The margin constants (`gunbc_ci_floor_runner_margin_num/den`) and `gunbc_ci_floor_whole_run_peak_rss_bytes` are now deleted alongside `within_run_spawn_budget()` (no remaining consumers); the reservation reconciliation with deep-otter-528 is a separate runway.

Carriers: [dsl/gunbc/ci_budget_tree.dag](../../dsl/gunbc/ci_budget_tree.dag) (the two-pool tree + two-number leaf accessors), [dsl/gunbc/ci_floor_measurement.dag](../../dsl/gunbc/ci_floor_measurement.dag) (the measured carriers), witness [dsl/test/claim/ci_budget_tree_witness_test.dag](../../dsl/test/claim/ci_budget_tree_witness_test.dag).

Expand Down
19 changes: 4 additions & 15 deletions dsl/gunbc/ci_budget_tree.dag
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
module gunbc.ci_budget_tree

import std.measure { ByteSize, byte_size, measure_scale_fraction_floor, Memory, One }
import std.measure { ByteSize, byte_size, Memory, One }
import std.types { Int, List, String, Bool }
import std.disposition { Disposition, Terminal }
import std.realization_width { byte_size_saturating_sub }
Expand All @@ -16,18 +16,15 @@ import gunbc.ci_floor_measurement {
HostFixedOverhead, HostFixedOverheadMeasured, HostFixedOverheadUnmeasured,
gunbc_ci_host_fixed_overhead,
gunbc_ci_host_container_memory_cap,
gunbc_ci_floor_whole_run_peak_rss_bytes,
gunbc_ci_floor_runner_margin_num,
gunbc_ci_floor_runner_margin_den,
gunbc_ci_session_reservation_mode
}
import gunbc.ci_runner_placement {
SessionSliceResolution, SessionSliceResolved, SessionSliceUnresolved,
resolve_session_slice
}
import gunbc.fleet_host_budget { gunbc_fleet_oomd_evidence }
import gunbc.fleet_host_budget { gunbc_fleet_oomd_evidence, gunbc_per_runner_memory_cap }

data gunbc_ci_budget_tree_deconfliction_disposition: Disposition = Terminal { reason: "DESIGN §3 deliberate carrier split: this BudgetNode governs INTER-run co-residence (host_ram partitioned as overhead + sessions_slice + runner_slice, conserving by construction via byte_size_saturating_sub). Intentionally NOT the within-run spawn-width budget: within_run_spawn_budget feeds memory_aware_spawn_width for parallelism INSIDE one run and must stay non-fail-closed so the live floor keeps running when the inter-run operating point is unset. Do not fold the two back together - see gunbc_ci_footprint_granularity_disposition." }
data gunbc_ci_budget_tree_deconfliction_disposition: Disposition = Terminal { reason: "DESIGN §3 deliberate carrier split: this BudgetNode governs INTER-run co-residence (host_ram partitioned as overhead + sessions_slice + runner_slice, conserving by construction via byte_size_saturating_sub). srv1_floor_memory_budget returns the measured per-runner cgroup cap (gunbc_per_runner_memory_cap = 8 GiB) -- the real binding constraint for within-run parallelism. Do NOT conflate with inter-run budget accounting; do NOT reintroduce within_run_spawn_budget (retired -- it used whole-run-peak x margin as the budget, which exceeded the real runner cgroup cap and caused OOM). See gunbc_ci_footprint_granularity_disposition." }

fn host_overhead_bytes() -> ByteSize {
match gunbc_ci_host_fixed_overhead {
Expand Down Expand Up @@ -129,16 +126,8 @@ fn srv1_fixed_overhead_bytes() -> ByteSize {
host_overhead_bytes()
}

fn within_run_spawn_budget() -> ByteSize {
measure_scale_fraction_floor(
m: gunbc_ci_floor_whole_run_peak_rss_bytes(),
num: gunbc_ci_floor_runner_margin_num,
den: gunbc_ci_floor_runner_margin_den
)
}

fn srv1_floor_memory_budget() -> ByteSize {
within_run_spawn_budget()
gunbc_per_runner_memory_cap
}

fn srv1_ci_run_container_hard_cap() -> ByteSize {
Expand Down
7 changes: 0 additions & 7 deletions dsl/gunbc/ci_floor_measurement.dag
Original file line number Diff line number Diff line change
Expand Up @@ -34,15 +34,8 @@ fn gunbc_ci_floor_per_shard_peak_rss_bytes() -> ByteSize {
}
}

fn gunbc_ci_floor_whole_run_peak_rss_bytes() -> ByteSize {
gunbc_ci_floor_measured_peak.peak
}

data gunbc_ci_host_container_memory_cap: ByteSize = byte_size(33578549248)

data gunbc_ci_floor_runner_margin_num: Int = 6
data gunbc_ci_floor_runner_margin_den: Int = 5

data gunbc_ci_floor_conservative_fallback_width: Int = 4

type JobCgroupPeakMeasurement
Expand Down
2 changes: 1 addition & 1 deletion dsl/gunbc/plans/budget_tree.dag
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ fn budget_tree_body() -> List<MarkdownBlock> {
p(text: "A third measured field validates the cap is not a false-killer: **worst-observed** = `srv1_ci_run_worst_observed()` = the worst per-job cgroup `memory.peak` deep-otter's srv2 monitor has caught (`gunbc_ci_floor_runner_worst_max` = `32434110464`, ~30.2 GiB, actions-runner@srv2-09, a rust-gate floor job with rustc children). `reservation < worst_observed ≤ hard_cap` is witnessed: the worst real job (30.2) fits *under* the kill ceiling (31.27) — by only ~1 GiB. That ~1 GiB is a **risk to retire by shrinking the footprint, not by raising a cap the host can't afford**; if a future worst exceeds the container cap the witness goes red, which is the honest signal that jobs are about to OOM-kill."),
p(text: "**Construction-first, not validation.** `R = floor(gha_runner_pool / reservation)` is *derived*, so an over-wide run count is unwritable; the leaf appropriation is the *measured* typical peak + margin, so the floor's spawn-width is governed by a real number, not a `totalMem / R` guess. Conservation across the three siblings is the residue lens (`node_conserves`) over the constructed tree."),
p(text: "**Reservation-fit vs hard-guarantee (the valve is load-bearing).** `srv1_runs_fit_in_pool()` = `floor(pool / reservation)` = 3 is the *bin-packing* count — it assumes typical usage, so a correlated burst of rust-gate jobs each spiking to the ~30 GiB worst would over-commit (3 × 30 > 49.45 GiB pool). The *hard-guarantee* count `srv1_runs_hard_guaranteed()` = `floor(pool / hard_cap)` = 1 is the number that never over-commits even if every job hits the container cap. `1 ≤ 3` is witnessed. The gap is covered by the host-RSS valve (deep-otter's admission backstop) — i.e. the reservation-based R is **valve-backstopped, not a hard guarantee**, exactly as the dashboard session pool is. The actuator that *enforces* R by start/stopping runner services (B5's \"GHA-runner-pool memory cap\") is a live-fleet apply and stays **operator-fenced** (§5); until it lands deep-otter holds the runner count at R=3 by hand, and the convergence proof is that the hand-walked count already equals the derived R."),
p(text: "**Values — provenance.** typical/reservation ← **B4 (quick-lynx-78) verified** (`11592347648`, run 28003119550); worst-observed ← **deep-otter-528's srv2 cgroup `memory.peak` monitor** (`32434110464`); hard cap ← the measured container `memory.max`. The two-driver invariant (parent): the reservation side is driven by typical claim_executor batches (B4 measures it), the cap/worst side by rust-gate rustc *children* (only deep-otter's rust-gate-present monitor sees it; B4's no-rust-gate run under-reports it). NOTE: B4's #5619 dedup moves the *typical* self-RSS only ~0.57 GiB (8.7→8.1, NOT the earlier-retracted 8.7→4.2) and never touches the cap side. The margin is a single knob (`gunbc_ci_floor_runner_margin_num/den`, currently 6/5 = 20%) and applies to the **reservation only**."),
p(text: "**Values — provenance.** typical/reservation ← **B4 (quick-lynx-78) verified** (`11592347648`, run 28003119550); worst-observed ← **deep-otter-528's srv2 cgroup `memory.peak` monitor** (`32434110464`); hard cap ← the measured container `memory.max`. The two-driver invariant (parent): the reservation side is driven by typical claim_executor batches (B4 measures it), the cap/worst side by rust-gate rustc *children* (only deep-otter's rust-gate-present monitor sees it; B4's no-rust-gate run under-reports it). NOTE: B4's #5619 dedup moves the *typical* self-RSS only ~0.57 GiB (8.7→8.1, NOT the earlier-retracted 8.7→4.2) and never touches the cap side. NOTE 2: `gunbc_ci_floor_runner_margin_num/den` (6/5 = 20%) was documented here as applying to the reservation, but its only code consumer was `within_run_spawn_budget()` (RETIRED in #5831 — was computing the wrong budget for within-run spawn-width, not the reservation). The margin constants (`gunbc_ci_floor_runner_margin_num/den`) and `gunbc_ci_floor_whole_run_peak_rss_bytes` are now deleted alongside `within_run_spawn_budget()` (no remaining consumers); the reservation reconciliation with deep-otter-528 is a separate runway."),
p(text: "Carriers: [dsl/gunbc/ci_budget_tree.dag](../../dsl/gunbc/ci_budget_tree.dag) (the two-pool tree + two-number leaf accessors), [dsl/gunbc/ci_floor_measurement.dag](../../dsl/gunbc/ci_floor_measurement.dag) (the measured carriers), witness [dsl/test/claim/ci_budget_tree_witness_test.dag](../../dsl/test/claim/ci_budget_tree_witness_test.dag)."),
]
}
Expand Down
8 changes: 4 additions & 4 deletions dsl/test/claim/ci_budget_tree_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -12,12 +12,12 @@ import gunbc.ci_budget_tree {
srv1_gha_runner_pool_budget,
srv1_dashboard_session_pool_budget,
srv1_floor_memory_budget,
within_run_spawn_budget,
host_allocatable_bytes,
host_budget_tree_at,
budget_tree_gha_runner_pool_node,
budget_tree_dashboard_session_pool_node,
}
import gunbc.fleet_host_budget { gunbc_per_runner_memory_cap }

fn fitting_slice() -> Int {
53687091200
Expand Down Expand Up @@ -95,9 +95,9 @@ fn witness_unknown_child_is_absent() -> Bool {
}
}

fn witness_spawn_width_budget_deconflated() -> Bool {
fn witness_spawn_width_budget_is_per_runner_cap() -> Bool {
byte_size_count(b: srv1_floor_memory_budget()) > 0
&& byte_size_count(b: srv1_floor_memory_budget()) == byte_size_count(b: within_run_spawn_budget())
&& byte_size_count(b: srv1_floor_memory_budget()) == byte_size_count(b: gunbc_per_runner_memory_cap)
&& byte_size_count(b: srv1_floor_memory_budget()) < byte_size_count(b: srv1_host_ram())
}

Expand All @@ -110,5 +110,5 @@ test fn ci_budget_tree_holds() -> Bool {
&& witness_srv2_symmetric_to_srv1()
&& witness_two_pools_present()
&& witness_unknown_child_is_absent()
&& witness_spawn_width_budget_deconflated()
&& witness_spawn_width_budget_is_per_runner_cap()
}
Loading