model: bugfix - w_modification_order handling current action
authorBrian Norris <banorris@uci.edu>
Tue, 18 Sep 2012 17:40:33 +0000 (10:40 -0700)
committerBrian Norris <banorris@uci.edu>
Tue, 18 Sep 2012 17:44:04 +0000 (10:44 -0700)
The current action should be skipped when iterating lists in
w_modification_order.

Bugfix thanks to Brian D.

model.cc

index 766e369..483e832 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -769,24 +769,33 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                action_list_t::reverse_iterator rit;
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
+                       if (act == curr) {
+                               /*
+                                * If RMW, we already have all relevant edges,
+                                * so just skip to next thread.
+                                * If normal write, we need to look at earlier
+                                * actions, so continue processing list.
+                                */
+                               if (curr->is_rmw())
+                                       break;
+                               else
+                                       continue;
+                       }
 
                        /*
                         * Include at most one act per-thread that "happens
-                        * before" curr. Only consider reflexively if curr is
-                        * RMW.
+                        * before" curr
                         */
-                       if (act->happens_before(curr) && (act != curr || curr->is_rmw())) {
+                       if (act->happens_before(curr)) {
                                /*
                                 * Note: if act is RMW, just add edge:
                                 *   act --mo--> curr
                                 * The following edge should be handled elsewhere:
                                 *   readfrom(act) --mo--> act
                                 */
-                               if (act->is_write()) {
-                                       //RMW shouldn't have an edge to themselves
-                                       if (act!=curr)
-                                               mo_graph->addEdge(act, curr);
-                               } else if (act->is_read() && act->get_reads_from() != NULL)
+                               if (act->is_write())
+                                       mo_graph->addEdge(act, curr);
+                               else if (act->is_read() && act->get_reads_from() != NULL)
                                        mo_graph->addEdge(act->get_reads_from(), curr);
                                added = true;
                                break;