model: always re-calculate clock vectors

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 1711e1a002b6d105cb413efec6c20e644f51f0f8..c4bc693ef5560f646684b3a2cb002e685f4be848 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -38,7 +38,8 @@ ModelChecker::ModelChecker(struct model_params params) :
        mo_graph(new CycleGraph()),
        failed_promise(false),
        too_many_reads(false),
-       asserted(false)
+       asserted(false),
+       bad_synchronization(false)
 {
        /* Allocate this "size" on the snapshotting heap */
        priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
@@ -80,6 +81,7 @@ void ModelChecker::reset_to_initial_state()
        node_stack->reset_execution();
        failed_promise = false;
        too_many_reads = false;
+       bad_synchronization = false;
        reset_asserted();
        snapshotObject->backTrackBeforeStep(0);
 }
@@ -523,7 +525,9 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
        if (curr->is_rmwc() || curr->is_rmw()) {
                newcurr = process_rmw(curr);
                delete curr;
-               compute_promises(newcurr);
+
+               if (newcurr->is_rmw())
+                       compute_promises(newcurr);
                return newcurr;
        }
 
@@ -539,9 +543,7 @@ 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()));
+               newcurr->create_cv(get_parent_action(newcurr->get_tid()));
        } else {
                newcurr = curr;
                /*
@@ -740,10 +742,12 @@ bool ModelChecker::isfeasibleotherthanRMW() {
                        DEBUG("Infeasible: failed promise\n");
                if (too_many_reads)
                        DEBUG("Infeasible: too many reads\n");
+               if (bad_synchronization)
+                       DEBUG("Infeasible: bad synchronization ordering\n");
                if (promises_expired())
                        DEBUG("Infeasible: promises expired\n");
        }
-       return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
+       return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired();
 }
 
 /** Returns whether the current completed trace is feasible. */
@@ -944,10 +948,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;
@@ -955,12 +959,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;
                }
@@ -1276,8 +1293,10 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
                complete = release_seq_head(rf, &release_heads);
                for (unsigned int i = 0; i < release_heads.size(); i++) {
                        if (!act->has_synchronized_with(release_heads[i])) {
-                               updated = true;
-                               act->synchronize_with(release_heads[i]);
+                               if (act->synchronize_with(release_heads[i]))
+                                       updated = true;
+                               else
+                                       set_bad_synchronization();
                        }
                }
 
@@ -1430,6 +1449,8 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                        //Next fix up the modification order for actions that happened
                        //after the read.
                        post_r_modification_order(read, write);
+                       //Make sure the promise's value matches the write's value
+                       ASSERT(promise->get_value() == write->get_value());
 
                        promises->erase(promises->begin() + promise_index);
                        resolved = true;
@@ -1636,6 +1657,7 @@ bool ModelChecker::take_step() {
 
                        priv->nextThread = check_current_action(priv->current_action);
                        priv->current_action = NULL;
+
                        if (curr->is_blocked() || curr->is_complete())
                                scheduler->remove_thread(curr);
                } else {