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
276 changes: 276 additions & 0 deletions dag/gunbc/floor/self_host_step_memory_demand.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,276 @@
module gunbc.self_host_step_memory_demand

import std.types { String, NonEmptyStr, Bool, List, Int }
import std.nat { Nat }
import std.measure { ByteSize, byte_size, measure_add, measure_le }
import std.algebra { trim }
import std.optional { Optional, Present, Absent }
import std.disposition { ConstructionMechanism, SingleAuthority }
import std.process { ProcessExit, ExitSuccess, exit_failure }
import extdeps.filesystem.filesystem_io { Filesystem, filesystem_read_outcome, FilesystemReadSucceeded, FilesystemReadRefused }

data self_host_step_memory_demand_disposition: ConstructionMechanism = SingleAuthority

// WHAT ONE `gunbc test //gunbc/instruments:self-host` (AND ITS SIBLING v2-native-cli) HOLDS, BY OWNER,
// BY SCALE AND BY THE CHANGE THAT ENDS IT. This module carries the CLASSIFICATION of each structure
// (owner, scale, ender: claims about the code, not measurements) and READS the bytes from the receipt
// the instrument wrote. It declares no byte figure of its own.
//
// THE RECEIPT is `tools/self_host_step_memory_receipt.tsv`, tab separated, one reading per line, ALL
// written by the seed itself under GUNBC_MEMORY_COMPOSITION=1 with
// GUNBC_MEMORY_COMPOSITION_RECEIPT=<path> during one `gunbc test //gunbc/instruments:self-host`:
// bucket <name> <bytes> what malloc_trim returned after releasing that structure
// stage <name> <rss> <peak_rss> the seed's own resident set at a seam inside the emission
// Nothing in the file is hand-assembled; the PR that commits it names the run that wrote it. What the
// seed cannot write (the cgroup sampler over rustc and the controls, the two-closure regression) is
// the declared frontier in docs/plans/self-host-step-memory-audit.md, not a line here.

type StepDemandOwner
= SeedProcess
| CargoAndRustc
| ProductUnderTest

// THE GROWTH AXES A STRUCTURE CAN HAVE, each naming what its bytes scale WITH:
// WholeTree -- the modules the seed acquires under the source roots, independent of the entry;
// EntryClosure -- the emitted entry's transitive closure (v2.compiler.compile's size);
// EmittedCrate -- the Rust crate rustc compiles, a consequence of the closure;
// Fixed -- the process baseline.
type StepDemandScale
= WholeTree
| EntryClosure
| EmittedCrate
| Fixed

// WHAT ENDS A STRUCTURE: a change, not a knob.
type StepDemandEnder
= ClosureScopedIngestion
| PoolReleasedAfterCensus
| PoolReleasedBeforeResolution
| NativeCompilerReplacesInterpreter
| ShrinksOnlyWithEmittedCrate
| NeverEnds

type StepMemoryStructure {
receipt_kind: NonEmptyStr
receipt_name: NonEmptyStr
structure: NonEmptyStr
owner: StepDemandOwner
scale: StepDemandScale
live_at_seed_peak: Bool
live_during_cargo: Bool
ender: StepDemandEnder
}

data self_host_step_memory_structures: List<StepMemoryStructure> = [
StepMemoryStructure { receipt_kind: "bucket", receipt_name: "resolve_store", structure: "shared resolve store (entry_resolve PROCESS_RESOLVE_STORE)", owner: SeedProcess, scale: WholeTree, live_at_seed_peak: true, live_during_cargo: true, ender: ClosureScopedIngestion },
StepMemoryStructure { receipt_kind: "bucket", receipt_name: "scope_and_reference_indexes", structure: "scope fragment, reference closure, scope order and reference edge caches (cli_run)", owner: SeedProcess, scale: WholeTree, live_at_seed_peak: true, live_during_cargo: true, ender: ClosureScopedIngestion },
StepMemoryStructure { receipt_kind: "bucket", receipt_name: "emit_check_and_census_memos", structure: "emit-check and diagnostic census memos (cli_run)", owner: SeedProcess, scale: WholeTree, live_at_seed_peak: true, live_during_cargo: true, ender: ClosureScopedIngestion },
StepMemoryStructure { receipt_kind: "bucket", receipt_name: "pool_content_tokens_newline", structure: "whole-tree token pool: V1LexArtifact + content + newline index of every pooled module (pool_acquire POOL)", owner: SeedProcess, scale: WholeTree, live_at_seed_peak: false, live_during_cargo: false, ender: ClosureScopedIngestion },
StepMemoryStructure { receipt_kind: "bucket", receipt_name: "pool_heads", structure: "whole-tree parsed heads (pool_acquire Acquired.heads)", owner: SeedProcess, scale: WholeTree, live_at_seed_peak: false, live_during_cargo: false, ender: ClosureScopedIngestion },
Comment on lines +68 to +69

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P1 Badge Do not classify the post-clear pool as whole-tree

The production path clears the whole-tree pool before resolution at cli_run.rs:7957, but release_stages measures its pool buckets only after emission. Consequently these rows can contain only an empty or subsequently reacquired subset, not the advertised token and heads data for every pooled module; treating them as WholeTree corrupts the audit's scale classification and trend conclusions.

Useful? React with 👍 / 👎.

StepMemoryStructure { receipt_kind: "bucket", receipt_name: "resolve_index", structure: "shared resolve index / name census (entry_resolve PROCESS_RESOLVE_INDEX)", owner: SeedProcess, scale: WholeTree, live_at_seed_peak: true, live_during_cargo: true, ender: ClosureScopedIngestion },
StepMemoryStructure { receipt_kind: "bucket", receipt_name: "module_graph_facts_and_path_index", structure: "module path index and graph facts caches (cli_run)", owner: SeedProcess, scale: WholeTree, live_at_seed_peak: true, live_during_cargo: true, ender: ClosureScopedIngestion },
]

