From 45012ab2b3d5df0a0532aceb1c1a8cc18f575e91 Mon Sep 17 00:00:00 2001 From: Martijn Date: Sun, 26 Sep 2021 15:17:35 +0200 Subject: [PATCH 01/18] #1 Add code of Sander and minor changes Beside adding the code, I did the following: - Minor style changes - Add MemoryStats class - Add statistics recording in ZDD classes --- .../java/com/github/javabdd/BDDFactory.java | 65 ++++++++- .../java/com/github/javabdd/JFactory.java | 127 +++++++++++++++++- 2 files changed, 182 insertions(+), 10 deletions(-) diff --git a/src/main/java/com/github/javabdd/BDDFactory.java b/src/main/java/com/github/javabdd/BDDFactory.java index 850246d..9bfaf97 100644 --- a/src/main/java/com/github/javabdd/BDDFactory.java +++ b/src/main/java/com/github/javabdd/BDDFactory.java @@ -1235,16 +1235,19 @@ public ReorderStats getReorderStats() { * Stores statistics about the operator cache. * * @author jwhaley + * @author sthuijsman + * @author mgoorden * @version $Id: BDDFactory.java 480 2010-11-16 01:29:49Z robimalik $ */ public static class CacheStats { - public int uniqueAccess; - public int uniqueChain; - public int uniqueHit; - public int uniqueMiss; - public int opHit; - public int opMiss; - public int swapCount; + public long uniqueAccess; + public long uniqueChain; + public long uniqueHit; + public long uniqueMiss; + public long opAccess; + public long opHit; + public long opMiss; + public long swapCount; protected CacheStats() { } @@ -1253,6 +1256,7 @@ void copyFrom(CacheStats that) { this.uniqueChain = that.uniqueChain; this.uniqueHit = that.uniqueHit; this.uniqueMiss = that.uniqueMiss; + this.opAccess = that.opAccess; this.opHit = that.opHit; this.opMiss = that.opMiss; this.swapCount = that.swapCount; @@ -1294,6 +1298,9 @@ public String toString() { else sb.append((float)0); sb.append(newLine); + sb.append("Operator Access: "); + sb.append(opAccess); + sb.append(newLine); sb.append("Operator Hits: "); sb.append(opHit); sb.append(newLine); @@ -1327,6 +1334,50 @@ public CacheStats getCacheStats() { return cachestats; } + /** + * Stores statistics about the memory usage. + * + * @author mgoorden + */ + public static class MemoryStats { + public long maxUsedMemory; + public long maxUsedBddNodes; + + protected MemoryStats() { } + + public String toString() { + StringBuffer sb = new StringBuffer(); + String newLine = getProperty("line.separator", "\n"); + sb.append(newLine); + sb.append("Memory statistics"); + sb.append(newLine); + sb.append("----------------"); + sb.append(newLine); + + sb.append("Max used memory: "); + sb.append(maxUsedMemory); + sb.append(newLine); + sb.append("Max used BDD nodes: "); + sb.append(maxUsedBddNodes); + sb.append(newLine); + return sb.toString(); + } + } + + /** + * Singleton object for memory statistics. + */ + protected MemoryStats memorystats = new MemoryStats(); + + /** + *

Return the current memory statistics for this BDD factory.

+ * + * @return memory statistics + */ + public MemoryStats getMemoryStats() { + return memorystats; + } + // TODO: bdd_sizeprobe_hook // TODO: bdd_reorder_probe diff --git a/src/main/java/com/github/javabdd/JFactory.java b/src/main/java/com/github/javabdd/JFactory.java index c6ae87a..70bd647 100644 --- a/src/main/java/com/github/javabdd/JFactory.java +++ b/src/main/java/com/github/javabdd/JFactory.java @@ -38,10 +38,16 @@ public class JFactory extends BDDFactoryIntImpl { public static boolean FLUSH_CACHE_ON_GC = true; static final boolean VERIFY_ASSERTIONS = false; - static final boolean CACHESTATS = false; static final boolean SWAPCOUNT = false; - + public static final boolean CACHESTATS = true; public static final String REVISION = "$Revision: 480 $"; + + // MeasureEffort: values below may be adapted + // TODO: add option to communicate to JFactory whether it needs to measure stats and which, so no hard coded + // options need to be changed manually. + public boolean measureEffort_MaxRAM = true; + public boolean measureEffort_MaxBDDnodes = true; + public boolean measureEffort_TrackContinuous = false; public String getVersion() { return "JFactory "+REVISION.substring(11, REVISION.length()-2); @@ -203,7 +209,6 @@ protected int makenode_impl(int lev, int lo, int hi) { public int setCacheSize(int v) { return bdd_setcachesize(v); } public boolean isZDD() { return ZDD; } public boolean isInitialized() { return bddrunning; } - public void done() { super.done(); bdd_done(); } public void setError(int code) { bdderrorcond = code; } public void clearError() { bdderrorcond = 0; } public int setMaxNodeNum(int size) { return bdd_setmaxnodenum(size); } @@ -975,6 +980,9 @@ int bdd_not(int r) { int not_rec(int r) { BddCacheDataI entry; int res; + + if (CACHESTATS) + cachestats.opAccess++; if (ISCONST(r)) return 1 - r; @@ -1035,6 +1043,9 @@ int ite_rec(int f, int g, int h) { BddCacheDataI entry; int res; + if (CACHESTATS) + cachestats.opAccess++; + if (ISONE(f)) return g; if (ISZERO(f)) @@ -1112,6 +1123,9 @@ int ite_rec(int f, int g, int h) { int zite_rec(int f, int g, int h) { BddCacheDataI entry; int res; + + if (CACHESTATS) + cachestats.opAccess++; if (ISONE(f)) return g; @@ -1226,6 +1240,9 @@ int replace_rec(int r) { BddCacheDataI entry; int res; + if (CACHESTATS) + cachestats.opAccess++; + if (ISCONST(r) || LEVEL(r) > replacelast) return r; @@ -1438,6 +1455,9 @@ int bdd_apply(int l, int r, int op) { int apply_rec(int l, int r) { BddCacheDataI entry; int res; + + if (CACHESTATS) + cachestats.opAccess++; if (VERIFY_ASSERTIONS) _assert(!ZDD); if (VERIFY_ASSERTIONS) _assert(applyop != bddop_and && applyop != bddop_or); @@ -1511,6 +1531,9 @@ int and_rec(int l, int r) { BddCacheDataI entry; int res; + if (CACHESTATS) + cachestats.opAccess++; + if (l == r) return l; if (ISZERO(l) || ISZERO(r)) @@ -1558,6 +1581,9 @@ int zand_rec(int l, int r) { BddCacheDataI entry; int res; + if (CACHESTATS) + cachestats.opAccess++; + if (l == r) return l; if (ISZERO(l) || ISZERO(r)) @@ -1596,6 +1622,9 @@ int zrelprod_rec(int l, int r, int lev) { BddCacheDataI entry; int res; + if (CACHESTATS) + cachestats.opAccess++; + if (l == r) return zquant_rec(l, lev); if (ISZERO(l) || ISZERO(r)) @@ -1672,6 +1701,9 @@ int or_rec(int l, int r) { BddCacheDataI entry; int res; + if (CACHESTATS) + cachestats.opAccess++; + if (l == r) return l; if (ISONE(l) || ISONE(r)) @@ -1717,6 +1749,9 @@ int or_rec(int l, int r) { int zor_rec(int l, int r) { BddCacheDataI entry; int res; + + if (CACHESTATS) + cachestats.opAccess++; if (l == r) return l; @@ -1763,6 +1798,9 @@ int zor_rec(int l, int r) { int zdiff_rec(int l, int r) { BddCacheDataI entry; int res; + + if (CACHESTATS) + cachestats.opAccess++; if (ISZERO(l) /*|| ISONE(r)*/ || l == r) return 0; @@ -1803,6 +1841,9 @@ int zdiff_rec(int l, int r) { int relprod_rec(int l, int r) { BddCacheDataI entry; int res; + + if (CACHESTATS) + cachestats.opAccess++; if (VERIFY_ASSERTIONS) _assert(!ZDD); @@ -1981,6 +2022,9 @@ int varset2svartable(int r) { int appquant_rec(int l, int r) { BddCacheDataI entry; int res; + + if (CACHESTATS) + cachestats.opAccess++; if (VERIFY_ASSERTIONS) _assert(appexop != bddop_and); @@ -2073,6 +2117,9 @@ else if (LEVEL(l) > quantlast && LEVEL(r) > quantlast) { int appuni_rec(int l, int r, int var) { BddCacheDataI entry; int res; + + if (CACHESTATS) + cachestats.opAccess++; int LEVEL_l, LEVEL_r, LEVEL_var; LEVEL_l = LEVEL(l); @@ -2161,6 +2208,9 @@ int unique_rec(int r, int q) { BddCacheDataI entry; int res; int LEVEL_r, LEVEL_q; + + if (CACHESTATS) + cachestats.opAccess++; LEVEL_r = LEVEL(r); LEVEL_q = LEVEL(q); @@ -2204,6 +2254,9 @@ int quant_rec(int r) { BddCacheDataI entry; int res; + if (CACHESTATS) + cachestats.opAccess++; + if (r < 2 || LEVEL(r) > quantlast) return r; @@ -2242,6 +2295,10 @@ int quant_rec(int r) { int zquant_rec(int r, int lev) { BddCacheDataI entry; int res; + + if (CACHESTATS) + cachestats.opAccess++; + for (;;) { if (lev > quantlast) @@ -2337,6 +2394,9 @@ int constrain_rec(int f, int c) { BddCacheDataI entry; int res; + if (CACHESTATS) + cachestats.opAccess++; + if (ISONE(c)) return f; if (ISCONST(f)) @@ -2434,6 +2494,9 @@ int compose_rec(int f, int g) { BddCacheDataI entry; int res; + if (CACHESTATS) + cachestats.opAccess++; + if (LEVEL(f) > composelevel) return f; @@ -2513,6 +2576,9 @@ int veccompose_rec(int f) { BddCacheDataI entry; int res; + if (CACHESTATS) + cachestats.opAccess++; + if (LEVEL(f) > replacelast) return f; @@ -2694,6 +2760,9 @@ int bdd_restrict(int r, int var) { int restrict_rec(int r) { BddCacheDataI entry; int res; + + if (CACHESTATS) + cachestats.opAccess++; if (ISCONST(r) || LEVEL(r) > quantlast) return r; @@ -2763,6 +2832,9 @@ int simplify_rec(int f, int d) { BddCacheDataI entry; int res; + if (CACHESTATS) + cachestats.opAccess++; + if (ISONE(d) || ISCONST(f)) return f; if (d == f) @@ -3432,7 +3504,36 @@ int bdd_addref(int root) { return root; } + int MeasureEffort_BDDCOUNT() { + for (int r = 0; r < bddrefstacktop; r++) + bdd_mark(bddrefstack[r]); + + for (int n = 0; n < bddnodesize; n++) { + if (HASREF(n)) bdd_mark(n); + } + + int MeasureEffort_BDD_FREECOUNT = 0; + + for (int n = bddnodesize - 1; n >= 2; n--) { + if (MARKED(n) && LOW(n) != INVALID_BDD) { + UNMARK(n); + } else { + MeasureEffort_BDD_FREECOUNT++; + } + } + + return bddnodesize - MeasureEffort_BDD_FREECOUNT; + } + int bdd_delref(int root) { + if (measureEffort_MaxBDDnodes) + memorystats.maxUsedBddNodes = Math.max(MeasureEffort_BDDCOUNT(), memorystats.maxUsedBddNodes); + if (measureEffort_MaxRAM) + memorystats.maxUsedMemory = Math.max(Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(), + memorystats.maxUsedMemory); + //if (measureEffort_TrackContinuous) + // OutputProvider.out("opMiss=" + cachestats.opMiss + ":USED_BDD_NODES=" + String.valueOf(MeasureEffort_BDDCOUNT())); + if (root == INVALID_BDD) bdd_error(BDD_BREAK); /* distinctive */ if (root < 2 || !bddrunning) @@ -4959,6 +5060,26 @@ int bdd_reorder_gain() { return (100 * (usednum_before - usednum_after)) / usednum_before; } + public void done() { + if (measureEffort_MaxRAM) { + + memorystats.maxUsedMemory = Math.max(Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(), + memorystats.maxUsedMemory); + bdd_gbc(); // To make sure new test is accurate. + System.gc(); // To make sure new test is accurate. + } + + if (measureEffort_MaxBDDnodes) { + memorystats.maxUsedBddNodes = Math.max(MeasureEffort_BDDCOUNT(), memorystats.maxUsedBddNodes); + bdd_gbc(); // To make sure new test is accurate. + System.gc(); // To make sure new test is accurate. + } + + super.done(); + bdd_done(); + } + + void bdd_done() { /*sanitycheck(); FIXME */ //bdd_fdd_done(); From 827d49776e14e0e4818ecec479e7e7a5afa9be78 Mon Sep 17 00:00:00 2001 From: Martijn Date: Sun, 26 Sep 2021 16:10:05 +0200 Subject: [PATCH 02/18] #1 Introduce continuous statistics class --- .../java/com/github/javabdd/BDDFactory.java | 75 ++++++++++++++++--- .../java/com/github/javabdd/JFactory.java | 18 ++--- 2 files changed, 73 insertions(+), 20 deletions(-) diff --git a/src/main/java/com/github/javabdd/BDDFactory.java b/src/main/java/com/github/javabdd/BDDFactory.java index 9bfaf97..e52171a 100644 --- a/src/main/java/com/github/javabdd/BDDFactory.java +++ b/src/main/java/com/github/javabdd/BDDFactory.java @@ -3,6 +3,7 @@ // Licensed under the terms of the GNU LGPL; see COPYING for details. package com.github.javabdd; +import java.util.ArrayList; import java.util.Arrays; import java.util.BitSet; import java.util.Collection; @@ -1335,21 +1336,21 @@ public CacheStats getCacheStats() { } /** - * Stores statistics about the memory usage. + * Stores statistics about the maximum memory usage. * * @author mgoorden */ - public static class MemoryStats { + public static class MaxMemoryStats { public long maxUsedMemory; - public long maxUsedBddNodes; + public int maxUsedBddNodes; - protected MemoryStats() { } + protected MaxMemoryStats() { } public String toString() { StringBuffer sb = new StringBuffer(); String newLine = getProperty("line.separator", "\n"); sb.append(newLine); - sb.append("Memory statistics"); + sb.append("Max memory statistics"); sb.append(newLine); sb.append("----------------"); sb.append(newLine); @@ -1365,17 +1366,69 @@ public String toString() { } /** - * Singleton object for memory statistics. + * Singleton object for maximum memory statistics. */ - protected MemoryStats memorystats = new MemoryStats(); + protected MaxMemoryStats maxmemorystats = new MaxMemoryStats(); /** - *

