new cyclegraph

diff --git a/cyclegraph.cc b/cyclegraph.cc
index a3e86cf00b5f78ce098b5161d10c0dc90bc88390..5d894f848d474444d4c482ae214e7f384a58be5d 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -59,32 +59,32 @@ CycleNode * CycleGraph::getNode(const ModelAction *action)
  * @param tonode The edge points to this CycleNode
  * @return True, if new edge(s) are added; otherwise false
  */
-void CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode)
+void CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode, bool forceedge)
 {
        //quick check whether edge is redundant
-       if (checkReachable(fromnode, tonode))
+       if (checkReachable(fromnode, tonode) && !forceedge) {
                return;
-
-       CycleNode *edgeSrcNode = fromnode;
+       }
 
        /*
         * If the fromnode has a rmwnode, we should
         * follow its RMW chain to add an edge at the end.
         */
-       CycleNode *rmwnode = fromnode->getRMW();
-       if (rmwnode) {
-               while (rmwnode->getRMW())
-                       rmwnode = rmwnode->getRMW();
-               edgeSrcNode = rmwnode;
+       while (fromnode->getRMW()) {
+               CycleNode *nextnode = fromnode->getRMW();
+               if (nextnode == tonode)
+                       break;
+               fromnode = nextnode;
        }
 
-       edgeSrcNode->addEdge(tonode);   //Add edge to edgeSrcNode
+       fromnode->addEdge(tonode);      //Add edge to edgeSrcNode
 
        /* Propagate clock vector changes */
-       if (tonode->cv->merge(edgeSrcNode->cv)) {
-               queue->push_back(edgeSrcNode);
+       if (tonode->cv->merge(fromnode->cv)) {
+               queue->push_back(fromnode);
                while(!queue->empty()) {
                        const CycleNode *node = queue->back();
+                       queue->pop_back();
                        unsigned int numedges = node->getNumEdges();
                        for(unsigned int i = 0;i < numedges;i++) {
                                CycleNode * enode = node->getEdge(i);
@@ -114,7 +114,6 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw)
 
        CycleNode *fromnode = getNode(from);
        CycleNode *rmwnode = getNode(rmw);
-
        /* We assume that this RMW has no RMW reading from it yet */
        ASSERT(!rmwnode->getRMW());
 
@@ -133,8 +132,9 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw)
                        rmwnode->addEdge(tonode);
                }
        }
-
-       addNodeEdge(fromnode, rmwnode);
+       fromnode->edges.clear();
+       
+       addNodeEdge(fromnode, rmwnode, true);
 }
 
 /**
@@ -159,7 +159,18 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to)
        CycleNode *fromnode = getNode(from);
        CycleNode *tonode = getNode(to);
 
-       addNodeEdge(fromnode, tonode);
+       addNodeEdge(fromnode, tonode, false);
+}
+
+void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to, bool forceedge)
+{
+       ASSERT(from);
+       ASSERT(to);
+
+       CycleNode *fromnode = getNode(from);
+       CycleNode *tonode = getNode(to);
+
+       addNodeEdge(fromnode, tonode, forceedge);
 }
 
 #if SUPPORT_MOD_ORDER_DUMP

diff --git a/cyclegraph.h b/cyclegraph.h
index 624ce885f2aadf4543dd9505b40a4192ceb802aa..e2b586403994b5573c863d4825857e7945d28c8d 100644 (file)
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -24,6 +24,7 @@ public:
        CycleGraph();
        ~CycleGraph();
        void addEdge(const ModelAction *from, const ModelAction *to);
+       void addEdge(const ModelAction *from, const ModelAction *to, bool forceedge);
        void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
        bool checkReachable(const ModelAction *from, const ModelAction *to) const;
 
@@ -37,7 +38,7 @@ public:
        CycleNode * getNode_noCreate(const ModelAction *act) const;
        SNAPSHOTALLOC
 private:
-       void addNodeEdge(CycleNode *fromnode, CycleNode *tonode);
+       void addNodeEdge(CycleNode *fromnode, CycleNode *tonode, bool forceedge);
        void putNode(const ModelAction *act, CycleNode *node);
        CycleNode * getNode(const ModelAction *act);
 

diff --git a/execution.cc b/execution.cc
index c286b2d78745005ba2bc9e8c84fc8efa2daa6411..213b26067bfda027be973d0166a1a7e1db634f51 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -272,8 +272,9 @@ bool ModelExecution::is_complete_execution() const
  * @param rf_set is the set of model actions we can possibly read from
  * @return True if processing this read updates the mo_graph.
  */
-bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
+void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
 {
+       SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
        while(true) {
 
                int index = fuzzer->selectWrite(curr, rf_set);
@@ -282,15 +283,16 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
 
                ASSERT(rf);
 
-               mo_graph->startChanges();
-               r_modification_order(curr, rf);
-               if (!is_infeasible()) {
+               if (r_modification_order(curr, rf, priorset)) {
+                       for(unsigned int i=0;i<priorset->size();i++) {
+                               mo_graph->addEdge((*priorset)[i], rf);
+                       }
                        read_from(curr, rf);
-                       mo_graph->commitChanges();
                        get_thread(curr)->set_return_value(curr->get_return_value());
-                       return updated;
+                       delete priorset;
+                       return;
                }
-               mo_graph->rollbackChanges();
+               priorset->clear();
                (*rf_set)[index] = rf_set->back();
                rf_set->pop_back();
        }
@@ -388,15 +390,13 @@ bool ModelExecution::process_mutex(ModelAction *curr)
  * @param curr The ModelAction to process
  * @return True if the mo_graph was updated or promises were resolved
  */
-bool ModelExecution::process_write(ModelAction *curr)
+void ModelExecution::process_write(ModelAction *curr)
 {
 
-       bool updated_mod_order = w_modification_order(curr);
+       w_modification_order(curr);
 
-       mo_graph->commitChanges();
 
        get_thread(curr)->set_return_value(VALUE_NONE);
-       return updated_mod_order;
 }
 
 /**
@@ -730,8 +730,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const
 {
        char buf[100];
        char *ptr = buf;
-       if (mo_graph->checkForCycles())
-               ptr += sprintf(ptr, "[mo cycle]");
        if (priv->bad_synchronization)
                ptr += sprintf(ptr, "[bad sw ordering]");
        if (ptr != buf)
@@ -746,8 +744,7 @@ void ModelExecution::print_infeasibility(const char *prefix) const
  */
 bool ModelExecution::is_infeasible() const
 {
-       return mo_graph->checkForCycles() ||
-                                priv->bad_synchronization;
+       return priv->bad_synchronization;
 }
 
 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
@@ -756,7 +753,6 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) {
        lastread->process_rmw(act);
        if (act->is_rmw()) {
                mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
-               mo_graph->commitChanges();
        }
        return lastread;
 }
@@ -778,7 +774,7 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) {
  * @return True if modification order edges were added; false otherwise
  */
 
-bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<ModelAction *> * priorset)
+bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset)
 {
        SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
        unsigned int i;
@@ -823,26 +819,26 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                                /* C++, Section 29.3 statement 5 */
                                if (curr->is_seqcst() && last_sc_fence_thread_local &&
                                                *act < *last_sc_fence_thread_local) {
-                                 if (mo_graph->checkReachable(rf, act))
-                                   return false;
-                                 priorset->add(act);
+                                       if (mo_graph->checkReachable(rf, act))
+                                               return false;
+                                       priorset->push_back(act);
                                        break;
                                }
                                /* C++, Section 29.3 statement 4 */
                                else if (act->is_seqcst() && last_sc_fence_local &&
                                                                 *act < *last_sc_fence_local) {
-                                 if (mo_graph->checkReachable(rf, act))
-                                   return false;
-                                 priorset->add(act);
-                                 break;
+                                       if (mo_graph->checkReachable(rf, act))
+                                               return false;
+                                       priorset->push_back(act);
+                                       break;
                                }
                                /* C++, Section 29.3 statement 6 */
                                else if (last_sc_fence_thread_before &&
                                                                 *act < *last_sc_fence_thread_before) {
-                                 if (mo_graph->checkReachable(rf, act))
-                                   return false;
-                                 priorset->add(act);
-                                 break;
+                                       if (mo_graph->checkReachable(rf, act))
+                                               return false;
+                                       priorset->push_back(act);
+                                       break;
                                }
                        }
 