// ── reading the receipt ─────────────────────────────────────────────────────────────────────────

data self_host_step_memory_receipt_path: NonEmptyStr = "tools/self_host_step_memory_receipt.tsv"

fn receipt_column(cols: List<String>, index: Int) -> String {
match cols.skip(n: index).first() {
Present { value: c } => trim(s: c)
Absent => ""
}
}

fn receipt_digit_value(c: String) -> Nat {
if c == "0" { 0 } else if c == "1" { 1 } else if c == "2" { 2 } else if c == "3" { 3 } else if c == "4" { 4 } else if c == "5" { 5 } else if c == "6" { 6 } else if c == "7" { 7 } else if c == "8" { 8 } else { 9 }
}

fn receipt_decimal_from(t: String, i: Int, acc: Nat) -> Nat {
if i >= string_length(s: t) { acc } else { receipt_decimal_from(t: t, i: i + 1, acc: acc * 10 + receipt_digit_value(c: char_at(s: t, pos: i))) }
}

fn receipt_is_decimal_from(t: String, i: Int) -> Bool {
if i >= string_length(s: t) { true } else { char_at(s: t, pos: i) >= "0" && char_at(s: t, pos: i) <= "9" && receipt_is_decimal_from(t: t, i: i + 1) }
}

fn receipt_is_decimal(t: String) -> Bool {
t != "" && receipt_is_decimal_from(t: t, i: 0)
}

fn receipt_rows(text: String) -> List<List<String>> {
map(filter(split(s: text, delimiter: "\n"), l => l != "" && char_at(s: l, pos: 0) != "#"), l => split(s: l, delimiter: "\t"))
}

// A reading the receipt may not hold: Absent is the refusal case (no, an ill-formed, or a duplicated
// line), never a number. Every sum below goes through it and so stays Absent if any term is.
fn bytes_none() -> Optional<ByteSize> {
Absent
}

fn bytes_some(b: ByteSize) -> Optional<ByteSize> {
Present { value: b }
}

fn receipt_bytes_at(rows: List<List<String>>, kind: String, name: String) -> Optional<ByteSize> {
let found = filter(rows, r => receipt_column(cols: r, index: 0) == kind && receipt_column(cols: r, index: 1) == name)
if length(xs: found) != 1 { bytes_none() } else {
match found.first() {
Present { value: r } =>
if receipt_is_decimal(t: receipt_column(cols: r, index: 2)) { bytes_some(b: byte_size(count: receipt_decimal_from(t: receipt_column(cols: r, index: 2), i: 0, acc: 0))) } else { bytes_none() }
Absent => bytes_none()
}
}
}

fn receipt_structure_bytes(rows: List<List<String>>, s: StepMemoryStructure) -> Optional<ByteSize> {
receipt_bytes_at(rows: rows, kind: s.receipt_kind as String, name: s.receipt_name as String)
}

// The seed's resident set at one named seam of the same run.
fn receipt_stage_rss(rows: List<List<String>>, stage: String) -> Optional<ByteSize> {
receipt_bytes_at(rows: rows, kind: "stage", name: stage)
}

fn step_structures_unreadable(rows: List<List<String>>) -> List<StepMemoryStructure> {
filter(self_host_step_memory_structures, s => match receipt_structure_bytes(rows: rows, s: s) { Present { value: _ } => false Absent => true })
}

