From: Brian Norris <banorris@uci.edu>
Date: Tue, 21 Aug 2012 06:56:10 +0000 (-0700)
Subject: cyclegraph: straighten out header vs. implementation vs. usage
X-Git-Tag: pldi2013~263
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=ad9f8597027acf647e4fc3a0b22ac3312d291878

cyclegraph: straighten out header vs. implementation vs. usage

The CycleGraph::addEdge and CycleGraph::addRMWEdge functions were a little
confusing to use, since their implementation and header prototypes had
different parameter naming. This swapped the 'to' and 'from' naming, such that
it appeared as if the addEdge() users were adding edges in the reverse
direction. The functionality was not actually incorrect, but my understanding
was...

This corrects the naming and switches the order of the arguments.
---

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 1eb1add..b140ded 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -31,7 +31,7 @@ CycleNode * CycleGraph::getNode(const ModelAction *action) {
  * @param to The edge points to this ModelAction
  * @param from The edge comes from this ModelAction
  */
-void CycleGraph::addEdge(const ModelAction *to, const ModelAction *from) {
+void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) {
 	CycleNode *fromnode=getNode(from);
 	CycleNode *tonode=getNode(to);
 
@@ -60,7 +60,7 @@ void CycleGraph::addEdge(const ModelAction *to, const ModelAction *from) {
  *  can occur in between the rmw and the from action.  Only one RMW
  *  action can read from a given write.
  */
-void CycleGraph::addRMWEdge(const ModelAction *rmw, const ModelAction *from) {
+void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
 	CycleNode *fromnode=getNode(from);
 	CycleNode *rmwnode=getNode(rmw);
 
diff --git a/cyclegraph.h b/cyclegraph.h
index d0258d1..c8ba531 100644
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -19,7 +19,7 @@ class CycleGraph {
 	~CycleGraph();
 	void addEdge(const ModelAction *from, const ModelAction *to);
 	bool checkForCycles();
-	void addRMWEdge(const ModelAction *from, const ModelAction *to);
+	void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
 
  private:
 	CycleNode * getNode(const ModelAction *);
diff --git a/model.cc b/model.cc
index b3ced38..dabdda7 100644
--- a/model.cc
+++ b/model.cc
@@ -379,7 +379,7 @@ ModelAction * ModelChecker::process_rmw(ModelAction * act) {
 	ModelAction *lastread = get_last_action(tid);
 	lastread->process_rmw(act);
 	if (act->is_rmw())
-		mo_graph->addRMWEdge(lastread, lastread->get_reads_from());
+		mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
 	return lastread;
 }
 
@@ -406,9 +406,9 @@ void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *r
 				if (act->is_read()) {
 					const ModelAction * prevreadfrom = act->get_reads_from();
 					if (prevreadfrom != NULL && rf != prevreadfrom)
-						mo_graph->addEdge(rf, prevreadfrom);
+						mo_graph->addEdge(prevreadfrom, rf);
 				} else if (rf != act) {
-					mo_graph->addEdge(rf, act);
+					mo_graph->addEdge(act, rf);
 				}
 				break;
 			}
@@ -443,9 +443,9 @@ void ModelChecker::post_r_modification_order(ModelAction * curr, const ModelActi
 			if (lastact->is_read()) {
 				const ModelAction * postreadfrom = lastact->get_reads_from();
 				if (postreadfrom != NULL&&rf != postreadfrom)
-					mo_graph->addEdge(postreadfrom, rf);
+					mo_graph->addEdge(rf, postreadfrom);
 			} else if (rf != lastact) {
-				mo_graph->addEdge(lastact, rf);
+				mo_graph->addEdge(rf, lastact);
 			}
 			break;
 		}
@@ -466,7 +466,7 @@ void ModelChecker::w_modification_order(ModelAction * curr) {
 			 so we are initialized. */
 		ModelAction * last_seq_cst = get_last_seq_cst(curr->get_location());
 		if (last_seq_cst != NULL)
-			mo_graph->addEdge(curr, last_seq_cst);
+			mo_graph->addEdge(last_seq_cst, curr);
 	}
 
 	/* Iterate over all threads */
@@ -480,9 +480,9 @@ void ModelChecker::w_modification_order(ModelAction * curr) {
 			/* Include at most one act per-thread that "happens before" curr */
 			if (act->happens_before(curr)) {
 				if (act->is_read())
-					mo_graph->addEdge(curr, act->get_reads_from());
+					mo_graph->addEdge(act->get_reads_from(), curr);
 				else
-					mo_graph->addEdge(curr, act);
+					mo_graph->addEdge(act, curr);
 				break;
 			} else if (act->is_read() && !act->is_synchronizing(curr) &&
 			                             !act->same_thread(curr)) {