cyclegraph: straighten out header vs. implementation vs. usage
authorBrian Norris <banorris@uci.edu>
Tue, 21 Aug 2012 06:56:10 +0000 (23:56 -0700)
committerBrian Norris <banorris@uci.edu>
Tue, 21 Aug 2012 06:56:10 +0000 (23:56 -0700)
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.

cyclegraph.cc
cyclegraph.h
model.cc

index 1eb1add33fc255e4f53e9044b3d3850b422668dd..b140ded1382c12cfc9fee46358bd36fc2720aa36 100644 (file)
@@ -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
  */
  * @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);
 
        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.
  */
  *  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);
 
        CycleNode *fromnode=getNode(from);
        CycleNode *rmwnode=getNode(rmw);
 
index d0258d180f6e60546bc9619b1b3f56c86bda33de..c8ba531427f29a3edc5613d1ba1f50bf63067ed8 100644 (file)
@@ -19,7 +19,7 @@ class CycleGraph {
        ~CycleGraph();
        void addEdge(const ModelAction *from, const ModelAction *to);
        bool checkForCycles();
        ~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 *);
 
  private:
        CycleNode * getNode(const ModelAction *);
index b3ced383b59c1b1cbca02fc135df87cd006d4523..dabdda7002206c293e6d0e49e39469f9584a18d2 100644 (file)
--- 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())
        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;
 }
 
        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)
                                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) {
                                } else if (rf != act) {
-                                       mo_graph->addEdge(rf, act);
+                                       mo_graph->addEdge(act, rf);
                                }
                                break;
                        }
                                }
                                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)
                        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) {
                        } else if (rf != lastact) {
-                               mo_graph->addEdge(lastact, rf);
+                               mo_graph->addEdge(rf, lastact);
                        }
                        break;
                }
                        }
                        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)
                         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 */
        }
 
        /* 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())
                        /* 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
                                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)) {
                                break;
                        } else if (act->is_read() && !act->is_synchronizing(curr) &&
                                                     !act->same_thread(curr)) {