From 59b62a130c9615c9ccd23c4354c7bc827d5eda3b Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Thu, 13 Sep 2012 01:33:24 -0700
Subject: [PATCH] lots of debugging here... finally working with my rmw
 example...

---
 cyclegraph.cc | 12 +++++++++---
 model.cc      | 18 +++++++++++-------
 2 files changed, 20 insertions(+), 10 deletions(-)

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 6233062..0a3d885 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -55,7 +55,11 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) {
 	//If the fromnode has a rmwnode that is not the tonode, we
 	//should add an edge between its rmwnode and the tonode
 
-	if (rmwnode!=NULL&&rmwnode!=tonode) {
+	//If tonode is also a rmw, don't do this check as the execution is
+	//doomed and we'll catch the problem elsewhere, but we want to allow
+	//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);
@@ -94,8 +98,10 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
 	std::vector<CycleNode *> * edges=fromnode->getEdges();
 	for(unsigned int i=0;i<edges->size();i++) {
 		CycleNode * tonode=(*edges)[i];
-		rollbackvector.push_back(rmwnode);
-		rmwnode->addEdge(tonode);
+		if (tonode!=rmwnode) {
+			rollbackvector.push_back(rmwnode);
+			rmwnode->addEdge(tonode);
+		}
 	}
 	rollbackvector.push_back(fromnode);
 
diff --git a/model.cc b/model.cc
index 795c4a9..50317d0 100644
--- a/model.cc
+++ b/model.cc
@@ -277,14 +277,15 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
 			mo_graph->startChanges();
 
 			value = reads_from->get_value();
+			bool r_status=false;
 
 			if (!second_part_of_rmw) {
 				check_recency(curr,false);
+				r_status=r_modification_order(curr, reads_from);
 			}
 
-			bool r_status=r_modification_order(curr,reads_from);
 
-			if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||!curr->get_node()->future_value_empty())) {
+			if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
 				mo_graph->rollbackChanges();
 				too_many_reads=false;
 				continue;
@@ -611,16 +612,19 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf
 
 			/* Include at most one act per-thread that "happens before" curr */
 			if (act->happens_before(curr)) {
-				if (act->is_read()) {
+				if (act->is_write()) {
+					if (rf != act && act != curr) {
+						mo_graph->addEdge(act, rf);
+						added = true;
+					}
+				} else {
 					const ModelAction *prevreadfrom = act->get_reads_from();
 					if (prevreadfrom != NULL && rf != prevreadfrom) {
 						mo_graph->addEdge(prevreadfrom, rf);
 						added = true;
 					}
-				} else if (rf != act) {
-					mo_graph->addEdge(act, rf);
-					added = true;
-				}
+				} 
+
 				break;
 			}
 		}
-- 
2.34.1