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
88 changes: 6 additions & 82 deletions dsl/gunbc/ci_fleet.dag
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
// gunbc/ci_fleet.dag — Phase 3a-ours: gunbc CI fleet ComputeOffer meta-model.
// gunbc/ci_fleet.dag — gunbc CI runner identity (ComputeOffer → GitHub Actions runs-on labels).
//
// OUR self-hosted runner fleet instantiated as compute_fabric data. Concrete srv1/srv2
// operator inventory remains private (ctrl); this module is public-in-repo meta-modeling
// consumed by ci_workflow / ci_yaml_emit via gunbc_ci_runner_spec().
// OUR self-hosted runner as compute_fabric data, consumed by ci_workflow / ci_yaml_emit via
// gunbc_ci_runner_spec(). The memory-aware spawn-width modeling was removed (the floor pins a
// flat width); the real per-host fleet inventory lives in gunbc.operator_fleet.

module gunbc.ci_fleet

Expand All @@ -22,24 +22,16 @@ import product.compute_fabric {
OwnedMarginalZero,
PerJobFilesystem,
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, byte_size_count, hertz, hardware_thread_count, hardware_thread_count_value, HardwareThreadCount }
import std.measure { byte_size, hertz }
import std.os.types {
OperatingSystemSurface,
Linux,
Posix,
PosixProcess,
}
import product.placement_supply { HostIdentity, PlacementSupplyRow }
import product.placement_supply { HostIdentity }

data gunbc_ci_host_identity: HostIdentity = "gunbc-ci-fleet"

Expand All @@ -60,11 +52,6 @@ data gunbc_ci_host: ComputeHost = ComputeHost {
identity: gunbc_ci_host_identity,
baseboard: none,
processors: [CpuProcessor { cpu: gunbc_ci_cpu }],
// 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: [],
Expand Down Expand Up @@ -98,66 +85,3 @@ data gunbc_ci_fleet_offer: ComputeOffer = ComputeOffer {
fn gunbc_ci_runner_spec() -> RunnerSpec {
runner_spec_from_offer(offer: gunbc_ci_fleet_offer)
}

// Corpus parallel breadth is the CALLER's fact: the floor plan derives it from the
// single-authority spec (gates + corpus cardinality), so it is NOT a tuned constant.
// This keeps the §3 split honest — demand = the work (floor plan), supply = the fleet.
fn gunbc_ci_floor_corpus_work_demand(corpus_shard_count: Int) -> WorkDemand {
WorkDemand {
resources: ResourceEnvelope {
cpu: none,
gpu: 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,
},
os: none,
isolation: IsolationRequirement { boundary: PerJobFilesystem },
toolchains: [],
parallelism: IndependentShards { shard_count: corpus_shard_count },
data_locality: [],
effects: [],
}
}

fn gunbc_ci_floor_placement_supply() -> PlacementSupplyRow? {
offer_placement_supply_row(offer: gunbc_ci_fleet_offer)
}

// 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)
Present { value: row } =>
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)
}
}
}
}
125 changes: 125 additions & 0 deletions dsl/gunbc/operator_fleet.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,125 @@
// gunbc/operator_fleet.dag — the operator fleet inventory (srv1 + srv2 as compute-fabric hosts).
//
// srv1 + srv2 as real ComputeOffer values (ASRock Rack ALTRAD8UD-1L2T, Ampere Altra M128-30,
// 128c/128t, 128 GiB DDR4). PUBLIC in gunbc — we skip the private ctrl repo. The privacy
// boundary is handled in-repo: rotated BMC credentials are std.credentials handles (never
// committed); operator-private distro left absent. The operator owns the fleet (provider).
//
// Plain inventory — the spawn-width/allocator/placement modeling was removed as unwired
// complexity; this is the authority that CI/sessions/placement can derive from when a real
// consumer needs it.

module gunbc.operator_fleet

import gunbc.operator_fleet_network { operator_host_srv1, operator_host_srv2 }
import extdeps.cpu.ampere { altra_max_m12830_catalog }
import extdeps.cpu.types { CpuFacts, CpuDeploymentFacts }
import extdeps.boards.asrock_rack { asrock_altrad8ud_1l2t_catalog }
import std.baseboard { ServerBaseboard }
import std.bmc { BmcEndpoint, Redfish }
import std.credentials { CredentialFlow, Stored }
import std.measure { gibibyte, gibibyte_to_byte_size, hertz }
import std.os.types { OperatingSystemSurface, Linux, Posix, PosixProcess }
import std.types { List }
import product.compute_fabric {
ComputeOffer,
ComputeSupplyFacts,
ComputeHost,
ExecutionSurface,
MemoryDevice,
CpuProcessor,
AvailabilityWindow,
CostModel,
ProviderCostModel,
OwnedMarginalZero,
PerJobFilesystem,
Dram,
}

// Shared host facts (the two hosts are identical hardware).
data operator_fleet_cpu: CpuFacts = CpuFacts {
catalog: altra_max_m12830_catalog,
deployment: CpuDeploymentFacts { sustained_per_thread_hz: hertz(3000000000) },
}

data operator_fleet_os_surface: OperatingSystemSurface = OperatingSystemSurface {
kernel: Linux,
distro_or_product: none, // operator-private — resolved at runtime, never committed (skip-ctrl)
version: none,
filesystem_semantics: Posix,
process_semantics: PosixProcess,
}

