X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=df06760893018d5bc1756cd89df263c6ed117cc6;hb=f71df291f0158236d46fc39e9c5ca02e3329f628;hp=33fc4c3c38c3b5affc65bf360a833f5de8f8175e;hpb=86ca0bf04682b0011466ab49abda78acbf024c54;p=model-checker.git diff --git a/model.cc b/model.cc index 33fc4c3..df06760 100644 --- a/model.cc +++ b/model.cc @@ -13,11 +13,26 @@ #include "promise.h" #include "datarace.h" #include "threads-model.h" +#include "output.h" #define INITIAL_THREAD_ID 0 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() { model_print("%s", msg); } + + SNAPSHOTALLOC +}; + /** * Structure for holding small ModelChecker members that should be snapshotted */ @@ -27,6 +42,8 @@ struct model_snapshot_members { modelclock_t used_sequence_numbers; Thread *nextThread; ModelAction *next_backtrack; + std::vector< bug_message *, SnapshotAlloc > bugs; + struct execution_stats stats; }; /** @brief Constructor */ @@ -34,8 +51,6 @@ ModelChecker::ModelChecker(struct model_params params) : /* 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()), @@ -56,7 +71,7 @@ ModelChecker::ModelChecker(struct model_params params) : bad_synchronization(false) { /* Allocate this "size" on the snapshotting heap */ - priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv)); + 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; @@ -88,6 +103,11 @@ ModelChecker::~ModelChecker() 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); } static action_list_t * get_safe_ptr_action(HashTable * hash, void * ptr) { @@ -120,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); } @@ -310,45 +334,153 @@ bool ModelChecker::is_complete_execution() const } /** - * Queries the model-checker for more executions to explore and, if one - * exists, resets the model-checker state to execute a new execution. + * @brief Assert a bug in the executing program. * - * @return If there are more executions to explore, return true. Otherwise, - * return false. + * 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::next_execution() +bool ModelChecker::assert_bug(const char *msg) { - DBG(); + 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()) { + 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++; + else + stats.num_redundant++; +} - num_executions++; +/** @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); + 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 (is_deadlocked()) - printf("ERROR: DEADLOCK\n"); - if (isfinalfeasible()) { - printf("Earliest divergence point since last feasible execution:\n"); + if (DBG_ENABLED() || params.verbose) { + 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++; + model_print("\n"); + print_stats(); } - DEBUG("Number of acquires waiting on pending release sequences: %zu\n", - pending_rel_seqs->size()); + /* 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"); - if (isfinalfeasible() || DBG_ENABLED()) { checkDataRaces(); - 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(); } @@ -595,10 +727,8 @@ bool ModelChecker::process_mutex(ModelAction *curr) { } //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 @@ -807,8 +937,7 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu } /* See if we have realized a data race */ - if (checkDataRaces()) - set_assert(); + checkDataRaces(); } /** @@ -957,7 +1086,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) /* 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(); @@ -1038,7 +1167,8 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) { } } -bool ModelChecker::promises_expired() { +bool ModelChecker::promises_expired() const +{ for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) { Promise *promise = (*promises)[promise_index]; if (promise->get_expiration()used_sequence_numbers) { @@ -1050,12 +1180,14 @@ bool ModelChecker::promises_expired() { /** @return whether the current partial trace must be a prefix of a * feasible trace. */ -bool ModelChecker::isfeasibleprefix() { +bool ModelChecker::isfeasibleprefix() const +{ return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible(); } /** @return whether the current partial trace is feasible. */ -bool ModelChecker::isfeasible() { +bool ModelChecker::isfeasible() const +{ if (DBG_ENABLED() && mo_graph->checkForRMWViolation()) DEBUG("Infeasible: RMW violation\n"); @@ -1064,7 +1196,8 @@ bool ModelChecker::isfeasible() { /** @return whether the current partial trace is feasible other than * multiple RMW reading from the same store. */ -bool ModelChecker::isfeasibleotherthanRMW() { +bool ModelChecker::isfeasibleotherthanRMW() const +{ if (DBG_ENABLED()) { if (mo_graph->checkForCycles()) DEBUG("Infeasible: modification order cycles\n"); @@ -1081,7 +1214,8 @@ bool ModelChecker::isfeasibleotherthanRMW() { } /** Returns whether the current completed trace is feasible. */ -bool ModelChecker::isfinalfeasible() { +bool ModelChecker::isfinalfeasible() const +{ if (DBG_ENABLED() && promises->size() != 0) DEBUG("Infeasible: unrevolved promises\n"); @@ -1734,9 +1868,7 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ } // If we resolved promises or data races, see if we have realized a data race. - if (checkDataRaces()) { - set_assert(); - } + checkDataRaces(); return updated; } @@ -2095,18 +2227,15 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) } } - 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"); + 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"); } } @@ -2126,20 +2255,22 @@ 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; - 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 @@ -2170,26 +2301,22 @@ void ModelChecker::dumpGraph(char *filename) { } #endif -void ModelChecker::print_summary() +/** @brief Prints an execution trace summary. */ +void ModelChecker::print_summary() const { - 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"); } /** @@ -2299,6 +2426,10 @@ bool ModelChecker::take_step() { /* 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) { @@ -2320,7 +2451,7 @@ bool ModelChecker::take_step() { */ 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,