kernel: conversion cache optimization experiment - #22401
Draft
olympichek wants to merge 11 commits into
Draft
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.
Entries in the conversion cache were boxed tuples holding lift values, scanned with `eq_lift` inside per-key assoc lists. Intern lifts to small ids (`hash_lift` added to `Esubst` for the interning table) so that each entry packs into two machine integers: the cell-id pair as the key (`(fid1 lsl 31) lor fid2`) and the lift ids, problem kind and result as the payload. The container is unchanged (a `Hashtbl`, several bindings per packed key). Problems whose lifts or ids exceed the packing range fall back to uncached conversion. Behaviour is otherwise unchanged: identical probe/hit/insert counts.
The packed entries still live in a `Hashtbl`, whose internal bucket cells are heap blocks: on a heavy check that inserts ~60M entries within a single session the major GC traces every one of them, and that tracing becomes the dominant cost. Since an entry is already two machine integers, store the cache in two flat 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.
The conversion cache memoizes verdicts by cell identity, which is blind to cells rebuilt over the same closure: the same (body, substitution) question asked through fresh `FCLOS` wrappers re-runs the whole recursive comparison. Add a second cache level, probed when the cell-id lookup misses on an `FCLOS`/`FCLOS` pair, keyed on the closure content: body `constr` by pointer and substitution by the spine of cells it contains, compared through the stable cell fids (`CClosure.subs_content_fid`, `subs_content_equal`, `Esubst.Internal.repr`), which survive in-place cell updates. Verdicts found at this level are fed back into the cell-id level. Session-scoped, same soundness domain as the cell-id cache. On by default; `ROCQ_CLOS_MEMO=0` disables, `=stats` observes without acting (diagnostics, includes a body-pair upper-bound counter), `ROCQ_CLOS_MEMO_STATS=1` prints counters at exit. SSGpd.v: 89.3 s -> 67.5 s (-24.5 %) at 5.36 GB -> 1.41 GB maxRSS (-74 %), byte-identical `.vo`. In observe mode 66 % of cell-id misses are exact (node, subst) repeats. On workloads whose repeats are nested (nutele) the effect is a mild win (-7 %/-14 %).
The (node, subst) probe cost was dominated by key bookkeeping rather than the table: `subs_hash`/`subs_equal` went through `Esubst.Internal.repr`, materializing both spines as lists on every probe, and the find-then-add pattern ran the two deep `Hashtbl.hash_param` body traversals twice on the miss path. Add `Esubst.Internal.fold` (allocation-free fold over the entries in `repr` order, also returning the total shift) and `Esubst.Internal.equal` (structural fast path, `repr` fallback for substitutions built through different construction paths), and precompute the key hash in a `ck_hash` field: bodies are hashed once per probe, the table hash is a field read, and equality prefilters on it. Cache decisions are unchanged: probe/hit/insert counters and the produced `.vo` are byte-identical to the previous code on SSGpd and the Bonak abstract-layer-module files; `Esubst.Internal.fold/equal` are validated against `repr` on 200k random substitutions. Paired runs: SSGpd 68.0 s -> 58.2 s (-14.5 %; maxRSS +6 % from the stored hash word). The default-on probe-tax regressions invert into wins: νSet 2.39 s -> 1.96 s and νDgnSet 8.38 s -> 7.11 s, both now faster than the memo-less baseline (2.25 s / 7.64 s); νGpd 94.2 s -> 82.8 s at -8.5 % maxRSS.
We quickly assess whether we may have a fconstr hit by recording the highest id present in the table. (cherry picked from commit 16d8830)
Some conversion problems involve fconstr freshly generated by mk_clos. These objects are not reference elsewhere, so it makes no sense to either check for their presence in the cache or even try to cache their result. We detect this situation by passing an additional cache-disabling flag to the conversion function, and let mk_clos set a fresh id when the fconstr is actually not fresh, i.e. when it comes from an expansion of a rel in the environment. (cherry picked from commit ab80f4f)
We reserve for the identity lift the specific uid 0 and do not try to query the hash table. Most lifts are identity. (cherry picked from commit bd10544)
(cherry picked from commit 6e793ee)
Inlining `clos_rel` into `mk_clos` collapsed its two `HigherOrder` branches into the "Uncaught pattern variable" anomaly, but `HigherOrder (0, mt)` is a legitimate case: it is a rewrite-rule hole applied to zero arguments, and `clos_rel` mapped it to `Regular mt`. Since the RHS substitution of every matched rewrite rule is built out of `HigherOrder` entries before being handed to `mk_clos`, any rule with a bare hole in its RHS raised the anomaly. `klt` handles the same case explicitly. Unlike the other cells `mk_clos` builds, the value behind a hole is shared across all its occurrences in the RHS, so it is worth interning for the conversion cache; hence the `get_fid`. Restore `test-suite/success/rewrule.v` and `test-suite/bugs/bug_20728.v`, which were removed because they tripped the anomaly. `test-suite/success/UnfoldDepHeuristic.v` stays as is: its negative control is defeated by the conversion cache itself, which this commit does not change. (cherry picked from commit 843ef3ccd4151589a2dc4c3fcab304fbc868554d)
`~cache` is a fid-assignment policy, not a caching policy: it decides whether to intern a cell nobody else references. That is a level-1 concern only. Level 1 is keyed on cell identity, so a freshly built cell gets a brand new id, the probe can never hit (`max_uid` rejects it) and the insert is pure bookkeeping. Level 2 is keyed on `(node, subst)` and needs no id for the compared cells themselves -- only for the substitution entries, which are shared by construction -- so it applies to freshly built closures as well. Those closures are exactly what the `~cache:false` sites produce: `convert_under_context` compares `mk_clos`-fresh branch bodies and return clauses, and fix/cofix bodies, prod codomains and `Zlcase` parameters are all `FCLOS`. Gating both levels on `~cache` therefore starved level 2 of nearly all its input. Gate level 1 on the old condition, gate level 2 on both sides being `FCLOS`, and skip the probes entirely only when neither applies. An out-of-range fid now falls back to level 2 alone instead of dropping both.
coqbot-app
Bot
added
the
needs: full CI
Contributor
Author
Member
|
@coqbot run full ci |
coqbot-app
Bot
removed
the
needs: full CI
Member
|
@coqbot bench |
Contributor
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 18.1 206 188.1772 1041.77% 32 coq-performance-tests-lite/src/pattern.v.html │ │ 18.8 207 188.1313 999.59% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 10.1 78.1 68.0243 673.31% 325 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 10.2 74.8 64.5722 631.71% 214 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 8.02 57.6 49.5928 618.03% 31 coq-performance-tests-lite/src/pattern.v.html │ │ 8.19 57.6 49.4041 603.19% 30 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 3.37 43.1 39.7375 1180.32% 109 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 16.178 44.977 28.7990 178.01% 1209 coq-vst/floyd/Component.v.html │ │ 16.043 44.431 28.3880 176.95% 1515 coq-vst/floyd/VSU.v.html │ │ 16.184 43.345 27.1610 167.83% 1223 coq-vst/floyd/Component.v.html │ │ 39.6 66.3 26.7581 67.65% 81 coq-fiat-crypto-with-bedrock/rupicola/src/Rupicola/Examples/Utf8/Utf8.v.html │ │ 43.7 65.1 21.3423 48.82% 221 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 37.4 56.1 18.6756 49.88% 222 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 31.5 47.2 15.6734 49.71% 223 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 7.825 22.953 15.1280 193.33% 1512 coq-vst/floyd/VSU.v.html │ │ 8.407 23.069 14.6620 174.40% 755 coq-vst/floyd/Component.v.html │ │ 7.813 22.105 14.2920 182.93% 1514 coq-vst/floyd/VSU.v.html │ │ 7.893 22.116 14.2230 180.20% 1222 coq-vst/floyd/Component.v.html │ │ 7.949 22.156 14.2070 178.73% 1221 coq-vst/floyd/Component.v.html │ │ 8.125 22.119 13.9940 172.23% 1509 coq-vst/floyd/Component.v.html │ │ 8.11 21.998 13.8880 171.25% 783 coq-vst/floyd/Component.v.html │ │ 3.45 17.1 13.6345 394.95% 30 coq-performance-tests-lite/src/pattern.v.html │ │ 7.93 21.507 13.5770 171.21% 1208 coq-vst/floyd/Component.v.html │ │ 3.50 17.0 13.5291 386.91% 29 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 7.959 21.305 13.3460 167.68% 1506 coq-vst/floyd/Component.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 63.3 1.94 -61.3298 -96.94% 608 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 63.1 1.95 -61.1894 -96.91% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 60.2 0.128 -60.0396 -99.79% 857 rocq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v.html │ │ 49.8 0.0743 -49.7372 -99.85% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 44.6 1.20 -43.3990 -97.31% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 41.2 1.22 -40.0303 -97.05% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 29.172 0.056 -29.1160 -99.81% 147 coq-vst/veric/expr_lemmas4.v.html │ │ 35.4 6.41 -28.9970 -81.90% 898 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 28.742 0.019 -28.7230 -99.93% 194 coq-vst/veric/expr_lemmas4.v.html │ │ 26.6 0.0134 -26.5745 -99.95% 374 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 26.5 0.0128 -26.5191 -99.95% 375 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 21.4 0.270 -21.1473 -98.74% 338 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 17.4 0.310 -17.0614 -98.22% 905 coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html │ │ 20.1 4.50 -15.6136 -77.63% 543 coq-unimath/UniMath/CategoryTheory/Presheaves/SigmaTypes.v.html │ │ 12.4 0.0996 -12.2720 -99.19% 97 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/HValuedSets.v.html │ │ 11.4 0.233 -11.1919 -97.96% 1828 rocq-mathcomp-analysis/theories/ftc.v.html │ │ 11.8 0.813 -10.9742 -93.10% 216 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 16.1 6.39 -9.6894 -60.27% 898 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 9.40 0.231 -9.1704 -97.54% 253 rocq-mathcomp-analysis/theories/gauss_integral.v.html │ │ 9.09 0.0462 -9.0453 -99.49% 127 coq-mathcomp-odd-order/theories/BGappendixAB.v.html │ │ 8.63 0.298 -8.3323 -96.55% 453 coq-unimath/UniMath/SyntheticHomotopyTheory/Circle2.v.html │ │ 15.3 8.50 -6.7573 -44.29% 6 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeCSR.v.html │ │ 7.47 0.729 -6.7459 -90.25% 136 coq-unimath/UniMath/CategoryTheory/Actegories/Examples/ActionOfEndomorphismsInCATElementary.v.html │ │ 6.42 0.00980 -6.4128 -99.85% 853 coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html │ │ 6.08 0.0190 -6.0618 -99.69% 323 coq-unimath/UniMath/RealNumbers/DedekindCuts.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
github-actions
Bot
added
the
needs: rebase
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.
A draft PR with some further optimizations on top of the conversion cache implementation proposed in PRs #22309, #22319, #22396