fn step_structure_sum(rows: List<List<String>>, chosen: List<StepMemoryStructure>) -> Optional<ByteSize> {
fold(chosen, init: bytes_some(b: byte_size(count: 0)), f: (acc, s) => match acc {
Absent => bytes_none()
Present { value: a } => match receipt_structure_bytes(rows: rows, s: s) {
Absent => bytes_none()
Present { value: b } => bytes_some(b: measure_add(a: a, b: b))
}
})
}

// WHAT IS LIVE at the seed's moment, summed from the receipt.
fn step_seed_moment_bytes(rows: List<List<String>>) -> Optional<ByteSize> {
step_structure_sum(rows: rows, chosen: filter(self_host_step_memory_structures, s => s.live_at_seed_peak))
}

// ── THE TREND, AS A ROW ─────────────────────────────────────────────────────────────────────────
//
// IS THE DEMAND STRICTLY DECREASING OVER TIME? NO, and the row says what would make it so. Over a
// growing corpus every WholeTree bucket grows monotonically with the module count (the seed pools and
// censuses the whole tree to emit one closure), and the EntryClosure bucket grows with
// v2.compiler.compile's own size; neither shrinks on its own. The demand falls only under a named
// change, and each change removes a SET of buckets, so the trend is a staircase that is flat or rising
// between changes, never a slope.
type StepDemandTrend {
change: StepDemandEnder
removes_scale: StepDemandScale
removes_from_seed_peak: Bool
removes_from_cargo_phase: Bool
lowers_step_peak: Bool
evidence: NonEmptyStr
}

data self_host_step_demand_trend: List<StepDemandTrend> = [
StepDemandTrend {
change: PoolReleasedAfterCensus,
removes_scale: WholeTree,
removes_from_seed_peak: false,
removes_from_cargo_phase: true,
lowers_step_peak: false,
evidence: "the staged release at the cargo seam is a read obligation: the receipt carries the seed's own seams only, so the cargo-phase effect is the declared sampler frontier; the pool is still needed by the seed's own resolution stage",
},
StepDemandTrend {
change: PoolReleasedBeforeResolution,
removes_scale: WholeTree,
removes_from_seed_peak: true,
removes_from_cargo_phase: true,
lowers_step_peak: true,
evidence: "the counterfactual is a production-path change and is measured in its own PR's receipt, not here; this row records only that the pool buckets are tree-scale and live at the seed moment",
},
StepDemandTrend {
change: ClosureScopedIngestion,
removes_scale: WholeTree,
removes_from_seed_peak: true,
removes_from_cargo_phase: true,
lowers_step_peak: true,
evidence: "every WholeTree structure in the receipt is built from the pooled modules of which almost all are compiled for the census only",
},
StepDemandTrend {
change: NativeCompilerReplacesInterpreter,
removes_scale: EntryClosure,
removes_from_seed_peak: true,
removes_from_cargo_phase: false,
lowers_step_peak: true,
evidence: "the native generation-two compiler would hold its own closure working set instead of the interpreter's; its footprint has not been measured and this row claims none",
},
StepDemandTrend {
change: ShrinksOnlyWithEmittedCrate,
removes_scale: EmittedCrate,
removes_from_seed_peak: false,
removes_from_cargo_phase: true,
lowers_step_peak: false,
evidence: "rustc's footprint scales with the emitted crate; it is read by the cgroup sampler, which is the declared frontier and not a line in the receipt, so this row is a classification not a reading",
},
]


// DECLARED FRONTIER (DESIGN 3c): this module has no executing consumer on the base this PR is cut
// from. The consumer it is built for is slot sizing: the cold-run receipt row of gunbc.cutover_receipt
// and the note of gunbc.runner_slot_desired, which take this readout as the carrier of the per-step
// memory figure. Trigger: those modules import it, on a base that carries them.

// A trend row must exist for every classified structure's ender and scale (NeverEnds excepted): the
// classification and the trend are one claim about what ends each structure, so a structure whose
// ender no row speaks to is refused rather than left classified-but-unexplained.
fn structure_has_trend_row(s: StepMemoryStructure) -> Bool {
let spoken_to = any(self_host_step_demand_trend, t => t.change == s.ender && t.removes_scale == s.scale)
match s.ender {
NeverEnds => true
ClosureScopedIngestion => spoken_to
PoolReleasedAfterCensus => spoken_to
PoolReleasedBeforeResolution => spoken_to
NativeCompilerReplacesInterpreter => spoken_to
ShrinksOnlyWithEmittedCrate => spoken_to
}
}

