ModelChecker *model;
+struct bug_message {
+ bug_message(const char *str) {
+ const char *fmt = " [BUG] %s\n";
+ msg = (char *)snapshot_malloc(strlen(fmt) + strlen(str));
+ sprintf(msg, fmt, str);
+ }
+ ~bug_message() { if (msg) snapshot_free(msg); }
+
+ char *msg;
+ void print() { printf("%s", msg); }
+
+ SNAPSHOTALLOC
+};
+
/**
* Structure for holding small ModelChecker members that should be snapshotted
*/
modelclock_t used_sequence_numbers;
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()),
delete scheduler;
delete mo_graph;
+ for (unsigned int i = 0; i < priv->bugs.size(); i++)
+ delete priv->bugs[i];
+ priv->bugs.clear();
snapshot_free(priv);
}
return true;
}
+/**
+ * @brief Assert a bug in the executing program.
+ *
+ * Use this function to assert any sort of bug in the user program. If the
+ * current trace is feasible (actually, a prefix of some feasible execution),
+ * then this execution will be aborted, printing the appropriate message. If
+ * the current trace is not yet feasible, the error message will be stashed and
+ * printed if the execution ever becomes feasible.
+ *
+ * @param msg Descriptive message for the bug (do not include newline char)
+ * @return True if bug is immediately-feasible
+ */
+bool ModelChecker::assert_bug(const char *msg)
+{
+ priv->bugs.push_back(new bug_message(msg));
+
+ if (isfeasibleprefix()) {
+ set_assert();
+ return true;
+ }
+ return false;
+}
+
+/**
+ * @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_user_bug(const char *msg)
+{
+ /* 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 */
+bool ModelChecker::have_bug_reports() const
+{
+ return priv->bugs.size() != 0;
+}
+
+/** @brief Print bug report listing for this execution (if any bugs exist) */
+void ModelChecker::print_bugs() const
+{
+ if (have_bug_reports()) {
+ printf("Bug report: %zu bugs detected\n", priv->bugs.size());
+ 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
+{
+ printf("Number of complete, bug-free executions: %d\n", stats.num_complete);
+ printf("Number of buggy executions: %d\n", stats.num_buggy_executions);
+ printf("Number of infeasible executions: %d\n", stats.num_infeasible);
+ printf("Total executions: %d\n", stats.num_total);
+ printf("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++;
+ record_stats();
- if (is_deadlocked())
- printf("ERROR: DEADLOCK\n");
- if (isfinalfeasible()) {
+ if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
printf("Earliest divergence point since last feasible execution:\n");
if (earliest_diverge)
earliest_diverge->print();
printf("(Not set)\n");
earliest_diverge = NULL;
- num_feasible_executions++;
- }
+ if (is_deadlocked())
+ assert_bug("Deadlock detected");
- if (isfinalfeasible() || DBG_ENABLED()) {
checkDataRaces();
+ print_bugs();
+ printf("\n");
+ print_stats();
+ print_summary();
+ } else if (DBG_ENABLED()) {
+ printf("\n");
print_summary();
}
}
//otherwise fall into the lock case
case ATOMIC_LOCK: {
- if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock) {
- printf("Lock access before initialization\n");
- set_assert();
- }
+ if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
+ assert_bug("Lock access before initialization");
state->islocked = true;
ModelAction *unlock = get_last_unlock(curr);
//synchronize with the previous unlock statement
}
/* See if we have realized a data race */
- if (checkDataRaces())
- set_assert();
+ checkDataRaces();
}
/**
/* Initialize work_queue with the "current action" work */
work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
- while (!work_queue.empty()) {
+ while (!work_queue.empty() && !has_asserted()) {
WorkQueueEntry work = work_queue.front();
work_queue.pop_front();
}
// If we resolved promises or data races, see if we have realized a data race.
- if (checkDataRaces()) {
- set_assert();
- }
+ checkDataRaces();
return updated;
}
}
}
- if (!initialized) {
- /** @todo Need a more informative way of reporting errors. */
- printf("ERROR: may read from uninitialized atomic\n");
- set_assert();
- }
+ if (!initialized)
+ assert_bug("May read from uninitialized atomic");
if (DBG_ENABLED() || !initialized) {
printf("Reached read action:\n");
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
/* Infeasible -> don't take any more steps */
if (!isfeasible())
return false;
+ else if (isfeasibleprefix() && have_bug_reports()) {
+ set_assert();
+ return false;
+ }
if (params.bound != 0) {
if (priv->used_sequence_numbers > params.bound) {
projects / c11tester.git / blobdiff