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
  */
  * @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
 {
        //quick check whether edge is redundant

-       if (checkReachable(fromnode, tonode))
+       if (checkReachable(fromnode, tonode) && !forceedge) {

                return;
                return;

-
-       CycleNode *edgeSrcNode = fromnode;
+       }

 
        /*
         * If the fromnode has a rmwnode, we should
         * follow its RMW chain to add an edge at the end.
         */
 
        /*
         * 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 */
 
        /* 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();
                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);
                        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);
 
        CycleNode *fromnode = getNode(from);
        CycleNode *rmwnode = getNode(rmw);

-

        /* We assume that this RMW has no RMW reading from it yet */
        ASSERT(!rmwnode->getRMW());
 
        /* 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);
                }
        }
                        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);
 
        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
 }
 
 #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);
        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;
 
        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:
        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);
 
        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.
  */
  * @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);
        while(true) {
 
                int index = fuzzer->selectWrite(curr, rf_set);


@@ -282,15 +283,16 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> *
 
                ASSERT(rf);
 
 
                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);
                        read_from(curr, rf);

-                       mo_graph->commitChanges();

                        get_thread(curr)->set_return_value(curr->get_return_value());
                        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();
        }
                (*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
  */
  * @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);
 
        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;
 {
        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)
        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
 {
  */
 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. */
 }
 
 /** 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);
        lastread->process_rmw(act);
        if (act->is_rmw()) {
                mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);

-               mo_graph->commitChanges();

        }
        return lastread;
 }
        }
        return lastread;
 }


@@ -778,7 +774,7 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) {
  * @return True if modification order edges were added; false otherwise
  */
 
  * @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;
 {
        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) {
                                /* 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) {
                                        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) {
                                }
                                /* 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 (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)) {
                                } 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;
                                        }
                                }
                                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;
                /* 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) {
                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.
                                 */
                                 * 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;
                                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) {
                        /* 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;
                        }
 
                                break;
                        }
 


@@ -964,10 +962,10 @@ void ModelExecution::w_modification_order(ModelAction *curr)
                                 *   readfrom(act) --mo--> act
                                 */
                                if (act->is_write())
                                 *   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
                                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) &&
                                }
                                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
  */
  * @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());
 
        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 *>();
                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++) {
 
        /* 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) {
                        }
 
                        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 */
                        }
 
                        /* 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 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);
 
        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);
 
        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;
        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;