right fix for avoid rmw cycles... bad assumption in the cyclegraph

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 2bac4de7cf0469c57818ceab835458a872bb7c29..62330624d6f08a233292ddfee1269380e8869beb 100644 (file)
--- 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 c3a8c8415a71ed684e18b19fc2e9284e6bc6fac1..015ca16796f9b9fdc9bae0ea0ff2b76dfdee4e7f 100644 (file)
--- 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 d47fe9677a78c57b0c6a8da46ac774b7749a7ef2..90180a993ecb065eeb062432b83342cc9fd785c4 100644 (file)
--- 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;