From c4497f6168d1af560d9305337139d35bcd4ee9bb Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Wed, 12 Sep 2012 22:06:51 -0700
Subject: [PATCH] right fix for avoid rmw cycles...  bad assumption in the
 cyclegraph

---
 cyclegraph.cc | 14 ++++++++++++--
 model.cc      | 37 +++++--------------------------------
 model.h       |  1 -
 3 files changed, 17 insertions(+), 35 deletions(-)

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 2bac4de7..62330624 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -85,8 +85,12 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
 	}
 
 	/* Transfer all outgoing edges from the from node to the rmw node */
-	/* This process cannot add a cycle because rmw should not have any
-		 incoming edges yet.*/
+	/* This process should not add a cycle because either: 
+	 * (1) The rmw should not have any incoming edges yet if it is the
+	 * new node or
+	 * (2) the fromnode is the new node and therefore it should not 
+	 * have any outgoing edges.
+	 */
 	std::vector<CycleNode *> * edges=fromnode->getEdges();
 	for(unsigned int i=0;i<edges->size();i++) {
 		CycleNode * tonode=(*edges)[i];
@@ -94,6 +98,12 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
 		rmwnode->addEdge(tonode);
 	}
 	rollbackvector.push_back(fromnode);
+
+	if (!hasCycles) {
+		// With promises we could be setting up a cycle here if we aren't
+		// careful...avoid it..
+		hasCycles=checkReachable(rmwnode, fromnode);
+	}
 	fromnode->addEdge(rmwnode);
 }
 
diff --git a/model.cc b/model.cc
index c3a8c841..015ca167 100644
--- a/model.cc
+++ b/model.cc
@@ -34,8 +34,7 @@ ModelChecker::ModelChecker(struct model_params params) :
 	mo_graph(new CycleGraph()),
 	failed_promise(false),
 	too_many_reads(false),
-	asserted(false),
-	rmw_cycle(false)
+	asserted(false)
 {
 	/* Allocate this "size" on the snapshotting heap */
 	priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
@@ -78,7 +77,6 @@ void ModelChecker::reset_to_initial_state()
 	node_stack->reset_execution();
 	failed_promise = false;
 	too_many_reads = false;
-	rmw_cycle=false;
 	reset_asserted();
 	snapshotObject->backTrackBeforeStep(0);
 }
@@ -261,29 +259,6 @@ ModelAction * ModelChecker::get_next_backtrack()
 }
 
 
-/** Checks whether making the ModelAction read read_from the
-		ModelAction write will introduce a cycle in the reads_from
-		relation.
-
-@return true if making it read from will be fine, false otherwise.
-
-*/
-
-bool ModelChecker::ensure_rmw_acyclic(const ModelAction * read, const ModelAction *write) {
-	if (!read->is_rmw())
-		return true;
-	if (!write->is_rmw())
-		return true;
-	while(write!=NULL) {
-		if (write==read) {
-			rmw_cycle=true;
-			return false;
-		}
-		write=write->get_reads_from();
-	}
-	return true;
-}
-
 /**
  * Processes a read or rmw model action.
  * @param curr is the read model action to process.
@@ -301,9 +276,7 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
 			mo_graph->startChanges();
 
 			value = reads_from->get_value();
-				/* Assign reads_from, perform release/acquire synchronization */
-			if (ensure_rmw_acyclic(curr, reads_from))
-				curr->read_from(reads_from);
+
 			if (!second_part_of_rmw) {
 				check_recency(curr,false);
 			}
@@ -316,6 +289,7 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
 				continue;
 			}
 
+			curr->read_from(reads_from);
 			mo_graph->commitChanges();
 			updated |= r_status;
 		} else if (!second_part_of_rmw) {
@@ -487,7 +461,7 @@ bool ModelChecker::isfeasible() {
 /** @returns whether the current partial trace is feasible other than
  * multiple RMW reading from the same store. */
 bool ModelChecker::isfeasibleotherthanRMW() {
-	return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !rmw_cycle && !promises_expired();
+	return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
 }
 
 /** Returns whether the current completed trace is feasible. */
@@ -1054,8 +1028,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 		Promise *promise = (*promises)[promise_index];
 		if (write->get_node()->get_promise(i)) {
 			ModelAction *read = promise->get_action();
-			if (ensure_rmw_acyclic(read, write))
-				read->read_from(write);
+			read->read_from(write);
 			if (read->is_rmw()) {
 				mo_graph->addRMWEdge(write, read);
 			}
diff --git a/model.h b/model.h
index d47fe967..90180a99 100644
--- a/model.h
+++ b/model.h
@@ -189,7 +189,6 @@ private:
 	bool failed_promise;
 	bool too_many_reads;
 	bool asserted;
-	bool rmw_cycle;
 };
 
 extern ModelChecker *model;
-- 
2.34.1