perf: cache the innermost scope state in ScopedEnvExtension.StateStack - #14968
Draft
Kha wants to merge 1 commit into
Draft
perf: cache the innermost scope state in ScopedEnvExtension.StateStack#14968Kha wants to merge 1 commit into
ScopedEnvExtension.StateStack#14968Kha wants to merge 1 commit into
Conversation
`ScopedEnvExtension.getState` is called on hot paths such as parsing, attribute lookup and simp set lookup, and had to walk into the head of `stateStack` and project `State.state` out of it, with reference counting on both intermediates. Cache that state in a new `StateStack.state` field so the lookup is a single projection, and keep it in sync in the (much colder) functions that push, pop or update the stack. The empty-stack `unreachable!` disappears with it. Because `StateStack` now stores a `σ`, its `Inhabited` instance depends on `Inhabited σ` and would have to be rebuilt, and hence allocated, on every `getState` call. `ScopedEnvExtension` therefore stores the witness in a `defaultState` field, built once at registration, which is why `registerScopedEnvExtension` now takes `[Inhabited σ]`; all existing callers already have that instance. `Inhabited` is erased at runtime, so `getState` just reads the field. Changing the layout of `StateStack` breaks the stage1 build (segfaults and corrupted parser state in modules that define and use meta code in the same file), so `interpreter.prefer_native` is enabled in `stage0/src/stdlib_flags.h` as described in `doc/dev/bootstrap.md`.
Member
Author
|
!bench |
|
Benchmark results for d1863d1 against e991a05 are in. No significant results found. @Kha
Small changes (2✅, 1🟥)
|
github-actions
Bot
added
toolchain-available
leanprover-bot
added
the
builds-manual
Collaborator
|
Reference manual CI status:
|
mathlib-lean-pr-testing
Bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
Member
Author
|
!bench mathlib |
|
Benchmarking leanprover-community/mathlib4-nightly-testing@d40ae5d against leanprover-community/mathlib4-nightly-testing@78f2465 (preliminary results). React with 👀 to be notified when the results are in. The command author is always notified. |
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.
ScopedEnvExtension.getStateis called on hot paths such as parsing, attribute lookup and simp set lookup, and had to walk into the head ofstateStackand projectState.stateout of it, with reference counting on both intermediates. Cache that state in a newStateStack.statefield so the lookup is a single projection, and keep it in sync in the (much colder) functions that push, pop or update the stack. The empty-stackunreachable!disappears with it.Because
StateStacknow stores aσ, itsInhabitedinstance depends onInhabited σand would have to be rebuilt, and hence allocated, on everygetStatecall.ScopedEnvExtensiontherefore stores the witness in adefaultStatefield, built once at registration, which is whyregisterScopedEnvExtensionnow takes[Inhabited σ]; all existing callers already have that instance.Inhabitedis erased at runtime, sogetStatejust reads the field.