cyclegraph: add edgeCreatesCycle() function

[c11tester.git] / cyclegraph.cc

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 168ad90cdb0c4930d045d2dd97d2d45cc2e2f068..ec0ce45f55ae65ae77325889b0aa0bfe84444cf8 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -6,7 +6,7 @@
 
 /** Initializes a CycleGraph object. */
 CycleGraph::CycleGraph() :
-       discovered(new HashTable<CycleNode *, CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free>(16)),
+       discovered(new HashTable<const CycleNode *, const CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free>(16)),
        hasCycles(false),
        oldCycles(false),
        hasRMWViolation(false),
@@ -20,6 +20,19 @@ CycleGraph::~CycleGraph()
        delete discovered;
 }
 
+/**
+ * Add a CycleNode to the graph, corresponding to a store ModelAction
+ * @param act The write action that should be added
+ * @param node The CycleNode that corresponds to the store
+ */
+void CycleGraph::putNode(const ModelAction *act, CycleNode *node)
+{
+       actionToNode.put(act, node);
+#if SUPPORT_MOD_ORDER_DUMP
+       nodeList.push_back(node);
+#endif
+}
+
 /**
  * @brief Returns the CycleNode corresponding to a given ModelAction
  * @param action The ModelAction to find a node for
@@ -30,10 +43,7 @@ CycleNode * CycleGraph::getNode(const ModelAction *action)
        CycleNode *node = actionToNode.get(action);
        if (node == NULL) {
                node = new CycleNode(action);
-               actionToNode.put(action, node);
-#if SUPPORT_MOD_ORDER_DUMP
-               nodeList.push_back(node);
-#endif
+               putNode(action, node);
        }
        return node;
 }
@@ -52,14 +62,8 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to)
        CycleNode *fromnode = getNode(from);
        CycleNode *tonode = getNode(to);
 
-       if (!hasCycles) {
-               // Reflexive edges are cycles
-               hasCycles = (from == to);
-       }
-       if (!hasCycles) {
-               // Check for Cycles
-               hasCycles = checkReachable(tonode, fromnode);
-       }
+       if (!hasCycles)
+               hasCycles = edgeCreatesCycle(fromnode, tonode);
 
        if (fromnode->addEdge(tonode))
                rollbackvector.push_back(fromnode);
@@ -76,10 +80,8 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to)
         * for the possibility of sending to's write value to rmwnode
         */
        if (rmwnode != NULL && !to->is_rmw()) {
-               if (!hasCycles) {
-                       // Check for Cycles
-                       hasCycles = checkReachable(tonode, rmwnode);
-               }
+               if (!hasCycles)
+                       hasCycles = edgeCreatesCycle(rmwnode, tonode);
 
                if (rmwnode->addEdge(tonode))
                        rollbackvector.push_back(rmwnode);
@@ -121,16 +123,9 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw)
                }
        }
 
+       if (!hasCycles)
+               hasCycles = edgeCreatesCycle(fromnode, rmwnode);
 
-       if (!hasCycles) {
-               // Reflexive edges are cycles
-               hasCycles = (from == rmw);
-       }
-       if (!hasCycles) {
-               // With promises we could be setting up a cycle here if we aren't
-               // careful...avoid it..
-               hasCycles = checkReachable(rmwnode, fromnode);
-       }
        if (fromnode->addEdge(rmwnode))
                rollbackvector.push_back(fromnode);
 }
@@ -165,6 +160,18 @@ void CycleGraph::dumpGraphToFile(const char *filename) const
 }
 #endif
 
+/**
+ * Checks whether the addition of an edge between these two nodes would create
+ * a cycle in the graph.
+ * @param from The CycleNode from which the edge would start
+ * @param to The CycleNode to which the edge would point
+ * @return True if this edge would create a cycle; false otherwise
+ */
+bool CycleGraph::edgeCreatesCycle(const CycleNode *from, const CycleNode *to) const
+{
+       return (from == to) || checkReachable(to, from);
+}
+
 /**
  * Checks whether one ModelAction can reach another.
  * @param from The ModelAction from which to begin exploration
@@ -188,15 +195,15 @@ bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to)
  * @param to The CycleNode to reach
  * @return True, @a from can reach @a to; otherwise, false
  */
-bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) const
+bool CycleGraph::checkReachable(const CycleNode *from, const CycleNode *to) const
 {
-       std::vector< CycleNode *, ModelAlloc<CycleNode *> > queue;
+       std::vector< const CycleNode *, ModelAlloc<const CycleNode *> > queue;
        discovered->reset();
 
        queue.push_back(from);
        discovered->put(from, from);
        while (!queue.empty()) {
-               CycleNode *node = queue.back();
+               const CycleNode *node = queue.back();
                queue.pop_back();
                if (node == to)
                        return true;
@@ -309,6 +316,16 @@ unsigned int CycleNode::getNumEdges() const
        return edges.size();
 }
 
+CycleNode * CycleNode::getBackEdge(unsigned int i) const
+{
+       return back_edges[i];
+}
+
+unsigned int CycleNode::getNumBackEdges() const
+{
+       return back_edges.size();
+}
+
 /**
  * Adds an edge from this CycleNode to another CycleNode.
  * @param node The node to which we add a directed edge
@@ -319,6 +336,7 @@ bool CycleNode::addEdge(CycleNode *node)
                if (edges[i] == node)
                        return false;
        edges.push_back(node);
+       node->back_edges.push_back(this);
        return true;
 }