Skip to content
Closed
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
322 changes: 322 additions & 0 deletions dag/gunbc/floor/self_host_step_memory_demand.dag

Large diffs are not rendered by default.

25 changes: 25 additions & 0 deletions dag/gunbc/memory_composition_seed_growth.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
module gunbc.memory_composition_seed_growth

import gunbc.roadmap_model { RoadmapNodeId }
import gunbc.seed_growth { SeedGrowthJustification }
import std.decl_ref { DeclarationRef, WholeDeclaration }

// FORWARD-FREEZE RECEIPT for the hand Rust that writes the self-host step memory receipt read by
// gunbc.self_host_step_memory_demand. It measures and records; it decides nothing about the emission
// and it refuses (exit 2) rather than writing a partial receipt.
data memory_composition_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
hand_authored_declarations: [
DeclarationRef { module_path: "v1_compiler.cli_run.memory_composition", decl_name: "readback", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.memory_composition", decl_name: "release_stages", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.memory_composition", decl_name: "record_line", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.memory_composition", decl_name: "record_bucket", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.memory_composition", decl_name: "configuration_cell", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.pool_acquire", decl_name: "pool_shape", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.pool_acquire", decl_name: "drop_pool_heads_for_measurement", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run.pool_acquire", decl_name: "drop_pool_for_measurement", field: WholeDeclaration }
],
reason: "PURPOSE admission serves the v2 self-host program: the self-host step's slot envelope is sized from a peak nobody had decomposed, and the structures live in the seed's own thread-locals, which only the seed can read and release. The hooks are gated on an env var that selects a stopped-line audit, not a production behavior.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete these declarations when the instrument entry is a .dag-declared TargetProducer row (gunbc.target_binding) that reads the seed's structure sizes through a modeled host fact, or when ingestion is closure-scoped and the whole-tree structures no longer exist.",
current_boundary: "Two modules (review 78425): memory_composition, called from compile_emission_over at three readback seams plus the post-emission release, and the three pool_acquire measurement entries it calls for the two largest buckets -- a shape reading and two staged drops that run only after emission under the measurement env; the production path returns before them. It writes only the file named by GUNBC_MEMORY_COMPOSITION_RECEIPT and only when GUNBC_MEMORY_COMPOSITION is set; every written line carries GUNBC_MEMORY_COMPOSITION_CONFIGURATION as its last column.",
}
2 changes: 2 additions & 0 deletions dag/gunbc/seed_growth_admission.dag
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ import gunbc.keyed_declaration_read_seed_growth { keyed_declaration_read_seed_gr
import gunbc.keyed_dependency_edge_read_seed_growth { keyed_dependency_edge_read_seed_growth_justification }
import gunbc.host_crypto_digest_seed_growth { host_crypto_digest_seed_growth_justification }
import gunbc.census_memo_seed_growth { census_memo_seed_growth_justification }
import gunbc.memory_composition_seed_growth { memory_composition_seed_growth_justification }
import gunbc.fixture_render_selection_seed_growth { fixture_render_selection_seed_growth_justification }
import gunbc.fixture_closure_union_emit_seed_growth { fixture_closure_union_emit_seed_growth_justification }
import gunbc.fabric_door_socket_seed_growth { fabric_door_socket_seed_growth_justification }
Expand Down Expand Up @@ -323,6 +324,7 @@ fn seed_growth_justification_roster() -> List<SeedGrowthJustification> {
native_route_refusal_summary_seed_growth_justification,
native_route_advisory_summary_seed_growth_justification,
census_memo_seed_growth_justification,
memory_composition_seed_growth_justification,
fixture_render_selection_seed_growth_justification,
fixture_closure_union_emit_seed_growth_justification,
fabric_door_socket_seed_growth_justification,
Expand Down
101 changes: 101 additions & 0 deletions dag/test/claim/floor/self_host_step_memory_demand_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,101 @@
module test.claim.floor.self_host_step_memory_demand_witness_test

import std.types { Bool, String, NonEmptyStr, List, Int }
import std.algebra { list_append }
import std.measure { byte_size }
import std.process { ProcessExit, ExitSuccess, ExitFailure }
import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
import gunbc.self_host_step_memory_demand {
self_host_step_memory_readout_over, measured_lowering_holds, receipt_column,
self_host_step_memory_receipt_configuration, self_host_step_memory_structures, self_host_step_demand_trend,
StepPeakEffect, PeakLoweringMeasured, PeakLoweringExpected, PeakEffectUnclaimed,
}

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

// SUPPLIED-VALUE CLAIMS AT THE READER'S INTERFACE (DESIGN 3): the receipt rows are constructed here
// in the writer's own column layout rather than read from the committed file, so each refusal arm of
// self_host_step_memory_readout_over is exercised by execution with a designed red. The real file's
// execution is the instrument named in the module (gunbc run ... --function
// self_host_step_memory_readout), whose result the PR body records per receipt.

fn cfg() -> String { self_host_step_memory_receipt_configuration as String }

fn bucket_line(name: String, released: String, configuration: String) -> List<String> {
["bucket", name, released, "0", configuration]
}

fn stage_line(name: String, rss: String, configuration: String) -> List<String> {
["stage", name, rss, rss, configuration]
}

// Every classified structure, one line each, under the row's own configuration.
fn classified_bucket_lines(released: String) -> List<List<String>> {
map(self_host_step_memory_structures, s => bucket_line(name: s.receipt_name as String, released: released, configuration: cfg()))
}

// For every trend row that claims a MEASURED lowering, the two post_resolve lines it names, before above after.
fn measured_lowering_lines(before: String, after: String) -> List<List<String>> {
flat_map(self_host_step_demand_trend, t => match t.step_peak {
PeakLoweringMeasured { before_configuration: b, after_configuration: a } =>
[stage_line(name: "compile_emission_over.post_resolve", rss: before, configuration: b as String),
stage_line(name: "compile_emission_over.post_resolve", rss: after, configuration: a as String)]
PeakLoweringExpected { ground: _ } => []
PeakEffectUnclaimed => []
})
}

fn complete_rows() -> List<List<String>> {
list_append(
left: list_append(left: classified_bucket_lines(released: "1048576"), right: [stage_line(name: "compile_emission_over.post_emit", rss: "104857600", configuration: cfg())]),
right: measured_lowering_lines(before: "20000000", after: "10000000"))
}

fn is_success(exit: ProcessExit) -> Bool {
match exit {
ExitSuccess => true
ExitFailure { code: _, reason: _ } => false
}
}

test fn a_complete_receipt_holds() -> Bool {
is_success(exit: self_host_step_memory_readout_over(rows: complete_rows()))
}

test fn a_missing_structure_line_refuses() -> Bool {
!is_success(exit: self_host_step_memory_readout_over(rows: filter(complete_rows(), r => !(receipt_column(cols: r, index: 1) == "pool_heads" && receipt_column(cols: r, index: 0) == "bucket"))))
}

test fn a_malformed_bytes_cell_refuses() -> Bool {
let rows = map(complete_rows(), r => if receipt_column(cols: r, index: 0) == "bucket" && receipt_column(cols: r, index: 1) == "resolve_index" { bucket_line(name: "resolve_index", released: "n/a", configuration: cfg()) } else { r })
!is_success(exit: self_host_step_memory_readout_over(rows: rows))
}

test fn a_resident_bound_violation_refuses() -> Bool {
let rows = map(complete_rows(), r => if receipt_column(cols: r, index: 0) == "stage" && receipt_column(cols: r, index: 1) == "compile_emission_over.post_emit" { stage_line(name: "compile_emission_over.post_emit", rss: "4096", configuration: cfg()) } else { r })
!is_success(exit: self_host_step_memory_readout_over(rows: rows))
}

// The measured-lowering check at its own interface: both cells present with after below before holds;
// a missing before cell, or an after that is not below the before, refuses; expectations and unclaimed
// rows are never refused by it.
test fn a_measured_lowering_is_re_derived_from_both_cells() -> Bool {
let effect = PeakLoweringMeasured { before_configuration: "pool=held;scope=x;run=r" as NonEmptyStr, after_configuration: "pool=released;scope=x;run=r" as NonEmptyStr }
let both = [stage_line(name: "compile_emission_over.post_resolve", rss: "200", configuration: "pool=held;scope=x;run=r"),
stage_line(name: "compile_emission_over.post_resolve", rss: "100", configuration: "pool=released;scope=x;run=r")]
let after_only = [stage_line(name: "compile_emission_over.post_resolve", rss: "100", configuration: "pool=released;scope=x;run=r")]
let not_lower = [stage_line(name: "compile_emission_over.post_resolve", rss: "100", configuration: "pool=held;scope=x;run=r"),
stage_line(name: "compile_emission_over.post_resolve", rss: "100", configuration: "pool=released;scope=x;run=r")]
measured_lowering_holds(rows: both, effect: effect)
&& !measured_lowering_holds(rows: after_only, effect: effect)
&& !measured_lowering_holds(rows: not_lower, effect: effect)
&& measured_lowering_holds(rows: after_only, effect: PeakLoweringExpected { ground: "a bet" as NonEmptyStr })
&& measured_lowering_holds(rows: after_only, effect: PeakEffectUnclaimed)
}

// A receipt written by the writer before review 78427 has four-column bucket lines; the reader must
// refuse it rather than read a trimmed-only figure as a resident drop.
test fn a_four_column_bucket_line_from_the_old_writer_refuses() -> Bool {
let rows = map(complete_rows(), r => if receipt_column(cols: r, index: 0) == "bucket" && receipt_column(cols: r, index: 1) == "resolve_store" { ["bucket", "resolve_store", "1048576", cfg()] } else { r })
!is_success(exit: self_host_step_memory_readout_over(rows: rows))
}
29 changes: 29 additions & 0 deletions docs/plans/self-host-step-memory-audit.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
# Self-host step memory audit

Subject: the slot memory peak of `gunbc test //gunbc/instruments:self-host` and of
`//gunbc/instruments:v2-native-cli`. This page carries NO measured figure (DESIGN §6): every number
lives in the receipt the instrument wrote, and the model reads it.

- Receipt: `tools/self_host_step_memory_receipt.tsv` (line kinds `bucket` and `stage`, both written by the seed in one run; every line's last column is the configuration cell `GUNBC_MEMORY_COMPOSITION_CONFIGURATION`; the model selects on that column).
- Model and reader: `gunbc.self_host_step_memory_demand` (`dag/gunbc/floor/self_host_step_memory_demand.dag`). Re-derive the readout from the repo root, under a cgroup budget:
`gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/floor/self_host_step_memory_demand.dag --function self_host_step_memory_readout`
- Instrument, buckets: `GUNBC_MEMORY_COMPOSITION=1 GUNBC_MEMORY_COMPOSITION_RECEIPT=<file> GUNBC_MEMORY_COMPOSITION_CONFIGURATION=<cell> gunbc test //gunbc/instruments:self-host` (`src/v1/stage0/src/cli_run/memory_composition.rs`) appends one `bucket` line per released structure; the hook releases only after emission and only when the env is set.
- Instrument, stages: the same hook appends one `stage` line (resident set and VmHWM) at each seam inside the emission; the model's readout checks the buckets against the post-emission stage line of the same run.
- DECLARED FRONTIER, not in the receipt: the cgroup-level phase attribution (a 1 s sampler over `systemd-run --user --scope -p MemoryMax=22G -p MemorySwapMax=0` cut at the step's log seams, covering cargo/rustc and the controls) and the two-closure regression that splits the reconcile transient. The seed cannot write either. Trigger: an instrument entry (an `instrument_targets` row or a seed-side sampler) that writes `phase` lines into the same receipt; until then the figures for cargo/rustc are not claimed by this page or the model.

- DECLARED FRONTIER, closure scale: the entry-closure ASTs, resolution and typecheck environments and emission buffers are NOT measured, so the model carries no `EntryClosure` structure and asserts no ordering between tree-scale and moment-scale sums (the earlier `tree <= moment` check was true by construction of the table and is deleted). Trigger: a seed-side release stage that drops one of those structures and writes its `bucket` line; its row then enters `self_host_step_memory_structures` with `scale: EntryClosure`, and the readout may then assert the tree/closure split because a receipt can violate it.
- Writer failure: the seed refuses (exit 2, located stderr line) when a resident-set reading, a trim reading or a receipt write fails; a missing or partial receipt is therefore never a measurement, and the reader refuses an absent or duplicated line.

## What the receipt shows (read it there)
- The tree-scale structures (token pool, parsed heads, resolve index, path/graph caches) are `WholeTree` and are read as `bucket` lines.
- Whether demand is strictly decreasing: no. Tree-scale structures grow with the module count and nothing shrinks by itself; each ender in `self_host_step_demand_trend` is a named change.
- Which phase holds the step's high-water mark, and the rustc/product shares, are the sampler frontier above and are not asserted here.

## Provenance
The committed `tools/self_host_step_memory_receipt.tsv` is the unedited output of one instrumented run by this head's writer: `GUNBC_MEMORY_COMPOSITION=1 GUNBC_MEMORY_COMPOSITION_RECEIPT=<file> GUNBC_MEMORY_COMPOSITION_CONFIGURATION="pool=held_through_resolution;scope=srv1_systemd_scope_22g_swap0;run=smart-gull-336-20261010T1157Z" gunbc test //gunbc/instruments:self-host` on srv1 under `systemd-run --user --scope -p MemoryMax=22G -p MemorySwapMax=0` (exit 0). Every line carries that cell as its last column; bucket lines carry the full resident drop across release and `malloc_trim` and the trimmed figure beside it. Re-derive the readout with `gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/floor/self_host_step_memory_demand.dag --function self_host_step_memory_readout`.

## Levers and recommendation
Levers and the slot/trip recommendation are the lane report's, not this page's, because the pool-release lever is a production-path change measured in its own PR with its own receipt (dissolution trigger: closure-scoped ingestion). This page does not restate it.

## Consumption (DESIGN §3c)
Executing consumers in this change: `test.claim.floor.self_host_step_memory_demand_witness_test`, which runs `self_host_step_memory_readout_over` and `measured_lowering_holds` over supplied receipt rows (a complete receipt holds; a missing structure line, a malformed bytes cell, a resident-set bound violation and an unverifiable measured lowering refuse), and the readout entry itself over the committed receipt, `gunbc run --source-root dag --source-root src/v2 --entry dag/gunbc/floor/self_host_step_memory_demand.dag --function self_host_step_memory_readout`, whose exit each PR records. Declared frontier: a `gunbc test` label for the readout, which needs a `TargetProducer` arm in `gunbc.target_binding` and its seed arm (the trigger `gunbc.memory_composition_seed_growth` names); until then the readout is on no required path. `gunbc.runner_slot_desired` is on main and sizes the slot as a policy row; it does not import an effectful entry, so it is not a consumer of this module.
4 changes: 4 additions & 0 deletions src/v1/stage0/src/cli_run.rs
Original file line number Diff line number Diff line change
Expand Up @@ -202,6 +202,7 @@ pub(crate) use test_migration::*;
// and a second acquisition of the corpus to answer a second question is the cost-shape defect
// DESIGN §6 names.
pub(crate) mod floor_discovery_snapshot;
mod memory_composition;
#[path = "namespace_baseline.rs"]
pub mod namespace_baseline;
#[path = "phase_profile.rs"]
Expand Down Expand Up @@ -8320,10 +8321,12 @@ pub fn compile_emission_over(request: &CompileRequest, residency: IndexResidency
// path through this pair is the same computation it was before multi-target routing --
// not an equivalent-looking substitute (checked against that function's body, which is
// exactly that composition).
memory_composition::readback("compile_emission_over.pre_resolve");
let resolved = v1_compiler_compile::compile_to_resolved_with_options(
Rc::new(closure.clone().into()),
options,
);
memory_composition::readback("compile_emission_over.post_resolve");
let emissions: Vec<TargetEmission> = request
.render_targets
.iter()
Expand All @@ -8333,6 +8336,7 @@ pub fn compile_emission_over(request: &CompileRequest, residency: IndexResidency
})
.collect();

memory_composition::readback("compile_emission_over.post_emit");
// THE REFUSAL IS OVER EVERY TARGET, NOT THE FIRST. Emission is per target, so a target
// that emits nothing or emits a blocking diagnostic must stop the line even when an
// earlier target completed -- citing target 1 while target 2 is silent is the
Expand Down
Loading