Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
033441f
WIP: Wave 3c-F FINISH-LINE-B Arc 1: eager-materialize the exemplared …
briansrls Jun 19, 2026
cf702e1
WIP: Wave 3c-F FINISH-LINE-B Arc 1: eager-materialize the exemplared …
briansrls Jun 19, 2026
89e4523
WIP: Wave 3c-F FINISH-LINE-B Arc 1: eager-materialize the exemplared …
briansrls Jun 19, 2026
7c2e339
WIP: Wave 3c-F FINISH-LINE-B Arc 1: eager-materialize the exemplared …
briansrls Jun 20, 2026
e2f3d3a
WIP: CI is extremely flakey
briansrls Jun 20, 2026
7625f84
floor spawn_width: derive from spec breadth (no hand-tuning) + discri…
briansrls Jun 20, 2026
412206f
review nit: use length(gates) instead of fold-count for breadth
briansrls Jun 20, 2026
87f61f5
WIP: Wave 3c-F FINISH-LINE-B Arc 1: eager-materialize the exemplared …
briansrls Jun 20, 2026
ffd13e0
WIP: Wave 3c-F FINISH-LINE-B Arc 1: eager-materialize the exemplared …
briansrls Jun 20, 2026
73cf952
Merge remote-tracking branch 'origin/main' into session/fierce-raven-…
briansrls Jun 20, 2026
215e542
Merge remote-tracking branch 'origin/main' into session/warm-crane-135
briansrls Jun 20, 2026
1ddc7ae
WIP: CI is extremely flakey
briansrls Jun 20, 2026
70a11f9
WIP: Wave 3c-F FINISH-LINE-B Arc 1: eager-materialize the exemplared …
briansrls Jun 20, 2026
00d9eda
Merge origin/main (028022c2d0: #5356 floor spawn_width 1→7 + bash hot…
briansrls Jun 20, 2026
f8e874c
fix(Arc 1): drop duplicate whole-corpus self-emit witness (OOM exit 137)
briansrls Jun 20, 2026
4bd78d0
WIP: CI is extremely flakey
briansrls Jun 20, 2026
d50c13b
fix(ci-floor): memory-aware spawn_width — bound batch-2 fan-out by cg…
briansrls Jun 20, 2026
acb1fd3
WIP: CI is extremely flakey
briansrls Jun 20, 2026
6d7a3a9
fix: resolve auto-committed merge conflict markers (take memory-aware…
briansrls Jun 20, 2026
60490b4
TEST ONLY: Arc 1 corpus + #5375 memory-aware spawn_width (validate wi…
briansrls Jun 20, 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
46 changes: 40 additions & 6 deletions dsl/gunbc/ci_fleet.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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: [],
}
Expand Down Expand Up @@ -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,
},
Expand All @@ -117,13 +130,34 @@ 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)
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)
}
}
}
}
53 changes: 46 additions & 7 deletions dsl/product/compute_fabric.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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<T>` container.
Expand Down Expand Up @@ -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 -------------------------------------------------------------
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,18 @@
module v2.test.manual.typescript_derive_grammar_relation_row_round_trip

import v2.extdeps.languages.typescript {
ts_eager_grammar_relation_row_witness,
ts_exemplar_emitted_for_lhs,
ts_formal_production_mvp1_fn_add,
ts_grammar_relation_row_node,
ts_inhabitant_atom,
ts_mvp1_emitted_add_fn_node,
ts_mvp1_fn_add_scaffold_relation_row_node,
ts_mvp1_grammar_relation_row,
ts_mvp1_canonical_add_fn_tokens,
ts_concrete_token_node,
ts_pr3_identity_relation_row_witness,
ts_pr3_identity_typed_fn_emitted,
ts_wave2a_task_formal_productions,
ts_wave2a_task_type_alias_emitted,
ts_wave2a_task_type_alias_relation_row_witness,
Expand Down Expand Up @@ -175,6 +180,28 @@ data claim_typescript_derive_grammar_relation_row_arrow_emitted_rejects: TestCla
classification: TestClassification { tier: Tier1, layer: Unit }
}

fn ts_pr3_identity_derive_row_round_trip_holds() -> Bool {
match ts_pr3_identity_relation_row_witness() {
Holds { value: eager_row } =>
match ts_eager_grammar_relation_row_witness(lhs: ^ts_production_pr3_typed_fn_decl) {
Holds { value: rederived } =>
content_hash(n: eager_row) == content_hash(n: rederived)
Violates { diagnostic: _ } => false
}
Violates { diagnostic: _ } => false
}
}

data claim_typescript_pr3_identity_derive_grammar_relation_row_round_trip: TestClaim = CompilesClaim {
label: "T-11 FINISH-LINE-B Arc 1: pr3_identity eager row content_hash round-trips derive_grammar_relation_row_node",
anchor: manual_claim_anchor(anchor: ManualAnchorAbsent),
input: ts_grammar_relation_round_trip_claim_input(
ok: ts_pr3_identity_derive_row_round_trip_holds()
),
expected_value: ts_grammar_relation_round_trip_pass_node(),
classification: TestClassification { tier: Tier1, layer: Unit }
}

data claim_typescript_derive_grammar_relation_row_surplus_conj_rejects: TestClaim = CompilesClaim {
label: "T-11 PR-1.5b: derive_grammar_relation_row_node rejects emitted Conj with surplus positional child",
anchor: manual_claim_anchor(anchor: ManualAnchorAbsent),
Expand Down
Loading
Loading