Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +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 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.

Comment thread
magoorden marked this conversation as resolved.
## [1.0.1] - 2020-03-17
* Updated SCM URL for proper Maven Central metadata.
Expand Down
143 changes: 136 additions & 7 deletions src/main/java/com/github/javabdd/BDDFactory.java
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -1235,16 +1236,20 @@ 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;
protected boolean enabled = false;
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() { }

Expand All @@ -1253,11 +1258,31 @@ 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;
}

public void enableMeasurements() {
Comment thread
magoorden marked this conversation as resolved.
Comment thread
magoorden marked this conversation as resolved.
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()
*/
Expand Down Expand Up @@ -1294,6 +1319,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);
Expand Down Expand Up @@ -1327,6 +1355,107 @@ public CacheStats getCacheStats() {
return cachestats;
}

/**
* Stores statistics about the maximum BDD nodes usage.
*
* @author mgoorden
*/
public static class MaxUsedBddNodesStats {
Comment thread
magoorden marked this conversation as resolved.
protected boolean enabled = false;
protected int maxUsedBddNodes;

protected MaxUsedBddNodesStats() { }

public void enableMeasurements() {
Comment thread
magoorden marked this conversation as resolved.
enabled = true;
}

public void disableMeasurements() {
Comment thread
magoorden marked this conversation as resolved.
enabled = false;
}

public void resetMeasurements() {
maxUsedBddNodes = 0;
}

public void newMeasurement(int newUsedBddNodes) {
maxUsedBddNodes = Math.max(newUsedBddNodes, maxUsedBddNodes);
}

public int getMaxUsedBddNodes() {
return maxUsedBddNodes;
}
}

/**
* Singleton object for maximum used BDD nodes statistics.
*/
protected MaxUsedBddNodesStats maxusedbddnodesstats = new MaxUsedBddNodesStats();

/**
* <p>Return the current maximum used BDD nodes statistics for this BDD factory.</p>
*
* @return maximum used BDD nodes statistics
*/
public MaxUsedBddNodesStats getMaxUsedBddNodesStats() {
return maxusedbddnodesstats;
}

/**
* 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<Integer> contUsedBddNodes = new ArrayList<Integer>();
protected List<Long> contOperations = new ArrayList<Long>();

protected ContinuousStats() { }

public void enableMeasurements() {
enabled = true;
}

public void disableMeasurements() {
enabled = false;
}

public void resetMeasurements() {
contUsedBddNodes = new ArrayList<Integer>();
contOperations = new ArrayList<Long>();
}

public List<Integer> getNodesStats() {
if (contUsedBddNodes.size() != contOperations.size()) {
throw new AssertionError("Incorrect data collection.");
}
return contUsedBddNodes;
}

public List<Long> getOperationsStats() {
Comment thread
magoorden marked this conversation as resolved.
if (contUsedBddNodes.size() != contOperations.size()) {
throw new AssertionError("Incorrect data collection.");
}
return contOperations;
}
}

/**
* Singleton object for continuous statistics.
*/
protected ContinuousStats continuousstats = new ContinuousStats();

/**
* <p>Return the current continuous statistics for this BDD factory.</p>
*
* @return continuous statistics
*/
public ContinuousStats getContinuousStats() {
return continuousstats;
}

// TODO: bdd_sizeprobe_hook
// TODO: bdd_reorder_probe

Expand Down
Loading