model: add "# redundant" stat

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 8dcb6f3ad8e69a0e82ad3991c4425a35f1a24640..df06760893018d5bc1756cd89df263c6ed117cc6 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -13,6 +13,7 @@
 #include "promise.h"
 #include "datarace.h"
 #include "threads-model.h"
+#include "output.h"
 
 #define INITIAL_THREAD_ID      0
 
@@ -139,6 +140,10 @@ void ModelChecker::reset_to_initial_state()
        too_many_reads = false;
        bad_synchronization = false;
        reset_asserted();
+
+       /* Print all model-checker output before rollback */
+       fflush(model_out);
+
        snapshotObject->backTrackBeforeStep(0);
 }
 
@@ -396,12 +401,15 @@ void ModelChecker::record_stats()
                stats.num_buggy_executions++;
        else if (is_complete_execution())
                stats.num_complete++;
+       else
+               stats.num_redundant++;
 }
 
 /** @brief Print execution stats */
 void ModelChecker::print_stats() const
 {
        model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
+       model_print("Number of redundant executions: %d\n", stats.num_redundant);
        model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
        model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
        model_print("Total executions: %d\n", stats.num_total);
@@ -409,40 +417,65 @@ void ModelChecker::print_stats() const
 }
 
 /**
- * Queries the model-checker for more executions to explore and, if one
- * exists, resets the model-checker state to execute a new execution.
- *
- * @return If there are more executions to explore, return true. Otherwise,
- * return false.
+ * @brief End-of-exeuction print
+ * @param printbugs Should any existing bugs be printed?
  */
-bool ModelChecker::next_execution()
+void ModelChecker::print_execution(bool printbugs) const
 {
-       DBG();
-
-       record_stats();
+       print_program_output();
 
-       if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
+       if (DBG_ENABLED() || params.verbose) {
                model_print("Earliest divergence point since last feasible execution:\n");
                if (earliest_diverge)
                        earliest_diverge->print();
                else
                        model_print("(Not set)\n");
 
-               earliest_diverge = NULL;
+               model_print("\n");
+               print_stats();
+       }
 
+       /* Don't print invalid bugs */
+       if (printbugs)
+               print_bugs();
+
+       model_print("\n");
+       print_summary();
+}
+
+/**
+ * Queries the model-checker for more executions to explore and, if one
+ * exists, resets the model-checker state to execute a new execution.
+ *
+ * @return If there are more executions to explore, return true. Otherwise,
+ * return false.
+ */
+bool ModelChecker::next_execution()
+{
+       DBG();
+       /* Is this execution a feasible execution that's worth bug-checking? */
+       bool complete = isfinalfeasible() && (is_complete_execution() ||
+                       have_bug_reports());
+
+       /* End-of-execution bug checks */
+       if (complete) {
                if (is_deadlocked())
                        assert_bug("Deadlock detected");
 
                checkDataRaces();
-               print_bugs();
-               model_print("\n");
-               print_stats();
-               print_summary();
-       } else if (DBG_ENABLED()) {
-               model_print("\n");
-               print_summary();
        }
 
+       record_stats();
+
+       /* Output */
+       if (DBG_ENABLED() || params.verbose || have_bug_reports())
+               print_execution(complete);
+       else
+               clear_program_output();
+
+       if (complete)
+               earliest_diverge = NULL;
+
        if ((diverge = get_next_backtrack()) == NULL)
                return false;
 
@@ -2222,12 +2255,14 @@ bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *wr
        }
 }
 
-static void print_list(action_list_t *list)
+static void print_list(action_list_t *list, int exec_num = -1)
 {
        action_list_t::iterator it;
 
        model_print("---------------------------------------------------------------------\n");
-       model_print("Trace:\n");
+       if (exec_num >= 0)
+               model_print("Execution %d:\n", exec_num);
+
        unsigned int hash=0;
 
        for (it = list->begin(); it != list->end(); it++) {
@@ -2266,7 +2301,8 @@ void ModelChecker::dumpGraph(char *filename) {
 }
 #endif
 
-void ModelChecker::print_summary()
+/** @brief Prints an execution trace summary. */
+void ModelChecker::print_summary() const
 {
 #if SUPPORT_MOD_ORDER_DUMP
        scheduler->print();
@@ -2279,7 +2315,7 @@ void ModelChecker::print_summary()
 
        if (!isfinalfeasible())
                model_print("INFEASIBLE EXECUTION!\n");
-       print_list(action_trace);
+       print_list(action_trace, stats.num_total);
        model_print("\n");
 }