Return the current memory statistics for this BDD factory.

+ *

Return the current maximum memory statistics for this BDD factory.

* - * @return memory statistics + * @return maximum memory statistics */ - public MemoryStats getMemoryStats() { - return memorystats; + public MaxMemoryStats getMemoryStats() { + return maxmemorystats; + } + + /** + * Stores continuously statistics about the memory usage and BDD operations. + * + * @author mgoorden + */ + public static class ContinousStats { + public List contMemory = new ArrayList (); + public List contOperations = new ArrayList (); + + protected ContinousStats() { } + + public String toString() { + StringBuffer sb = new StringBuffer(); + String newLine = getProperty("line.separator", "\n"); + sb.append(newLine); + sb.append("Continuous memory statistics"); + sb.append(newLine); + sb.append("----------------"); + sb.append(newLine); + + if (contMemory.size() != contOperations.size()) { + sb.append("Incorrect data collection."); + sb.append(newLine); + + return sb.toString(); + } + + for (int i = 0; i < contMemory.size(); i++) { + sb.append(contMemory.get(i)); + sb.append(","); + sb.append(contOperations.get(i)); + sb.append(newLine); + } + + return sb.toString(); + } + } + + /** + * Singleton object for continuous statistics. + */ + protected ContinousStats continousstats = new ContinousStats(); + + /** + *

Return the current continuous statistics for this BDD factory.

+ * + * @return continuous statistics + */ + public ContinousStats getContinousStats() { + return continousstats; } // TODO: bdd_sizeprobe_hook diff --git a/src/main/java/com/github/javabdd/JFactory.java b/src/main/java/com/github/javabdd/JFactory.java index 70bd647..2da7fa5 100644 --- a/src/main/java/com/github/javabdd/JFactory.java +++ b/src/main/java/com/github/javabdd/JFactory.java @@ -3527,12 +3527,13 @@ int MeasureEffort_BDDCOUNT() { int bdd_delref(int root) { if (measureEffort_MaxBDDnodes) - memorystats.maxUsedBddNodes = Math.max(MeasureEffort_BDDCOUNT(), memorystats.maxUsedBddNodes); + maxmemorystats.maxUsedBddNodes = Math.max(MeasureEffort_BDDCOUNT(), maxmemorystats.maxUsedBddNodes); if (measureEffort_MaxRAM) - memorystats.maxUsedMemory = Math.max(Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(), - memorystats.maxUsedMemory); - //if (measureEffort_TrackContinuous) - // OutputProvider.out("opMiss=" + cachestats.opMiss + ":USED_BDD_NODES=" + String.valueOf(MeasureEffort_BDDCOUNT())); + maxmemorystats.maxUsedMemory = Math.max(Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(), + maxmemorystats.maxUsedMemory); + if (measureEffort_TrackContinuous) + continousstats.contMemory.add(MeasureEffort_BDDCOUNT()); + continousstats.contOperations.add(cachestats.opMiss); if (root == INVALID_BDD) bdd_error(BDD_BREAK); /* distinctive */ @@ -5062,15 +5063,14 @@ int bdd_reorder_gain() { public void done() { if (measureEffort_MaxRAM) { - - memorystats.maxUsedMemory = Math.max(Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(), - memorystats.maxUsedMemory); + maxmemorystats.maxUsedMemory = Math.max(Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(), + maxmemorystats.maxUsedMemory); bdd_gbc(); // To make sure new test is accurate. System.gc(); // To make sure new test is accurate. } if (measureEffort_MaxBDDnodes) { - memorystats.maxUsedBddNodes = Math.max(MeasureEffort_BDDCOUNT(), memorystats.maxUsedBddNodes); + maxmemorystats.maxUsedBddNodes = Math.max(MeasureEffort_BDDCOUNT(), maxmemorystats.maxUsedBddNodes); bdd_gbc(); // To make sure new test is accurate. System.gc(); // To make sure new test is accurate. } From 7ca9e6715fc1f868c0e1a8a79f48bcd7845346ef Mon Sep 17 00:00:00 2001 From: Martijn Date: Sun, 26 Sep 2021 16:23:54 +0200 Subject: [PATCH 03/18] #1 Measure only when requested --- .../java/com/github/javabdd/BDDFactory.java | 19 ++++++++++ .../java/com/github/javabdd/JFactory.java | 35 +++++++------------ 2 files changed, 32 insertions(+), 22 deletions(-) diff --git a/src/main/java/com/github/javabdd/BDDFactory.java b/src/main/java/com/github/javabdd/BDDFactory.java index e52171a..4ff9716 100644 --- a/src/main/java/com/github/javabdd/BDDFactory.java +++ b/src/main/java/com/github/javabdd/BDDFactory.java @@ -1263,6 +1263,10 @@ void copyFrom(CacheStats that) { this.swapCount = that.swapCount; } + public void enableMeasurements() { + CACHESTATS = true; + } + /* (non-Javadoc) * @see java.lang.Object#toString() */ @@ -1320,6 +1324,11 @@ public String toString() { return sb.toString(); } } + + /** + * Whether to measure cache statistics. + */ + public static boolean CACHESTATS; /** * Singleton object for cache statistics. @@ -1341,11 +1350,16 @@ public CacheStats getCacheStats() { * @author mgoorden */ public static class MaxMemoryStats { + public boolean measuring = false; public long maxUsedMemory; public int maxUsedBddNodes; protected MaxMemoryStats() { } + public void enableMeasurments() { + measuring = true; + } + public String toString() { StringBuffer sb = new StringBuffer(); String newLine = getProperty("line.separator", "\n"); @@ -1385,10 +1399,15 @@ public MaxMemoryStats getMemoryStats() { * @author mgoorden */ public static class ContinousStats { + public boolean measuring = false; public List contMemory = new ArrayList (); public List contOperations = new ArrayList (); protected ContinousStats() { } + + public void enableMeasurments() { + measuring = true; + } public String toString() { StringBuffer sb = new StringBuffer(); diff --git a/src/main/java/com/github/javabdd/JFactory.java b/src/main/java/com/github/javabdd/JFactory.java index 2da7fa5..143b1be 100644 --- a/src/main/java/com/github/javabdd/JFactory.java +++ b/src/main/java/com/github/javabdd/JFactory.java @@ -39,15 +39,7 @@ public class JFactory extends BDDFactoryIntImpl { static final boolean VERIFY_ASSERTIONS = false; static final boolean SWAPCOUNT = false; - public static final boolean CACHESTATS = true; public static final String REVISION = "$Revision: 480 $"; - - // MeasureEffort: values below may be adapted - // TODO: add option to communicate to JFactory whether it needs to measure stats and which, so no hard coded - // options need to be changed manually. - public boolean measureEffort_MaxRAM = true; - public boolean measureEffort_MaxBDDnodes = true; - public boolean measureEffort_TrackContinuous = false; public String getVersion() { return "JFactory "+REVISION.substring(11, REVISION.length()-2); @@ -3504,7 +3496,7 @@ int bdd_addref(int root) { return root; } - int MeasureEffort_BDDCOUNT() { + int bdd_count() { for (int r = 0; r < bddrefstacktop; r++) bdd_mark(bddrefstack[r]); @@ -3524,16 +3516,20 @@ int MeasureEffort_BDDCOUNT() { return bddnodesize - MeasureEffort_BDD_FREECOUNT; } - + + // TODO move max function to maxmemorystats. + int bdd_delref(int root) { - if (measureEffort_MaxBDDnodes) - maxmemorystats.maxUsedBddNodes = Math.max(MeasureEffort_BDDCOUNT(), maxmemorystats.maxUsedBddNodes); - if (measureEffort_MaxRAM) + if (maxmemorystats.measuring) { + maxmemorystats.maxUsedBddNodes = Math.max(bdd_count(), maxmemorystats.maxUsedBddNodes); maxmemorystats.maxUsedMemory = Math.max(Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(), maxmemorystats.maxUsedMemory); - if (measureEffort_TrackContinuous) - continousstats.contMemory.add(MeasureEffort_BDDCOUNT()); + } + + if (continousstats.measuring) { + continousstats.contMemory.add(bdd_count()); continousstats.contOperations.add(cachestats.opMiss); + } if (root == INVALID_BDD) bdd_error(BDD_BREAK); /* distinctive */ @@ -5062,15 +5058,10 @@ int bdd_reorder_gain() { } public void done() { - if (measureEffort_MaxRAM) { + if (maxmemorystats.measuring) { maxmemorystats.maxUsedMemory = Math.max(Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(), maxmemorystats.maxUsedMemory); - bdd_gbc(); // To make sure new test is accurate. - System.gc(); // To make sure new test is accurate. - } - - if (measureEffort_MaxBDDnodes) { - maxmemorystats.maxUsedBddNodes = Math.max(MeasureEffort_BDDCOUNT(), maxmemorystats.maxUsedBddNodes); + maxmemorystats.maxUsedBddNodes = Math.max(bdd_count(), maxmemorystats.maxUsedBddNodes); bdd_gbc(); // To make sure new test is accurate. System.gc(); // To make sure new test is accurate. } From f16146ca6ca47fb635541f44fbab9c153ce9b8d3 Mon Sep 17 00:00:00 2001 From: Martijn Date: Sun, 26 Sep 2021 16:26:29 +0200 Subject: [PATCH 04/18] #1 Move update of max memory stats to stats class --- src/main/java/com/github/javabdd/BDDFactory.java | 5 +++++ src/main/java/com/github/javabdd/JFactory.java | 12 ++++-------- 2 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/main/java/com/github/javabdd/BDDFactory.java b/src/main/java/com/github/javabdd/BDDFactory.java index 4ff9716..cd670ff 100644 --- a/src/main/java/com/github/javabdd/BDDFactory.java +++ b/src/main/java/com/github/javabdd/BDDFactory.java @@ -1360,6 +1360,11 @@ public void enableMeasurments() { measuring = true; } + public void newMeasurement(int newBddNodes, long newMemory) { + maxUsedBddNodes = Math.max(newBddNodes, maxUsedBddNodes); + maxUsedMemory = Math.max(newMemory, maxUsedMemory); + } + public String toString() { StringBuffer sb = new StringBuffer(); String newLine = getProperty("line.separator", "\n"); diff --git a/src/main/java/com/github/javabdd/JFactory.java b/src/main/java/com/github/javabdd/JFactory.java index 143b1be..6369450 100644 --- a/src/main/java/com/github/javabdd/JFactory.java +++ b/src/main/java/com/github/javabdd/JFactory.java @@ -3517,13 +3517,10 @@ int bdd_count() { return bddnodesize - MeasureEffort_BDD_FREECOUNT; } - // TODO move max function to maxmemorystats. - int bdd_delref(int root) { if (maxmemorystats.measuring) { - maxmemorystats.maxUsedBddNodes = Math.max(bdd_count(), maxmemorystats.maxUsedBddNodes); - maxmemorystats.maxUsedMemory = Math.max(Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(), - maxmemorystats.maxUsedMemory); + long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); + maxmemorystats.newMeasurement(bdd_count(), memory); } if (continousstats.measuring) { @@ -5059,9 +5056,8 @@ int bdd_reorder_gain() { public void done() { if (maxmemorystats.measuring) { - maxmemorystats.maxUsedMemory = Math.max(Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(), - maxmemorystats.maxUsedMemory); - maxmemorystats.maxUsedBddNodes = Math.max(bdd_count(), maxmemorystats.maxUsedBddNodes); + long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); + maxmemorystats.newMeasurement(bdd_count(), memory); bdd_gbc(); // To make sure new test is accurate. System.gc(); // To make sure new test is accurate. } From 8b246e6c8a29ea14053c0fabb25978f4263e4085 Mon Sep 17 00:00:00 2001 From: Martijn Date: Sun, 26 Sep 2021 16:41:14 +0200 Subject: [PATCH 05/18] #1 Remove system memory usage measurements As system memory usages fluctuates over time, tool implementation, hardware, etc., measuring these statistics are 'removed' by commenting the out. If one (who knows what he is doing) still wants to measure the system memory usage, the code is still available. By removing system memory statistics, the statistics output is completely deterministic for the same input and bdd operations. --- .../java/com/github/javabdd/BDDFactory.java | 26 ++++++++++++++----- .../java/com/github/javabdd/JFactory.java | 23 +++++++++++++--- 2 files changed, 38 insertions(+), 11 deletions(-) diff --git a/src/main/java/com/github/javabdd/BDDFactory.java b/src/main/java/com/github/javabdd/BDDFactory.java index cd670ff..eb477c2 100644 --- a/src/main/java/com/github/javabdd/BDDFactory.java +++ b/src/main/java/com/github/javabdd/BDDFactory.java @@ -1360,6 +1360,10 @@ public void enableMeasurments() { measuring = true; } + public void newMeasurement(int newBddNodes) { + maxUsedBddNodes = Math.max(newBddNodes, maxUsedBddNodes); + } + public void newMeasurement(int newBddNodes, long newMemory) { maxUsedBddNodes = Math.max(newBddNodes, maxUsedBddNodes); maxUsedMemory = Math.max(newMemory, maxUsedMemory); @@ -1374,9 +1378,15 @@ public String toString() { sb.append("----------------"); sb.append(newLine); - sb.append("Max used memory: "); - sb.append(maxUsedMemory); - sb.append(newLine); + // 'max memory usages'. + // Measuring max memory usages fluctuates over time, tool implementation, + // used hardware, etc. Therefore, if one wants to display this information, + // he/she should uncomment lines below. + //sb.append("Max used memory: "); + //sb.append(maxUsedMemory); + //sb.append(newLine); + // End of 'max memory usages' comment. + sb.append("Max used BDD nodes: "); sb.append(maxUsedBddNodes); sb.append(newLine); @@ -1405,8 +1415,8 @@ public MaxMemoryStats getMemoryStats() { */ public static class ContinousStats { public boolean measuring = false; - public List contMemory = new ArrayList (); - public List contOperations = new ArrayList (); + public List contMemory = new ArrayList(); + public List contOperations = new ArrayList(); protected ContinousStats() { } @@ -1420,6 +1430,8 @@ public String toString() { sb.append(newLine); sb.append("Continuous memory statistics"); sb.append(newLine); + sb.append("Cumulative BDD operations, BDD nodes"); + sb.append(newLine); sb.append("----------------"); sb.append(newLine); @@ -1431,9 +1443,9 @@ public String toString() { } for (int i = 0; i < contMemory.size(); i++) { - sb.append(contMemory.get(i)); - sb.append(","); sb.append(contOperations.get(i)); + sb.append(","); + sb.append(contMemory.get(i)); sb.append(newLine); } diff --git a/src/main/java/com/github/javabdd/JFactory.java b/src/main/java/com/github/javabdd/JFactory.java index 6369450..ddb1e75 100644 --- a/src/main/java/com/github/javabdd/JFactory.java +++ b/src/main/java/com/github/javabdd/JFactory.java @@ -3519,8 +3519,15 @@ int bdd_count() { int bdd_delref(int root) { if (maxmemorystats.measuring) { - long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); - maxmemorystats.newMeasurement(bdd_count(), memory); + maxmemorystats.newMeasurement(bdd_count()); + + // 'max memory usages'. + // Measuring max memory usages fluctuates over time, tool implementation, + // used hardware, etc. Therefore, if one wants to collect this information, + // he/she should uncomment lines below. + //long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); + //maxmemorystats.newMeasurement(bdd_count(), memory); + // End of 'max memory usages' comment. } if (continousstats.measuring) { @@ -5056,8 +5063,16 @@ int bdd_reorder_gain() { public void done() { if (maxmemorystats.measuring) { - long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); - maxmemorystats.newMeasurement(bdd_count(), memory); + maxmemorystats.newMeasurement(bdd_count()); + + // 'max memory usages'. + // Measuring max memory usages fluctuates over time, tool implementation, + // used hardware, etc. Therefore, if one wants to collect this information, + // he/she should uncomment lines below. + //long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); + //maxmemorystats.newMeasurement(bdd_count(), memory); + // End of 'max memory usages' comment. + bdd_gbc(); // To make sure new test is accurate. System.gc(); // To make sure new test is accurate. } From 946158227b389dc47de00e27fd76b3e3404c5863 Mon Sep 17 00:00:00 2001 From: Martijn Date: Sun, 26 Sep 2021 17:00:56 +0200 Subject: [PATCH 06/18] #1 Remove formatting of stats for printing Now the caller of the BDD package should determine how to format the stats printing. We now just return the stats. --- .../java/com/github/javabdd/BDDFactory.java | 69 ++++++------------- .../java/com/github/javabdd/JFactory.java | 6 +- 2 files changed, 25 insertions(+), 50 deletions(-) diff --git a/src/main/java/com/github/javabdd/BDDFactory.java b/src/main/java/com/github/javabdd/BDDFactory.java index eb477c2..9adf78c 100644 --- a/src/main/java/com/github/javabdd/BDDFactory.java +++ b/src/main/java/com/github/javabdd/BDDFactory.java @@ -1369,29 +1369,18 @@ public void newMeasurement(int newBddNodes, long newMemory) { maxUsedMemory = Math.max(newMemory, maxUsedMemory); } - public String toString() { - StringBuffer sb = new StringBuffer(); - String newLine = getProperty("line.separator", "\n"); - sb.append(newLine); - sb.append("Max memory statistics"); - sb.append(newLine); - sb.append("----------------"); - sb.append(newLine); - - // 'max memory usages'. - // Measuring max memory usages fluctuates over time, tool implementation, - // used hardware, etc. Therefore, if one wants to display this information, - // he/she should uncomment lines below. - //sb.append("Max used memory: "); - //sb.append(maxUsedMemory); - //sb.append(newLine); - // End of 'max memory usages' comment. - - sb.append("Max used BDD nodes: "); - sb.append(maxUsedBddNodes); - sb.append(newLine); - return sb.toString(); + public int getMaxNodes() { + return maxUsedBddNodes; } + + // 'max memory usages'. + // Measuring max memory usages fluctuates over time, tool implementation, + // used hardware, etc. Therefore, if one wants to collect this information, + // he/she should uncomment lines below and in JFactory.java. + //public long getMaxUsedMemory() { + // return maxUsedMemory; + //} + // End of 'max memory usages' comment. } /** @@ -1415,7 +1404,7 @@ public MaxMemoryStats getMemoryStats() { */ public static class ContinousStats { public boolean measuring = false; - public List contMemory = new ArrayList(); + public List contNodes = new ArrayList(); public List contOperations = new ArrayList(); protected ContinousStats() { } @@ -1424,32 +1413,18 @@ public void enableMeasurments() { measuring = true; } - public String toString() { - StringBuffer sb = new StringBuffer(); - String newLine = getProperty("line.separator", "\n"); - sb.append(newLine); - sb.append("Continuous memory statistics"); - sb.append(newLine); - sb.append("Cumulative BDD operations, BDD nodes"); - sb.append(newLine); - sb.append("----------------"); - sb.append(newLine); - - if (contMemory.size() != contOperations.size()) { - sb.append("Incorrect data collection."); - sb.append(newLine); - - return sb.toString(); + public List getNodesStats() { + if (contNodes.size() != contOperations.size()) { + throw new AssertionError("Incorrect data collection."); } - - for (int i = 0; i < contMemory.size(); i++) { - sb.append(contOperations.get(i)); - sb.append(","); - sb.append(contMemory.get(i)); - sb.append(newLine); + return contNodes; + } + + public List getOperationsStats() { + if (contNodes.size() != contOperations.size()) { + throw new AssertionError("Incorrect data collection."); } - - return sb.toString(); + return contOperations; } } diff --git a/src/main/java/com/github/javabdd/JFactory.java b/src/main/java/com/github/javabdd/JFactory.java index ddb1e75..e488d93 100644 --- a/src/main/java/com/github/javabdd/JFactory.java +++ b/src/main/java/com/github/javabdd/JFactory.java @@ -3524,14 +3524,14 @@ int bdd_delref(int root) { // 'max memory usages'. // Measuring max memory usages fluctuates over time, tool implementation, // used hardware, etc. Therefore, if one wants to collect this information, - // he/she should uncomment lines below. + // he/she should uncomment lines below and in BDDFactory.java. //long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); //maxmemorystats.newMeasurement(bdd_count(), memory); // End of 'max memory usages' comment. } if (continousstats.measuring) { - continousstats.contMemory.add(bdd_count()); + continousstats.contNodes.add(bdd_count()); continousstats.contOperations.add(cachestats.opMiss); } @@ -5068,7 +5068,7 @@ public void done() { // 'max memory usages'. // Measuring max memory usages fluctuates over time, tool implementation, // used hardware, etc. Therefore, if one wants to collect this information, - // he/she should uncomment lines below. + // he/she should uncomment lines below and in BDDFactory.java. //long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); //maxmemorystats.newMeasurement(bdd_count(), memory); // End of 'max memory usages' comment. From b65cbc27ab1f7cf9aaa1217dacfd204488fe1561 Mon Sep 17 00:00:00 2001 From: Martijn Date: Sun, 26 Sep 2021 17:02:34 +0200 Subject: [PATCH 07/18] #1 Update CHANGES.md --- CHANGES.md | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index e854cf4..a690e8a 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,12 +1,13 @@ -# Changelog for com.github.javabdd - -All notable changes to this project will be documented in this file. - -## [Unreleased] -* Added CHANGES.md to track changes between releases. - -## [1.0.1] - 2020-03-17 -* Updated SCM URL for proper Maven Central metadata. - -## [1.0.0] - 2020-03-13 -* First release of com.github.javabdd. +# Changelog for com.github.javabdd + +All notable changes to this project will be documented in this file. + +## [Unreleased] +* Added CHANGES.md to track changes between releases. +* Added the collection of performance statistics. + +## [1.0.1] - 2020-03-17 +* Updated SCM URL for proper Maven Central metadata. + +## [1.0.0] - 2020-03-13 +* First release of com.github.javabdd. From 75de33568c15bd1b99510bf186077c8489b4d990 Mon Sep 17 00:00:00 2001 From: Martijn Date: Sun, 26 Sep 2021 17:02:34 +0200 Subject: [PATCH 08/18] Revert "#1 Update CHANGES.md" This reverts commit b65cbc27ab1f7cf9aaa1217dacfd204488fe1561. --- CHANGES.md | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index a690e8a..e854cf4 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,13 +1,12 @@ -# Changelog for com.github.javabdd - -All notable changes to this project will be documented in this file. - -## [Unreleased] -* Added CHANGES.md to track changes between releases. -* Added the collection of performance statistics. - -## [1.0.1] - 2020-03-17 -* Updated SCM URL for proper Maven Central metadata. - -## [1.0.0] - 2020-03-13 -* First release of com.github.javabdd. +# Changelog for com.github.javabdd + +All notable changes to this project will be documented in this file. + +## [Unreleased] +* Added CHANGES.md to track changes between releases. + +## [1.0.1] - 2020-03-17 +* Updated SCM URL for proper Maven Central metadata. + +## [1.0.0] - 2020-03-13 +* First release of com.github.javabdd. From aad28d551d7a38973dc72f93302ad3e70ad8565e Mon Sep 17 00:00:00 2001 From: Martijn Date: Thu, 21 Oct 2021 10:56:37 +0200 Subject: [PATCH 09/18] #1 Fix textual changes from review --- CHANGES.md | 1 + .../java/com/github/javabdd/BDDFactory.java | 50 +++++++++---------- .../java/com/github/javabdd/JFactory.java | 47 +++++++++-------- 3 files changed, 53 insertions(+), 45 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index e854cf4..3470451 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -4,6 +4,7 @@ All notable changes to this project will be documented in this file. ## [Unreleased] * Added CHANGES.md to track changes between releases. +* Added the collection of performance statistics. ## [1.0.1] - 2020-03-17 * Updated SCM URL for proper Maven Central metadata. diff --git a/src/main/java/com/github/javabdd/BDDFactory.java b/src/main/java/com/github/javabdd/BDDFactory.java index 9adf78c..62fdb31 100644 --- a/src/main/java/com/github/javabdd/BDDFactory.java +++ b/src/main/java/com/github/javabdd/BDDFactory.java @@ -1350,22 +1350,22 @@ public CacheStats getCacheStats() { * @author mgoorden */ public static class MaxMemoryStats { - public boolean measuring = false; - public long maxUsedMemory; - public int maxUsedBddNodes; + protected boolean enabled = false; + protected long maxUsedMemory; + protected int maxUsedBddNodes; protected MaxMemoryStats() { } - public void enableMeasurments() { - measuring = true; + public void enableMeasurements() { + enabled = true; } - public void newMeasurement(int newBddNodes) { - maxUsedBddNodes = Math.max(newBddNodes, maxUsedBddNodes); + public void newMeasurement(int newUsedBddNodes) { + maxUsedBddNodes = Math.max(newUsedBddNodes, maxUsedBddNodes); } - public void newMeasurement(int newBddNodes, long newMemory) { - maxUsedBddNodes = Math.max(newBddNodes, maxUsedBddNodes); + public void newMeasurement(int newUsedBddNodes, long newMemory) { + maxUsedBddNodes = Math.max(newUsedBddNodes, maxUsedBddNodes); maxUsedMemory = Math.max(newMemory, maxUsedMemory); } @@ -1402,44 +1402,44 @@ public MaxMemoryStats getMemoryStats() { * * @author mgoorden */ - public static class ContinousStats { - public boolean measuring = false; - public List contNodes = new ArrayList(); - public List contOperations = new ArrayList(); + public static class ContinuousStats { + protected boolean enabled = false; + protected List contUsedBddNodes = new ArrayList(); + protected List contUsedOperations = new ArrayList(); - protected ContinousStats() { } + protected ContinuousStats() { } - public void enableMeasurments() { - measuring = true; + public void enableMeasurements() { + enabled = true; } public List getNodesStats() { - if (contNodes.size() != contOperations.size()) { - throw new AssertionError("Incorrect data collection."); + if (contUsedBddNodes.size() != contUsedOperations.size()) { + throw new AssertionError("Incorrect data collection."); } - return contNodes; + return contUsedBddNodes; } public List getOperationsStats() { - if (contNodes.size() != contOperations.size()) { - throw new AssertionError("Incorrect data collection."); + if (contUsedBddNodes.size() != contUsedOperations.size()) { + throw new AssertionError("Incorrect data collection."); } - return contOperations; + return contUsedOperations; } } /** * Singleton object for continuous statistics. */ - protected ContinousStats continousstats = new ContinousStats(); + protected ContinuousStats continuousstats = new ContinuousStats(); /** *

Return the current continuous statistics for this BDD factory.

* * @return continuous statistics */ - public ContinousStats getContinousStats() { - return continousstats; + public ContinuousStats getContinousStats() { + return continuousstats; } // TODO: bdd_sizeprobe_hook diff --git a/src/main/java/com/github/javabdd/JFactory.java b/src/main/java/com/github/javabdd/JFactory.java index e488d93..8899416 100644 --- a/src/main/java/com/github/javabdd/JFactory.java +++ b/src/main/java/com/github/javabdd/JFactory.java @@ -39,6 +39,7 @@ public class JFactory extends BDDFactoryIntImpl { static final boolean VERIFY_ASSERTIONS = false; static final boolean SWAPCOUNT = false; + public static final String REVISION = "$Revision: 480 $"; public String getVersion() { @@ -1615,7 +1616,7 @@ int zrelprod_rec(int l, int r, int lev) { int res; if (CACHESTATS) - cachestats.opAccess++; + cachestats.opAccess++; if (l == r) return zquant_rec(l, lev); @@ -3496,7 +3497,7 @@ int bdd_addref(int root) { return root; } - int bdd_count() { + int bdd_used_nodes_count() { for (int r = 0; r < bddrefstacktop; r++) bdd_mark(bddrefstack[r]); @@ -3504,22 +3505,27 @@ int bdd_count() { if (HASREF(n)) bdd_mark(n); } - int MeasureEffort_BDD_FREECOUNT = 0; + int freeBddCount = 0; for (int n = bddnodesize - 1; n >= 2; n--) { if (MARKED(n) && LOW(n) != INVALID_BDD) { UNMARK(n); } else { - MeasureEffort_BDD_FREECOUNT++; + freeBddCount++; } } - return bddnodesize - MeasureEffort_BDD_FREECOUNT; + return bddnodesize - freeBddCount; } int bdd_delref(int root) { - if (maxmemorystats.measuring) { - maxmemorystats.newMeasurement(bdd_count()); + // The number of currently used BDD nodes, between 0 and bddnodesize. + // -1 indicates that it has not yet been calculated. + int usedBddNodes = -1; + + if (maxmemorystats.enabled) { + if (usedBddNodes == -1) usedBddNodes = bdd_used_nodes_count(); + maxmemorystats.newMeasurement(usedBddNodes); // 'max memory usages'. // Measuring max memory usages fluctuates over time, tool implementation, @@ -3528,11 +3534,12 @@ int bdd_delref(int root) { //long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); //maxmemorystats.newMeasurement(bdd_count(), memory); // End of 'max memory usages' comment. - } - - if (continousstats.measuring) { - continousstats.contNodes.add(bdd_count()); - continousstats.contOperations.add(cachestats.opMiss); + } + + if (continuousstats.enabled) { + if (usedBddNodes == -1) usedBddNodes = bdd_used_nodes_count(); + continuousstats.contUsedBddNodes.add(usedBddNodes); + continuousstats.contUsedOperations.add(cachestats.opMiss); } if (root == INVALID_BDD) @@ -5062,8 +5069,8 @@ int bdd_reorder_gain() { } public void done() { - if (maxmemorystats.measuring) { - maxmemorystats.newMeasurement(bdd_count()); + if (maxmemorystats.enabled) { + maxmemorystats.newMeasurement(bdd_used_nodes_count()); // 'max memory usages'. // Measuring max memory usages fluctuates over time, tool implementation, @@ -5073,12 +5080,12 @@ public void done() { //maxmemorystats.newMeasurement(bdd_count(), memory); // End of 'max memory usages' comment. - bdd_gbc(); // To make sure new test is accurate. - System.gc(); // To make sure new test is accurate. - } - - super.done(); - bdd_done(); + bdd_gbc(); // To make sure new test is accurate. + System.gc(); // To make sure new test is accurate. + } + + super.done(); + bdd_done(); } From 899dc6038eead93ab728cb1c62734c4f25325275 Mon Sep 17 00:00:00 2001 From: Martijn Date: Thu, 21 Oct 2021 11:12:47 +0200 Subject: [PATCH 10/18] Add maxMemoryStats class measuring memory usage --- .../java/com/github/javabdd/BDDFactory.java | 62 +++++++++++++------ .../java/com/github/javabdd/JFactory.java | 47 +++++++------- 2 files changed, 70 insertions(+), 39 deletions(-) diff --git a/src/main/java/com/github/javabdd/BDDFactory.java b/src/main/java/com/github/javabdd/BDDFactory.java index 62fdb31..2beaf8f 100644 --- a/src/main/java/com/github/javabdd/BDDFactory.java +++ b/src/main/java/com/github/javabdd/BDDFactory.java @@ -1345,16 +1345,15 @@ public CacheStats getCacheStats() { } /** - * Stores statistics about the maximum memory usage. + * Stores statistics about the maximum BDD nodes usage. * * @author mgoorden */ - public static class MaxMemoryStats { + public static class MaxUsedBddNodesStats { protected boolean enabled = false; - protected long maxUsedMemory; protected int maxUsedBddNodes; - protected MaxMemoryStats() { } + protected MaxUsedBddNodesStats() { } public void enableMeasurements() { enabled = true; @@ -1364,23 +1363,47 @@ public void newMeasurement(int newUsedBddNodes) { maxUsedBddNodes = Math.max(newUsedBddNodes, maxUsedBddNodes); } - public void newMeasurement(int newUsedBddNodes, long newMemory) { - maxUsedBddNodes = Math.max(newUsedBddNodes, maxUsedBddNodes); - maxUsedMemory = Math.max(newMemory, maxUsedMemory); - } - public int getMaxNodes() { return maxUsedBddNodes; } + } + + /** + * Singleton object for maximum BDD nodes statistics. + */ + protected MaxUsedBddNodesStats maxbddnodesstats = new MaxUsedBddNodesStats(); + + /** + *

Return the current maximum BDD nodes statistics for this BDD factory.

+ * + * @return maximum memory statistics + */ + public MaxUsedBddNodesStats getMaxBddNodesStats() { + return maxbddnodesstats; + } + + /** + * Stores statistics about the maximum memory usage. + * + * @author mgoorden + */ + public static class MaxMemoryStats { + protected boolean enabled = false; + protected long maxUsedMemory; - // 'max memory usages'. - // Measuring max memory usages fluctuates over time, tool implementation, - // used hardware, etc. Therefore, if one wants to collect this information, - // he/she should uncomment lines below and in JFactory.java. - //public long getMaxUsedMemory() { - // return maxUsedMemory; - //} - // End of 'max memory usages' comment. + protected MaxMemoryStats() { } + + public void enableMeasurements() { + enabled = true; + } + + public void newMeasurement(long newMemory) { + maxUsedMemory = Math.max(newMemory, maxUsedMemory); + } + + public long getMaxUsedMemory() { + return maxUsedMemory; + } } /** @@ -1390,10 +1413,13 @@ public int getMaxNodes() { /** *

Return the current maximum memory statistics for this BDD factory.

+ * + *

Note that measuring max memory usages fluctuates over time, tool + * implementation, used hardware, etc.

* * @return maximum memory statistics */ - public MaxMemoryStats getMemoryStats() { + public MaxMemoryStats getMaxMemoryStats() { return maxmemorystats; } diff --git a/src/main/java/com/github/javabdd/JFactory.java b/src/main/java/com/github/javabdd/JFactory.java index 8899416..22aed89 100644 --- a/src/main/java/com/github/javabdd/JFactory.java +++ b/src/main/java/com/github/javabdd/JFactory.java @@ -3523,17 +3523,14 @@ int bdd_delref(int root) { // -1 indicates that it has not yet been calculated. int usedBddNodes = -1; - if (maxmemorystats.enabled) { + if (maxbddnodesstats.enabled) { if (usedBddNodes == -1) usedBddNodes = bdd_used_nodes_count(); - maxmemorystats.newMeasurement(usedBddNodes); - - // 'max memory usages'. - // Measuring max memory usages fluctuates over time, tool implementation, - // used hardware, etc. Therefore, if one wants to collect this information, - // he/she should uncomment lines below and in BDDFactory.java. - //long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); - //maxmemorystats.newMeasurement(bdd_count(), memory); - // End of 'max memory usages' comment. + maxbddnodesstats.newMeasurement(usedBddNodes); + } + + if (maxmemorystats.enabled) { + long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); + maxmemorystats.newMeasurement(memory); } if (continuousstats.enabled) { @@ -5069,20 +5066,28 @@ int bdd_reorder_gain() { } public void done() { + // The number of currently used BDD nodes, between 0 and bddnodesize. + // -1 indicates that it has not yet been calculated. + int usedBddNodes = -1; + + if (maxbddnodesstats.enabled) { + if (usedBddNodes == -1) usedBddNodes = bdd_used_nodes_count(); + maxbddnodesstats.newMeasurement(usedBddNodes); + } + if (maxmemorystats.enabled) { - maxmemorystats.newMeasurement(bdd_used_nodes_count()); - - // 'max memory usages'. - // Measuring max memory usages fluctuates over time, tool implementation, - // used hardware, etc. Therefore, if one wants to collect this information, - // he/she should uncomment lines below and in BDDFactory.java. - //long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); - //maxmemorystats.newMeasurement(bdd_count(), memory); - // End of 'max memory usages' comment. + long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); + maxmemorystats.newMeasurement(memory); + } - bdd_gbc(); // To make sure new test is accurate. - System.gc(); // To make sure new test is accurate. + if (continuousstats.enabled) { + if (usedBddNodes == -1) usedBddNodes = bdd_used_nodes_count(); + continuousstats.contUsedBddNodes.add(usedBddNodes); + continuousstats.contUsedOperations.add(cachestats.opMiss); } + + bdd_gbc(); // To make sure new test is accurate. + System.gc(); // To make sure new test is accurate. super.done(); bdd_done(); From 24d5f37b5c8fd4cef014d2357474dac31dc36f0d Mon Sep 17 00:00:00 2001 From: Martijn Date: Thu, 21 Oct 2021 11:19:44 +0200 Subject: [PATCH 11/18] Move CACHESTATS into the CacheStats class Instead of calling it CACHESTATS, it is now called enabled, as the static variable indicates whether cache statistics should be recorded. --- .../java/com/github/javabdd/BDDFactory.java | 10 +- .../java/com/github/javabdd/JFactory.java | 154 +++++++++--------- 2 files changed, 80 insertions(+), 84 deletions(-) diff --git a/src/main/java/com/github/javabdd/BDDFactory.java b/src/main/java/com/github/javabdd/BDDFactory.java index 2beaf8f..6bf2c5f 100644 --- a/src/main/java/com/github/javabdd/BDDFactory.java +++ b/src/main/java/com/github/javabdd/BDDFactory.java @@ -1241,6 +1241,7 @@ public ReorderStats getReorderStats() { * @version $Id: BDDFactory.java 480 2010-11-16 01:29:49Z robimalik $ */ public static class CacheStats { + protected boolean enabled = false; public long uniqueAccess; public long uniqueChain; public long uniqueHit; @@ -1264,7 +1265,7 @@ void copyFrom(CacheStats that) { } public void enableMeasurements() { - CACHESTATS = true; + enabled = true; } /* (non-Javadoc) @@ -1324,16 +1325,11 @@ public String toString() { return sb.toString(); } } - - /** - * Whether to measure cache statistics. - */ - public static boolean CACHESTATS; /** * Singleton object for cache statistics. */ - protected CacheStats cachestats = new CacheStats(); + protected static CacheStats cachestats = new CacheStats(); /** *

Return the current cache statistics for this BDD factory.

diff --git a/src/main/java/com/github/javabdd/JFactory.java b/src/main/java/com/github/javabdd/JFactory.java index 22aed89..30cfc31 100644 --- a/src/main/java/com/github/javabdd/JFactory.java +++ b/src/main/java/com/github/javabdd/JFactory.java @@ -54,7 +54,7 @@ private JFactory() { } public static BDDFactory init(int nodenum, int cachesize) { BDDFactory f = new JFactory(); f.initialize(nodenum, cachesize); - if (CACHESTATS) addShutdownHook(f); + if (cachestats.enabled) addShutdownHook(f); return f; } @@ -974,7 +974,7 @@ int not_rec(int r) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (ISCONST(r)) @@ -983,11 +983,11 @@ int not_rec(int r) { entry = BddCache_lookupI(applycache, NOTHASH(r)); if (entry.a == r && entry.c == bddop_not) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; PUSHREF(not_rec(LOW(r))); @@ -1036,7 +1036,7 @@ int ite_rec(int f, int g, int h) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (ISONE(f)) @@ -1052,11 +1052,11 @@ int ite_rec(int f, int g, int h) { entry = BddCache_lookupI(itecache, ITEHASH(f, g, h)); if (entry.a == f && entry.b == g && entry.c == h) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; if (LEVEL(f) == LEVEL(g)) { @@ -1117,7 +1117,7 @@ int zite_rec(int f, int g, int h) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (ISONE(f)) @@ -1137,11 +1137,11 @@ int zite_rec(int f, int g, int h) { entry = BddCache_lookupI(itecache, ITEHASH(f, g, h)); if (entry.a == f && entry.b == g && entry.c == h) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; if (LEVEL(f) == LEVEL(g)) { @@ -1233,7 +1233,7 @@ int replace_rec(int r) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (ISCONST(r) || LEVEL(r) > replacelast) @@ -1241,11 +1241,11 @@ int replace_rec(int r) { entry = BddCache_lookupI(replacecache, REPLACEHASH(r)); if (entry.a == r && entry.c == replaceid) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; PUSHREF(replace_rec(LOW(r))); @@ -1449,7 +1449,7 @@ int apply_rec(int l, int r) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (VERIFY_ASSERTIONS) _assert(!ZDD); @@ -1488,11 +1488,11 @@ int apply_rec(int l, int r) { entry = BddCache_lookupI(applycache, APPLYHASH(l, r, applyop)); if (entry.a == l && entry.b == r && entry.c == applyop) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; if (LEVEL(l) == LEVEL(r)) { @@ -1524,7 +1524,7 @@ int and_rec(int l, int r) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (l == r) @@ -1539,11 +1539,11 @@ int and_rec(int l, int r) { entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_and)); if (entry.a == l && entry.b == r && entry.c == bddop_and) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; if (LEVEL(l) == LEVEL(r)) { @@ -1574,7 +1574,7 @@ int zand_rec(int l, int r) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (l == r) @@ -1590,11 +1590,11 @@ else if (LEVEL(l) > LEVEL(r)) entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_and)); if (entry.a == l && entry.b == r && entry.c == bddop_and) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; PUSHREF(zand_rec(LOW(l), LOW(r))); @@ -1615,7 +1615,7 @@ int zrelprod_rec(int l, int r, int lev) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (l == r) @@ -1647,11 +1647,11 @@ int zrelprod_rec(int l, int r, int lev) { entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, bddop_and)); if (entry.a == l && entry.b == r && entry.c == appexid) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; if (LEVEL_l == LEVEL_r) { @@ -1694,7 +1694,7 @@ int or_rec(int l, int r) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (l == r) @@ -1708,11 +1708,11 @@ int or_rec(int l, int r) { entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_or)); if (entry.a == l && entry.b == r && entry.c == bddop_or) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; if (LEVEL(l) == LEVEL(r)) { @@ -1743,7 +1743,7 @@ int zor_rec(int l, int r) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (l == r) @@ -1757,11 +1757,11 @@ int zor_rec(int l, int r) { entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_or)); if (entry.a == l && entry.b == r && entry.c == bddop_or) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; if (LEVEL(l) == LEVEL(r)) { @@ -1792,7 +1792,7 @@ int zdiff_rec(int l, int r) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (ISZERO(l) /*|| ISONE(r)*/ || l == r) @@ -1805,11 +1805,11 @@ int zdiff_rec(int l, int r) { entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_diff)); if (entry.a == l && entry.b == r && entry.c == bddop_diff) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; if (LEVEL(l) == LEVEL(r)) { @@ -1835,7 +1835,7 @@ int relprod_rec(int l, int r) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (VERIFY_ASSERTIONS) _assert(!ZDD); @@ -1858,11 +1858,11 @@ int relprod_rec(int l, int r) { } else { entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, bddop_and)); if (entry.a == l && entry.b == r && entry.c == appexid) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; if (LEVEL_l == LEVEL_r) { @@ -2016,7 +2016,7 @@ int appquant_rec(int l, int r) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (VERIFY_ASSERTIONS) _assert(appexop != bddop_and); @@ -2064,11 +2064,11 @@ else if (LEVEL(l) > quantlast && LEVEL(r) > quantlast) { } else { entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, appexop)); if (entry.a == l && entry.b == r && entry.c == appexid) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; int lev; @@ -2111,7 +2111,7 @@ int appuni_rec(int l, int r, int var) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; int LEVEL_l, LEVEL_r, LEVEL_var; @@ -2138,11 +2138,11 @@ else if (ISCONST(var)) { } else { entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, appexop)); if (entry.a == l && entry.b == r && entry.c == appexid) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; int lev; @@ -2202,7 +2202,7 @@ int unique_rec(int r, int q) { int res; int LEVEL_r, LEVEL_q; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; LEVEL_r = LEVEL(r); @@ -2217,11 +2217,11 @@ int unique_rec(int r, int q) { entry = BddCache_lookupI(quantcache, QUANTHASH(r)); if (entry.a == r && entry.c == quantid) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; if (LEVEL_r == LEVEL_q) { @@ -2247,7 +2247,7 @@ int quant_rec(int r) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (r < 2 || LEVEL(r) > quantlast) @@ -2255,11 +2255,11 @@ int quant_rec(int r) { entry = BddCache_lookupI(quantcache, QUANTHASH(r)); if (entry.a == r && entry.c == quantid) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; PUSHREF(quant_rec(LOW(r))); @@ -2289,7 +2289,7 @@ int zquant_rec(int r, int lev) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; @@ -2317,11 +2317,11 @@ int zquant_rec(int r, int lev) { entry = BddCache_lookupI(quantcache, QUANTHASH(r)); if (entry.a == r && entry.c == quantid) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; int nlev = LEVEL(r) + 1; @@ -2387,7 +2387,7 @@ int constrain_rec(int f, int c) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (ISONE(c)) @@ -2401,11 +2401,11 @@ int constrain_rec(int f, int c) { entry = BddCache_lookupI(misccache, CONSTRAINHASH(f, c)); if (entry.a == f && entry.b == c && entry.c == miscid) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; if (LEVEL(f) == LEVEL(c)) { @@ -2487,7 +2487,7 @@ int compose_rec(int f, int g) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (LEVEL(f) > composelevel) @@ -2495,11 +2495,11 @@ int compose_rec(int f, int g) { entry = BddCache_lookupI(replacecache, COMPOSEHASH(f, g)); if (entry.a == f && entry.b == g && entry.c == replaceid) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; if (LEVEL(f) < composelevel) { @@ -2569,7 +2569,7 @@ int veccompose_rec(int f) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (LEVEL(f) > replacelast) @@ -2577,11 +2577,11 @@ int veccompose_rec(int f) { entry = BddCache_lookupI(replacecache, VECCOMPOSEHASH(f)); if (entry.a == f && entry.c == replaceid) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; PUSHREF(veccompose_rec(LOW(f))); @@ -2754,7 +2754,7 @@ int restrict_rec(int r) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (ISCONST(r) || LEVEL(r) > quantlast) @@ -2762,11 +2762,11 @@ int restrict_rec(int r) { entry = BddCache_lookupI(misccache, RESTRHASH(r, miscid)); if (entry.a == r && entry.c == miscid) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; if (INSVARSET(LEVEL(r))) { @@ -2825,7 +2825,7 @@ int simplify_rec(int f, int d) { BddCacheDataI entry; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.opAccess++; if (ISONE(d) || ISCONST(f)) @@ -2838,11 +2838,11 @@ int simplify_rec(int f, int d) { entry = BddCache_lookupI(applycache, APPLYHASH(f, d, bddop_simplify)); if (entry.a == f && entry.b == d && entry.c == bddop_simplify) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.opHit++; return entry.res; } - if (CACHESTATS) + if (cachestats.enabled) cachestats.opMiss++; if (LEVEL(f) == LEVEL(d)) { @@ -3602,7 +3602,7 @@ void bdd_unmark(int i) { int bdd_makenode(int level, int low, int high) { if (VERIFY_ASSERTIONS) _assert(!ZDD); - if (CACHESTATS) + if (cachestats.enabled) cachestats.uniqueAccess++; // check whether children are equal @@ -3615,7 +3615,7 @@ int bdd_makenode(int level, int low, int high) { int zdd_makenode(int level, int low, int high) { if (VERIFY_ASSERTIONS) _assert(ZDD); - if (CACHESTATS) + if (cachestats.enabled) cachestats.uniqueAccess++; // check whether high child is zero @@ -3636,18 +3636,18 @@ private int makenode(int level, int low, int high) { while (res != 0) { if (LEVEL(res) == level && LOW(res) == low && HIGH(res) == high) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.uniqueHit++; return res; } res = NEXT(res); - if (CACHESTATS) + if (cachestats.enabled) cachestats.uniqueChain++; } /* No existing node => build one */ - if (CACHESTATS) + if (cachestats.enabled) cachestats.uniqueMiss++; /* Any free nodes to use ? */ @@ -3800,7 +3800,7 @@ void bdd_init(int initnodesize, int cs) { bdderrorcond = 0; - if (CACHESTATS) { + if (cachestats.enabled) { //cachestats = new CacheStats(); } @@ -5796,7 +5796,7 @@ int reorder_makenode(int var, int low, int high) { int hash; int res; - if (CACHESTATS) + if (cachestats.enabled) cachestats.uniqueAccess++; /* Note: We know that low,high has a refcou greater than zero, so @@ -5822,19 +5822,19 @@ int reorder_makenode(int var, int low, int high) { while (res != 0) { if (LOW(res) == low && HIGH(res) == high) { - if (CACHESTATS) + if (cachestats.enabled) cachestats.uniqueHit++; INCREF(res); return res; } res = NEXT(res); - if (CACHESTATS) + if (cachestats.enabled) cachestats.uniqueChain++; } /* No existing node -> build one */ - if (CACHESTATS) + if (cachestats.enabled) cachestats.uniqueMiss++; /* Any free nodes to use ? */ From 956937f805a510ff06e7799abb551aafedcc0e6c Mon Sep 17 00:00:00 2001 From: Martijn Date: Thu, 21 Oct 2021 16:42:17 +0200 Subject: [PATCH 12/18] Let bdd_count count the number of used nodes instead of free nodes Also improve garbage collection in done() --- .../java/com/github/javabdd/JFactory.java | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/main/java/com/github/javabdd/JFactory.java b/src/main/java/com/github/javabdd/JFactory.java index 30cfc31..0727b95 100644 --- a/src/main/java/com/github/javabdd/JFactory.java +++ b/src/main/java/com/github/javabdd/JFactory.java @@ -3498,6 +3498,8 @@ int bdd_addref(int root) { } int bdd_used_nodes_count() { + // Mark all used bdd nodes. + // bdd_mark(n) also marks the children of n. for (int r = 0; r < bddrefstacktop; r++) bdd_mark(bddrefstack[r]); @@ -3505,17 +3507,18 @@ int bdd_used_nodes_count() { if (HASREF(n)) bdd_mark(n); } - int freeBddCount = 0; - + // Now go through all nodes and count the number of marked ones. + // Initial value is 2, as we always have the zero and one terminal nodes. + int bddCount = 2; + for (int n = bddnodesize - 1; n >= 2; n--) { if (MARKED(n) && LOW(n) != INVALID_BDD) { - UNMARK(n); - } else { - freeBddCount++; + UNMARK(n); + bddCount++; } } - return bddnodesize - freeBddCount; + return bddCount; } int bdd_delref(int root) { @@ -5078,6 +5081,7 @@ public void done() { if (maxmemorystats.enabled) { long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); maxmemorystats.newMeasurement(memory); + System.gc(); // To make sure subsequent memory measurements are accurate. } if (continuousstats.enabled) { @@ -5085,9 +5089,6 @@ public void done() { continuousstats.contUsedBddNodes.add(usedBddNodes); continuousstats.contUsedOperations.add(cachestats.opMiss); } - - bdd_gbc(); // To make sure new test is accurate. - System.gc(); // To make sure new test is accurate. super.done(); bdd_done(); From c94c742a00af161e93245f1dd3297adb2a0d47a9 Mon Sep 17 00:00:00 2001 From: Martijn Date: Sun, 24 Oct 2021 20:29:53 +0200 Subject: [PATCH 13/18] Fixes from review - Allow stat measurements to be disabled - More consistent naming of stat objects and methods. - Move stats measurements at several places to a separate method. --- .../java/com/github/javabdd/BDDFactory.java | 55 ++++++++++++------- .../java/com/github/javabdd/JFactory.java | 46 ++++++---------- 2 files changed, 50 insertions(+), 51 deletions(-) diff --git a/src/main/java/com/github/javabdd/BDDFactory.java b/src/main/java/com/github/javabdd/BDDFactory.java index 6bf2c5f..af9da44 100644 --- a/src/main/java/com/github/javabdd/BDDFactory.java +++ b/src/main/java/com/github/javabdd/BDDFactory.java @@ -1355,27 +1355,31 @@ public void enableMeasurements() { enabled = true; } + public void disableMeasurements() { + enabled = false; + } + public void newMeasurement(int newUsedBddNodes) { maxUsedBddNodes = Math.max(newUsedBddNodes, maxUsedBddNodes); } - public int getMaxNodes() { + public int getMaxUsedNodes() { return maxUsedBddNodes; } } /** - * Singleton object for maximum BDD nodes statistics. + * Singleton object for maximum used BDD nodes statistics. */ - protected MaxUsedBddNodesStats maxbddnodesstats = new MaxUsedBddNodesStats(); + protected MaxUsedBddNodesStats maxusedbddnodesstats = new MaxUsedBddNodesStats(); /** - *

Return the current maximum BDD nodes statistics for this BDD factory.

+ *

Return the current maximum used BDD nodes statistics for this BDD factory.

* - * @return maximum memory statistics + * @return maximum used BDD statistics */ - public MaxUsedBddNodesStats getMaxBddNodesStats() { - return maxbddnodesstats; + public MaxUsedBddNodesStats getMaxUsedBddNodesStats() { + return maxusedbddnodesstats; } /** @@ -1383,16 +1387,20 @@ public MaxUsedBddNodesStats getMaxBddNodesStats() { * * @author mgoorden */ - public static class MaxMemoryStats { + public static class MaxUsedMemoryStats { protected boolean enabled = false; protected long maxUsedMemory; - protected MaxMemoryStats() { } + protected MaxUsedMemoryStats() { } public void enableMeasurements() { enabled = true; } + public void disableMeasurements() { + enabled = false; + } + public void newMeasurement(long newMemory) { maxUsedMemory = Math.max(newMemory, maxUsedMemory); } @@ -1403,31 +1411,32 @@ public long getMaxUsedMemory() { } /** - * Singleton object for maximum memory statistics. + * Singleton object for maximum used memory statistics. */ - protected MaxMemoryStats maxmemorystats = new MaxMemoryStats(); + protected MaxUsedMemoryStats maxusedmemorystats = new MaxUsedMemoryStats(); /** - *

Return the current maximum memory statistics for this BDD factory.

+ *

Return the current maximum used memory statistics for this BDD factory.

* - *

Note that measuring max memory usages fluctuates over time, tool + *

Note that measuring max used memory usages fluctuates over time, tool * implementation, used hardware, etc.

* - * @return maximum memory statistics + * @return maximum used memory statistics */ - public MaxMemoryStats getMaxMemoryStats() { - return maxmemorystats; + public MaxUsedMemoryStats getMaxUsedMemoryStats() { + return maxusedmemorystats; } /** - * Stores continuously statistics about the memory usage and BDD operations. + * Stores continuously statistics about the BDD nodes usage and BDD operations, + * where BDD operations is a proxy for time. * * @author mgoorden */ public static class ContinuousStats { protected boolean enabled = false; protected List contUsedBddNodes = new ArrayList(); - protected List contUsedOperations = new ArrayList(); + protected List contOperations = new ArrayList(); protected ContinuousStats() { } @@ -1435,18 +1444,22 @@ public void enableMeasurements() { enabled = true; } + public void disableMeasurements() { + enabled = false; + } + public List getNodesStats() { - if (contUsedBddNodes.size() != contUsedOperations.size()) { + if (contUsedBddNodes.size() != contOperations.size()) { throw new AssertionError("Incorrect data collection."); } return contUsedBddNodes; } public List getOperationsStats() { - if (contUsedBddNodes.size() != contUsedOperations.size()) { + if (contUsedBddNodes.size() != contOperations.size()) { throw new AssertionError("Incorrect data collection."); } - return contUsedOperations; + return contOperations; } } diff --git a/src/main/java/com/github/javabdd/JFactory.java b/src/main/java/com/github/javabdd/JFactory.java index 0727b95..aecce0f 100644 --- a/src/main/java/com/github/javabdd/JFactory.java +++ b/src/main/java/com/github/javabdd/JFactory.java @@ -3522,25 +3522,7 @@ int bdd_used_nodes_count() { } int bdd_delref(int root) { - // The number of currently used BDD nodes, between 0 and bddnodesize. - // -1 indicates that it has not yet been calculated. - int usedBddNodes = -1; - - if (maxbddnodesstats.enabled) { - if (usedBddNodes == -1) usedBddNodes = bdd_used_nodes_count(); - maxbddnodesstats.newMeasurement(usedBddNodes); - } - - if (maxmemorystats.enabled) { - long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); - maxmemorystats.newMeasurement(memory); - } - - if (continuousstats.enabled) { - if (usedBddNodes == -1) usedBddNodes = bdd_used_nodes_count(); - continuousstats.contUsedBddNodes.add(usedBddNodes); - continuousstats.contUsedOperations.add(cachestats.opMiss); - } + bdd_add_per_stats(); if (root == INVALID_BDD) bdd_error(BDD_BREAK); /* distinctive */ @@ -5069,32 +5051,36 @@ int bdd_reorder_gain() { } public void done() { + bdd_add_per_stats(); + + super.done(); + bdd_done(); + } + + void bdd_add_per_stats() { // The number of currently used BDD nodes, between 0 and bddnodesize. // -1 indicates that it has not yet been calculated. int usedBddNodes = -1; - if (maxbddnodesstats.enabled) { + if (maxusedbddnodesstats.enabled) { if (usedBddNodes == -1) usedBddNodes = bdd_used_nodes_count(); - maxbddnodesstats.newMeasurement(usedBddNodes); + maxusedbddnodesstats.newMeasurement(usedBddNodes); } - if (maxmemorystats.enabled) { + if (maxusedmemorystats.enabled) { long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); - maxmemorystats.newMeasurement(memory); - System.gc(); // To make sure subsequent memory measurements are accurate. + maxusedmemorystats.newMeasurement(memory); } - + if (continuousstats.enabled) { if (usedBddNodes == -1) usedBddNodes = bdd_used_nodes_count(); continuousstats.contUsedBddNodes.add(usedBddNodes); - continuousstats.contUsedOperations.add(cachestats.opMiss); + // cachestats.opMiss is the number of BDD operations performed until now that could not + // be taken from the cache. Thus it approximates time. + continuousstats.contOperations.add(cachestats.opMiss); } - - super.done(); - bdd_done(); } - void bdd_done() { /*sanitycheck(); FIXME */ //bdd_fdd_done(); From 8bc444d143e3e0722a7dbed8631eeadad3817a2e Mon Sep 17 00:00:00 2001 From: Martijn Date: Sun, 24 Oct 2021 20:32:58 +0200 Subject: [PATCH 14/18] Remove memory measurements --- .../java/com/github/javabdd/BDDFactory.java | 45 ------------------- .../java/com/github/javabdd/JFactory.java | 5 --- 2 files changed, 50 deletions(-) diff --git a/src/main/java/com/github/javabdd/BDDFactory.java b/src/main/java/com/github/javabdd/BDDFactory.java index af9da44..5fd45a8 100644 --- a/src/main/java/com/github/javabdd/BDDFactory.java +++ b/src/main/java/com/github/javabdd/BDDFactory.java @@ -1382,51 +1382,6 @@ public MaxUsedBddNodesStats getMaxUsedBddNodesStats() { return maxusedbddnodesstats; } - /** - * Stores statistics about the maximum memory usage. - * - * @author mgoorden - */ - public static class MaxUsedMemoryStats { - protected boolean enabled = false; - protected long maxUsedMemory; - - protected MaxUsedMemoryStats() { } - - public void enableMeasurements() { - enabled = true; - } - - public void disableMeasurements() { - enabled = false; - } - - public void newMeasurement(long newMemory) { - maxUsedMemory = Math.max(newMemory, maxUsedMemory); - } - - public long getMaxUsedMemory() { - return maxUsedMemory; - } - } - - /** - * Singleton object for maximum used memory statistics. - */ - protected MaxUsedMemoryStats maxusedmemorystats = new MaxUsedMemoryStats(); - - /** - *

Return the current maximum used memory statistics for this BDD factory.

- * - *

Note that measuring max used memory usages fluctuates over time, tool - * implementation, used hardware, etc.

- * - * @return maximum used memory statistics - */ - public MaxUsedMemoryStats getMaxUsedMemoryStats() { - return maxusedmemorystats; - } - /** * Stores continuously statistics about the BDD nodes usage and BDD operations, * where BDD operations is a proxy for time. diff --git a/src/main/java/com/github/javabdd/JFactory.java b/src/main/java/com/github/javabdd/JFactory.java index aecce0f..841eee9 100644 --- a/src/main/java/com/github/javabdd/JFactory.java +++ b/src/main/java/com/github/javabdd/JFactory.java @@ -5067,11 +5067,6 @@ void bdd_add_per_stats() { maxusedbddnodesstats.newMeasurement(usedBddNodes); } - if (maxusedmemorystats.enabled) { - long memory = Runtime.getRuntime().totalMemory() - Runtime.getRuntime().freeMemory(); - maxusedmemorystats.newMeasurement(memory); - } - if (continuousstats.enabled) { if (usedBddNodes == -1) usedBddNodes = bdd_used_nodes_count(); continuousstats.contUsedBddNodes.add(usedBddNodes); From 5583903b04b7019c97bbab2bcec962c719ae5e4d Mon Sep 17 00:00:00 2001 From: Martijn Date: Sun, 24 Oct 2021 20:40:28 +0200 Subject: [PATCH 15/18] Make cachestats nonstatic and remove shutdown hook --- src/main/java/com/github/javabdd/BDDFactory.java | 2 +- src/main/java/com/github/javabdd/JFactory.java | 9 --------- 2 files changed, 1 insertion(+), 10 deletions(-) diff --git a/src/main/java/com/github/javabdd/BDDFactory.java b/src/main/java/com/github/javabdd/BDDFactory.java index 5fd45a8..4eba44a 100644 --- a/src/main/java/com/github/javabdd/BDDFactory.java +++ b/src/main/java/com/github/javabdd/BDDFactory.java @@ -1329,7 +1329,7 @@ public String toString() { /** * Singleton object for cache statistics. */ - protected static CacheStats cachestats = new CacheStats(); + protected CacheStats cachestats = new CacheStats(); /** *

Return the current cache statistics for this BDD factory.

diff --git a/src/main/java/com/github/javabdd/JFactory.java b/src/main/java/com/github/javabdd/JFactory.java index 841eee9..2d8f646 100644 --- a/src/main/java/com/github/javabdd/JFactory.java +++ b/src/main/java/com/github/javabdd/JFactory.java @@ -54,17 +54,8 @@ private JFactory() { } public static BDDFactory init(int nodenum, int cachesize) { BDDFactory f = new JFactory(); f.initialize(nodenum, cachesize); - if (cachestats.enabled) addShutdownHook(f); return f; } - - static void addShutdownHook(final BDDFactory f) { - Runtime.getRuntime().addShutdownHook(new Thread() { - public void run() { - System.out.println(f.getCacheStats().toString()); - } - }); - } boolean ZDD = false; From f479c2fb3782e0f08475bbfab6242acab8b39db5 Mon Sep 17 00:00:00 2001 From: Martijn Date: Mon, 25 Oct 2021 09:29:42 +0200 Subject: [PATCH 16/18] Fixes from review --- .../java/com/github/javabdd/BDDFactory.java | 30 +++++++++++++++++-- .../java/com/github/javabdd/JFactory.java | 6 ++-- 2 files changed, 30 insertions(+), 6 deletions(-) diff --git a/src/main/java/com/github/javabdd/BDDFactory.java b/src/main/java/com/github/javabdd/BDDFactory.java index 4eba44a..614df62 100644 --- a/src/main/java/com/github/javabdd/BDDFactory.java +++ b/src/main/java/com/github/javabdd/BDDFactory.java @@ -1268,6 +1268,21 @@ public void enableMeasurements() { enabled = true; } + public void disableMeasurements() { + enabled = false; + } + + public void resetMeasurements() { + uniqueAccess = 0; + uniqueChain = 0; + uniqueHit = 0; + uniqueMiss = 0; + opAccess = 0; + opHit = 0; + opMiss = 0; + swapCount = 0; + } + /* (non-Javadoc) * @see java.lang.Object#toString() */ @@ -1359,11 +1374,15 @@ public void disableMeasurements() { enabled = false; } + public void resetMeasurements() { + maxUsedBddNodes = 0; + } + public void newMeasurement(int newUsedBddNodes) { maxUsedBddNodes = Math.max(newUsedBddNodes, maxUsedBddNodes); } - public int getMaxUsedNodes() { + public int getMaxUsedBddNodes() { return maxUsedBddNodes; } } @@ -1376,7 +1395,7 @@ public int getMaxUsedNodes() { /** *

Return the current maximum used BDD nodes statistics for this BDD factory.

* - * @return maximum used BDD statistics + * @return maximum used BDD nodes statistics */ public MaxUsedBddNodesStats getMaxUsedBddNodesStats() { return maxusedbddnodesstats; @@ -1403,6 +1422,11 @@ public void disableMeasurements() { enabled = false; } + public void resetMeasurements() { + contUsedBddNodes = new ArrayList(); + contOperations = new ArrayList(); + } + public List getNodesStats() { if (contUsedBddNodes.size() != contOperations.size()) { throw new AssertionError("Incorrect data collection."); @@ -1428,7 +1452,7 @@ public List getOperationsStats() { * * @return continuous statistics */ - public ContinuousStats getContinousStats() { + public ContinuousStats getContinuousStats() { return continuousstats; } diff --git a/src/main/java/com/github/javabdd/JFactory.java b/src/main/java/com/github/javabdd/JFactory.java index 2d8f646..f297462 100644 --- a/src/main/java/com/github/javabdd/JFactory.java +++ b/src/main/java/com/github/javabdd/JFactory.java @@ -3513,7 +3513,7 @@ int bdd_used_nodes_count() { } int bdd_delref(int root) { - bdd_add_per_stats(); + bdd_add_perf_stats(); if (root == INVALID_BDD) bdd_error(BDD_BREAK); /* distinctive */ @@ -5042,13 +5042,13 @@ int bdd_reorder_gain() { } public void done() { - bdd_add_per_stats(); + bdd_add_perf_stats(); super.done(); bdd_done(); } - void bdd_add_per_stats() { + void bdd_add_perf_stats() { // The number of currently used BDD nodes, between 0 and bddnodesize. // -1 indicates that it has not yet been calculated. int usedBddNodes = -1; From fd618760c53b1ba93ebb60996877f2b89e98c6ff Mon Sep 17 00:00:00 2001 From: Martijn Date: Mon, 25 Oct 2021 09:40:03 +0200 Subject: [PATCH 17/18] Update CHANGES.md --- CHANGES.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index 3470451..ffa6680 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -5,6 +5,11 @@ All notable changes to this project will be documented in this file. ## [Unreleased] * Added CHANGES.md to track changes between releases. * Added the collection of performance statistics. +* Added bdd_used_nodes_count() that counts the number of used nodes. +* Replaced static CACHESTATS by non-static cachestats.enabled, which is adaptable by user. +* Removed shutdown hook from JFactory. +* Changed Cache statistics from int to long. +* Added opAccess statistic to cache statistics. ## [1.0.1] - 2020-03-17 * Updated SCM URL for proper Maven Central metadata. From bd6c873cbec9fedf25866b706259cf25ac58b7ff Mon Sep 17 00:00:00 2001 From: Martijn Date: Mon, 25 Oct 2021 11:51:16 +0200 Subject: [PATCH 18/18] Improve CHANGES.md --- CHANGES.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index ffa6680..fdd8590 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -4,12 +4,13 @@ All notable changes to this project will be documented in this file. ## [Unreleased] * Added CHANGES.md to track changes between releases. -* Added the collection of performance statistics. -* Added bdd_used_nodes_count() that counts the number of used nodes. -* Replaced static CACHESTATS by non-static cachestats.enabled, which is adaptable by user. -* Removed shutdown hook from JFactory. -* Changed Cache statistics from int to long. -* Added opAccess statistic to cache statistics. +* Added the collection of platform-independent performance statistics. +* Added `bdd_used_nodes_count()` that counts the number of used nodes. +* Replaced static `CACHESTATS` by non-static `cachestats.enabled`, which is adaptable by user and configurable per BDD factory instance. +* Removed global JVM shutdown hook, that prints cache statistics to `stdout`, from `JFactory`. +* Cache statistics are now measured using `longs` rather than `ints` to reduce integer overflow issues. +* Added `opAccess` statistic to cache statistics. +* Added functionality to reset statistics. ## [1.0.1] - 2020-03-17 * Updated SCM URL for proper Maven Central metadata.