From: Brian Norris <banorris@uci.edu>
Date: Wed, 20 Mar 2013 20:44:24 +0000 (-0700)
Subject: cyclegraph: propagate RMW atomicity edges down the chain
X-Git-Tag: oopsla2013~133
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=d62cd6e5bbba2975923540d99bae0587fe03b791

cyclegraph: propagate RMW atomicity edges down the chain

When we add an edge between 'rmwnode' and 'tonode', we are trying to
ensure RMW atomicity. But 'rmwnode' may itself be read by another RMW
(or, in fact, a chain). So we must follow this chain down before
propagating the atomicity edge.

Also, we have the potential to run into the same problem in
addRMWEdge(), except that in that function, we assume that the RMW is
newly-explored and so does not yet have an outgoing RMW edge. This adds
an ASSERT() to check this property.
---

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 8d37dea..26ea215 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -198,29 +198,33 @@ bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node)
  */
 bool CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode)
 {
-	bool added;
-
-	if ((added = fromnode->addEdge(tonode))) {
+	if (fromnode->addEdge(tonode)) {
 		rollbackvector.push_back(fromnode);
 		if (!hasCycles)
 			hasCycles = checkReachable(tonode, fromnode);
-	}
+	} else
+		return false; /* No new edge */
 
 	/*
-	 * If the fromnode has a rmwnode that is not the tonode, we should add
-	 * an edge between its rmwnode and the tonode
+	 * If the fromnode has a rmwnode that is not the tonode, we should
+	 * follow its RMW chain to add an edge at the end, unless we encounter
+	 * tonode along the way
 	 */
 	CycleNode *rmwnode = fromnode->getRMW();
-	if (rmwnode && rmwnode != tonode) {
-		if (rmwnode->addEdge(tonode)) {
-			if (!hasCycles)
-				hasCycles = checkReachable(tonode, rmwnode);
+	if (rmwnode) {
+		while (rmwnode != tonode && rmwnode->getRMW())
+			rmwnode = rmwnode->getRMW();
 
-			rollbackvector.push_back(rmwnode);
-			added = true;
+		if (rmwnode != tonode) {
+			if (rmwnode->addEdge(tonode)) {
+				if (!hasCycles)
+					hasCycles = checkReachable(tonode, rmwnode);
+
+				rollbackvector.push_back(rmwnode);
+			}
 		}
 	}
-	return added;
+	return true;
 }
 
 /**
@@ -244,6 +248,9 @@ void CycleGraph::addRMWEdge(const T *from, const ModelAction *rmw)
 	CycleNode *fromnode = getNode(from);
 	CycleNode *rmwnode = getNode(rmw);
 
+	/* We assume that this RMW has no RMW reading from it yet */
+	ASSERT(!rmwnode->getRMW());
+
 	/* Two RMW actions cannot read from the same write. */
 	if (fromnode->setRMW(rmwnode))
 		hasCycles = true;