Two change:

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 62e75205e4ee9681bcef321856c744978c9cc5c1..a22e0214a6c2a3fdabd01a5442b3cba6643c616d 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -543,19 +543,19 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
                /* Discard duplicate ModelAction; use action from NodeStack */
                delete curr;
 
-               /* If we have diverged, we need to reset the clock vector. */
-               if (diverge == NULL) {
-                       newcurr->create_cv(get_parent_action(newcurr->get_tid()));
-               }
+               /* Always compute new clock vector */
+               newcurr->create_cv(get_parent_action(newcurr->get_tid()));
        } else {
                newcurr = curr;
+
+               /* Always compute new clock vector */
+               newcurr->create_cv(get_parent_action(newcurr->get_tid()));
                /*
                 * Perform one-time actions when pushing new ModelAction onto
                 * NodeStack
                 */
-               curr->create_cv(get_parent_action(curr->get_tid()));
-               if (curr->is_write())
-                       compute_promises(curr);
+               if (newcurr->is_write())
+                       compute_promises(newcurr);
        }
        return newcurr;
 }
@@ -658,7 +658,8 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                        bool updated = false;
 
                        if (act->is_read()) {
-                               if (r_modification_order(act, act->get_reads_from()))
+                               const ModelAction *rf = act->get_reads_from();
+                               if (rf != NULL && r_modification_order(act, rf))
                                        updated = true;
                        }
                        if (act->is_write()) {
@@ -951,10 +952,10 @@ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio
                action_list_t::reverse_iterator rit;
                ModelAction *lastact = NULL;
 
-               /* Find last action that happens after curr */
+               /* Find last action that happens after curr that is either not curr or a rmw */
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *act = *rit;
-                       if (curr->happens_before(act)) {
+                       if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
                                lastact = act;
                        } else
                                break;
@@ -962,12 +963,25 @@ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio
 
                        /* Include at most one act per-thread that "happens before" curr */
                if (lastact != NULL) {
-                       if (lastact->is_read()) {
+                       if (lastact==curr) {
+                               //Case 1: The resolved read is a RMW, and we need to make sure
+                               //that the write portion of the RMW mod order after rf
+
+                               mo_graph->addEdge(rf, lastact);
+                       } else if (lastact->is_read()) {
+                               //Case 2: The resolved read is a normal read and the next
+                               //operation is a read, and we need to make sure the value read
+                               //is mod ordered after rf
+
                                const ModelAction *postreadfrom = lastact->get_reads_from();
                                if (postreadfrom != NULL&&rf != postreadfrom)
                                        mo_graph->addEdge(rf, postreadfrom);
-                       } else if (rf != lastact) {
-                               mo_graph->addEdge(rf, lastact);
+                       } else {
+                               //Case 3: The resolved read is a normal read and the next
+                               //operation is a write, and we need to make sure that the
+                               //write is mod ordered after rf
+                               if (lastact!=rf)
+                                       mo_graph->addEdge(rf, lastact);
                        }
                        break;
                }