X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;ds=inline;f=cyclegraph.cc;h=2dc2eae9503a92f1117be1345441242d3a8f1437;hb=bd6db524d36605b8eae0159f943b7e9e9361d7a5;hp=edf582b318d05bc731fb1fee943589fbd373610e;hpb=ecba3e5519898cbf612e7d4e2eaef63d1d8af7d3;p=c11tester.git

diff --git a/cyclegraph.cc b/cyclegraph.cc
index edf582b3..2dc2eae9 100644
--- 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),
@@ -17,6 +17,20 @@ CycleGraph::CycleGraph() :
 /** CycleGraph destructor */
 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
 }
 
 /**
@@ -29,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;
 }
@@ -51,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
+	if (!hasCycles)
 		hasCycles = checkReachable(tonode, fromnode);
-	}
 
 	if (fromnode->addEdge(tonode))
 		rollbackvector.push_back(fromnode);
@@ -75,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
+		if (!hasCycles)
 			hasCycles = checkReachable(tonode, rmwnode);
-		}
 
 		if (rmwnode->addEdge(tonode))
 			rollbackvector.push_back(rmwnode);
@@ -120,16 +123,9 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw)
 		}
 	}
 
-
-	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..
+	if (!hasCycles)
 		hasCycles = checkReachable(rmwnode, fromnode);
-	}
+
 	if (fromnode->addEdge(rmwnode))
 		rollbackvector.push_back(fromnode);
 }
@@ -187,15 +183,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;
@@ -308,6 +304,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
@@ -318,6 +324,7 @@ bool CycleNode::addEdge(CycleNode *node)
 		if (edges[i] == node)
 			return false;
 	edges.push_back(node);
+	node->back_edges.push_back(this);
 	return true;
 }