From a1b119052d16810d6289855635c2b0e66a6b93b8 Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Wed, 12 Sep 2012 21:03:37 -0700
Subject: [PATCH] another bug fix...

---
 model.cc | 41 ++++++++++++++++++++++++++++++++++++-----
 model.h  |  4 ++++
 2 files changed, 40 insertions(+), 5 deletions(-)

diff --git a/model.cc b/model.cc
index bd4ade2..c3a8c84 100644
--- a/model.cc
+++ b/model.cc
@@ -34,7 +34,8 @@ ModelChecker::ModelChecker(struct model_params params) :
 	mo_graph(new CycleGraph()),
 	failed_promise(false),
 	too_many_reads(false),
-	asserted(false)
+	asserted(false),
+	rmw_cycle(false)
 {
 	/* Allocate this "size" on the snapshotting heap */
 	priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
@@ -77,6 +78,7 @@ 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);
 }
@@ -258,6 +260,30 @@ ModelAction * ModelChecker::get_next_backtrack()
 	return next;
 }
 
+
+/** 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.
@@ -276,7 +302,8 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
 
 			value = reads_from->get_value();
 				/* Assign reads_from, perform release/acquire synchronization */
-			curr->read_from(reads_from);
+			if (ensure_rmw_acyclic(curr, reads_from))
+				curr->read_from(reads_from);
 			if (!second_part_of_rmw) {
 				check_recency(curr,false);
 			}
@@ -457,9 +484,10 @@ bool ModelChecker::isfeasible() {
 	return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
 }
 
-/** @returns whether the current partial trace is feasible. */
+/** @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 && !promises_expired();
+	return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !rmw_cycle && !promises_expired();
 }
 
 /** Returns whether the current completed trace is feasible. */
@@ -1026,7 +1054,8 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 		Promise *promise = (*promises)[promise_index];
 		if (write->get_node()->get_promise(i)) {
 			ModelAction *read = promise->get_action();
-			read->read_from(write);
+			if (ensure_rmw_acyclic(read, write))
+				read->read_from(write);
 			if (read->is_rmw()) {
 				mo_graph->addRMWEdge(write, read);
 			}
@@ -1040,6 +1069,8 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 	return resolved;
 }
 
+
+
 /**
  * Compute the set of promises that could potentially be satisfied by this
  * action. Note that the set computation actually appears in the Node, not in
diff --git a/model.h b/model.h
index fec8d1f..d47fe96 100644
--- a/model.h
+++ b/model.h
@@ -89,6 +89,9 @@ private:
 	/** The scheduler to use: tracks the running/ready Threads */
 	Scheduler *scheduler;
 	
+	bool ensure_rmw_acyclic(const ModelAction * read, const ModelAction *write);
+
+
 	bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
 	bool has_asserted() {return asserted;}
 	void reset_asserted() {asserted=false;}
@@ -186,6 +189,7 @@ private:
 	bool failed_promise;
 	bool too_many_reads;
 	bool asserted;
+	bool rmw_cycle;
 };
 
 extern ModelChecker *model;
-- 
2.34.1