From 19f422a472cb304848bd062e6706781e09abfcb4 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Thu, 13 Aug 2015 10:05:00 +0000 Subject: [PATCH] Refactor DebugJDD handling, add node tracing. The DebugJDD class provides Java-side reference counting for JDDNodes and tries to detect problems with the reference counting, such as to many derefs (can lead to crashes during garbage collection) or too few derefs (leads to memory leakage and a warning when exiting PRISM). When debugging is enabled, each JDDNode is assigned a unique, sequential ID that should be stable across runs of PRISM with the same command-line arguments, in contrast to the underlying CUDD DDNode pointers, which can and do change with each invokation. A tracing mechanism allows to print all the ref/deref events for a particular JDDNode. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10506 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/include/DebugJDD.h | 13 +- prism/src/jdd/DebugJDD.java | 376 +++++++++++++++++++++++++----------- prism/src/jdd/JDD.java | 3 + prism/src/jdd/JDDNode.java | 54 ++++-- 4 files changed, 307 insertions(+), 139 deletions(-) diff --git a/prism/include/DebugJDD.h b/prism/include/DebugJDD.h index b7963c20..bc9f4b0e 100644 --- a/prism/include/DebugJDD.h +++ b/prism/include/DebugJDD.h @@ -7,8 +7,6 @@ #ifdef __cplusplus extern "C" { #endif -#undef jdd_DebugJDD_debugEnabled -#define jdd_DebugJDD_debugEnabled 0L /* * Class: jdd_DebugJDD * Method: DebugJDD_GetRefCount @@ -29,3 +27,14 @@ JNIEXPORT jlongArray JNICALL Java_jdd_DebugJDD_DebugJDD_1GetExternalRefCounts } #endif #endif +/* Header for class jdd_DebugJDD_DebugJDDNode */ + +#ifndef _Included_jdd_DebugJDD_DebugJDDNode +#define _Included_jdd_DebugJDD_DebugJDDNode +#ifdef __cplusplus +extern "C" { +#endif +#ifdef __cplusplus +} +#endif +#endif diff --git a/prism/src/jdd/DebugJDD.java b/prism/src/jdd/DebugJDD.java index bf3da6e5..1f8c9c28 100644 --- a/prism/src/jdd/DebugJDD.java +++ b/prism/src/jdd/DebugJDD.java @@ -4,6 +4,7 @@ // Authors: // * Vojtech Forejt (University of Oxford) // * Christian von Essen (VERIMAG) +// * Joachim Klein (TU Dresden) // //------------------------------------------------------------------------------ // @@ -27,11 +28,14 @@ package jdd; +import java.util.ArrayList; import java.util.HashMap; -import java.util.Iterator; -import java.util.LinkedList; +import java.util.HashSet; +import java.util.LinkedHashMap; import java.util.List; -import java.util.ListIterator; +import java.util.Map; +import java.util.Map.Entry; +import java.util.TreeMap; public class DebugJDD { @@ -48,157 +52,293 @@ public class DebugJDD } /** - * determines if the debugging of JDD nodes is enabled. + * A DebugJDDNode extends a JDDNode with additional information + * useful for tracking refs/derefs and tracing. */ - public static final boolean debugEnabled = false; + protected static class DebugJDDNode extends JDDNode { - /** - * Where stack traces are kept. - * Key: hashcode of a JDDNode - * Value: stack trace from the moment the JDDNode was constructed. - */ - protected static HashMap stackTraces; + /** A static counter that is used to provide a unique ID for each JDDNode */ + private static long nextId = 0; + + /** + * The ID for this JDDNode. In contrast with the DdNode* ptr, this will be + * stable across PRISM invocations and can thus be used for tracing. + */ + private long id; + + /** The balance of reference/dereference calls this specific JDDNode */ + private int nodeRefs = 0; + + /** + * Constructor, with DdNode* ptr. + * @param ptr the DdNode pointer in CUDD + * @param isReferenced Does this JDDNode already have a reference + * (like for ptrToNode) or not (like for getThen / getElse) + */ + public DebugJDDNode(long ptr, boolean isReferenced) + { + // instantiate underlying JDDNode + super(ptr); + // generate and store globally unique ID + id = nextId++; + // the initial number of references for this JDDNode + nodeRefs = (isReferenced ? 1 : 0); + if (isReferenced) { + // increase javaRefs counter for this ptr + int jrefs = getJavaRefCount(ptr()); + javaRefs.put(ptr(), jrefs+1); + } + // store to keep track of this DebugJDDNode + DebugJDD.addToSet(this); + } + + /** Get the ID of this node */ + public long getID() + { + return id; + } + + /** Increment the reference count for this JDDNode */ + public void incRef() + { + // increment count for node + nodeRefs++; + // increment javaRefs counter for this ptr + int jrefs = getJavaRefCount(ptr()); + javaRefs.put(ptr(), jrefs + 1); + } + + /** Decrement the reference count for this JDDNode */ + public void decRef() + { + // decrement count for node + nodeRefs--; + // decrement javaRefs counter for this ptr + int jrefs = getJavaRefCount(ptr()) - 1; + javaRefs.put(ptr(), jrefs); + + // Checks: + // (1) There is a negative number of Java references for the DdNode pointer + if (jrefs < 0) { + throw new RuntimeException("DebugJDD: The number of Java references is negative for ptr=0x"+Long.toHexString(ptr())+", ID="+getID()+", Java refs = "+jrefs+", CUDD refs = "+DebugJDD_GetRefCount(ptr())); + } + // (2) There are more Java references than Cudd references + if (jrefs > DebugJDD_GetRefCount(ptr())) { + throw new RuntimeException("DebugJDD: More Java refs than CUDD refs for ptr=0x"+Long.toHexString(ptr())+", ID="+getID()+", Java refs = "+jrefs+", CUDD refs = "+DebugJDD_GetRefCount(ptr())); + } + // (3) This node has more refs than there are Java refs in total + if (jrefs < getNodeRefs()) { + throw new RuntimeException("DebugJDD: JDDNode has more refs than Java refs in total?! ID="+getID()+", refs = "+getNodeRefs()+", Java refs = "+jrefs+", CUDD refs = "+DebugJDD_GetRefCount(ptr())); + } + } + + /** Get the number of active references for this JDDNode */ + public int getNodeRefs() + { + return nodeRefs; + } + } /** - * Keeps track of refs and derefs made in Java - * Key: hashcode of a JDDNode - * Value: 1 + (number of times the node was refed) - (number of times the node was derefed) + * Flag, determines if the debugging of JDD nodes is enabled. */ - protected static HashMap localCounters; + public static boolean debugEnabled = false; /** - * Keeps track of instances of JDDNode pointing to (native) DdNode - * Key: pointer to a DdNode - * Value: list of hashcodes of JDDNodes pointing to the DdNode + * Map from DebugJDDNode IDs to DebugJDDNode. + * LinkedHashMap to ensure that iterating over the map returns the + * DebugJDDNodes in a consistent order, sorted by ID. */ - protected static HashMap> instances; + protected static LinkedHashMap nodes = new LinkedHashMap(); + + /** A map from DdNode pointers to the current sum of the nodeRefs of all JDDNodes for that pointer */ + protected static HashMap javaRefs = new HashMap(); - protected static void addToSet(JDDNode node, int count) + /** An optional set of DebugJDDNode IDs that will be traced */ + protected static HashSet traceIDs = null; + + /** Enable debugging */ + public static void enable() { - //not thread safe - if (instances == null) { - instances = new HashMap>(); - localCounters = new HashMap(); - stackTraces = new HashMap(); + debugEnabled = true; + } + /** Activate tracing for the DebugJDDNode with ID id */ + public static void enableTracingForID(long id) { + if (traceIDs == null) { + traceIDs = new HashSet(); } - - int hc = System.identityHashCode(node); - if (instances.containsKey(node.ptr())) { - long ptr = node.ptr(); - instances.get(ptr).add(hc); - } else { - long ptr = node.ptr(); - List al = new LinkedList(); - al.add(hc); - instances.put(ptr, al); + traceIDs.add(id); + System.out.println("DebugJDD: Enable tracing for "+id); + enable(); // tracing implies debugging + } + /** Store a DebugJDDNode for tracking of the references */ + protected static void addToSet(DebugJDDNode node) + { + if (nodes.put(node.getID(), node) != null) { + // implementation error, should not happen + throw new RuntimeException("DebugJDD: Adding the same JDDNode multiple times, ID="+node.getID()); } - localCounters.put(hc, count); - - StackTraceElement[] st = Thread.currentThread().getStackTrace(); - //ignore first two elements which are Thread and this constructor - int num = st.length - 2; - StackTraceElement[] creator = new StackTraceElement[num]; - for (int i = 0; i < num; i++) { - creator[i] = st[i + 2]; + if (traceIDs != null && traceIDs.contains(node.id)) { + trace("create", node); } - stackTraces.put(hc, creator); } + /** Notification from JDD.Deref(node) */ protected static void decrement(JDDNode node) { - int hc = System.identityHashCode(node); - int newValue = localCounters.get(hc) - 1; + if (!(node instanceof DebugJDDNode)) { + // deref of a node that is not wrapped in a DebugJDDNode + // -> probably came from JDDNode.getThen()/getElse(), should not be derefed + throw new RuntimeException("DebugJDD: Trying to Deref a plain JDDNode (obtained from getThen()/getElse()?)"); + } + DebugJDDNode dNode = (DebugJDDNode) node; + if (dNode.getNodeRefs() == 0) { + // This is only a warning as currently there are places + // where referencing / derefencing happens across multiple JDDNodes + System.out.println("Warning, DebugJDD: Deref of a JDDNode that has 0 references, ID = "+dNode.getID()); + printStack(0); + } + dNode.decRef(); int cuddRefCount = DebugJDD_GetRefCount(node.ptr()); - assert cuddRefCount > 0; - assert cuddRefCount - 1 >= newValue; - if (newValue < 0 && cuddRefCount == newValue) { - System.out.println("Dereferencing node " + node + " too often. Printing stack trace where it was created."); - //print only top 5 methods from stack - int i = 0; - for (StackTraceElement st : stackTraces.get(hc)) { - if (i++ > 5) { - break; - } - System.out.println(" " + st.toString()); - } - assert false; + if (cuddRefCount <= 0) { + throw new RuntimeException("DebugJDD: Trying to deref a JDDNode with a non-positive CUDD ref count, ptr=0x"+Long.toHexString(dNode.ptr())+", ID = "+dNode.getID()+", Java ref = "+getJavaRefCount(dNode.ptr())+", CUDD refs = "+cuddRefCount); + } + if (traceIDs != null && traceIDs.contains(dNode.id)) { + trace("deref", dNode); } - - localCounters.put(hc, newValue); } + /** Notification from JDD.Ref(node) */ protected static void increment(JDDNode node) { - int hc = System.identityHashCode(node); - int newValue = localCounters.get(hc) + 1; - int cuddRefCount = DebugJDD_GetRefCount(node.ptr()); - assert cuddRefCount + 1 >= newValue; - localCounters.put(hc, newValue); + if (!(node instanceof DebugJDDNode)) { + // ref of a node that is not wrapped in a DebugJDDNode + // -> probably came from JDDNode.getThen()/getElse(), should not be refed + throw new RuntimeException("DebugJDD: Trying to Ref a plain JDDNode (obtained from getThen()/getElse()?)"); + } + DebugJDDNode dNode = (DebugJDDNode) node; + dNode.incRef(); + if (traceIDs != null && traceIDs.contains(dNode.id)) { + trace("ref", dNode); + } } public static void endLifeCycle() { - // Kick everybody who hasn't got a reference count higher than zero out - for (Iterator itt = instances.keySet().iterator(); itt.hasNext(); ) { - Long ptr = itt.next(); - for (Iterator it = instances.get(ptr).iterator(); it.hasNext(); ) { - int localRefCount = localCounters.get(it.next()); - if (localRefCount != 0) { - it.remove(); - } - } - if (instances.get(ptr).isEmpty()) { - itt.remove(); - } + // Get the external reference count from CUDD + Map externalRefCounts = getExternalRefCounts(); + if (externalRefCounts.size() == 0) { + // everthing is fine + return; } - for (Long ptr : instances.keySet()) { - //check if cudd has nonzero number of references - int cuddRefCount = DebugJDD_GetRefCount(ptr); - if (cuddRefCount != 0) { - //check if there is a JDD object with nonzero refcount - boolean hasSuspicious = false; - for (Integer hc : instances.get(ptr)) { - int localRefCount = localCounters.get(hc); - if (localRefCount > 0) { - hasSuspicious = true; - break; + + System.out.println("\nWarning: Found " + externalRefCounts.size() + " leaked JDDNode references."); + System.out.flush(); + for (Entry extRef : externalRefCounts.entrySet()) { + long ptr = extRef.getKey(); + List matchingNodes = new ArrayList(); + List posRewNodes = new ArrayList(); + for (DebugJDDNode node : nodes.values()) { + if (node.ptr() == ptr) { + // node matches + matchingNodes.add(node); + // node still has positive reference count + if (node.getNodeRefs() > 0) { + posRewNodes.add(node); } } + } - //if !hasSuspicious, there is no useful output we could give. - //Either it's false alarm, or the problem is in c++ - if (!hasSuspicious) - continue; - System.out.println("WARNING: there are nodes with nonzero references, printing debug info. " - + "Note that the stack traces below are from moments JDDNodes were " - + "created. The actual problem can be elsewhere where the node is used"); - //print warning together with suspicious nodes - System.out.println("Node " + new JDDNode(ptr, false) + " has " + cuddRefCount + " reference(s), printing out stack traces of suspicious node instances:"); - boolean first = true; - for (Integer hc : instances.get(ptr)) { - int localRefCount = localCounters.get(hc); - if (localRefCount != 0) { - if (!first) { - System.out.println(" &"); - //first=false; - } else { - first = false; - } - //print only top 5 methods from stack - int i = 0; - for (StackTraceElement st : stackTraces.get(hc)) { - if (i++ > 8) { - break; - } - System.out.println(" " + st.toString()); - } - } + System.out.println("DdNode ptr=0x" + Long.toHexString(ptr)+", "+nodeInfo(ptr)+" has "+extRef.getValue()+" remaining external references."); + if (posRewNodes.size() > 0) { + System.out.println(" Candidates:"); + for (DebugJDDNode node : posRewNodes) { + System.out.println(" ID="+node.getID()+" with "+node.getNodeRefs()+" references"); + } + } else { + System.out.println(" No candidates, here are all JDDNodes for that DdNode:"); + for (DebugJDDNode node : matchingNodes) { + System.out.println(" ID="+node.getID()+" with "+node.getNodeRefs()+" references"); } } } } - + + /** Get the CUDD reference count for the pointer of the JDDNode */ public static int getRefCount(JDDNode n) { return DebugJDD_GetRefCount(n.ptr()); } + + /** Get the number of DebugJDDNodes that reference the pointer */ + private static int getJavaRefCount(long ptr) { + Integer jrefs = javaRefs.get(ptr); + if (jrefs == null) return 0; + return jrefs; + } + + /** Get a map, mapping DdNode pointers to the external reference counts expected by CUDD */ + public static Map getExternalRefCounts() + { + Map result = new TreeMap(); + // Array consists of (pointer, count) pairs + long[] externalRefCounts = DebugJDD_GetExternalRefCounts(); + int i=0; + while (i 0 && printed++ >= limit) { + System.out.println(" ..."); + break; + } else { + System.out.println(" at " + st); + } + } + System.out.println(); + System.out.flush(); + } + } diff --git a/prism/src/jdd/JDD.java b/prism/src/jdd/JDD.java index 98aacb98..e2a455bc 100644 --- a/prism/src/jdd/JDD.java +++ b/prism/src/jdd/JDD.java @@ -1394,6 +1394,9 @@ public class JDD if (ptr == 0L) { throw new CuddOutOfMemoryException(); } + if (DebugJDD.debugEnabled) { + return new DebugJDD.DebugJDDNode(ptr, true); + } return new JDDNode(ptr); } diff --git a/prism/src/jdd/JDDNode.java b/prism/src/jdd/JDDNode.java index 11395650..6670ef35 100644 --- a/prism/src/jdd/JDDNode.java +++ b/prism/src/jdd/JDDNode.java @@ -49,20 +49,14 @@ public class JDDNode } } - public JDDNode(long p, boolean increased_reference) + /** + * Protected constructor from a DdNode pointer. + * In general, to get a JDDNode from a pointer, + * use JDD.ptrToNode(). + */ + protected JDDNode(long p) { ptr = p; - if (DebugJDD.debugEnabled) - DebugJDD.addToSet(this, increased_reference ? 1 : 0); - } - - public JDDNode(long p) { - this(p, true); - } - - public JDDNode(JDDNode dd) - { - this(dd.ptr()); } public long ptr() @@ -85,18 +79,34 @@ public class JDDNode return DDN_GetValue(ptr); } + /** + * Returns the Then child of a (non-constant) JDDNode. + *
+ * This method does NOT increase the reference count of the returned + * node, it is therefore illegal to call JDD.Deref on the result. + *
[ REFS: none, DEREFS: none ] + */ public JDDNode getThen() { assert !this.isConstant(); - // TODO I believe that this breaks debug reference counting - // JDDNode will create a reference to this, but DDN_GetThen will not. - return new JDDNode(DDN_GetThen(ptr), false); + + // just return the node, even if DebugJDD is enabled + return new JDDNode(DDN_GetThen(ptr)); } - + + /** + * Returns the Else child of a (non-constant) JDDNode. + *
+ * This method does NOT increase the reference count of the returned + * node, it is therefore illegal to call JDD.Deref on the result. + *
[ REFS: none, DEREFS: none ] + */ public JDDNode getElse() { assert !this.isConstant(); - return new JDDNode(DDN_GetElse(ptr), false); + + // just return the node, even if DebugJDD is enabled + return new JDDNode(DDN_GetElse(ptr)); } public boolean equals(Object o) @@ -127,8 +137,14 @@ public class JDDNode */ public JDDNode copy() { - JDD.Ref(this); - return new JDDNode(this); + JDDNode result; + if (DebugJDD.debugEnabled) { + result = new DebugJDD.DebugJDDNode(ptr, false); + } else { + result = new JDDNode(ptr()); + } + JDD.Ref(result); + return result; } }