model: fixup "infeasible" messages

These messages should be much more compact and targeted. Currently, we
either get no infeasibility messages (when verbose=0) or we get messages
every time is_infeasible() is executed. Neither is helpful for debugging,
since the infeasibility may be temporary, as we choose a new path for
execution on the fly. So instead, just print the infeasibility message
at the end of infeasible executions.

Also, rather than spread the messages across multiple lines, just put
them together into a single string.

diff --git a/model.cc b/model.cc
index 88d5e710a18e2dbdb2978e6ca9b5856a41ff1c34..f2d40fe6f724022ee2b50c783df310ce0b47ff99 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1339,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, "[unrevolved 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;
 }
 
@@ -1359,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();
 }
 
@@ -1375,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();
@@ -2627,7 +2636,7 @@ void ModelChecker::print_summary() const
 #endif
 
        if (!isfeasibleprefix())
-               model_print("INFEASIBLE EXECUTION!\n");
+               print_infeasibility("INFEASIBLE EXECUTION");
        print_list(action_trace, stats.num_total);
        model_print("\n");
 }

diff --git a/model.h b/model.h
index 4fd2667753f4b3ae85698c6422921a1cf18163f7..97a898926e49dfd8480412c67a2900dfd8db5f15 100644 (file)
--- a/model.h
+++ b/model.h
@@ -255,6 +255,7 @@ private:
        struct execution_stats stats;
        void record_stats();
 
+       void print_infeasibility(const char *prefix) const;
        bool is_feasible_prefix_ignore_relseq() const;
        bool is_infeasible_ignoreRMW() const;
        bool is_infeasible() const;