#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
};
* Structure for holding small ModelChecker members that should be snapshotted
*/
struct model_snapshot_members {
+ model_snapshot_members() :
+ current_action(NULL),
+ /* First thread created will have id INITIAL_THREAD_ID */
+ next_thread_id(INITIAL_THREAD_ID),
+ used_sequence_numbers(0),
+ nextThread(NULL),
+ next_backtrack(NULL),
+ bugs(),
+ stats(),
+ failed_promise(false),
+ too_many_reads(false),
+ bad_synchronization(false),
+ asserted(false)
+ { }
+
+ ~model_snapshot_members() {
+ for (unsigned int i = 0; i < bugs.size(); i++)
+ delete bugs[i];
+ bugs.clear();
+ }
+
ModelAction *current_action;
unsigned int next_thread_id;
modelclock_t used_sequence_numbers;
ModelAction *next_backtrack;
std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
struct execution_stats stats;
+ bool failed_promise;
+ bool too_many_reads;
+ /** @brief Incorrectly-ordered synchronization was made */
+ bool bad_synchronization;
+ bool asserted;
+
+ SNAPSHOTALLOC
};
/** @brief Constructor */
pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
node_stack(new NodeStack()),
- mo_graph(new CycleGraph()),
- failed_promise(false),
- too_many_reads(false),
- asserted(false),
- bad_synchronization(false)
+ priv(new struct model_snapshot_members()),
+ mo_graph(new CycleGraph())
{
- /* Allocate this "size" on the snapshotting heap */
- priv = (struct model_snapshot_members *)snapshot_calloc(1, sizeof(*priv));
- /* First thread created will have id INITIAL_THREAD_ID */
- priv->next_thread_id = INITIAL_THREAD_ID;
-
/* Initialize a model-checker thread, for special ModelActions */
model_thread = new Thread(get_next_id());
thread_map->put(id_to_int(model_thread->get_id()), model_thread);
delete node_stack;
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);
+ delete priv;
}
static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr) {
{
DEBUG("+++ Resetting to initial state +++\n");
node_stack->reset_execution();
- failed_promise = false;
- too_many_reads = false;
- bad_synchronization = false;
- reset_asserted();
+
+ /* Print all model-checker output before rollback */
+ fflush(model_out);
+
snapshotObject->backTrackBeforeStep(0);
}
}
}
+/** @brief Alert the model-checker that an incorrectly-ordered
+ * synchronization was made */
+void ModelChecker::set_bad_synchronization()
+{
+ priv->bad_synchronization = true;
+}
+
+bool ModelChecker::has_asserted() const
+{
+ return priv->asserted;
+}
+
+void ModelChecker::set_assert()
+{
+ priv->asserted = true;
+}
+
/**
* Check if we are in a deadlock. Should only be called at the end of an
* execution, although it should not give false positives in the middle of an
* 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();
}
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
{
- 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());
+ 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);
+ model_print("Total nodes created: %d\n", node_stack->get_total_nodes());
+}
+
+/**
+ * @brief End-of-exeuction print
+ * @param printbugs Should any existing bugs be printed?
+ */
+void ModelChecker::print_execution(bool printbugs) const
+{
+ print_program_output();
+
+ 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");
+
+ model_print("\n");
+ print_stats();
+ }
+
+ /* Don't print invalid bugs */
+ if (printbugs)
+ print_bugs();
+
+ model_print("\n");
+ print_summary();
}
/**
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());
- record_stats();
-
- if (isfinalfeasible() && (is_complete_execution() || have_bug_reports())) {
- printf("Earliest divergence point since last feasible execution:\n");
- if (earliest_diverge)
- earliest_diverge->print();
- else
- printf("(Not set)\n");
-
- earliest_diverge = NULL;
-
+ /* End-of-execution bug checks */
+ if (complete) {
if (is_deadlocked())
assert_bug("Deadlock detected");
- print_bugs();
checkDataRaces();
- printf("\n");
- print_stats();
- print_summary();
- } else if (DBG_ENABLED()) {
- printf("\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;
if (DBG_ENABLED()) {
- printf("Next execution will diverge at:\n");
+ model_print("Next execution will diverge at:\n");
diverge->print();
}
case ATOMIC_READ:
case ATOMIC_WRITE:
case ATOMIC_RMW: {
+ /* Optimization: relaxed operations don't need backtracking */
+ if (act->is_relaxed())
+ return NULL;
/* linear search: from most recent to oldest */
action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
action_list_t::reverse_iterator rit;
}
- if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
+ if (!second_part_of_rmw&&is_infeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
mo_graph->rollbackChanges();
- too_many_reads = false;
+ priv->too_many_reads = false;
continue;
}
}
/* See if we have realized a data race */
- if (checkDataRaces())
- assert_bug("Datarace");
+ checkDataRaces();
}
/**
* feasible trace. */
bool ModelChecker::isfeasibleprefix() const
{
- return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
+ return promises->size() == 0 && pending_rel_seqs->size() == 0 && !is_infeasible();
}
-/** @return whether the current partial trace is feasible. */
-bool ModelChecker::isfeasible() const
+/**
+ * Check if the current partial trace is infeasible. Does not check any
+ * end-of-execution flags, which might rule out the execution. Thus, this is
+ * useful only for ruling an execution as infeasible.
+ * @return whether the current partial trace is infeasible.
+ */
+bool ModelChecker::is_infeasible() const
{
if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
DEBUG("Infeasible: RMW violation\n");
- return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
+ return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW();
}
-/** @return whether the current partial trace is feasible other than
- * multiple RMW reading from the same store. */
-bool ModelChecker::isfeasibleotherthanRMW() const
+/**
+ * Check If the current partial trace is infeasible, while ignoring
+ * infeasibility related to 2 RMW's reading from the same store. It does not
+ * check end-of-execution feasibility.
+ * @see ModelChecker::is_infeasible
+ * @return whether the current partial trace is infeasible, ignoring multiple
+ * RMWs reading from the same store.
+ * */
+bool ModelChecker::is_infeasible_ignoreRMW() const
{
if (DBG_ENABLED()) {
if (mo_graph->checkForCycles())
DEBUG("Infeasible: modification order cycles\n");
- if (failed_promise)
+ if (priv->failed_promise)
DEBUG("Infeasible: failed promise\n");
- if (too_many_reads)
+ if (priv->too_many_reads)
DEBUG("Infeasible: too many reads\n");
- if (bad_synchronization)
+ if (priv->bad_synchronization)
DEBUG("Infeasible: bad synchronization ordering\n");
if (promises_expired())
DEBUG("Infeasible: promises expired\n");
}
- return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired();
+ return mo_graph->checkForCycles() || priv->failed_promise ||
+ priv->too_many_reads || priv->bad_synchronization ||
+ promises_expired();
}
/** Returns whether the current completed trace is feasible. */
if (DBG_ENABLED() && promises->size() != 0)
DEBUG("Infeasible: unrevolved promises\n");
- return isfeasible() && promises->size() == 0;
+ return !is_infeasible() && promises->size() == 0;
}
/** Close out a RMWR by converting previous RMWR into a RMW or READ. */
return;
//Must make sure that execution is currently feasible... We could
//accidentally clear by rolling back
- if (!isfeasible())
+ if (is_infeasible())
return;
std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
int tid = id_to_int(curr->get_tid());
/* Test to see whether this is a feasible write to read from*/
mo_graph->startChanges();
r_modification_order(curr, write);
- bool feasiblereadfrom = isfeasible();
+ bool feasiblereadfrom = !is_infeasible();
mo_graph->rollbackChanges();
if (!feasiblereadfrom)
}
}
if (feasiblewrite) {
- too_many_reads = true;
+ priv->too_many_reads = true;
return;
}
}
*/
if (thin_air_constraint_may_allow(curr, act)) {
- if (isfeasible() ||
- (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) {
+ 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);
}
}
// If we resolved promises or data races, see if we have realized a data race.
- if (checkDataRaces())
- assert_bug("Datarace");
+ checkDataRaces();
return updated;
}
merge_cv->synchronized_since(act)) {
if (promise->increment_threads(tid)) {
//Promise has failed
- failed_promise = true;
+ priv->failed_promise = true;
return;
}
}
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
if (promise->check_promise()) {
- failed_promise = true;
+ priv->failed_promise = true;
return;
}
}
promise->set_write(write);
//The pwrite cannot happen before the promise
if (write->happens_before(act) && (write != act)) {
- failed_promise = true;
+ priv->failed_promise = true;
return;
}
}
if (mo_graph->checkPromise(write, promise)) {
- failed_promise = true;
+ priv->failed_promise = true;
return;
}
}
if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) {
if (promise->increment_threads(tid)) {
- failed_promise = true;
+ priv->failed_promise = true;
return;
}
}
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
}
#endif
-void ModelChecker::print_summary()
+/** @brief Prints an execution trace summary. */
+void ModelChecker::print_summary() const
{
#if SUPPORT_MOD_ORDER_DUMP
scheduler->print();
#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");
}
/**
Thread *next = scheduler->next_thread(priv->nextThread);
/* Infeasible -> don't take any more steps */
- if (!isfeasible())
+ if (is_infeasible())
return false;
else if (isfeasibleprefix() && have_bug_reports()) {
set_assert();
*/
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,
return (Thread::swap(&system_context, next) == 0);
}
-/** Runs the current execution until threre are no more steps to take. */
-void ModelChecker::finish_execution() {
- DBG();
+/** Wrapper to run the user's main function, with appropriate arguments */
+void user_main_wrapper(void *)
+{
+ user_main(model->params.argc, model->params.argv);
+}
+
+/** @brief Run ModelChecker for the user program */
+void ModelChecker::run()
+{
+ do {
+ thrd_t user_thread;
+
+ /* Start user program */
+ add_thread(new Thread(&user_thread, &user_main_wrapper, NULL));
+
+ /* Wait for all threads to complete */
+ while (take_step());
+ } while (next_execution());
- while (take_step());
+ print_stats();
}
projects / c11tester.git / blobdiff