diff --git a/dsl/gunbc/ci_fleet.dag b/dsl/gunbc/ci_fleet.dag index 2066dafca4c..19058df734d 100644 --- a/dsl/gunbc/ci_fleet.dag +++ b/dsl/gunbc/ci_fleet.dag @@ -24,13 +24,15 @@ import product.compute_fabric { Dram, WorkDemand, ResourceEnvelope, + MemoryRequirement, IsolationRequirement, IndependentShards, offer_placement_supply_row, placement_spawn_width, + placement_floor_memory_budget_bytes, } import extdeps.cpu.types { CpuFacts, CpuDeploymentFacts } -import std.measure { byte_size, hertz, hardware_thread_count, HardwareThreadCount } +import std.measure { byte_size, byte_size_count, hertz, hardware_thread_count, hardware_thread_count_value, HardwareThreadCount } import std.os.types { OperatingSystemSurface, Linux, @@ -58,7 +60,12 @@ data gunbc_ci_host: ComputeHost = ComputeHost { identity: gunbc_ci_host_identity, baseboard: none, processors: [CpuProcessor { cpu: gunbc_ci_cpu }], - memory: [MemoryDevice { capacity: byte_size(274877906944), memory_kind: Dram, bandwidth: none }], + // 125 GiB measured on the real fleet host (Ampere Altra Max M128, 1 NUMA node). The prior + // 256 GiB was a stub; the memory-aware spawn-width bound (placement_spawn_width) needs a + // real RAM figure or it cannot back fan-out off before the cgroup OOM. CPU thread count + // (catalog) is still the 64-thread stub — corrected with the ctrl fleet grounding; the + // memory bound dominates the floor width regardless, so it is not load-bearing here. + memory: [MemoryDevice { capacity: byte_size(134217728000), memory_kind: Dram, bandwidth: none }], storage: [], network_interfaces: [], } @@ -100,7 +107,13 @@ fn gunbc_ci_floor_corpus_work_demand(corpus_shard_count: Int) -> WorkDemand { resources: ResourceEnvelope { cpu: none, gpu: none, - memory: none, + // Per-shard peak resolve memory. Grounded in the deterministic floor-OOM evidence + // (eager-boar-790, 3 runs of a grown corpus at width=7): srv2's ~87.6 GiB cgroup cap + // passes 7 concurrent ~2900-item resolves only by a thin margin (~12.5 GiB/unit), and + // srv1's ~65.6 GiB cap OOM-kills (exit 137). 14 GiB/unit carries headroom for corpus + // growth; the memory-aware width then floors batch-2 below the OOM ceiling on both + // hosts. Grounds-tighter when a peak-RSS probe per resolve lands. + memory: Present { value: MemoryRequirement { min_bytes: byte_size(15032385536) } }, storage: none, network: none, }, @@ -117,9 +130,11 @@ fn gunbc_ci_floor_placement_supply() -> PlacementSupplyRow? { offer_placement_supply_row(offer: gunbc_ci_fleet_offer) } -// Host spawn-width = min(caller's corpus breadth, this fleet's hardware threads). -// No hand-tuned width: add a gate to the spec → breadth re-derives; change the host → -// supply re-derives; spawn_width follows from both with zero edits here. +// Host spawn-width = min(corpus breadth, hardware threads, memory_budget / per-shard peak). +// No hand-tuned width: add a gate to the spec → breadth re-derives; change the host → supply +// re-derives; raise the per-shard memory → the memory bound re-derives; spawn_width follows +// from all three via placement_spawn_width with zero edits here. The memory term is what +// keeps batch-2 from OOM-killing as the corpus grows (the CPU-only bound was memory-blind). fn ci_fleet_floor_spawn_width(corpus_shard_count: Int) -> HardwareThreadCount { match gunbc_ci_floor_placement_supply() { Absent => hardware_thread_count(1) @@ -127,3 +142,22 @@ fn ci_fleet_floor_spawn_width(corpus_shard_count: Int) -> HardwareThreadCount { placement_spawn_width(supply: row, demand: gunbc_ci_floor_corpus_work_demand(corpus_shard_count: corpus_shard_count)) } } + +// §5 OOM oracle: the chosen floor width times the per-shard peak memory must fit the +// conservative memory budget — i.e. batch-2's concurrent memory peak stays under the cgroup +// MemoryMax. Discriminating: a memory-blind width (= min(breadth, threads), ignoring the +// memory term) would exceed the budget and flip this false. Absent supply / Absent memory +// demand are vacuously safe (no concurrent memory pressure to bound). +fn ci_fleet_floor_spawn_fits_memory_budget(corpus_shard_count: Int) -> Bool { + match gunbc_ci_floor_placement_supply() { + Absent => true + Present { value: row } => + match gunbc_ci_floor_corpus_work_demand(corpus_shard_count: corpus_shard_count).resources.memory { + Absent => true + Present { value: req } => { + let width = hardware_thread_count_value(t: ci_fleet_floor_spawn_width(corpus_shard_count: corpus_shard_count)) + width * byte_size_count(req.min_bytes) <= placement_floor_memory_budget_bytes(supply: row) + } + } + } +} diff --git a/dsl/product/compute_fabric.dag b/dsl/product/compute_fabric.dag index 1451bfac5d0..55fcd571f1e 100644 --- a/dsl/product/compute_fabric.dag +++ b/dsl/product/compute_fabric.dag @@ -80,7 +80,7 @@ import extdeps.toolchain.types { } import product.placement_supply { HostIdentity, PlacementSupplyRow } import std.baseboard { ServerBaseboard } -import std.realization_width { bounded_host_spawn_width } +import std.realization_width { bounded_host_spawn_width, int_min } // 🟡 forward — v2.std.witness / v2.std.diagnostic at harness (P-CF-WITNESS). // Kept intentionally distinct from the kernel `Witness` container. @@ -505,14 +505,53 @@ fn work_demand_shard_count(demand: WorkDemand) -> Int { } } -// Width projection: min(shard_count, PlacementSupplyRow.hardware_threads) — single authority. -// Eligibility is NOT rejected when demand exceeds supply — the peripheral host fold caps -// fan-out; satisfies records DemandParallelism as proven when IndependentShards is present. +// Conservative memory budget for concurrent fan-out on a host. A floor batch is killed by +// its runner-slice cgroup MemoryMax (NOT total RAM), which on the tightest fleet host caps +// near half of RAM. Until ctrl/BMC grounds the exact per-host MemoryMax bytes, approximate +// the budget as 0.50×RAM so a single fleet-wide spawn width stays safe on the TIGHTEST host +// (the floor lands on either host). Grounds-later: replace 0.50×RAM with measured MemoryMax. +fn placement_floor_memory_budget_bytes(supply: PlacementSupplyRow) -> Int { + byte_size_count(supply.ram_bytes) / 2 +} + +// Memory width BOUND: how many concurrent units fit under the memory budget, each peaking at +// the demand's per-unit memory requirement. `none` = no memory bound (Absent demand, or a +// degenerate non-positive per-unit guarded against divide-by-zero). A budget under one unit +// still admits 1 (fail-closed forward progress, never 0 width). Returned as `Int?` so the +// "no bound" case never has to unify with the Int division result. +fn placement_memory_width_bound(supply: PlacementSupplyRow, demand: WorkDemand) -> Int? { + match demand.resources.memory { + Absent => none + Present { value: req } => { + let per_unit = byte_size_count(req.min_bytes) + if per_unit <= 0 { none } else { + let fits = placement_floor_memory_budget_bytes(supply: supply) / per_unit + Present { value: if fits < 1 { 1 } else { fits } } + } + } + } +} + +// Width projection: min(shard_count, hardware_threads, memory_budget / per_unit_peak) — +// single authority, MEMORY-AWARE. The CPU bound (bounded_host_spawn_width) alone is +// memory-blind: N concurrent resolves each peak at the demand's per-unit memory, and N×peak +// must stay under the floor's cgroup MemoryMax or the batch is OOM-killed (exit 137). The +// memory term backs fan-out off BEFORE the kill — §1's safety axis made structural, and the +// connected model §6 ('fix related systems together') requires: CPU and memory are ONE width +// relationship, not a CPU bound patched after an OOM. Eligibility is NOT rejected when demand +// exceeds supply — the peripheral host fold caps fan-out; satisfies records DemandParallelism +// as proven when IndependentShards is present. fn placement_spawn_width(supply: PlacementSupplyRow, demand: WorkDemand) -> HardwareThreadCount { - bounded_host_spawn_width( - shard_count: work_demand_shard_count(demand: demand), - hardware_threads: supply.hardware_threads + let cpu_width = hardware_thread_count_value( + t: bounded_host_spawn_width( + shard_count: work_demand_shard_count(demand: demand), + hardware_threads: supply.hardware_threads + ) ) + match placement_memory_width_bound(supply: supply, demand: demand) { + Absent => hardware_thread_count(count: cpu_width) + Present { value: mem_width } => hardware_thread_count(count: int_min(a: cpu_width, b: mem_width)) + } } // --- §1.2 demand ------------------------------------------------------------- diff --git a/src/v2/test/claim/ci_floor_plan_witness_test.dag b/src/v2/test/claim/ci_floor_plan_witness_test.dag index 076576baf4a..1d6f4484d8f 100644 --- a/src/v2/test/claim/ci_floor_plan_witness_test.dag +++ b/src/v2/test/claim/ci_floor_plan_witness_test.dag @@ -15,7 +15,8 @@ import std.realization { } import v2.workflow.ci_floor_plan { gunbc_ci_floor_batches, corpus_runnable, - gunbc_ci_floor_breadth, gunbc_ci_floor_spawn_width + gunbc_ci_floor_breadth, gunbc_ci_floor_spawn_width, + gunbc_ci_floor_spawn_fits_memory_budget } import std.measure { hardware_thread_count_value } import gunbc.ci_layer_roots { witness_discovery_scan_dirs, witness_layer_roots } @@ -102,11 +103,12 @@ fn witness_corpus_skip_node_frontier_enabled() -> Bool { } } -// Connected relationship: spawn_width is DERIVED from the floor breadth, not tuned. -// When breadth <= hardware threads (true on the real fleet), spawn_width == breadth — -// so the host runs the independent layer concurrently, not one-at-a-time. -fn witness_spawn_width_tracks_breadth() -> Bool { - hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) == gunbc_ci_floor_breadth() +// Connected relationship: spawn_width is DERIVED (min of breadth, hardware threads, and the +// memory budget / per-shard peak), never a tuned constant. It is positive and never exceeds +// the work breadth — fanning out more workers than shards would be wasted concurrency. +fn witness_spawn_width_bounded_by_breadth() -> Bool { + let width = hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) + (width >= 1) && (width <= gunbc_ci_floor_breadth()) } // Discriminating: the floor is NOT serial. A revert to a constant shard_count (=1) or a @@ -116,6 +118,22 @@ fn witness_floor_not_serial() -> Bool { (hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) > 1) } +// Connected memory relationship (the §5 OOM oracle): the scheduled width's concurrent memory +// peak fits the fleet memory budget. DISCRIMINATING against the memory-blind regression — if +// placement_spawn_width dropped its memory term, width would jump to min(breadth, threads)=7 +// and 7×(per-shard peak) would blow the budget, flipping this RED. This is the witness that +// would have caught the deterministic floor-OOM (exit 137) at model time, not on the fleet. +fn witness_floor_width_fits_memory_budget() -> Bool { + gunbc_ci_floor_spawn_fits_memory_budget() +} + +// Discriminating: the memory term is ACTIVE — on the real fleet the per-shard peak caps the +// width strictly below the CPU/breadth bound (mem budget admits fewer than `breadth` units). +// A memory-blind width would equal breadth, flipping this RED. +fn witness_floor_width_memory_bounded() -> Bool { + hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) < gunbc_ci_floor_breadth() +} + test fn ci_floor_plan_witnesses() -> Bool { witness_two_readiness_layers() && witness_compile_root_runs_first() && @@ -125,6 +143,8 @@ test fn ci_floor_plan_witnesses() -> Bool { witness_scan_dirs_match_layer_authority() && witness_corpus_has_no_explicit_entries() && witness_corpus_skip_node_frontier_enabled() && - witness_spawn_width_tracks_breadth() && - witness_floor_not_serial() + witness_spawn_width_bounded_by_breadth() && + witness_floor_not_serial() && + witness_floor_width_fits_memory_budget() && + witness_floor_width_memory_bounded() } diff --git a/src/v2/workflow/ci_floor_plan.dag b/src/v2/workflow/ci_floor_plan.dag index 9facb18f89c..c9d9924ee85 100644 --- a/src/v2/workflow/ci_floor_plan.dag +++ b/src/v2/workflow/ci_floor_plan.dag @@ -37,7 +37,7 @@ import v2.std.collection { List } import v2.std.dependency { DataDependsOn, DependencyView } import v2.std.node { Atom, Node, TypeNode } import v2.std.text { String } -import gunbc.ci_fleet { ci_fleet_floor_spawn_width } +import gunbc.ci_fleet { ci_fleet_floor_spawn_width, ci_fleet_floor_spawn_fits_memory_budget } import std.types { ContentHash } import std.measure { HardwareThreadCount } import std.realization_width { width_fold_objective_goals } @@ -222,8 +222,16 @@ fn gunbc_ci_floor_breadth() -> Int { length(xs: gunbc_ci_spec.gates) } -// claim_executor spawn-width companion: min(floor breadth, fleet hardware threads). -// The relationship is the model; nothing here is hand-tuned per host or per gate. +// claim_executor spawn-width companion: min(floor breadth, fleet hardware threads, memory +// budget / per-shard peak). The relationship is the model; nothing here is hand-tuned per +// host or per gate — the memory term backs fan-out off before the cgroup OOM-kill. fn gunbc_ci_floor_spawn_width() -> HardwareThreadCount { ci_fleet_floor_spawn_width(corpus_shard_count: gunbc_ci_floor_breadth()) } + +// §5 OOM oracle at the floor breadth: the scheduled width's concurrent memory peak fits the +// fleet memory budget. A revert to a memory-blind width (= min(breadth, threads)) flips this +// false on the real fleet (7×14 GiB > 0.50×125 GiB budget). +fn gunbc_ci_floor_spawn_fits_memory_budget() -> Bool { + ci_fleet_floor_spawn_fits_memory_budget(corpus_shard_count: gunbc_ci_floor_breadth()) +}