Make proof-tree painting cheap on large proofs #3863
Merged
Merged
Conversation
A thread dump on a ~300k-node proof showed the EDT RUNNABLE with 70+s of CPU in ProofRenderer.renderBranch: for every OPEN branch node, on every repaint, it ran a breadth-first search over the branch's whole subtree and called the linear-scan Proof.getOpenGoal on each visited node -- O(subtree x openGoals) per branch, per paint -- purely to decide the rare linked-folder icon. On a large proof with many open goals that is billions of operations per paint, which is the GUI sluggishness. Replace it with a scan over the proof's open goals (far fewer than a big subtree), short-circuited by the cheap isLinked() pre-check, walking ancestors only for the linked ones. Equivalent result, no caching/staleness. Also skip the getOpenGoal scan for closed leaves in renderLeaf (a closed leaf has no open goal). This is stock-KeY behaviour, exposed now that MT makes such large proofs reachable.
unp1
changed the title
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
ProofTreeView.ProofRenderer.renderBranchdecides the rare "linked-folder" icon by running abreadth-first search over the branch's entire subtree on every repaint, calling the
linear-scan
Proof.getOpenGoalon each visited node. That is O(subtree × open goals) per open branch,per paint no matter whether the merge rule is used or not. On large proofs (tens of thousands of nodes, many open goals) this turns tree painting
into billions of operations and freezes the EDT. A thread dump on a ~300k-node proof showed the
EDT RUNNABLE with 70+s of CPU in
renderBranch.The fix iterates the proof's open goals instead of the whole subtree (far fewer of them),
short-circuited by the cheap
isLinked()test and walking ancestors only for linked goals. Abranch is still marked linked iff it contains a linked open goal — same result, a tiny fraction of
the cost.
renderLeafadditionally skips thegetOpenGoalscan for closed leaves (a closed leafhas no open goal). Behaviour is unchanged; only the cost of computing the icon changes, and large
proof trees now paint smoothly.
Type of pull request
Ensuring quality
still appears for branches that contain a linked goal); on a >300k-node proof the tree now paints
smoothly instead of freezing the GUI.
Additional information and contact(s)
Found via a thread dump while working on the multi-core prover branch (#3842), which makes such
large proofs easy to reach, but the fix is stock-KeY and independent of it — factored out here as a
standalone change.
PR created with AI tooling
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.