lots of debugging here... finally working with my rmw example...

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 62330624d6f08a233292ddfee1269380e8869beb..0a3d8858e795849f16ab1cae667b2e34bb1367cc 100644 (file)
--- 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 795c4a99fea347b1d610c62df8172c55c447f91d..50317d07daa539d8f6643f16c3892c89aaddf60e 100644 (file)
--- 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;
                        }
                }