Skip to content

Fix memory leaks - #3994

Merged
wadoon merged 2 commits into
mainfrom
bubel/fix-mem-leaks
Oct 18, 2026
Merged

wadoon merged 2 commits into
mainfrom
bubel/fix-mem-leaks

Conversation

@unp1

@unp1 unp1 commented Oct 17, 2026 •

Copy link
Copy Markdown
Member

Fixes two memory leaks:

  • GUI: nodes of closed proofs were still kept in memory due to references from the GUIProofTreeModel and possibly sequent views
  • Thread-Local Caches: two thread-local caches kept also references; these would have been eventually replaced, but as they are kept by the Java default Swing threads (assume N threads) it could happen that up to N proofs remained if each next proof would have been single core and execute don a different one

Encountered when working on a proofs for a paper on ETAPS and the GUI showed 3GB used with all proofs removed (even after running GC). Now after running GC only 100 MB usage remains.

Intended Change

Fix memory leak

Type of pull request

  • Bug fix (non-breaking change which fixes an issue)

Ensuring quality

  • I have tested the feature as follows:
    • checked memory usage in the GUI after loading, running a proof (Which used 6GB) and closing it (several times); before fix: 3GB remained; after fix: only 100 MB
  • I have checked that runtime performance has not deteriorated.
    • used the benchmarking tool

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2, or (at your option) any later version, for inclusion in KeY.

Nodes of disposed/abandoned proofs were still reachable via cached state information
@unp1 unp1 self-assigned this Oct 17, 2026
@unp1 unp1 added the 🐞 Bug label Oct 17, 2026
@unp1 unp1 added this to the v3.1.0 milestone Oct 17, 2026
not permanent, but old proof nodes stayed reachable via threadlocal caches
and if the JVM threads were not reused these proofs could accumulate
@unp1
unp1 force-pushed the bubel/fix-mem-leaks branch from f70850e to 9c5d587 Compare October 17, 2026 22:48
@wadoon
wadoon self-requested a review October 18, 2026 00:03
@wadoon
wadoon enabled auto-merge October 18, 2026 00:05
@wadoon
wadoon added this pull request to the merge queue Oct 18, 2026
Merged via the queue into main with commit ae82277 Oct 18, 2026
39 checks passed
@wadoon
wadoon deleted the bubel/fix-mem-leaks branch October 18, 2026 00:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants