model: utilize bad_synchronization flag

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index fdefcc2bcf390dd4a2615a411920466a8f901022..47c6cdb92d442f0b0f460e353e9d25c93cfb6dc7 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);
 }
@@ -334,7 +336,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
                        bool r_status = false;
 
                        if (!second_part_of_rmw) {
-                               check_recency(curr);
+                               check_recency(curr, reads_from);
                                r_status = r_modification_order(curr, reads_from);
                        }
 
@@ -660,6 +662,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                                if (w_modification_order(act))
                                        updated = true;
                        }
+                       mo_graph->commitChanges();
 
                        if (updated)
                                work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
@@ -723,6 +726,9 @@ bool ModelChecker::isfeasibleprefix() {
 
 /** @return whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
+       if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
+               DEBUG("Infeasible: RMW violation\n");
+
        return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
 }
 
@@ -736,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. */
@@ -773,23 +781,21 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
  *
  * If so, we decide that the execution is no longer feasible.
  */
-void ModelChecker::check_recency(ModelAction *curr) {
+void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
        if (params.maxreads != 0) {
+
                if (curr->get_node()->get_read_from_size() <= 1)
                        return;
-
                //Must make sure that execution is currently feasible...  We could
                //accidentally clear by rolling back
                if (!isfeasible())
                        return;
-
                std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
                int tid = id_to_int(curr->get_tid());
 
                /* Skip checks */
                if ((int)thrd_lists->size() <= tid)
                        return;
-
                action_list_t *list = &(*thrd_lists)[tid];
 
                action_list_t::reverse_iterator rit = list->rbegin();
@@ -808,17 +814,18 @@ void ModelChecker::check_recency(ModelAction *curr) {
                        ModelAction *act = *rit;
                        if (!act->is_read())
                                return;
-                       if (act->get_reads_from() != curr->get_reads_from())
+                       
+                       if (act->get_reads_from() != rf)
                                return;
                        if (act->get_node()->get_read_from_size() <= 1)
                                return;
                }
-
                for (int i = 0; i<curr->get_node()->get_read_from_size(); i++) {
                        //Get write
                        const ModelAction * write = curr->get_node()->get_read_from_at(i);
+
                        //Need a different write
-                       if (write==curr->get_reads_from())
+                       if (write==rf)
                                continue;
 
                        /* Test to see whether this is a feasible write to read from*/
@@ -1108,6 +1115,10 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con
  */
 bool ModelChecker::release_seq_head(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;
+
        while (rf) {
                ASSERT(rf->is_write());
 
@@ -1269,8 +1280,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();
                        }
                }
 
@@ -1413,16 +1426,17 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                Promise *promise = (*promises)[promise_index];
                if (write->get_node()->get_promise(i)) {
                        ModelAction *read = promise->get_action();
-                       read->read_from(write);
                        if (read->is_rmw()) {
                                mo_graph->addRMWEdge(write, read);
                        }
+                       read->read_from(write);
                        //First fix up the modification order for actions that happened
                        //before the read
                        r_modification_order(read, write);
                        //Next fix up the modification order for actions that happened
                        //after the read.
                        post_r_modification_order(read, write);
+
                        promises->erase(promises->begin() + promise_index);
                        resolved = true;
                } else