kernel: cache conversion results within a session - #22309
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.
coqbot-app
Bot
added
the
needs: full CI
|
I might be missing something, but I do not understand the point of the |
|
How do you hash physical equality to use it as a hashtbl key? |
|
@coqbot run full ci |
coqbot-app
Bot
removed
the
needs: full CI
|
@coqbot bench |
|
🏁 Bench results: 🐢 Top 25 slow downs┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 15.972 51.917 35.9450 225.05% 1209 coq-vst/floyd/Component.v.html │ │ 16.059 51.489 35.4300 220.62% 1223 coq-vst/floyd/Component.v.html │ │ 15.975 48.456 32.4810 203.32% 1515 coq-vst/floyd/VSU.v.html │ │ 12.4 38.8 26.3486 212.28% 97 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/HValuedSets.v.html │ │ 6.01 30.8 24.7800 412.33% 196 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/HValuedSets.v.html │ │ 8.031 26.518 18.4870 230.20% 1509 coq-vst/floyd/Component.v.html │ │ 8.019 24.017 15.9980 199.50% 783 coq-vst/floyd/Component.v.html │ │ 2.76 13.5 10.7721 389.83% 160 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/HValuedSets.v.html │ │ 7.50 16.7 9.2379 123.16% 136 coq-unimath/UniMath/CategoryTheory/Actegories/Examples/ActionOfEndomorphismsInCATElementary.v.html │ │ 2.019 5.018 2.9990 148.54% 243 coq-vst/floyd/subsume_funspec.v.html │ │ 35.3 38.1 2.8415 8.06% 898 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 10.2 13.0 2.7356 26.74% 2300 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 0.577 3.22 2.6418 458.02% 298 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/HValuedSets.v.html │ │ 3.23 5.75 2.5182 77.89% 118 coq-unimath/UniMath/Semantics/LinearLogic/LiftingModel.v.html │ │ 2.19 4.03 1.8380 83.84% 265 coq-unimath/UniMath/CategoryTheory/Chains/OmegaContFunctors.v.html │ │ 2.33 4.09 1.7583 75.37% 8 coq-engine-bench-lite/coq/PerformanceDemos/repeated_conj.v.html │ │ 49.6 51.3 1.7150 3.46% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 5.58 7.20 1.6120 28.86% 217 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 77.4 79.0 1.5399 1.99% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 42.7 44.0 1.2947 3.03% 221 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 103 104 1.2090 1.18% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 0.984 2.19 1.2060 122.56% 1346 coq-vst/floyd/Component.v.html │ │ 31.5 32.6 1.1570 3.68% 255 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html │ │ 61.8 62.9 1.1176 1.81% 857 coq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v.html │ │ 39.8 40.9 1.1055 2.78% 246 coq-category-theory/Construction/DecoratedCospan/Category.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 67.8 2.67 -65.1436 -96.06% 608 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 63.2 2.65 -60.5878 -95.81% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 50.0 0.0461 -49.9238 -99.91% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 29.205 0.064 -29.1410 -99.78% 147 coq-vst/veric/expr_lemmas4.v.html │ │ 28.819 0.041 -28.7780 -99.86% 194 coq-vst/veric/expr_lemmas4.v.html │ │ 24.6 0.247 -24.3802 -99.00% 550 coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 24.4 0.247 -24.1583 -98.99% 550 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 44.2 20.3 -23.9189 -54.11% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 21.4 0.199 -21.2358 -99.07% 338 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 39.5 21.4 -18.0380 -45.69% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 18.0 0.239 -17.7681 -98.68% 905 coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html │ │ 11.7 0.906 -10.8086 -92.26% 216 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 16.0 6.91 -9.0716 -56.77% 898 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 8.63 0.489 -8.1375 -94.33% 453 coq-unimath/UniMath/SyntheticHomotopyTheory/Circle2.v.html │ │ 11.4 6.38 -4.9824 -43.86% 118 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 4.974 0.1 -4.8740 -97.99% 407 coq-vst/floyd/for_lemmas.v.html │ │ 19.9 16.1 -3.8482 -19.30% 543 coq-unimath/UniMath/CategoryTheory/Presheaves/SigmaTypes.v.html │ │ 3.38 0.121 -3.2558 -96.42% 233 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/RecodeProofs.v.html │ │ 2.13 0.0561 -2.0753 -97.37% 243 coq-unimath/UniMath/ModelCategories/Examples.v.html │ │ 2.12 0.0538 -2.0703 -97.47% 459 coq-unimath/UniMath/ModelCategories/Examples.v.html │ │ 5.23 3.25 -1.9800 -37.89% 210 coq-fiat-crypto-with-bedrock/src/Demo.v.html │ │ 2.11 0.131 -1.9796 -93.81% 323 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/RecodeProofs.v.html │ │ 2.03 0.142 -1.8915 -93.03% 348 coq-unimath/UniMath/CategoryTheory/Presheaf.v.html │ │ 202 201 -1.4596 -0.72% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 42.3 41.0 -1.3708 -3.24% 115 coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
|
Whoopf, that's a crazy speedup in bedrock2 (cc @JasonGross). For VST there is an increase in total time but a non-trivial reduction in instructions, how come? |
|
The number of instructions is a meaningful metric only if the memory access patterns do not change. Remember that the memory latency grows exponentially with the processor cache level (e.g., 2 cycles for L1, 10 cycles for L2, 50 cycles for L3, 250 cycles for main memory, but depending on the architecture, it can be even steeper). Here, |
|
The problem with VST is not only the time. Requiring 8G to compile it seems much worse than the time slowdown. Maybe capping the size of the cache with |
|
I think we could add cache misses to what Line 24 in 8641bb7 |
|
The mark only needs 2 bits, so the new |
|
Note that, even if the By the way, the code strongly depends on the fact that the compiler is not a 32-bit one (so no more jsCoq, which is fine by me). |
coqbot-app
Bot
added
the
needs: full CI
|
Sorry, I pushed here by mistake... I'll revert the push. |
8c14f68 to
739cf01
Compare
I totally agree we should try to use weak tables here. But if in the end we don't, please cap the cache size. |
I asked Fable to prototype a design with ephemerons, but it appears it doesn't give significant gains (tested on Bonak's SSGpd example): olympichek@62222da |
|
Can you ask the AI to find a good default for the cache size running multiple time that example, push the commit here and run again the benchmark on all our bench suite? |
|
Moreover, what is the expected length of the lists in the cache buckets? Unless it is small (e.g., 4), it would make sense to use hash tables as the buckets rather than lists. Also, since |
I was wondering whether it is worth it before submitting a PR. I decided not to do this, as other existing session-scoped tables in Rocq's kernel don't have such a cap: Note that it can also depend on how exactly the cap semantics works. There might be multiple ways to do it:
The way it is currently implemented in this PR is freeze, and it appears it doesn't behave well on Bonak's
I will continue investigating it.. |
Yes, they are expected to be small, most of the occurrences are just a single element. Measured on Bonak's
I am not sure if hash table would be better here, it appears hash tables have higher overhead than lists. However, I have an experimental patch that replaces the whole structure with buckets with just a pair of integers:
The thing is, we cache not only successes, but also failures of conversion problem. However, it appears caching only |
7 participants
Kernel: cache conversion results within a session
Summary
Kernel conversion runs on the closure machine of
kernel/cClosure.ml: the lazy reduction machine that represents a term as a graph of mutable cells (fconstr), each holding a subterm together with its environment, and updates a cell in place with its reduct once it has been forced. Because substitution is delayed in the environment rather than performed on the syntax, substituting a term for a variable makes every occurrence of that variable point at one and the same cell instead of at a copy of it.Today, conversion does not exploit that sharing. A problem posed on two such terms decomposes into subproblems that confront the same pair of cells once per occurrence, and
ccnvretains nothing between those encounters, so each is reduced and compared from scratch. The cost of the check then scales with how many times a shared subterm occurs, not with how large it is.This PR makes conversion remember. Each cell gets a stable identity, and a table local to one conversion session records, for a pair of cells, whether they were found convertible. A pair that comes back is answered from the table instead of being reduced again.
This is a follow-up for the recently merged #22299, which discharges a pair up front when both sides are the same pointer.
Implementation
fconstrgains a mutablefidfield (0= unassigned), handed out lazily byCClosure.get_fid. It is preserved by the in-placeupdatethe machine performs when it reduces a cell, and reset to0on every copy of a cell (lft_fconstr,resubst,zip,mkFApp, and the other places that build fresh cells). All the noise inkernel/cClosure.mlis just this field being added to record literals.conv_tabgains an optionalconv_cache: aHashtblfrom(fid1, fid2, cv_pb)to a bucket of(lift1, lift2, result)entries, compared witheq_lift.ccnvlooks the pair up before callingeqappr, and records the outcome afterwards. Both successes and failures are cached: a hit replayscunivunchanged or re-raisesNotConvertible.FLIFTlayers are stripped off both sides and folded into the corresponding lift withel_shft, so that cells that differ only by a lift wrapper share cache entries. This mirrors what the existingfast_testpre-check already does.ROCQ_CONV_CACHE=0disables it andROCQ_CONV_CACHE_MAX=<n>caps the number of entries (0or unset means unlimited). It is unbounded by default because, likeclos_tab, the table is session-scoped, so its lifetime bounds its memory.This PR was made with assistance of Claude Fable 5.
Why it's correct
The cache is only installed for checked conversion (
gen_conv, i.e.conv/conv_leq), where the answer is a deterministic function of a fixed environment and universe graph, and no universe constraints are accumulated that would need to be replayed on a hit. Inference-mode conversion (generic_conv, used by unification and evarconv, which backtracks and discards constraints) passes~use_cache:falseand never consults the cache, as does thecompare_under-style entry point registered onCClosure.Two further points:
fidis stable across in-place reduction:updaterewrites a cell'stermto a reduct of what was there, which is convertible to it, so a previously recorded verdict for that cell remains valid. Copies get a freshfid, so no unrelated cell can inherit a verdict.CONVvsCUMUL) are part of the key, so a result is never reused at a different de Bruijn offset or in the wrong direction.l2ris fixed for the whole session and so needs no keying.Performance
The motivating development is Bonak, whose dimension-indexed definitions compare heavily shared closures over and over. Below is compilation of
theories/νSet/SSGpd.v, each row adding to the previous one. All rows assume #22272 (refolding of global fixpoints), without which the file is too slow to measure.compare_underfast paths (#22299)The cache is worth 4.74x here, 12.5x cumulatively from the first row. It buys that with memory: peak usage goes from 1.00 GB to 8.13 GB, which
ROCQ_CONV_CACHE_MAXcan bound.The broader impact is unknown: this is an extreme case, and we have not measured whether other developments gain, are unaffected, or lose to the bookkeeping and the extra memory. This can be tested by the CI benchmark. If the cache does not pay off outside workloads like this one, we are happy to make it off by default behind an explicit option, something like
Set Conversion Cache.Checklist