kernel: store the conversion cache as flat integer arrays - #22319
Draft
JasonGross wants to merge 2 commits into
Draft
kernel: store the conversion cache as flat integer arrays#22319JasonGross wants to merge 2 commits into
JasonGross wants to merge 2 commits into
Conversation
A telescope-heavy kernel check compares the same pair of closures over and over: beta-substitution shares payload cells across every occurrence of a variable, so the same two cells meet again at each copy of the term they were substituted into. The reduction machine has no memory of this and re-derives each convertibility subproblem from scratch. Give each fconstr cell a stable id (a new lazily-assigned mutable field, preserved by the in-place [update] the machine uses for reduction and reset on every copy), and add a per-session table in `ccnv` mapping a pair of cell ids plus lift pair and conversion problem to the outcome (convertible or not). On a hit the outcome is replayed directly; both successes and failures are cached. Enabled only for checked conversion, where the result is a deterministic function of the fixed environment and no universe constraints are accumulated to replay; inference-mode conversion (which backtracks and discards constraints) never consults the cache. On by default; ROCQ_CONV_CACHE=0 disables it, ROCQ_CONV_CACHE_MAX bounds the table. Cuts the heaviest checked conversion we measured by ~4x.
The cache from the previous commit used a Hashtbl of boxed entries. On a heavy check that inserts ~60M entries within a single session, the entries themselves become the dominant cost: not the hashing, but the major GC tracing every one of those live boxed tuples and list cells. Everything in an entry is a small integer once lift values are interned: the cell-id pair packs into one machine int, and the interned lift ids, problem kind and result pack into a second. Store them in two int arrays with open addressing (linear probing, integer mix hash, doubling growth). No per-entry allocation and nothing for the GC to trace. Behaviour is unchanged (identical probe/hit/insert counts on the benchmark, digit for digit). On the heaviest check this is a further ~2.6x in time and drops peak memory by about a third.
coqbot-app
Bot
added
the
needs: full CI
Member
|
@coqbot bench |
Contributor
|
🏁 Bench results: 🐢 Top 25 slow downs┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 16.307 24.527 8.2200 50.41% 1515 coq-vst/floyd/VSU.v.html │ │ 16.212 24.077 7.8650 48.51% 1209 coq-vst/floyd/Component.v.html │ │ 16.355 23.672 7.3170 44.74% 1223 coq-vst/floyd/Component.v.html │ │ 6.09 11.5 5.4054 88.69% 196 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/HValuedSets.v.html │ │ 8.153 12.47 4.3170 52.95% 783 coq-vst/floyd/Component.v.html │ │ 8.109 12.083 3.9740 49.01% 1509 coq-vst/floyd/Component.v.html │ │ 2.82 5.26 2.4388 86.39% 160 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/HValuedSets.v.html │ │ 5.59 6.97 1.3765 24.62% 217 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 7.41 8.61 1.2012 16.22% 571 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 41.6 42.5 0.9163 2.20% 246 coq-category-theory/Construction/DecoratedCospan/Category.v.html │ │ 11.0 11.8 0.8352 7.59% 2300 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 50.6 51.4 0.7736 1.53% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 12.6 13.3 0.7264 5.76% 97 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/HValuedSets.v.html │ │ 202 203 0.7023 0.35% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 61.6 62.2 0.6280 1.02% 857 coq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v.html │ │ 1.006 1.539 0.5330 52.98% 1346 coq-vst/floyd/Component.v.html │ │ 0.586 1.12 0.5292 90.26% 298 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/HValuedSets.v.html │ │ 48.6 49.1 0.5285 1.09% 277 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 47.4 47.9 0.4853 1.02% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html │ │ 105 105 0.4575 0.44% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 2.38 2.83 0.4485 18.82% 8 coq-engine-bench-lite/coq/PerformanceDemos/repeated_conj.v.html │ │ 2.071 2.511 0.4400 21.25% 243 coq-vst/floyd/subsume_funspec.v.html │ │ 2.66 3.08 0.4273 16.09% 335 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 0.0130 0.438 0.4252 3267.04% 159 coq-mathcomp-analysis/theories/hoelder.v.html │ │ 0.0247 0.438 0.4133 1673.28% 130 coq-mathcomp-analysis/theories/lebesgue_integral_theory/measurable_fun_approximation.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 64.2 2.05 -62.1404 -96.80% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 64.1 2.06 -62.0551 -96.78% 608 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 50.6 0.0434 -50.5919 -99.91% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 45.1 10.1 -34.9765 -77.52% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 29.673 0.057 -29.6160 -99.81% 147 coq-vst/veric/expr_lemmas4.v.html │ │ 40.2 10.9 -29.2451 -72.76% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 29.229 0.025 -29.2040 -99.91% 194 coq-vst/veric/expr_lemmas4.v.html │ │ 25.4 0.252 -25.1035 -99.01% 550 coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 25.2 0.251 -24.9754 -99.01% 550 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 21.7 0.186 -21.5483 -99.14% 338 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 20.3 2.99 -17.3171 -85.27% 543 coq-unimath/UniMath/CategoryTheory/Presheaves/SigmaTypes.v.html │ │ 17.5 0.227 -17.2723 -98.70% 905 coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html │ │ 12.0 0.830 -11.1452 -93.07% 216 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 16.0 6.36 -9.6449 -60.25% 898 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 8.78 0.283 -8.4946 -96.77% 453 coq-unimath/UniMath/SyntheticHomotopyTheory/Circle2.v.html │ │ 11.7 6.58 -5.0983 -43.64% 118 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 5.029 0.102 -4.9270 -97.97% 407 coq-vst/floyd/for_lemmas.v.html │ │ 3.39 0.121 -3.2699 -96.43% 233 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/RecodeProofs.v.html │ │ 5.30 3.14 -2.1620 -40.78% 210 coq-fiat-crypto-with-bedrock/src/Demo.v.html │ │ 2.17 0.0542 -2.1167 -97.50% 243 coq-unimath/UniMath/ModelCategories/Examples.v.html │ │ 2.16 0.0528 -2.1118 -97.56% 459 coq-unimath/UniMath/ModelCategories/Examples.v.html │ │ 2.13 0.132 -2.0013 -93.83% 323 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/RecodeProofs.v.html │ │ 2.05 0.0937 -1.9609 -95.44% 348 coq-unimath/UniMath/CategoryTheory/Presheaf.v.html │ │ 2.19 0.573 -1.6157 -73.84% 515 coq-unimath/UniMath/CategoryTheory/Presheaves/PiTypesStable.v.html │ │ 235 234 -1.4839 -0.63% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
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
3 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.
Summary
This is a stacked follow-up to #22309. It replaces the conversion cache's
Hashtblof boxed entries with two flat integer arrays using open addressing.Please review #22309 first. The first commit in this draft is exactly that PR's current head; the new change is the second commit,
kernel: store the conversion cache as flat integer arrays. Once #22309 lands, this PR can be rebased to contain only the latter.Motivation
On the motivating Bonak check, the cache can grow to roughly 60 million entries in one conversion session. With boxed tuples and hash-table bucket lists, those entries become a substantial allocation and major-GC tracing cost.
Each entry is representable by two machine integers after lift values are interned:
The replacement table uses linear probing and doubles on growth. It allocates no object per entry, and its integer arrays do not add pointer fields for the GC to trace.
Performance evidence
The motivating heavy check retained identical probe, hit, and insertion counts digit-for-digit. Relative to the boxed cache in #22309, the flat representation reportedly gave a further approximately 2.6x runtime improvement and reduced peak memory by about one third.
This draft does not claim to solve all memory concerns noted on #22309: in particular, it does not remove the additional ID field from
fconstr. It specifically reduces the cache table's representation overhead.Validation
opam exec --switch=rocq-dev-testing -- dune build kernel/kernel.cmaopam exec --switch=rocq-dev-testing -- dune runtest kernelBoth pass locally.