Space bounds: measure the live-heap peak, and bound it statically - #151
Open
hhefesto wants to merge 3 commits into
Open
Space bounds: measure the live-heap peak, and bound it statically#151hhefesto wants to merge 3 commits into
hhefesto wants to merge 3 commits into
Conversation
The memory figure Meter.hs deliberately left undone. runMeter defunctionalized into a CEK machine whose values live in an explicit IntMap store: sharing is id-sharing, so the live heap is reachability from the machine's roots (environment, continuation frames, returning value) over distinct cells, and the peak is the maximum along the run. Retention needs no rule: a value a frame still holds is reachable. Steps and built tick exactly where runMeter's counters do, and the conformance suite now asserts that parity tick for tick alongside value agreement -- that is what keeps a third interpreter honest. Gate branches stay syntax in their frame, so the unchosen branch is never evaluated, same as the other evaluators. Two sweep policies: every allocation (exact, for tests) and adaptive (amortized, brackets the peak between a reached figure and a never- exceeded one). Sweeps drop unreachable nodes, which is what makes the bracket's upper end valid. The metered loop runs at the adaptive cadence, so a metered session now prints the peak alongside the step and build counts. The hand-computed fixtures pin what "live" means: a literal pair is its three cells; an argument referenced twice is counted once (a tree count of the same result reads 7 for a peak of 5); and a transient the result drops still shows up, growing with its size -- the retention case the sibling project's cost algebra could not see. The README's metered sample is refreshed from a measured run: its step and build counts had drifted. Profiling output joins .gitignore.
The same machine at compile time, over an abstract input. Bounds are maxima of affine expressions in input-part sizes -- sum of c_p * |p| plus a constant -- with dominated alternatives pruned, widening to pointwise-maximum coefficients, and substitution of the sizes a refinement pins. That language is what a static answer has to be: a program's peak depends on how big its input is, so a single number would be either wrong or vacuous. The walk runs on the sized term, so every recursion is a church tower it unrolls exactly its inferred count of times, and retention is measured on the abstract run by reachability rather than modelled by per-combinator rules -- the dead end design/SPACE.md records. The abstract input mirrors the sizing pass's initialInput: refinement- guaranteed pairs expand, refinement-guaranteed zeroes are concrete, and the rest are symbolic nodes whose cell bound is |p|. A gate on an unknown takes both branches and joins the values in a superposition whose frozen bound is the maximum of its sides' reachable subgraphs. Four things keep that from exploding, and together they are why tictactoe.tel converges -- 2.6M transitions under the default fuel, about eight seconds after sizing: - World-consistency tags, the sizing pass's filterLeft/filterRight discipline: a fork is about an input path, that commitment is in force while its branch runs, and a repeated test of the same unknown dispatches to the committed side instead of re-forking. k tests of one unknown cost two worlds, not 2^k. - A pointwise pair merge: a superposition of two pairs joins as a pair of superpositions, sound because a maximum of sums never exceeds the sum of maxima. Closure superpositions collapse to one closure over superposed environments, and nesting depth resets at every pair. - Widening of deep data superpositions, at supDepthCap = 4, guarded by a per-node has-function flag so a value that must still be applied is never reduced to a bound alone. Board cells touched by k moves stay bounded-depth instead of depth k, which is what keeps whoWon's nested gates from forking over an unbounded frontier. - Deep-forced peak and debt accumulators: left lazy, each allocation parked a thunk retaining the machine state it was made from, and the walk's memory grew with its history instead of its live set. A join memo, rare store pruning and a pin stack for ids the machine holds mid-transition keep the walk near 3.7M transitions a second, and the measuring sweep is amortized: fresh one-cell and symbolic-input allocations enter a debt, join-produced nodes measure on the spot, and last live plus debt bounds any intermediate live set because the store only grows between sweeps. sizeTermM hands back the InputRestrictions it already computes; the sizing report carries the bound lazily, so a plain run never forces the walk; the artifact encoding gains it and moves to version 3. The bound covers refinement-valid runs: a run on invalid input constructs and retains the failed check's aborted message, which is outside the restricted abstract input. The space meter now counts constructed aborted values so a harness can tell those runs apart, and the headline test asserts, on every corpus program, that the bound with actual input sizes substituted stands at or above the exactly measured peak of every abort-free iteration, and that at least one such iteration exists. simpleplus comes out at 116 input parts + 4337 cells; tictactoe at a maximum of thirteen affines whose largest constant, near ninety thousand cells, is about four times the measured peak of a completed game -- loose where a deep superposition is widened to its bound alone, but finite and sound.
The certificate gains a space section between sizing and structure: the bound as an expression over input-part sizes, stated for refinement- valid inputs (a run whose input fails a check builds and retains the aborted message, which is outside it), or an honest unknown with the reason it could not be found. --compile's summary line carries the same figure, so the line that says what was written also says what running it will cost. Affines over many input parts are summarized in report lines rather than spelled out path by path. The README's timings are refreshed from measured runs, since two of them had drifted: sizing tictactoe.tel takes about 13 seconds, not the 70 it claimed before the sizing pass got faster, the abstract walk adds some eight more, and the sample certificate's nesting columns are restated from real output.
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
1 participant
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.
Telomare certifies time — the sizing pass infers a concrete iteration count
for every recursion site and
--certificateprints the certified caps. It hasno memory figure at all. This branch adds one, on both sides: a measured
live-heap peak for a run, and a static bound over input sizes for the program,
with the second tested against the first on every corpus program.
Three commits, each one idea, fast-forwardable onto
master.Why it took until now
The codebase records two failed attempts, and they fail in opposite directions:
Eval/Meter.hscounts the nodes a runbuilds; counting what it holds as a tree counts shared structure once per
reference. Application in telomare is environment binding, so the residual is
a graph with heavy sharing — for
tictactoe.tela tree count reads about1.2TB for a run that fits in a few GB.
map sucover n elementsis Θ(n) live, and an algebra over combinators computes a constant.
Both are answered by the same move: evaluate over an explicit store so
sharing is id-sharing, and take the live heap as reachability over distinct
nodes from what the machine still holds. Retention needs no rule — a value a
frame still holds is reachable. Then run that same machine at compile time over
a symbolic input, and the bound falls out of the same reachability.
What lands
1. Measure the live-heap peak and report it from
--meterTelomare.Eval.Space: the reference interpreter defunctionalized into a CEKmachine over an
IntMapstore. Steps and builds tick exactly where the oldmeter's counters do, and the conformance suite asserts that parity tick for
tick — the drift guard for the rewrite. Two sweep policies: exact
(per-allocation, for tests) and adaptive (amortized, brackets the peak).
2. Bound the live-heap peak statically, over input sizes
Telomare.SpaceBound— maxima of affinesΣ c_p·|p| + kover input-partsizes, with dominance pruning, widening and substitution of refinement-pinned
sizes.
Telomare.Space.Static— the same machine over the sized term and anabstract input shaped by the sizing pass's own
InputRestrictions; a gate onan unknown takes both branches and joins them in a superposition. Convergence
on
tictactoe.telcomes from four things: world-consistency tags (k tests ofone unknown cost 2 worlds, not 2^k), a pointwise pair merge (a superposition of
pairs is a pair of superpositions), depth-capped widening guarded by a
has-function flag, and deep-forced accumulators.
sizeTermMhands back therestrictions it already computes; the sizing report carries the bound lazily;
the artifact moves to version 3 so a
.telcre-reports without re-walking.3. Report the space bound in the certificate and after
--compileOn
tictactoe.telthe bound is a maximum of thirteen affines whose largestconstant, 90,428 cells, is about four times the measured peak of a completed
game (15,640..20,473).
What it costs
A/B against
master(db63967) in a worktree, both built the same way (cabal-O1, GHC 9.10.3, same box), 3 runs each, median wall time:tictactoe.tel--certificate--compile--metersimpleplus.tel: certificate 0.109s → 0.135s, meter 0.097s → 0.111s.Where the time goes, isolated in one process: sizing 12.74s, abstract walk
7.97s (2,583,177 transitions, 661,011 allocations; 7.84s at
-O2, so this isthe walk's real cost, not a missing optimization). Three things worth knowing
about that table:
sizingReportSpaceis a lazyfield; only a report forces the walk. The +6% on the run is not the walk — it
is the extra live data surviving the sizing call (compiler max residency
1469MB → 1603MB in that run); sizing's hot path is untouched.
.telctakes0.043s; the artifact grew 57,651 → 64,745 bytes.
both sides. The walk adds ~22GB of allocation churn (9.1GB → 31GB total
allocation for a certificate run) and no peak.
How it is checked
test/SpaceTests.hs): on every corpus programand every refinement-valid iteration, the static bound with the actual input
sizes substituted stands at or above the exactly measured peak. Iterations
that fire an abort are detected via
spAbortsand skipped — an invalid inputbuilds and retains the failure message, which is outside the restricted
abstract input — and at least one comparison must remain, or the test fails
as vacuous.
test/ConformanceTests.hs): the space machine must agreewith the old meter on the value and on both counters, tick for tick.
version-refusal message for older files.
build counts, identical node count and source hash. The only new text in the
certificate is the space section.
Known looseness (documented, not soundness holes)
affine sits ~4x above the measured peak. Tightening candidates: sup-aware
sharing credit, and a canonical merge for small domains (a board cell is one
of three values).
so on its own line.
Also in here
The README's timings are restated from measured runs. Two had drifted before
this work: sizing
tictactoe.telis about 13 seconds, not the 70 the READMEclaimed (it predates the sizing speedup), and the sample certificate's nesting
columns and metered step counts no longer matched real output.
Reproducing the numbers