test: rmwprog: support command-line argument

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 84c42689425f257d594c969df0b758038001ab83..e6df37f8372949f610057599181402ddf673ce84 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -159,7 +159,7 @@ void ModelChecker::reset_to_initial_state()
        /* Print all model-checker output before rollback */
        fflush(model_out);
 
-       snapshotObject->backTrackBeforeStep(0);
+       snapshot_backtrack_before(0);
 }
 
 /** @return a thread ID for a new Thread */
@@ -614,7 +614,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
        Node *node = prev->get_node()->get_parent();
 
        int low_tid, high_tid;
-       if (node->is_enabled(t)) {
+       if (node->enabled_status(t->get_id()) == THREAD_ENABLED) {
                low_tid = id_to_int(act->get_tid());
                high_tid = low_tid + 1;
        } else {
@@ -853,6 +853,15 @@ bool ModelChecker::process_mutex(ModelAction *curr)
        return false;
 }
 
+void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader)
+{
+       /* Do more ambitious checks now that mo is more complete */
+       if (mo_may_allow(writer, reader) &&
+                       reader->get_node()->add_future_value(writer->get_value(),
+                               writer->get_seq_number() + params.maxfuturedelay))
+               set_latest_backtrack(reader);
+}
+
 /**
  * Process a write ModelAction
  * @param curr The ModelAction to process
@@ -866,12 +875,9 @@ bool ModelChecker::process_write(ModelAction *curr)
        if (promises->size() == 0) {
                for (unsigned int i = 0; i < futurevalues->size(); i++) {
                        struct PendingFutureValue pfv = (*futurevalues)[i];
-                       //Do more ambitious checks now that mo is more complete
-                       if (mo_may_allow(pfv.writer, pfv.act) &&
-                                       pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number() + params.maxfuturedelay))
-                               set_latest_backtrack(pfv.act);
+                       add_future_value(pfv.writer, pfv.act);
                }
-               futurevalues->resize(0);
+               futurevalues->clear();
        }
 
        mo_graph->commitChanges();
@@ -1333,15 +1339,39 @@ bool ModelChecker::isfeasibleprefix() const
        return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq();
 }
 
+/**
+ * Print disagnostic information about an infeasible execution
+ * @param prefix A string to prefix the output with; if NULL, then a default
+ * message prefix will be provided
+ */
+void ModelChecker::print_infeasibility(const char *prefix) const
+{
+       char buf[100];
+       char *ptr = buf;
+       if (mo_graph->checkForRMWViolation())
+               ptr += sprintf(ptr, "[RMW atomicity]");
+       if (mo_graph->checkForCycles())
+               ptr += sprintf(ptr, "[mo cycle]");
+       if (priv->failed_promise)
+               ptr += sprintf(ptr, "[failed promise]");
+       if (priv->too_many_reads)
+               ptr += sprintf(ptr, "[too many reads]");
+       if (priv->bad_synchronization)
+               ptr += sprintf(ptr, "[bad sw ordering]");
+       if (promises_expired())
+               ptr += sprintf(ptr, "[promise expired]");
+       if (promises->size() != 0)
+               ptr += sprintf(ptr, "[unresolved promise]");
+       if (ptr != buf)
+               model_print("%s: %s\n", prefix ? prefix : "Infeasible", buf);
+}
+
 /**
  * Returns whether the current completed trace is feasible, except for pending
  * release sequences.
  */
 bool ModelChecker::is_feasible_prefix_ignore_relseq() const
 {
-       if (DBG_ENABLED() && promises->size() != 0)
-               DEBUG("Infeasible: unrevolved promises\n");
-
        return !is_infeasible() && promises->size() == 0;
 }
 
@@ -1353,9 +1383,6 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const
  */
 bool ModelChecker::is_infeasible() const
 {
-       if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
-               DEBUG("Infeasible: RMW violation\n");
-
        return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW();
 }
 
@@ -1369,18 +1396,6 @@ bool ModelChecker::is_infeasible() const
  * */
 bool ModelChecker::is_infeasible_ignoreRMW() const
 {
-       if (DBG_ENABLED()) {
-               if (mo_graph->checkForCycles())
-                       DEBUG("Infeasible: modification order cycles\n");
-               if (priv->failed_promise)
-                       DEBUG("Infeasible: failed promise\n");
-               if (priv->too_many_reads)
-                       DEBUG("Infeasible: too many reads\n");
-               if (priv->bad_synchronization)
-                       DEBUG("Infeasible: bad synchronization ordering\n");
-               if (promises_expired())
-                       DEBUG("Infeasible: promises expired\n");
-       }
        return mo_graph->checkForCycles() || priv->failed_promise ||
                priv->too_many_reads || priv->bad_synchronization ||
                promises_expired();
@@ -1773,8 +1788,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                if (thin_air_constraint_may_allow(curr, act)) {
                                        if (!is_infeasible() ||
                                                        (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) {
-                                               struct PendingFutureValue pfv = {curr, act};
-                                               futurevalues->push_back(pfv);
+                                               futurevalues->push_back(PendingFutureValue(curr, act));
                                        }
                                }
                        }
@@ -2562,13 +2576,11 @@ ModelAction * ModelChecker::new_uninitialized_action(void *location) const
        return act;
 }
 
-static void print_list(action_list_t *list, int exec_num = -1)
+static void print_list(action_list_t *list)
 {
        action_list_t::iterator it;
 
        model_print("---------------------------------------------------------------------\n");
-       if (exec_num >= 0)
-               model_print("Execution %d:\n", exec_num);
 
        unsigned int hash = 0;
 
@@ -2621,9 +2633,12 @@ void ModelChecker::print_summary() const
        dumpGraph(buffername);
 #endif
 
-       if (!isfeasibleprefix())
-               model_print("INFEASIBLE EXECUTION!\n");
-       print_list(action_trace, stats.num_total);
+       model_print("Execution %d:", stats.num_total);
+       if (isfeasibleprefix())
+               model_print("\n");
+       else
+               print_infeasibility(" INFEASIBLE");
+       print_list(action_trace);
        model_print("\n");
 }