#include "promise.h"
#include "datarace.h"
#include "threads-model.h"
+#include "output.h"
#define INITIAL_THREAD_ID 0
~bug_message() { if (msg) snapshot_free(msg); }
char *msg;
- void print() { printf("%s", msg); }
+ void print() { model_print("%s", msg); }
+
+ SNAPSHOTALLOC
};
/**
Thread *nextThread;
ModelAction *next_backtrack;
std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
+ struct execution_stats stats;
};
/** @brief Constructor */
/* Initialize default scheduler */
params(params),
scheduler(new Scheduler()),
- num_executions(0),
- num_feasible_executions(0),
diverge(NULL),
earliest_diverge(NULL),
action_trace(new action_list_t()),
too_many_reads = false;
bad_synchronization = false;
reset_asserted();
+
+ /* Print all model-checker output before rollback */
+ fflush(model_out);
+
snapshotObject->backTrackBeforeStep(0);
}
* the current trace is not yet feasible, the error message will be stashed and
* printed if the execution ever becomes feasible.
*
- * This function can also be used to immediately trigger the bug; that is, we
- * don't wait for a feasible execution before aborting. Only use the
- * "immediate" option when you know that the infeasibility is justified (e.g.,
- * pending release sequences are not a problem)
- *
* @param msg Descriptive message for the bug (do not include newline char)
- * @param user_thread Was this assertion triggered from a user thread?
- * @param immediate Should this bug be triggered immediately?
+ * @return True if bug is immediately-feasible
*/
-void ModelChecker::assert_bug(const char *msg, bool user_thread, bool immediate)
+bool ModelChecker::assert_bug(const char *msg)
{
priv->bugs.push_back(new bug_message(msg));
- if (immediate || isfeasibleprefix()) {
+ if (isfeasibleprefix()) {
set_assert();
- if (user_thread)
- switch_to_master(NULL);
+ return true;
}
+ return false;
}
/**
- * @brief Assert a bug in the executing program, with a default message
- * @see ModelChecker::assert_bug
- * @param user_thread Was this assertion triggered from a user thread?
- */
-void ModelChecker::assert_bug(bool user_thread)
-{
- assert_bug("bug detected", user_thread);
-}
-
-/**
- * @brief Assert a bug in the executing program immediately
+ * @brief Assert a bug in the executing program, asserted by a user thread
* @see ModelChecker::assert_bug
* @param msg Descriptive message for the bug (do not include newline char)
*/
-void ModelChecker::assert_bug_immediate(const char *msg)
+void ModelChecker::assert_user_bug(const char *msg)
{
- printf("Feasible: %s\n", isfeasibleprefix() ? "yes" : "no");
- assert_bug(msg, false, true);
+ /* If feasible bug, bail out now */
+ if (assert_bug(msg))
+ switch_to_master(NULL);
}
/** @return True, if any bugs have been reported for this execution */
void ModelChecker::print_bugs() const
{
if (have_bug_reports()) {
- printf("Bug report: %zu bugs detected\n", priv->bugs.size());
+ model_print("Bug report: %zu bug%s detected\n",
+ priv->bugs.size(),
+ priv->bugs.size() > 1 ? "s" : "");
for (unsigned int i = 0; i < priv->bugs.size(); i++)
priv->bugs[i]->print();
}
}
+/**
+ * @brief Record end-of-execution stats
+ *
+ * Must be run when exiting an execution. Records various stats.
+ * @see struct execution_stats
+ */
+void ModelChecker::record_stats()
+{
+ stats.num_total++;
+ if (!isfinalfeasible())
+ stats.num_infeasible++;
+ else if (have_bug_reports())
+ stats.num_buggy_executions++;
+ else if (is_complete_execution())
+ stats.num_complete++;
+}
+
+/** @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 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);
+ model_print("Total nodes created: %d\n", node_stack->get_total_nodes());
+}
+
/**
* Queries the model-checker for more executions to explore and, if one
* exists, resets the model-checker state to execute a new execution.
{
DBG();
- num_executions++;
-
if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
- printf("Earliest divergence point since last feasible execution:\n");
+ model_print("Earliest divergence point since last feasible execution:\n");
if (earliest_diverge)
earliest_diverge->print();
else
- printf("(Not set)\n");
+ model_print("(Not set)\n");
earliest_diverge = NULL;
- num_feasible_executions++;
if (is_deadlocked())
assert_bug("Deadlock detected");
- print_bugs();
checkDataRaces();
+ print_bugs();
+ model_print("\n");
print_summary();
} else if (DBG_ENABLED()) {
+ model_print("\n");
print_summary();
}
+ record_stats();
+
if ((diverge = get_next_backtrack()) == NULL)
return false;
if (DBG_ENABLED()) {
- printf("Next execution will diverge at:\n");
+ model_print("Next execution will diverge at:\n");
diverge->print();
}
}
/* See if we have realized a data race */
- if (checkDataRaces())
- assert_bug("Datarace");
+ checkDataRaces();
}
/**
}
// If we resolved promises or data races, see if we have realized a data race.
- if (checkDataRaces())
- assert_bug("Datarace");
+ checkDataRaces();
return updated;
}
assert_bug("May read from uninitialized atomic");
if (DBG_ENABLED() || !initialized) {
- printf("Reached read action:\n");
+ model_print("Reached read action:\n");
curr->print();
- printf("Printing may_read_from\n");
+ model_print("Printing may_read_from\n");
curr->get_node()->print_may_read_from();
- printf("End printing may_read_from\n");
+ model_print("End printing may_read_from\n");
}
}
}
}
-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;
- printf("---------------------------------------------------------------------\n");
- printf("Trace:\n");
+ model_print("---------------------------------------------------------------------\n");
+ if (exec_num >= 0)
+ model_print("Execution %d:\n", exec_num);
+
unsigned int hash=0;
for (it = list->begin(); it != list->end(); it++) {
(*it)->print();
hash=hash^(hash<<3)^((*it)->hash());
}
- printf("HASH %u\n", hash);
- printf("---------------------------------------------------------------------\n");
+ model_print("HASH %u\n", hash);
+ model_print("---------------------------------------------------------------------\n");
}
#if SUPPORT_MOD_ORDER_DUMP
void ModelChecker::print_summary()
{
- printf("\n");
- printf("Number of executions: %d\n", num_executions);
- printf("Number of feasible executions: %d\n", num_feasible_executions);
- printf("Total nodes created: %d\n", node_stack->get_total_nodes());
-
#if SUPPORT_MOD_ORDER_DUMP
scheduler->print();
char buffername[100];
- sprintf(buffername, "exec%04u", num_executions);
+ sprintf(buffername, "exec%04u", stats.num_total);
mo_graph->dumpGraphToFile(buffername);
- sprintf(buffername, "graph%04u", num_executions);
+ sprintf(buffername, "graph%04u", stats.num_total);
dumpGraph(buffername);
#endif
if (!isfinalfeasible())
- printf("INFEASIBLE EXECUTION!\n");
- print_list(action_trace);
- printf("\n");
+ model_print("INFEASIBLE EXECUTION!\n");
+ print_list(action_trace, stats.num_total);
+ model_print("\n");
}
/**
*/
if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
isfinalfeasible() && !unrealizedraces.empty()) {
- printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
+ model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
pending_rel_seqs->size());
ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
std::memory_order_seq_cst, NULL, VALUE_NONE,
projects / c11tester.git / blobdiff