@@ -852,15 +848,15 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                         */
                        if (act->happens_before(curr)) {
                                if (act->is_write()) {
-                                 if (mo_graph->checkReachable(rf, act))
-                                   return false;
-                                 priorset->add(act);
+                                       if (mo_graph->checkReachable(rf, act))
+                                               return false;
+                                       priorset->push_back(act);
                                } else {
                                        const ModelAction *prevrf = act->get_reads_from();
                                        if (!prevrf->equals(rf)) {
-                                         if (mo_graph->checkReachable(rf, prevrf))
-                                           return false;
-                                         priorset->add(prevrf);
+                                               if (mo_graph->checkReachable(rf, prevrf))
+                                                       return false;
+                                               priorset->push_back(prevrf);
                                        }
                                }
                                break;
@@ -922,6 +918,7 @@ void ModelExecution::w_modification_order(ModelAction *curr)
                /* Iterate over actions in thread, starting from most recent */
                action_list_t *list = &(*thrd_lists)[i];
                action_list_t::reverse_iterator rit;
+               bool force_edge = false;
                for (rit = list->rbegin();rit != list->rend();rit++) {
                        ModelAction *act = *rit;
                        if (act == curr) {
@@ -936,6 +933,7 @@ void ModelExecution::w_modification_order(ModelAction *curr)
                                 * 3) If normal write, we need to look at earlier actions, so
                                 * continue processing list.
                                 */
+                               force_edge = true;
                                if (curr->is_rmw()) {
                                        if (curr->get_reads_from() != NULL)
                                                break;
@@ -948,7 +946,7 @@ void ModelExecution::w_modification_order(ModelAction *curr)
                        /* C++, Section 29.3 statement 7 */
                        if (last_sc_fence_thread_before && act->is_write() &&
                                        *act < *last_sc_fence_thread_before) {
-                               mo_graph->addEdge(act, curr);
+                               mo_graph->addEdge(act, curr, force_edge);
                                break;
                        }
 
@@ -964,10 +962,10 @@ void ModelExecution::w_modification_order(ModelAction *curr)
                                 *   readfrom(act) --mo--> act
                                 */
                                if (act->is_write())
-                                       mo_graph->addEdge(act, curr);
+                                       mo_graph->addEdge(act, curr, force_edge);
                                else if (act->is_read()) {
                                        //if previous read accessed a null, just keep going
-                                       mo_graph->addEdge(act->get_reads_from(), curr);
+                                       mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
                                }
                                break;
                        } else if (act->is_read() && !act->could_synchronize_with(curr) &&
@@ -1047,12 +1045,8 @@ bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *
  * @return true, if the ModelExecution is certain that release_heads is complete;
  * false otherwise
  */
-bool ModelExecution::release_seq_heads(const ModelAction *rf,
-                                                                                                                                                        rel_heads_list_t *release_heads) const
+bool ModelExecution::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const
 {
-       /* Only check for release sequences if there are no cycles */
-       if (mo_graph->checkForCycles())
-               return false;
 
        for ( ;rf != NULL;rf = rf->get_reads_from()) {
                ASSERT(rf->is_write());
@@ -1331,7 +1325,6 @@ SnapVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *cu
                last_sc_write = get_last_seq_cst_write(curr);
 
        SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
-       SnapVector<ModelAction *> * priorset = new SnapVector<ModelAction *>();
 
        /* Iterate over all threads */
        for (i = 0;i < thrd_lists->size();i++) {
@@ -1366,8 +1359,8 @@ SnapVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *cu
                        }
 
                        if (allow_read) {
-                         /* Only add feasible reads */
-                         rf_set->push_back(act);
+                               /* Only add feasible reads */
+                               rf_set->push_back(act);
                        }
 
                        /* Include at most one act per-thread that "happens before" curr */

diff --git a/execution.h b/execution.h
index 40cd3ac03ba1360013c64bc52bef7b24c03293f7..b78837fc7219bd77dcea34744ff6214fb5fecaa6 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -127,8 +127,8 @@ private:
        bool next_execution();
        ModelAction * check_current_action(ModelAction *curr);
        bool initialize_curr_action(ModelAction **curr);
-       bool process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set);
-       bool process_write(ModelAction *curr);
+       void process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set);
+       void process_write(ModelAction *curr);
        bool process_fence(ModelAction *curr);
        bool process_mutex(ModelAction *curr);
 
@@ -144,7 +144,7 @@ private:
        SnapVector<ModelAction *> * build_may_read_from(ModelAction *curr);
        ModelAction * process_rmw(ModelAction *curr);
 
-  bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<ModelAction *> *priorset);
+       bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> *priorset);
        void w_modification_order(ModelAction *curr);
        void get_release_seq_heads(ModelAction *acquire, ModelAction *read, rel_heads_list_t *release_heads);
        bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const;