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
2 changes: 1 addition & 1 deletion dag/gunbc/census_memo_seed_growth.dag
Original file line number Diff line number Diff line change
Expand Up @@ -51,5 +51,5 @@ data census_memo_seed_growth_justification: SeedGrowthJustification = SeedGrowth
reason: "Caching a host builtin is a property of the host that runs it. compile_dag_diagnostic_census_uncached is the unmemoized body, split out so the memoized entry point and the compile it caches stay one authority; compile_dag_diagnostic_census_memo_counts reports hits and misses so the memo's effect is measured rather than asserted -- both halves, because a hit count with no denominator is not a measurement. Neither decides anything: the census vocabulary they carry is unchanged and pre-existing, and the severity policy stays in compile_clean_diagnostic_is_hard.\n\nENUMERATED RATHER THAN COUNTED. Both are free functions, so the citable count and the real count are both two; nothing lands in seed_growth_uncitable_item_keys. The three added statics are not declarations and are disclosed in this file's header instead.\n\nPURITY IS THE REASON THE SECOND ITEM EXISTS AT ALL. The memo is armed only under the floor's prepared-inventory snapshot and keyed on the source TOGETHER WITH that inventory's content digest, because build_module_path_index_from_witness_roots reads those bytes and the census is a function of the corpus as well as of the source. Outside the guard there is no snapshot and the call falls through to the uncached item, so a hit can never assert something about disk that nothing established.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete both when compile_dag_diagnostic_census and its sibling compile_dag_rust_emit_check are MODELED operations rather than host builtins -- at which point their cache is the substrate's own Realization memoization on a content hash (DESIGN section 2, one kernel spanning resolve-cost to sccache) and a hand-rolled per-builtin map is exactly the duplicated caching authority that carrier dissolves. The two memos migrate together or not at all: leaving one hand-rolled beside a modeled sibling would be the fork this receipt's own single-authority argument refuses.",
current_boundary: "Confined to one call site and one process. The memo is thread-local, is consulted only inside compile_dag_diagnostic_census, and is unreachable outside the floor's prepared-inventory guard -- so no caller outside the required floor observes it at all. It changes no verdict: a hit returns the value the uncached body returned for the identical source under the identical inventory, and the cost split it makes visible is reported, never subtracted from what a claim is charged (that attribution is gunbc#9477's, not this row's)."
current_boundary: "Confined to one call site and one process. The memo is thread-local, is consulted only inside compile_dag_diagnostic_census, and is unreachable outside the floor's prepared-inventory guard -- so no caller outside the required floor observes it at all. It changes no verdict: a hit returns the value the uncached body returned for the identical source under the identical inventory. A MISS's fill interval is recorded through v1_compiler.cli_run record_shared_artifact_fill_cpu, the same accumulator the sibling emit-check memo writes, so the claim that pays a census compile is charged its marginal half and the fill is reported beside it. That bracket was NOT here when this receipt was first authored -- the attribution landed on the emit-check memo alone -- and the omission is what made test.claim.callable_candidate_ambiguity_witness .neither_green_source_refuses_and_neither_mis_resolves refuse the floor at 5812ms against the 5000ms fail-stop on main run 33131296988, having paid for two shared compiles that two later claims then read free. One accounting rule with two homes, applied in one of them, is the fork this receipt's own single-authority argument refuses."
}
37 changes: 35 additions & 2 deletions dag/gunbc/shared_fill_attribution_seed_growth.dag
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,39 @@ import std.decl_ref { DeclarationRef, WholeDeclaration }
// rather than minting a second one (operator ruling on gunbc#9477 -- reuse the existing
// provenance field rather than inventing an exemption).
//
// THE FORCING CLASS IS THE DISCRIMINATOR, AND THE THIRD STATE IS THE DEFECT. A shared artifact
// is in one of two arms depending on WHEN it can be forced, and the arm decides its treatment:
//
// PREPARATION-FORCEABLE -- every identity it can be asked for is knowable before the fold, so
// the floor BUILDS it ahead and bills preparation. both_closure_edge_index is this arm:
// run_required_floor warms it over both index identities its resolves can reach, and the run
// reports provenance=built-by-preparation. No claim window ever contains that build, which is
// why it correctly carries no fill bracket -- absence of a bracket is not evidence of a defect
// here, and reasoning from that absence is what this receipt exists to stop.
//
// CLAIM-FORCED -- what it will be asked for is a property of the claim, so it CANNOT be warmed
// ahead. A witness's synthetic source is not knowable before the fold. This arm must record
// its fill through record_shared_artifact_fill_cpu so run_claim_measured charges the marginal
// half and reports the shared half.
//
// THE THIRD STATE MUST NOT EXIST: claim-forced and unbracketed. Its cost lands entirely on
// whichever claim arrives first, and the number it produces is REAL -- a true measurement of
// something, charged to a row that does not own it -- so nothing looks wrong. The census memo was
// in this state from gunbc#9428 until this change, and it refused the required floor at 5812ms
// against a 5000ms fail-stop while two later claims read the same compiles free. The danger is
// worse than a wrong number: gunbc#9517 proposes freezing rows above the line in a shrink-only
// contract, and a row frozen for cost it does not own can never be made cheap, so it can never
// leave. A miswarded measurement becomes permanent.
//
// THIS PROSE IS NOT A WALL, AND SAYING SO IS PART OF THE ROW (DESIGN section 4b(1) -- the reported
// rung must be the rung executed evidence establishes). The two treatments are two hand-written
// call sites with no carrier relating them, so "claim-forced and unbracketed" stays WRITABLE and
// nothing refuses it; the next memo reintroduces the defect and this paragraph will not stop it.
// RUNG: mitigatable, on review diligence. NEXT-RUNG TRIGGER: a memoized host artifact DECLARES its
// forcing class and the warm-or-net treatment is DERIVED from that declaration, at which point the
// third state has no spelling and the bracket cannot be forgotten. That is a construction this
// change does not make and does not claim.
//
// WHY IT IS RUST AND NOT .dag. The measured subject is a host builtin. compile_dag_rust_emit_check
// runs the seed compiler synchronously and its memo lives beside it, so the fill interval exists
// only inside the host call; the substrate has no representation of that call to time. A
Expand All @@ -45,8 +78,8 @@ data shared_fill_attribution_seed_growth_justification: SeedGrowthJustification
DeclarationRef { module_path: "v1_compiler.cli_run", decl_name: "record_shared_artifact_fill_cpu", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.cli_run", decl_name: "shared_artifact_fill_cpu_nanos", field: WholeDeclaration }
],
reason: "Accounting for a host-side shared artifact is a property of the host that fills it. record_shared_artifact_fill_cpu accumulates the interval a MISS spent filling the shared emit-check memo; shared_artifact_fill_cpu_nanos reads that accumulator so run_claim_measured can subtract the shared half from the claim's own. Both exist because the two halves must be read at the same seam: a total with no split is the order-dependent number this change exists to remove.\n\nENUMERATED RATHER THAN COUNTED. Both are free functions, so the citable count and the real count are both two; nothing lands in seed_growth_uncitable_item_keys. The added thread-local is not a declaration and is disclosed in this file's header instead.\n\nTHE SPLIT IS REPORTED, NOT SILENTLY APPLIED. Every claim whose fill interval is nonzero emits a [floor-shared-fill] line naming the claim, its marginal CPU, the fill CPU and the measured total, so the subtraction is visible in the run that made it and can be disagreed with. A subtraction that only ever shrank a number without saying so would be an unaccounted widening of the safety limit -- the absorbing-fallback shape DESIGN section 5 forbids -- and the line is what keeps it a measurement instead.",
reason: "Accounting for a host-side shared artifact is a property of the host that fills it. record_shared_artifact_fill_cpu accumulates the interval a MISS spent filling a shared memoized host compile -- the emit-check memo and its census sibling both call it, because one accounting rule with two homes must be applied in both; shared_artifact_fill_cpu_nanos reads that accumulator so run_claim_measured can subtract the shared half from the claim's own. Both exist because the two halves must be read at the same seam: a total with no split is the order-dependent number this change exists to remove.\n\nWHICH ARTIFACTS MUST CALL IT is decided by forcing class, stated in this file's header: an artifact the floor can warm ahead of the fold is billed to preparation and needs no bracket, and an artifact only a claim can force must record its fill here. An artifact in neither arm is the defect, and it is a state this receipt describes rather than forbids -- the relation between the two treatments is prose, not a carrier, so nothing refuses a memo that declares no class.\n\nENUMERATED RATHER THAN COUNTED. Both are free functions, so the citable count and the real count are both two; nothing lands in seed_growth_uncitable_item_keys. The added thread-local is not a declaration and is disclosed in this file's header instead.\n\nTHE SPLIT IS REPORTED, NOT SILENTLY APPLIED. Every claim whose fill interval is nonzero emits a [floor-shared-fill] line naming the claim, its marginal CPU, the fill CPU and the measured total, so the subtraction is visible in the run that made it and can be disagreed with. A subtraction that only ever shrank a number without saying so would be an unaccounted widening of the safety limit -- the absorbing-fallback shape DESIGN section 5 forbids -- and the line is what keeps it a measurement instead.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete both when compile_dag_rust_emit_check and its census sibling are MODELED operations rather than host builtins -- at which point the shared artifact is the substrate's own Realization on a content hash, its fill is an ordinary node the cost model already sees, and attributing it by hand is the duplicated accounting authority that carrier dissolves. This receipt and gunbc.census_memo_seed_growth retire in the same change or neither does: they are the cache and the bill for one artifact, and separating them would leave a hand-rolled accounting beside a modeled one.",
current_boundary: "Confined to one process and one call site pair. The accumulator is thread-local, is written only on an emit-check MISS and is read only by run_claim_measured, so nothing outside the required floor observes it. It changes no verdict for any claim that fills nothing: with a zero fill interval the subtraction is the identity and no line is emitted. What it does change is a claim that pays for a shared compile, which is the whole point -- and the value it reports is the claim's own marginal cost, never a reduced form of the shared cost, which is still paid and still measured."
current_boundary: "Confined to one process and one call site pair. The accumulator is thread-local, is written only on a shared-memo MISS -- the emit-check memo and its census sibling, which are the two memoized host compiles the floor arms -- and is read only by run_claim_measured, so nothing outside the required floor observes it. It changes no verdict for any claim that fills nothing: with a zero fill interval the subtraction is the identity and no line is emitted. What it does change is a claim that pays for a shared compile, which is the whole point -- and the value it reports is the claim's own marginal cost, never a reduced form of the shared cost, which is still paid and still measured."
}
20 changes: 20 additions & 0 deletions src/v1/stage0/src/cli_run.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1994,7 +1994,27 @@ pub fn compile_dag_diagnostic_census(source: &str) -> CompileDiagnosticCensus {
return hit;
}
COMPILE_DAG_DIAGNOSTIC_CENSUS_MEMO_MISSES.fetch_add(1, std::sync::atomic::Ordering::Relaxed);
// A MISS FILLS A SHARED ARTIFACT, and this memo's fill is the same quantity its sibling's is.
// The memo above was landed without this bracket, so the census half of the attribution went
// unrecorded: `record_shared_artifact_fill_cpu` was wired into `compile_dag_rust_emit_check`
// only, and a claim that filled a CENSUS entry was still charged the whole compile. That is
// one accounting rule with two homes, one of which does not apply it (DESIGN §3) — and it is
// load-bearing rather than cosmetic, because the ceiling it feeds is a fail-stop: measured on
// main run 33131296988, `test.claim.callable_candidate_ambiguity_witness
// .neither_green_source_refuses_and_neither_mis_resolves` was the first claim to reach BOTH
// green sources, paid both compiles, and refused the floor at 5812ms against 5000ms, while the
// two later claims naming those same sources read them free. The number was a fact about
// discovery order, not about the row.
//
// NOTHING IS EXEMPTED. As at the sibling seam, the fill is measured on the same thread clock
// the claim loop enforces against, recorded rather than subtracted here, and reported by
// `run_claim_measured` as its own `[floor-shared-fill]` column — the claim's marginal and fill
// halves still sum to what it actually spent.
let fill_started = v1_interpreter::thread_cpu_nanos();
let census = compile_dag_diagnostic_census_uncached(source);
record_shared_artifact_fill_cpu(
v1_interpreter::thread_cpu_nanos().saturating_sub(fill_started),
);
Comment on lines +2013 to +2017

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 Exclude census fills from the in-evaluation deadline

When a census miss pushes total thread CPU over the claim limit and the witness subsequently reaches a stride poll (for example, it evaluates at least 4,096 further expressions), the poll in eval_expr still compares the unadjusted thread CPU against the original baseline and returns EvaluationBudgetExceeded. run_claim_measured only subtracts this newly recorded fill after evaluation has ended, so it cannot undo that refusal. As a result, census fill cost remains charged depending on the witness's post-census expression count, despite the intended marginal-cost attribution; the deadline baseline or polling calculation must be adjusted when recording the fill.

Useful? React with 👍 / 👎.

COMPILE_DAG_DIAGNOSTIC_CENSUS_MEMO.with(|m| m.borrow_mut().insert(memo_key, census.clone()));
census
}
Expand Down
Loading