perf: move ref into the Core.Context cold subobject - #15027
Draft
Kha wants to merge 2 commits into
Draft
Conversation
…bobject This PR cuts the reference count traffic paid by the recursion-depth and `withRef` steps that dominate elaboration, from ten increments per reconstruction to three. Measured against master it saves between 0.35% and 1.24% of elaboration instructions across match-, simp- and grind-heavy workloads. `withReader` can never reuse the `Context` record, so every reconstruction pays one increment per pointer field. The original split classified fields by their number of update *sites*; this classifies them by measured update *frequency* instead. On a representative module `withIncRecDepth` runs about 1.0M times and `withRef` about 31k, while `withOptions` runs once, so `options`, `maxRecDepth`, `currNamespace`, `openDecls`, `initHeartbeats`, `maxHeartbeats` and `currMacroScope` join the cold group and only `currRecDepth` and `ref` stay hot. The `Context` constructor goes from `(0, 10, 2)` to `(0, 3, 2)`. Rebuilding the wider cold record does make the rare paths that update those fields more expensive: `withCurrHeartbeats` goes from ten increments to fourteen. At roughly 4.9k such calls against 1.05M reconstructions, the trade is strongly positive. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This PR removes the last per-recursion-step reference count increment on a thread-shared object, leaving `withIncRecDepth` copying only the cold subobject pointer. The instruction saving is small, but the increment it removes is expected to be a contended atomic one, so the effect on wall-clock should be larger than on instructions. `ref` points into the command's parsed syntax tree, which is shared with async elaboration tasks and therefore marked multi-threaded, making each increment on it a locked read-modify-write. The cold subobject is instead rebuilt often enough (about 18k times per module, by `withFreshMacroScope` and `withCurrHeartbeats`) that its instances are usually fresh, single-threaded and cheap to increment. Moving `ref` across therefore trades roughly 1.0M contended increments on the recursion path for about 155k on the 31k `withRef` calls that now rebuild the cold record. Measured on a representative module, `withIncRecDepth` drops from three increments to two and `withRef` rises from three to fourteen; the `Context` constructor becomes `(0, 2, 2)`. The trade rests on `withRef` staying far rarer than `withIncRecDepth` — about 31k against 1.0M there — so it should be checked on syntax-heavy workloads before being relied upon. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Member
Author
|
!bench |
|
Benchmark results for 1ed4f9a against 5877442 are in. There are significant results. @Kha
Medium changes (1✅)
Small changes (92✅, 8🟥)
|
Kha
added
the
downstream-force
github-actions
Bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
|
The adaptation PR for this PR is leanprover/downstream-lean4#46. |
leanprover-bot
added
the
builds-manual
Collaborator
|
Reference manual CI status:
|
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.
No description provided.