Memory Usage Profiling

[maphih]

Profile Protege while trying to prove VegetarianPizzaEquivalent1 SubClassOf VegetarianPizzaEquivalent2 with multiple proof generators. To see whether the memory usage is still problematic, and which part of the code created the largest data structures.

Stefan Borgwardt
7 Dec 2023
@idsi032f Can you summarize the findings here, or link to a document? I recall that there was some issue with the "detailed lethe proofs" that we should fix.

Ida Sri Rejeki Siahaan
7 Dec 2023
The link to the document is https://gitlab.tcs.inf.tu-dresden.de/tofr961c/evee-internal/-/wikis/Profiling-on-VM

Please see Point 2. Profiling on Windows VM for VegetarianPizza1 EquivalentTo VegetarianPizza2 for "Detailed Proof LETHE" was running for 29 hours with no result.\

Stefan Borgwardt
7 Dec 2023
This is very strange. The proof "only" takes a few minutes on my MacBook, with only 4GB heap space instead of 6GB. Could you run the "Sampler" of VisualVM to find out what the proof generator is doing all this time on the VM?

Ida Sri Rejeki Siahaan
7 Dec 2023
The problem we had before was on the version on that day. It might have been fixed with many of our updates.

Stefan Borgwardt
7 Feb 2024
@koopmann Could you have a look at the report here: https://gitlab.tcs.inf.tu-dresden.de/tofr961c/evee-internal/-/wikis/Profiling-on-VM

Detailed LETHE proofs fills the memory with lots of instances of ConceptClause and Scala Sets/RedBlackTrees. Cancelling doesn't work, because the VM just gets too slow. If we actually get an OutOfMemoryError, we also have to restart Protégé. Do you have an idea to decrease the memory usage, or at least stop the proof generation, without having to restart Protégé?

Patrick Koopmann
7 Feb 2024
Thanks, this is indeed insightful! This is not relevant for the study yet, since we do not use proofs there, right?

Stefan Borgwardt
7 Feb 2024
No, but we are also looking at the open bugs again for the next release.