Performance Series 2 (3/5): Incremental taclet re-indexing for a single added taclet#3876
Merged
Conversation
unp1
changed the title
unp1
force-pushed
the
bubel/reindex-fastpath
branch
from
c1e2a8d to
6be6cea
Compare
When a NoPosTacletApp is added, addedNoPosTacletApp re-walks the affected formulas and, at every position, fetched that position's full operator taclet list and filtered it through a SetRuleFilter to keep the single new taclet. For common operators that list is large, so this membership scan dominated re-indexing (~12.8% of CPU on the wide-branching bike example; 60.7% of all HashMap lookups). Instead, feed the walk a one-taclet index built from just the new taclet, reusing the identical getList/match logic, so matchTaclets iterates ~one candidate per position. The single-threaded index is used deliberately: the multi-threaded matcher only parallelizes above 256 taclets, so a one-taclet index always takes its sequential path anyway. Byte-identical -- the multi-taclet addedNoPosTacletApps path is unchanged. New differential + unit tests in TestTermTacletAppIndex compare the mini-index re-index against the SetRuleFilter path (identical fired apps and apps at every position); full testRAP is green. On bike this cuts automode time ~16% (HashMap.getNode 12.1% -> 4.9%). Created with AI tooling support
unp1
force-pushed
the
bubel/reindex-fastpath
branch
from
6be6cea to
9bf03e2
Compare
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.
Intended Change
Each time a single taclet is added to a goal,
TacletAppIndexrebuilt its rule-application index over the entire taclet set. This change re-indexes only the one newly added taclet, via a small one-taclet index, instead of rebuilding everything. Behaviour-preserving.Benchmark
Automode time, median of 3 runs, serial forks (
-PrapForks=1), isolateduser.homeper run; baseline = current main (8 representative proofs: 4 quantifier-heavy + 4 mixed). ArrayList.remove.1 is high-variance run-to-run — treat as noise.Plan
Type of pull request
Ensuring quality
Additional information and contact(s)
Part of Performance Series 2 — see the overview (#3879) for the combined benchmark and series context.
Created with AI tooling support.
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.