Optimize: ancestor-chain rewrite-cache reuse, large-table growth policy, opt-in retention diagnostics - #160
Open
colll78 wants to merge 10 commits into
Open
Conversation
…nd miscellaneous optimizations
Diagnostic instrumentation for the #prep_uplc memory blowup: every N driver iterations (BLASTER_RETENTION_EVERY, default 20000) append one flushed CSV line with the live entry count of every collection reachable from TranslateEnv, the driver stack depth, and VmRSS from /proc/self/status. Also one line on normal completion. Entirely gated on the BLASTER_RETENTION_PROFILE env var (the output path), read once at Optimize.mainAux entry. With it unset the only cost is one IO.Ref read per driver iteration (Retention.due short-circuits on a 0 sentinel) and nothing is opened or written -- zero behaviour change. Data/HashMap gains an O(capacity) 'vals' accessor (diagnostics only) so the nested tables (rewriteCache, the ContextMaps, contextReuseCache) can report total entries, not just key counts.
A full sample walks every table, so at a 20k-iteration period the 1600 prep emitted 2785 of them and ran 187 s instead of 66 s. Samples are now additionally rate limited to one per BLASTER_RETENTION_MIN_MS (default 2000); the iteration counter still advances by N on every period, so the iters column keeps its meaning. Measured at budget 1600: 64 s instrumented vs 69 s uninstrumented (within run-to-run noise), identical 2.87 GB peak. VmRSS parsing was returning 0 because the tab after the colon survived the split; take the digit run out of the trimmed remainder instead.
…rowth Counters (all gated on BLASTER_RETENTION_PROFILE, one IO.Ref read when off): - p0a: on a local rewrite-cache miss, 1-in-64-sampled probe of the global cache and every other active context for the same key (would-have-hit rate = the go/no-go for taint-bit global promotion) - p0b: iteSimp? else-branch contexts destroyed vs propagated, with the live-reuse-entry split (go/no-go for the asymmetric-restart fix) - p0c: constMatchPropagation?/constDITEPropagation? pull-out firings and inner/outer alt fan-out (case-of-case duplication exposure) - hypq: hash-cons interns attributed to hypothesis-query construction (inHypMap, notInHypMap, *InHyps, predCstLTInHyp) Growth policy (HashSet+HashMap growImpl): x4 below 2^20 slots, x2 above -- caps the hash-cons 2^28->2^30 step (~12 GB in one insert) at ~4.8 GB transient; predicted -1.2 GB RSS at budget 1900.
The 2^20 threshold taxed the whole run: steady-state load factor roughly doubles under x2 growth, and probe-chain lengthening on the hash-cons set (the hottest structure) measured +14.5% wall at budget 1900 (1719 s vs 1501 s baseline, profiler off). At 2^27 the x2 branch is unreachable below 201 M entries, so every capacity chain is identical to baseline x4 until exactly the resize that detonates a budget-2288 run: 2^28 -> 2^29 (+4.8 GB transient) instead of 2^28 -> 2^30 (~12 GB). Verified at 1900 profiler-off: 1554 s / 12.6 GB (baseline 1501 s / 13.5 GB), residual olean byte-identical (3,913,776 B).
findLocalCache now walks curCtx -> parents -> ... -> 0 (parents recorded by newCtx in the new OptimizeOptions.parents map) instead of probing only rewriteCache[curCtx]. Entries cached under an ancestor were derived from a subset of the current hypotheses, so returned equivalences remain valid in every descendant; the walk can only under-optimize, never unsound. Motivated by the p0a counters: 97.2-97.4% of local rewrite-cache misses would have hit in an active ancestor (budgets 1600/1700/1900). Measured at 1600 (instrumented): driver iterations 55.7M -> 25.9M (2.15x), hash-cons interns 13.7M -> 8.0M (-41%), RSS 2.86 -> 1.93 GB (-33%), p0a misses 12.2M -> 0.31M with active-hits 0. The residual CHANGES shape (631,880 -> 575,400 B, 9% smaller) but is equivalent: solve stanzas A and C both re-verify Valid in baseline time/memory (C: 114 s / 7.4 GB vs 90-102 s / 7.4 GB baseline).
… GC v1 (rejected: table doubles as DAG-visited set) Both changes are env-gated and DEFAULT OFF; committed as measured negative results with the data in-code. - walkMemoRef / BLASTER_MEMO_DEPTH: memoizing deep ancestor-walk hits into curCtx loses at both quick rungs (1600: 39.7 vs 36.9 s; 1700: 92.1 vs 87.2 s; residuals identical) -- insert traffic exceeds walk savings. - maybeGCHashCons / BLASTER_HASHCONS_GC: bulk-clearing the intern table hangs budget 1600 deterministically at ~12.7 M iterations: hashconsAux uses table hits as the DAG-visited set, so a cleared table makes the next hashcons of a shared DAG exponential. Spec for GC v2: mark-and-rebuild that FILTERS every PtrExpr/InstKey-keyed structure by reachability; nothing may be bulk-cleared mid-run. Also: corrected attribution -- true profiler-off 1600 for the ancestor build is ~37 s (1.79x over baseline); earlier 66 s reading was profiler overhead.
The complete arc, for the record: - Mechanism: threshold-triggered mark-and-rebuild (maybeGCv2): roots = driver stack + semantic env + ALL alive holders (memo caches keys+values, reuse scopes, original term via gcExtraRootsRef); pointer-closure mark (tagged-Nat GCAddr wrapper, single-probe inserts); filter table + InstKey caches by liveness; mask-selectable memo clear / map eviction; proportional rearm. All env-gated: BLASTER_HASHCONS_GC / BLASTER_GC_MASK. - THE two real defects, found by controlled bisection + a fresh-context diagnosis agent after six failed eviction-semantics theories: (1) every 'stall' was a TIMEOUT ARTIFACT -- rearm places fire input-output-hk#2 at ~99.5% of interning; its sweep ran 300+ s; all kill caps landed inside it (mask-33 with a 1200 s cap completed at 416 s, olean byte-identical); (2) the sweep cost was ONE loop: iterating LocalContext's PersistentArray decls directly in the deep monad = ~215 us/element (54.77 s of a 54.91 s sweep; all other sections 1-43 ms). Fix: decls.toArray then iterate (flat loops in the same monad do 800K pushes in 28 ms). Why PersistentArray.forIn degrades at our monad stack is unpinned (agent's isolation bench: 0.25 us/elem) -- see the hypothesis appendix in the diagnosis report. - Validated at 1600, 150 s caps, profiler on: observe 42.9 s/pause 2.6 s; EVICTING (mask 5) 44.7 s/pause 5.1 s/table 8.04M->3.49M (-57%); evict+clear (mask 7) 43.5 s. Iterations invariant (25,860,000) and residual BYTE-IDENTICAL (575,400 B) in all arms. - Temporary GCT section instrumentation (gated, marked TEMPORARY) kept for the 1700/1900 measurement runs; strip before upstreaming.
1900, profiler on, mask 134 (minimal roots + memo clear + InstKey filter): 538.7 s / 6.98 GB vs no-GC 565 s / 9.76 GB -- FASTER (-4.6%) and -28.5% memory, residual byte-identical, iterations identical (245,880,000: the re-derivation cost of evicting memo-reachable entries is zero here). 11 fires, ~6 s each; gc_live 32.3M -> 14.1M confirms the aggressive all-alive-holders rooting (a fix for the phantom stall) was the memory bottleneck of the GC itself. Wall win = memory-pressure dividend (round-2: superlinear wall growth is memory-driven).
…path) OptimizeOptions.chain mirrors the live scope stack as (ctxId, mapRef): maintained at the four curCtx transition sites (newCtx/setAndCommitCtx push, endCtx/resetChoiceContext pop), repointed on lazy map creation in updateLocalRewriteCache; walk steps drop from 4 dependent random loads to <=2; parents walk kept as invariant-checked fallback. Measured at 1900 (same-conditions A/B, oleans byte-identical): no-GC 565->537.5 s (-4.9%), GC m134 538.7->527.4 s (-2.1%) — consistent with the round-2 walk-tax bound. Micro-rung (1500) showed 1.55-1.95x but against a PRIOR-build baseline; recorded as a harness lesson: micro-rung deltas are bankable only same-build, back-to-back, box quiet.
This was referenced Sep 9, 2026
Open
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Optimize: ancestor-chain rewrite-cache reuse, large-table growth policy, and opt-in retention diagnostics
Stacked on #155 (
839c6f5is this branch's base — the diff vsmainincludes it; rebases cleanly when #155 merges). Direct follow-up to the #138 memory investigation, with production measurements from the CIP-153programmableLogicGlobalvalidator (3,444 term nodes, symbolicScriptContext,#prep_uplcat CEK budgets 1600–2100).1. Ancestor-chain rewrite-cache lookup (the headline change)
findLocalCachepreviously probed onlyrewriteCache[curCtx]. Instrumentation showed 97.2–97.4% of local-cache misses would have hit in an enclosing (active) context's cache — the driver was re-deriving already-computed rewrites at almost every miss, and this redundancy is the dominant super-linear cost driver (contexts multiply ~12× from budget 1600→2200 while per-context work stays flat).findLocalCachenow walkscurCtx → parent → … → 0via a new append-onlyOptimizeOptions.parentsmap recorded bynewCtx.Soundness: an entry cached under ancestor
Cwas derived using only hypotheses onC's scope chain — a subset of every descendant's hypotheses — so the recorded equivalence remains valid at any descendant probe. The walk can only under-optimize (a descendant's extra hypotheses might have simplified further), never produce an invalid rewrite.Measured (profiler off, vs this branch's base):
Driver iterations at 1600 drop 55.7 M → 25.9 M; hash-cons interns 13.7 M → 8.0 M. The residual term changes shape (~9–14% smaller, equivalent by construction); downstream
#solveobligations over the new residuals re-verify✅ Validin baseline time/memory.2. Table growth: ×2 above 2^27 slots (was ×4 everywhere)
The terminal memory burst reported in #138 is the hash-cons set's ×4 resize staircase: at 201 M entries the table steps 2^28→2^30, allocating ~9.7 GB of new arrays while 2.4 GB are still live — a ~12 GB single-insert spike. Above 2^27 slots the policy is now ×2 (2^28→2^29, ~4.8 GB transient). Below the threshold nothing changes, so small/medium runs keep ×4's low load factor — a 2^20 threshold was measured to cost +14.5% wall via probe-chain lengthening, hence the high cutoff.
3. Opt-in retention/behavior diagnostics (
BLASTER_RETENTION_PROFILE)CSV sampling of every collection reachable from
TranslateEnv(entry counts, RSS, driver iterations) plus the counters that motivated change 1. Fully inert unless the env var is set: the disabled cost is oneIO.Refread at each instrumented site. This is the instrumentation that produced the #138 memory-cliff data and the measurements above.Correctness evidence
#solvetheorems over this validator's 1600-step residual re-proveValidwith unchanged time/memory.lake build Blasterclean; no test-suite changes required.Impact on the #138 goal
The unshaped prep ceiling on a 61 GB machine moves from <2000 to ≥2000 CEK steps, and the cost curve's base drops from ~×2.9 to ~×2.6 per 100 steps. The workload's target rung (2288, the first non-vacuous containment-theorem budget) extrapolates from ~26 h / ~100 GB to ~5–6 h / 50–70 GB. Further reduction needs additional work on the remaining super-linear drivers; this PR is the measured first installment.
Second wave (
f313c65..9caca28): hash-cons GC, direct-ref scope chain, and an allocator findingThree new commits plus one zero-code operational discovery:
f313c65— hash-cons GC v2 (mark-and-rebuild; opt-in viaBLASTER_HASHCONS_GC=<threshold>+BLASTER_GC_MASK, default off)adfd199— minimal-roots marking (mask bit 128): live set 32.3 M → 14.1 M at 19009caca28— direct-ref scope chain for the ancestor walk (≤2 dependent loads per chain step vs 4 on theparents-map path)Second-wave config: retention profiler off, GC off,
MIMALLOC_GENERIC_COLLECT=1000000. Single runs, measured underperfsampling (≤2% overhead).Measurement re-baselining (part of the Δ is a correction, and it's stated here rather than pocketed). Re-measurement on this head shows the first-wave 1900/2000 walls are consistent with profiler-enabled runs — the CSV sampler's cost grows with rung (at 1600, one and the same build measures 66 s profiler-on / 37 s off). Strictly profiler-off walls on this head without the allocator knob are 411.9 s @1900 / 1499.5 s @2000. So the honest decomposition of the headline rows is: measurement correction + chain ≈ 565→412 and 1804→1500; the allocator knob provides the rest (−7.5% @1900, −37.7% @2000).
The allocator finding —
MIMALLOC_GENERIC_COLLECT=1000000. mimalloc (Lean bundles v2.2.3) runs a full heap-page walk every 10,000 generic allocations (_mi_malloc_generic→mi_heap_collect, optiongeneric_collect). Cost per fire ∝ heap pages, fire rate ∝ allocation rate, so the tax grows with the working set: CPU-profile share ~0% @1600 (1.9 GB heap) → 13.7% @1900 (9.7 GB) → 36.3% @2000 (16.4 GB). Raising the interval to its 1,000,000 clamp removes the symbol from the profile entirely; RSS is unchanged (this workload is retention-bound — there is little for the collector to reclaim, so the walks were near-pure overhead). Given the share curve, this is a prime suspect for the never-completing 2100 marathon (~21 GB, throughput collapse) — untested, flagged as extrapolation.GC v2 is a memory/feasibility tool, not a time win: at 1900 (mask 134, threshold 4 M) it holds RSS at 6.95 GB vs 9.75 GB (−29%) and the end-of-run intern table at 25.1 M vs 75.7 M entries (−67%), while wall stays neutral within the measured ±15% single-run band (3 replicates per arm; all arms perform identical work — driver iterations agree to the unit). Its value is headroom at the memory-governed rungs, composing with the growth-policy change above.
Correctness: all second-wave features are opt-in and default-off; with defaults, residual oleans are byte-identical to the first wave's across every intermediate build of this branch. GC arms at 1900 also produce byte-identical oleans (3,352,168 B).
Recommended operating point at large budgets:
MIMALLOC_GENERIC_COLLECT=1000000unconditionally; addBLASTER_GC_MASK=134 BLASTER_HASHCONS_GC=4000000when memory-bound. The first-wave 2288 extrapolation (~5–6 h) tightens by the top-rung factors above; a serious re-extrapolation belongs after a 2100 attempt under this operating point.