From f0839fd1477d6a16221a3084a570624763de5856 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Sat, 20 Jun 2026 21:27:24 +0200 Subject: [PATCH 1/2] Fix per-proof memory leak: clear JavaParserFacade cache on dispose Disposed proofs were never collected: live heap grew ~56.6 MB per load/prove/dispose cycle of the same obligation in one JVM (linearly), which is why RunAllProofs forks a JVM per group. Root cause is javaparser's JavaParserFacade.instances, a static WeakHashMap whose value (new JavaParserFacade(typeSolver)) strongly references its own weak key. A weak key that stays strongly reachable from its own value never becomes weakly reachable, so the entry is never evicted. KeY's JavaParserFactory type solvers transitively reference the owning Services, so each disposed proof's whole proof tree was retained through this cache. A proof registers several short-lived type-solver keys (the DynamicTypeSolver wrapper plus every CombinedTypeSolver from rebuild()), and the fork exposes no per-key removal, so JavaParserFactory.dispose() drops the cache wholesale via the public clearInstances(), synchronized on the JavaParserFacade monitor that get() uses (the backing map is a plain WeakHashMap and clearInstances() is itself unsynchronized). The facade is a load-time-only resolution cache, rebuilt lazily, so this is safe. Proof.dispose() invokes it via the new nullable accessor Services.getJavaServiceOrNull() (avoids the assert in getJavaService() for pure first-order proofs). Measured with MtRetentionProbe (8 reps, symmArray): +56.6 MB/proof before, +0.1 MB/proof after. --- .../java/de/uka/ilkd/key/java/Services.java | 9 +++++ .../key/java/loader/JavaParserFactory.java | 33 +++++++++++++++++++ .../java/de/uka/ilkd/key/proof/Proof.java | 7 ++++ 3 files changed, 49 insertions(+) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Services.java b/key.core/src/main/java/de/uka/ilkd/key/java/Services.java index c35f79a9552..b4a0970e06c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Services.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Services.java @@ -473,6 +473,15 @@ public JavaService getJavaService() { return javaService; } + /** + * @return the {@link JavaService}, or {@code null} if Java was never activated for this + * {@link Services} (e.g. a pure first-order proof). Unlike {@link #getJavaService()} + * this never asserts and is safe to call during disposal. + */ + public @Nullable JavaService getJavaServiceOrNull() { + return javaService; + } + private JavaService activateJavaPath(@NonNull Path bootClassPath, @NonNull Collection libraryPaths, FileRepo fileRepo) { if (javaService != null && javaService.getBootClassPath().equals(bootClassPath) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java index 0c846670cca..061e521bcc3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/loader/JavaParserFactory.java @@ -28,6 +28,7 @@ import com.github.javaparser.resolution.declarations.ResolvedReferenceTypeDeclaration; import com.github.javaparser.resolution.model.SymbolReference; import com.github.javaparser.symbolsolver.JavaSymbolSolver; +import com.github.javaparser.symbolsolver.javaparsermodel.JavaParserFacade; import com.github.javaparser.symbolsolver.resolution.typesolvers.CombinedTypeSolver; import com.google.common.cache.Cache; import com.google.common.cache.CacheBuilder; @@ -118,6 +119,38 @@ public TypeSolver getTypeSolver() { return typeSolver; } + /** + * Drops the global {@link JavaParserFacade} resolution cache so that this factory's + * {@link #typeSolver} (and through it the owning {@link Services} and its whole proof tree) can + * be garbage-collected once the proof is disposed. + * + *

+ * {@link JavaParserFacade} keeps a {@code static WeakHashMap} + * ({@code JavaParserFacade.instances}) whose value strongly references its own + * key: each value is created as {@code new JavaParserFacade(typeSolver)} and stores + * that very type solver. A weak key that stays strongly reachable from its own value can never + * become weakly reachable, so the entry is never evicted. Since our type solvers transitively + * reference the owning {@link Services}, every disposed proof would otherwise be retained + * forever through this cache — a long-standing, proof-sized memory leak. + * + *

+ * A single proof registers several short-lived type-solver keys (the {@code DynamicTypeSolver} + * wrapper plus every {@code CombinedTypeSolver} produced by {@code rebuild()}), and the fork + * exposes no per-key removal, so the only complete remedy is to drop the cache wholesale via + * the + * public {@link JavaParserFacade#clearInstances()}. This is safe: the facade is a pure + * resolution cache that is only populated while parsing Java during loading and is rebuilt + * lazily on the next {@code get}. We synchronize on the same monitor + * {@code JavaParserFacade.get} + * uses, because the backing map is a plain {@link java.util.WeakHashMap} and + * {@code clearInstances()} is itself unsynchronized. + */ + public void dispose() { + synchronized (JavaParserFacade.class) { + JavaParserFacade.clearInstances(); + } + } + public JavaSymbolSolver getSymbolSolver() { return symbolResolver; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java index 5e1ecaa95ec..3e504851cf8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java @@ -278,6 +278,13 @@ public void dispose() { // Do required cleanup if (getServices() != null) { getServices().getSpecificationRepository().removeProof(this); + // Drop the global JavaParserFacade resolution cache. It is a WeakHashMap whose values + // strongly reference their own (weak) keys, so without this the proof's Services - and + // thus the whole proof tree - would leak through it. See JavaParserFactory#dispose. + var javaService = getServices().getJavaServiceOrNull(); + if (javaService != null) { + javaService.getProgramFactory().dispose(); + } } if (localMgt != null) { localMgt.removeProofListener(); // This is strongly required because the listener is From e15580cef8ef548eb9d5321823003c2c6bec7ea4 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Sat, 20 Jun 2026 21:27:34 +0200 Subject: [PATCH 2/2] Add retention probe and in-process GC-root finder (opt-in) Test-only diagnostics for the dispose leak, all gated behind -Dkey.mt.retention=true so they never run in normal CI: - MtRetentionProbe: loads/proves/disposes an obligation N times, forces GC each cycle and reports live MB per rep, a verdict, and (with .histo) the top live-instance growth. Serves as a regression guard for the dispose leak. - HeapRootFinder: MAT-free, in-process "path to GC roots". Enumerates loaded classes via the gcClassHistogram diagnostic command, BFS-walks the object graph from their static fields and from every thread's ThreadLocalMap, excludes weak/soft referents, and prints the shortest strong reference chain to a target object. This is how the JavaParserFacade.instances root was identified after JFR/OldObjectSample only reached "VM Global / Global Object Handle". build.gradle forwards -Dkey.mt.retention* and -PstressHeap to the test JVM, and adds --add-opens for java.base packages when -Dkey.mt.retention.root=true (the root finder reflects into JDK collection internals). --- key.core/build.gradle | 15 + .../ilkd/key/prover/mt/HeapRootFinder.java | 290 ++++++++++++++++++ .../ilkd/key/prover/mt/MtRetentionProbe.java | 194 ++++++++++++ 3 files changed, 499 insertions(+) create mode 100644 key.core/src/test/java/de/uka/ilkd/key/prover/mt/HeapRootFinder.java create mode 100644 key.core/src/test/java/de/uka/ilkd/key/prover/mt/MtRetentionProbe.java diff --git a/key.core/build.gradle b/key.core/build.gradle index 128931a290c..a0a0a14cc34 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -97,6 +97,21 @@ classes.dependsOn << generateSolverPropsList tasks.withType(Test) { enableAssertions = true + // Forward retention-probe knobs (see MtRetentionProbe) to the test JVM. + systemProperties += System.properties.findAll { it.key.toString().startsWith("key.mt.retention") } + if (project.hasProperty("stressHeap")) { + maxHeapSize = project.property("stressHeap") + } + if (System.getProperty("key.mt.retention.root") == "true") { + jvmArgs += [ + "--add-opens", "java.base/java.lang=ALL-UNNAMED", + "--add-opens", "java.base/java.lang.ref=ALL-UNNAMED", + "--add-opens", "java.base/java.util=ALL-UNNAMED", + "--add-opens", "java.base/java.util.concurrent=ALL-UNNAMED", + "--add-opens", "java.base/java.util.concurrent.locks=ALL-UNNAMED", + "--add-opens", "java.base/java.util.concurrent.atomic=ALL-UNNAMED" + ] + } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/prover/mt/HeapRootFinder.java b/key.core/src/test/java/de/uka/ilkd/key/prover/mt/HeapRootFinder.java new file mode 100644 index 00000000000..2fef257f5cb --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/prover/mt/HeapRootFinder.java @@ -0,0 +1,290 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.prover.mt; + +import java.lang.management.ManagementFactory; +import java.lang.reflect.Array; +import java.lang.reflect.Field; +import java.lang.reflect.Modifier; +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.IdentityHashMap; +import java.util.List; + +/** + * In-process, MAT-free "path to GC roots" finder. Seeds a breadth-first search from the static + * fields of every loaded class (discovered via the {@code gcClassHistogram} diagnostic command) and + * walks the object graph by reflection until it reaches a given target object, then prints the + * shortest static-rooted reference chain. Used by {@link MtRetentionProbe} to name the exact static + * field/cache pinning a disposed {@code Proof}. + * + *

+ * The target is held only in a stack local of the caller, never in a static or in any field + * reachable + * from a static, so the only chain this search can find is the genuine leak path. + */ +final class HeapRootFinder { + + private HeapRootFinder() {} + + /** edge to the object that referenced this one, plus a human label for the edge. */ + private record Edge(Object parent, String label) { + } + + static void reportPath(Object target) { + System.out.println("[root] searching for static path to " + brief(target)); + IdentityHashMap parent = new IdentityHashMap<>(); + ArrayDeque queue = new ArrayDeque<>(); + + // ---- seed from static fields of every loaded class ---- + int seeded = 0; + for (String cn : loadedClassNames()) { + Class c; + try { + c = Class.forName(cn, false, HeapRootFinder.class.getClassLoader()); + } catch (Throwable t) { + continue; + } + for (Field f : declaredFieldsSafe(c)) { + if (!Modifier.isStatic(f.getModifiers()) || f.getType().isPrimitive()) { + continue; + } + Object v = readStatic(f); + if (v == null) { + continue; + } + if (parent.containsKey(v)) { + continue; + } + parent.put(v, new Edge(null, c.getName() + "." + f.getName())); + if (v == target) { + printChain(parent, target); + return; + } + queue.add(v); + seeded++; + } + } + System.out.println("[root] seeded " + seeded + " static roots"); + + // ---- seed from live threads and their thread-locals ---- + int threadSeeds = 0; + for (Thread t : Thread.getAllStackTraces().keySet()) { + for (Object v : threadRoots(t)) { + if (v == null || parent.containsKey(v)) { + continue; + } + parent.put(v, new Edge(null, "Thread[" + t.getName() + "] threadLocal/field")); + if (v == target) { + printChain(parent, target); + return; + } + queue.add(v); + threadSeeds++; + } + } + System.out.println( + "[root] seeded " + threadSeeds + " thread roots; walking graph..."); + + // ---- BFS over the object graph ---- + long visited = 0; + while (!queue.isEmpty()) { + Object cur = queue.poll(); + visited++; + for (Edge e : children(cur)) { + Object child = e.parent(); // here Edge.parent holds the child value + if (child == null || parent.containsKey(child)) { + continue; + } + parent.put(child, new Edge(cur, e.label())); + if (child == target) { + System.out.println("[root] found after visiting " + visited + " objects"); + printChain(parent, target); + return; + } + if (traversable(child)) { + queue.add(child); + } + } + } + System.out.println("[root] NO static path found after visiting " + visited + + " objects (target is not statically reachable, or is held by a thread/JNI root)"); + } + + /** Returns the outgoing references of {@code o} as (child, label) pairs (reusing Edge). */ + private static List children(Object o) { + List out = new ArrayList<>(); + Class c = o.getClass(); + if (c.isArray()) { + if (!c.getComponentType().isPrimitive()) { + int n = Array.getLength(o); + for (int i = 0; i < n; i++) { + Object v = Array.get(o, i); + if (v != null) { + out.add(new Edge(v, "[" + i + "]")); + } + } + } + return out; + } + boolean isRef = o instanceof java.lang.ref.Reference; + for (Class k = c; k != null && k != Object.class; k = k.getSuperclass()) { + for (Field f : declaredFieldsSafe(k)) { + if (Modifier.isStatic(f.getModifiers()) || f.getType().isPrimitive()) { + continue; + } + // Exclude weak/soft/phantom edges: only report a strong retention path. + if (isRef && f.getName().equals("referent")) { + continue; + } + Object v = readInstance(f, o); + if (v != null) { + out.add(new Edge(v, "." + f.getName())); + } + } + } + return out; + } + + /** Skip walking through huge value-type fan-outs that can't be a short root path. */ + private static boolean traversable(Object o) { + return !(o instanceof String) && !(o instanceof Number) && !(o instanceof Boolean) + && !(o instanceof Character) && !(o instanceof Class); + } + + private static void printChain(IdentityHashMap parent, Object target) { + ArrayList chain = new ArrayList<>(); + Object node = target; + Edge e = parent.get(node); + chain.add(brief(node)); + while (e != null && e.parent() != null) { + chain.add(e.label() + " -> " + brief(e.parent())); + node = e.parent(); + e = parent.get(node); + } + if (e != null) { + chain.add("[static root] " + e.label()); + } + System.out.println("[root] ===== PATH TO GC ROOT (root first) ====="); + for (int i = chain.size() - 1; i >= 0; i--) { + System.out.println("[root] " + chain.get(i)); + } + } + + private static String brief(Object o) { + if (o == null) { + return "null"; + } + String cn = o.getClass().getName(); + String extra = ""; + try { + if (o.getClass().isArray()) { + extra = "[len=" + Array.getLength(o) + "]"; + } + } catch (Throwable ignore) { + // ignore + } + return cn + "@" + Integer.toHexString(System.identityHashCode(o)) + extra; + } + + private static Field[] declaredFieldsSafe(Class c) { + try { + return c.getDeclaredFields(); + } catch (Throwable t) { + return new Field[0]; + } + } + + private static Object readStatic(Field f) { + try { + f.setAccessible(true); + return f.get(null); + } catch (Throwable t) { + return null; + } + } + + private static Object readInstance(Field f, Object o) { + try { + f.setAccessible(true); + return f.get(o); + } catch (Throwable t) { + return null; + } + } + + /** ThreadLocal values + non-primitive instance fields of a thread (its target, locals map). */ + private static List threadRoots(Thread t) { + List out = new ArrayList<>(); + // instance fields of the Thread object itself (e.g. the Runnable target) + for (Field f : declaredFieldsSafe(Thread.class)) { + if (Modifier.isStatic(f.getModifiers()) || f.getType().isPrimitive()) { + continue; + } + Object v = readInstance(f, t); + if (v != null) { + out.add(v); + } + } + // ThreadLocalMap entries (both thread-local and inheritable) + for (String mapField : new String[] { "threadLocals", "inheritableThreadLocals" }) { + try { + Field f = Thread.class.getDeclaredField(mapField); + f.setAccessible(true); + Object map = f.get(t); + if (map == null) { + continue; + } + Field tableF = map.getClass().getDeclaredField("table"); + tableF.setAccessible(true); + Object table = tableF.get(map); + if (table == null) { + continue; + } + int n = Array.getLength(table); + Field valF = null; + for (int i = 0; i < n; i++) { + Object entry = Array.get(table, i); + if (entry == null) { + continue; + } + if (valF == null) { + valF = entry.getClass().getDeclaredField("value"); + valF.setAccessible(true); + } + Object val = valF.get(entry); + if (val != null) { + out.add(val); + } + } + } catch (Throwable ignore) { + // field layout differs or inaccessible + } + } + return out; + } + + private static List loadedClassNames() { + List names = new ArrayList<>(); + try { + String out = (String) ManagementFactory.getPlatformMBeanServer().invoke( + new javax.management.ObjectName("com.sun.management:type=DiagnosticCommand"), + "gcClassHistogram", new Object[] { new String[0] }, + new String[] { String[].class.getName() }); + for (String line : out.split("\n")) { + String[] p = line.trim().split("\\s+"); + if (p.length >= 4 && p[0].endsWith(":")) { + String name = p[3]; + if (name.startsWith("[") || name.contains("/")) { + continue; // arrays, lambdas/hidden classes + } + names.add(name); + } + } + } catch (Exception e) { + System.out.println("[root] class enumeration failed: " + e); + } + return names; + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/prover/mt/MtRetentionProbe.java b/key.core/src/test/java/de/uka/ilkd/key/prover/mt/MtRetentionProbe.java new file mode 100644 index 00000000000..8d3b0674b1a --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/prover/mt/MtRetentionProbe.java @@ -0,0 +1,194 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.prover.mt; + +import java.lang.management.ManagementFactory; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.Comparator; +import java.util.Map; +import java.util.TreeMap; + +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.util.ProofStarter; + +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; +import org.junit.jupiter.api.condition.EnabledIfSystemProperty; + +/** + * Measures whether memory accumulates across repeated load/prove/dispose cycles of the + * same obligation in one JVM. The 128-core stress run #1 was GC-bound with a steadily growing ~17 + * GB + * live set, which suggested per-proof state was retained after {@link KeYEnvironment#dispose()} + * rather + * than something intrinsic to the parallel prover; this probe isolates that on a single thread. + * + *

+ * It proves the obligation {@code reps} times, and after each cycle forces a full GC and records + * the + * live heap. A flat trend means {@code dispose()} releases everything; a rising trend quantifies + * the + * leak (MB per proof). With {@code -Dkey.mt.retention.histo=true} it additionally prints, at the + * end, + * the classes whose live-instance count grew the most between an early and the final cycle (a cheap + * "what is being retained" histogram via the diagnostic command on this JVM). + * + *

+ * Enable with {@code -Dkey.mt.retention=true}. Knobs: {@code -Dkey.mt.retention.proof} (example + * relative, default symmArray), {@code -Dkey.mt.retention.reps} (default 12), + * {@code -Dkey.mt.retention.histo} (default false). Run with a fixed, modest {@code -Xmx} so growth + * is visible (e.g. {@code -PstressHeap} on the dedicated task), single-threaded by default. + * + */ +@EnabledIfSystemProperty(named = "key.mt.retention", matches = "true") +public class MtRetentionProbe { + + private static final long MB = 1024 * 1024; + + @Test + void retention() throws Exception { + String rel = + System.getProperty("key.mt.retention.proof", "standard_key/java_dl/symmArray.key"); + int reps = Integer.getInteger("key.mt.retention.reps", 12); + boolean histo = Boolean.getBoolean("key.mt.retention.histo"); + + Path examples = FindResources.getExampleDirectory(); + if (examples == null) { + System.out.println("[retention] examples directory not found; nothing to do"); + return; + } + Path keyFile = examples.resolve(rel); + if (!Files.exists(keyFile)) { + System.out.printf("[retention] missing proof %s%n", rel); + return; + } + + System.out.printf("[retention] proof=%s reps=%d maxHeap=%dMB histo=%s%n", rel, reps, + Runtime.getRuntime().maxMemory() / MB, histo); + + boolean findRoot = Boolean.getBoolean("key.mt.retention.root"); + + Map histoEarly = null; + long[] usedMb = new long[reps]; + Proof retainedTarget = null; // stack-local only: the genuine leak path is the only one + // found + for (int i = 0; i < reps; i++) { + KeYEnvironment env = KeYEnvironment.load(keyFile); + Proof proof = null; + try { + proof = env.getLoadedProof(); + ProofStarter starter = new ProofStarter(false); + starter.init(proof); + starter.start(); + } finally { + env.dispose(); + } + if (findRoot && i == 0) { + retainedTarget = proof; // a disposed proof; we will hunt its static referrer + } + usedMb[i] = usedAfterGc() / MB; + System.out.printf("[retention] rep=%-2d liveMB=%d%n", i, usedMb[i]); + if (histo && i == 1) { + histoEarly = classHistogram(); + } + } + + long first = usedMb[0]; + long last = usedMb[reps - 1]; + double perRep = reps > 1 ? (double) (last - first) / (reps - 1) : 0.0; + System.out.printf("[retention] RESULT first=%dMB last=%dMB delta=%dMB (%+.1f MB/proof)%n", + first, last, last - first, perRep); + System.out.printf("[retention] verdict: %s%n", + perRep > 2.0 ? "RETENTION (live heap grows across disposed proofs)" + : "flat (dispose releases per-proof state)"); + + if (histo && histoEarly != null) { + printGrowth(histoEarly, classHistogram()); + } + + String dump = System.getProperty("key.mt.retention.dump"); + if (dump != null) { + usedAfterGc(); // settle before dumping + dumpHeap(dump); + } + + if (findRoot && retainedTarget != null) { + usedAfterGc(); + HeapRootFinder.reportPath(retainedTarget); + } + } + + /** Writes a live-objects-only HPROF heap dump for Eclipse MAT analysis. */ + private static void dumpHeap(String path) { + try { + Path p = Path.of(path); + Files.deleteIfExists(p); + Object bean = ManagementFactory.newPlatformMXBeanProxy( + ManagementFactory.getPlatformMBeanServer(), + "com.sun.management:type=HotSpotDiagnostic", + Class.forName("com.sun.management.HotSpotDiagnosticMXBean")); + bean.getClass().getMethod("dumpHeap", String.class, boolean.class) + .invoke(bean, p.toAbsolutePath().toString(), true); + System.out.printf("[retention] heap dump written: %s%n", p.toAbsolutePath()); + } catch (Exception e) { + System.out.println("[retention] heap dump failed: " + e); + } + } + + /** Live heap after several full GCs, to drain finalizers/soft refs as far as is practical. */ + private static long usedAfterGc() throws InterruptedException { + Runtime rt = Runtime.getRuntime(); + for (int k = 0; k < 5; k++) { + System.gc(); + Thread.sleep(120); + } + return rt.totalMemory() - rt.freeMemory(); + } + + /** class name -> live instance count, via the JVM's GC.class_histogram diagnostic command. */ + private static Map classHistogram() { + Map m = new TreeMap<>(); + try { + String out = (String) ManagementFactory.getPlatformMBeanServer().invoke( + new javax.management.ObjectName("com.sun.management:type=DiagnosticCommand"), + "gcClassHistogram", new Object[] { new String[0] }, + new String[] { String[].class.getName() }); + for (String line : out.split("\n")) { + String[] p = line.trim().split("\\s+"); + // columns: num #instances #bytes class name + if (p.length >= 4 && p[0].endsWith(":")) { + try { + m.put(p[3], Long.parseLong(p[1])); + } catch (NumberFormatException ignore) { + // header / non-data line + } + } + } + } catch (Exception e) { + System.out.println("[retention] histogram unavailable: " + e); + } + return m; + } + + private static void printGrowth(Map early, Map late) { + record Growth(String cls, long delta, long late) { + } + var list = new java.util.ArrayList(); + for (var e : late.entrySet()) { + long d = e.getValue() - early.getOrDefault(e.getKey(), 0L); + if (d > 0) { + list.add(new Growth(e.getKey(), d, e.getValue())); + } + } + list.sort(Comparator.comparingLong((Growth g) -> g.delta).reversed()); + System.out.println("[retention] top live-instance growth (rep1 -> final):"); + for (int i = 0; i < Math.min(25, list.size()); i++) { + Growth g = list.get(i); + System.out.printf("[retention] +%-10d (now %-10d) %s%n", g.delta, g.late, g.cls); + } + } +}