X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=0e650a3c5b3c530d1fc398c4a07964e59b65dd64;hp=05e767981554a0c301169905a95ea5081d3cb8c0;hb=71a4f2447c7f0a20120da4e751d78cdeb4495ddd;hpb=19bf5b6e02169d18d1481876e50bfca7a29f4034 diff --git a/model.cc b/model.cc index 05e76798..0e650a3c 100644 --- 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 @@ -27,7 +28,7 @@ struct bug_message { ~bug_message() { if (msg) snapshot_free(msg); } char *msg; - void print() { printf("%s", msg); } + void print() { model_print("%s", msg); } SNAPSHOTALLOC }; @@ -36,6 +37,27 @@ struct bug_message { * 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; @@ -43,6 +65,13 @@ struct model_snapshot_members { ModelAction *next_backtrack; std::vector< bug_message *, SnapshotAlloc > 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 */ @@ -63,17 +92,9 @@ ModelChecker::ModelChecker(struct model_params params) : pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc >()), thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc >(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); @@ -102,11 +123,7 @@ 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); + delete priv; } static action_list_t * get_safe_ptr_action(HashTable * hash, void * ptr) { @@ -135,10 +152,10 @@ void ModelChecker::reset_to_initial_state() { 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); } @@ -292,6 +309,23 @@ void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) { } } +/** @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 @@ -373,7 +407,7 @@ bool ModelChecker::have_bug_reports() const void ModelChecker::print_bugs() const { if (have_bug_reports()) { - printf("Bug report: %zu bug%s detected\n", + 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++) @@ -396,16 +430,46 @@ 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 { - 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(); } /** @@ -418,36 +482,34 @@ void ModelChecker::print_stats() const 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"); checkDataRaces(); - print_bugs(); - 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(); } @@ -461,6 +523,9 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) 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; @@ -630,9 +695,9 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) } - 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; } @@ -1149,35 +1214,48 @@ bool ModelChecker::promises_expired() const * 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. */ @@ -1186,7 +1264,7 @@ bool ModelChecker::isfinalfeasible() const 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. */ @@ -1218,7 +1296,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { return; //Must make sure that execution is currently feasible... We could //accidentally clear by rolling back - if (!isfeasible()) + if (is_infeasible()) return; std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); int tid = id_to_int(curr->get_tid()); @@ -1261,7 +1339,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { /* 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) @@ -1286,7 +1364,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { } } if (feasiblewrite) { - too_many_reads = true; + priv->too_many_reads = true; return; } } @@ -1521,8 +1599,8 @@ bool ModelChecker::w_modification_order(ModelAction *curr) */ 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); } @@ -2028,7 +2106,7 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec merge_cv->synchronized_since(act)) { if (promise->increment_threads(tid)) { //Promise has failed - failed_promise = true; + priv->failed_promise = true; return; } } @@ -2039,7 +2117,7 @@ void ModelChecker::check_promises_thread_disabled() { 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; } } @@ -2090,12 +2168,12 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) 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; } } @@ -2106,7 +2184,7 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) { if (promise->increment_threads(tid)) { - failed_promise = true; + priv->failed_promise = true; return; } } @@ -2198,11 +2276,11 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) 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"); } } @@ -2222,20 +2300,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 @@ -2266,7 +2346,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(); @@ -2278,9 +2359,9 @@ void ModelChecker::print_summary() #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"); } /** @@ -2388,7 +2469,7 @@ bool ModelChecker::take_step() { 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(); @@ -2415,7 +2496,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, @@ -2442,9 +2523,24 @@ bool ModelChecker::take_step() { 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(); }