// Baseboards (out-of-band BMC management plane).
data srv1_baseboard: ServerBaseboard = ServerBaseboard {
catalog: asrock_altrad8ud_1l2t_catalog,
bmc: BmcEndpoint { host: "192.168.1.183", protocol: Redfish },
}
data srv2_baseboard: ServerBaseboard = ServerBaseboard {
catalog: asrock_altrad8ud_1l2t_catalog,
bmc: BmcEndpoint { host: "192.168.1.184", protocol: Redfish },
}

// Rotated BMC credentials: HANDLES only, value NEVER committed (the skip-ctrl privacy).
data srv1_bmc_credential: CredentialFlow = Stored { secret_name: "bmc-srv1-admin" }
data srv2_bmc_credential: CredentialFlow = Stored { secret_name: "bmc-srv2-admin" }

data srv1_host: ComputeHost = ComputeHost {
identity: operator_host_srv1,
baseboard: Present { value: srv1_baseboard },
processors: [CpuProcessor { cpu: operator_fleet_cpu }],
memory: [MemoryDevice { capacity: gibibyte_to_byte_size(g: gibibyte(128)), memory_kind: Dram, bandwidth: none }],
storage: [],
network_interfaces: [],
}
data srv2_host: ComputeHost = ComputeHost {
identity: operator_host_srv2,
baseboard: Present { value: srv2_baseboard },
processors: [CpuProcessor { cpu: operator_fleet_cpu }],
memory: [MemoryDevice { capacity: gibibyte_to_byte_size(g: gibibyte(128)), memory_kind: Dram, bandwidth: none }],
storage: [],
network_interfaces: [],
}

fn operator_fleet_execution_surface() -> ExecutionSurface {
ExecutionSurface {
os: operator_fleet_os_surface,
isolation: PerJobFilesystem,
container_runtime: none,
toolchains: [],
mounted_storage: [],
network: [],
}
}

fn operator_owned_cost() -> CostModel {
CostModel { cost_class: OwnedMarginalZero, rates: ProviderCostModel { placeholder: true } }
}

data srv1_offer: ComputeOffer = ComputeOffer {
provider: "gunbc-operator-srv1",
supply: ComputeSupplyFacts {
physical: srv1_host,
execution: operator_fleet_execution_surface(),
cost: Present { value: operator_owned_cost() },
observed_performance: [],
},
available_window: AvailabilityWindow { open: "always-open", close: none },
cost_quote: none,
constraints: [],
}
data srv2_offer: ComputeOffer = ComputeOffer {
provider: "gunbc-operator-srv2",
supply: ComputeSupplyFacts {
physical: srv2_host,
execution: operator_fleet_execution_surface(),
cost: Present { value: operator_owned_cost() },
observed_performance: [],
},
available_window: AvailabilityWindow { open: "always-open", close: none },
cost_quote: none,
constraints: [],
}

// The fleet: the single inventory authority CI / sessions / placement derive from.
data operator_fleet_offers: List<ComputeOffer> = [srv1_offer, srv2_offer]
49 changes: 0 additions & 49 deletions dsl/product/compute_fabric.dag
Original file line number Diff line number Diff line change
Expand Up @@ -503,55 +503,6 @@ fn work_demand_shard_count(demand: WorkDemand) -> Int {
}
}

// 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 {
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 -------------------------------------------------------------

type ResourceEnvelope {
Expand Down
40 changes: 1 addition & 39 deletions src/v2/test/claim/ci_floor_plan_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,7 @@ 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_spawn_fits_memory_budget
}
import std.measure { hardware_thread_count_value }
import gunbc.ci_layer_roots { witness_discovery_scan_dirs, witness_layer_roots }
import v2.std.algebra { length, list_snoc_item }
import v2.std.collection { List }
Expand Down Expand Up @@ -103,37 +100,6 @@ fn witness_corpus_skip_node_frontier_enabled() -> Bool {
}
}

// 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
// supply that collapsed to one thread makes breadth/width 1 → this goes RED.
fn witness_floor_not_serial() -> Bool {
(gunbc_ci_floor_breadth() > 1) &&
(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() &&
Expand All @@ -142,9 +108,5 @@ test fn ci_floor_plan_witnesses() -> Bool {
witness_discovery_scan_dirs_in_plan() &&
witness_scan_dirs_match_layer_authority() &&
witness_corpus_has_no_explicit_entries() &&
witness_corpus_skip_node_frontier_enabled() &&
witness_spawn_width_bounded_by_breadth() &&
witness_floor_not_serial() &&
witness_floor_width_fits_memory_budget() &&
witness_floor_width_memory_bounded()
witness_corpus_skip_node_frontier_enabled()
}
18 changes: 5 additions & 13 deletions src/v2/workflow/ci_floor_plan.dag
Original file line number Diff line number Diff line change
Expand Up @@ -37,9 +37,8 @@ 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, ci_fleet_floor_spawn_fits_memory_budget }
import std.types { ContentHash }
import std.measure { HardwareThreadCount }
import std.measure { HardwareThreadCount, hardware_thread_count }
import std.realization_width { width_fold_objective_goals }
import std.realization_schedule {
RealizationPlan,
Expand Down Expand Up @@ -222,16 +221,9 @@ fn gunbc_ci_floor_breadth() -> Int {
length(xs: gunbc_ci_spec.gates)
}

// 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.
// claim_executor spawn-width companion (host never decides width). Pinned constant: the
// memory-aware placement model was unwired complexity; a flat width is what the fleet
// effectively ran. Re-derive from real load if it ever earns its keep.
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())
hardware_thread_count(4)
}