// THE READOUT. Reads the receipt the instrument wrote and refuses unless every classified structure
// has exactly one well-formed line, every structure has a trend row, and the structures live at the
// seed's moment fit inside the seed's own resident set at the post-emission seam of the same run
// (a plain resident-set read, a different reading from the trim that produced the buckets).
//
// THE BOUND. Every bucket is a KB-granular resident-set difference, so a bucket can exceed its true
// size by less than one KB and the sum of N buckets by less than N KB: the tolerance is
// structure_count * 1024 bytes and nothing larger. A receipt violates it by reporting buckets that
// together return more than the seed held resident. The classified structures are a LOWER bound on
// the resident set, not a partition of it: the unclassified remainder (the closure-scale ASTs,
// resolution and typecheck environments, emission buffers, allocator baseline) is the declared
// frontier of docs/plans/self-host-step-memory-audit.md, so no check here asserts coverage or
// scale ordering.
fn self_host_step_memory_readout() -> ProcessExit {
let read = Filesystem.Read(path: self_host_step_memory_receipt_path as String)
match filesystem_read_outcome(content: read.content, success: read.success, error: read.error) {
FilesystemReadRefused { error } => exit_failure(reason: concat("self-host step memory receipt unreadable: ", error))
FilesystemReadSucceeded { content } => self_host_step_memory_readout_over(rows: receipt_rows(text: content))
}
}

fn self_host_step_memory_readout_over(rows: List<List<String>>) -> ProcessExit {
if length(xs: step_structures_unreadable(rows: rows)) > 0 {
exit_failure(reason: "the receipt lacks exactly one well-formed line for a classified structure")
} else if length(xs: filter(self_host_step_memory_structures, s => !structure_has_trend_row(s: s))) > 0 {
exit_failure(reason: "a classified structure has no trend row for its ender and scale")
} else {
match receipt_stage_rss(rows: rows, stage: "compile_emission_over.post_emit") {
Absent => exit_failure(reason: "the receipt has no post-emission stage line")
Present { value: resident } =>
match step_seed_moment_bytes(rows: rows) {
Absent => exit_failure(reason: "the structures live at the seed's moment are not all readable")
Present { value: moment } =>
if !measure_le(a: moment, b: measure_add(a: resident, b: byte_size(count: length(xs: self_host_step_memory_structures) * 1024))) {
exit_failure(reason: "the structures live at the seed's moment exceed the seed's own resident set at that seam beyond KB rounding")
} else {
ExitSuccess
}
}
}
}
}
21 changes: 21 additions & 0 deletions dag/gunbc/memory_composition_seed_growth.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
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 }
],
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: "One module, called from compile_emission_over at three readback seams plus the post-emission release; writes only the file named by GUNBC_MEMORY_COMPOSITION_RECEIPT and only when GUNBC_MEMORY_COMPOSITION is set.",
}
22 changes: 22 additions & 0 deletions dag/gunbc/pool_release_after_census_seed_growth.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
module gunbc.pool_release_after_census_seed_growth

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

// FORWARD-FREEZE RECEIPT for the one hand Rust item that releases the seed's whole-tree acquisition
// pool once the pre-entry census has finished. It deletes retention past the last demand; it adds no
// arm, no mode and no decision. The measurement that motivated it is the audit
// instrument of gunbc.self_host_step_memory_demand (`gunbc test //gunbc/instruments:self-host` with
// GUNBC_MEMORY_COMPOSITION_RECEIPT set), re-derived per head, never transcribed here; the derivation
// is the doc comment on pool_acquire release_whole_tree_after_census, and the measurement is its
// adversary, not its justification.
data pool_release_after_census_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
hand_authored_declarations: [
DeclarationRef { module_path: "v1_compiler.cli_run.pool_acquire", decl_name: "release_whole_tree_after_census", field: WholeDeclaration }
],
reason: "PURPOSE admission serves the v2 self-host program: the self-host gate's slot envelope is set by the seed process holding the whole-tree pool beside the closure's resolution. The pool is a host structure of the seed's acquisition, so its release is a property of the host that built it; the substrate has no representation of it to attach the release to. The change is unconditional on the production path and has no env gate or mode.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete this declaration and justification when ingestion is closure-scoped, so that the seed never builds a whole-tree pool and there is nothing to release: the census then reads per-module content-keyed facts for the closure only.",
current_boundary: "One call site, in compile_emission_over immediately before compile_to_resolved_with_options, one thread-local, one process. It changes no verdict: a later demand for a released file takes the pool's own miss path and re-acquires the identical bytes.",
}
Loading
Loading