X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=d615e1ada44c7fa0af87478c14e04065ddf6387b;hp=ff1fdf932ee302fb6cc36c9199cd54c15f3bb50d;hb=004ffe355e33b1b5e88095a0873fa5119993c7bc;hpb=f6d2ca10d64791d283db4786e7333770c003eb56 diff --git a/model.cc b/model.cc index ff1fdf93..d615e1ad 100644 --- a/model.cc +++ b/model.cc @@ -13,42 +13,88 @@ #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 + */ +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; + Thread *nextThread; + 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 */ 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()), thread_map(new HashTable()), - obj_map(new HashTable()), - lock_waiters_map(new HashTable()), - condvar_waiters_map(new HashTable()), - obj_thrd_map(new HashTable, uintptr_t, 4 >()), + obj_map(new HashTable()), + lock_waiters_map(new HashTable()), + condvar_waiters_map(new HashTable()), + obj_thrd_map(new HashTable *, uintptr_t, 4 >()), promises(new std::vector< Promise *, SnapshotAlloc >()), futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc >()), 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 *)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); @@ -77,6 +123,25 @@ ModelChecker::~ModelChecker() delete node_stack; delete scheduler; delete mo_graph; + delete priv; +} + +static action_list_t * get_safe_ptr_action(HashTable * hash, void * ptr) { + action_list_t * tmp=hash->get(ptr); + if (tmp==NULL) { + tmp=new action_list_t(); + hash->put(ptr, tmp); + } + return tmp; +} + +static std::vector * get_safe_ptr_vect_action(HashTable *, uintptr_t, 4> * hash, void * ptr) { + std::vector * tmp=hash->get(ptr); + if (tmp==NULL) { + tmp=new std::vector(); + hash->put(ptr, tmp); + } + return tmp; } /** @@ -87,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); } @@ -107,7 +172,7 @@ unsigned int ModelChecker::get_num_threads() const } /** @return The currently executing Thread. */ -Thread * ModelChecker::get_current_thread() +Thread * ModelChecker::get_current_thread() const { return scheduler->get_current_thread(); } @@ -118,7 +183,8 @@ modelclock_t ModelChecker::get_next_seq_num() return ++priv->used_sequence_numbers; } -Node * ModelChecker::get_curr_node() { +Node * ModelChecker::get_curr_node() const +{ return node_stack->get_head(); } @@ -244,44 +310,207 @@ 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; +} + /** - * Queries the model-checker for more executions to explore and, if one - * exists, resets the model-checker state to execute a new execution. + * 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 + * execution (there should be some ENABLED thread). * - * @return If there are more executions to explore, return true. Otherwise, - * return false. + * @return True if program is in a deadlock; false otherwise */ -bool ModelChecker::next_execution() +bool ModelChecker::is_deadlocked() const { - DBG(); + bool blocking_threads = false; + for (unsigned int i = 0; i < get_num_threads(); i++) { + thread_id_t tid = int_to_id(i); + if (is_enabled(tid)) + return false; + Thread *t = get_thread(tid); + if (!t->is_model_thread() && t->get_pending()) + blocking_threads = true; + } + return blocking_threads; +} + +/** + * Check if this is a complete execution. That is, have all thread completed + * execution (rather than exiting because sleep sets have forced a redundant + * execution). + * + * @return True if the execution is complete. + */ +bool ModelChecker::is_complete_execution() const +{ + for (unsigned int i = 0; i < get_num_threads(); i++) + if (is_enabled(int_to_id(i))) + return false; + 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; +} - num_executions++; +/** + * @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 (!isfeasibleprefix()) + stats.num_infeasible++; + else if (have_bug_reports()) + 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 +{ + 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()); +} - if (isfinalfeasible()) { - printf("Earliest divergence point since last feasible execution:\n"); +/** + * @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 - 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 = isfeasibleprefix() && (is_complete_execution() || + have_bug_reports()); + /* End-of-execution bug checks */ + if (complete) { + if (is_deadlocked()) + assert_bug("Deadlock detected"); - if (isfinalfeasible() || (params.bound != 0 && priv->used_sequence_numbers > params.bound ) || 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(); } @@ -295,8 +524,11 @@ 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 = obj_map->get_safe_ptr(act->get_location()); + action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -308,7 +540,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) case ATOMIC_LOCK: case ATOMIC_TRYLOCK: { /* linear search: from most recent to oldest */ - action_list_t *list = obj_map->get_safe_ptr(act->get_location()); + action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -319,7 +551,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) } case ATOMIC_UNLOCK: { /* linear search: from most recent to oldest */ - action_list_t *list = obj_map->get_safe_ptr(act->get_location()); + action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -330,7 +562,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) } case ATOMIC_WAIT: { /* linear search: from most recent to oldest */ - action_list_t *list = obj_map->get_safe_ptr(act->get_location()); + action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -345,7 +577,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) case ATOMIC_NOTIFY_ALL: case ATOMIC_NOTIFY_ONE: { /* linear search: from most recent to oldest */ - action_list_t *list = obj_map->get_safe_ptr(act->get_location()); + action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -464,9 +696,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; } @@ -528,10 +760,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 @@ -545,7 +775,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) { //unlock the lock state->islocked = false; //wake up the other threads - action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location()); + action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location()); //activate all the waiting threads for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) { scheduler->wake(get_thread(*rit)); @@ -557,7 +787,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) { //unlock the lock state->islocked = false; //wake up the other threads - action_list_t *waiters = lock_waiters_map->get_safe_ptr((void *) curr->get_value()); + action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value()); //activate all the waiting threads for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) { scheduler->wake(get_thread(*rit)); @@ -565,14 +795,14 @@ bool ModelChecker::process_mutex(ModelAction *curr) { waiters->clear(); //check whether we should go to sleep or not...simulate spurious failures if (curr->get_node()->get_misc()==0) { - condvar_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr); + get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr); //disable us scheduler->sleep(get_current_thread()); } break; } case ATOMIC_NOTIFY_ALL: { - action_list_t *waiters = condvar_waiters_map->get_safe_ptr(curr->get_location()); + action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location()); //activate all the waiting threads for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) { scheduler->wake(get_thread(*rit)); @@ -581,7 +811,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) { break; } case ATOMIC_NOTIFY_ONE: { - action_list_t *waiters = condvar_waiters_map->get_safe_ptr(curr->get_location()); + action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location()); int wakeupthread=curr->get_node()->get_misc(); action_list_t::iterator it = waiters->begin(); advance(it, wakeupthread); @@ -740,8 +970,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(); } /** @@ -772,7 +1001,7 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr) (*curr)->set_seq_number(get_next_seq_num()); - newcurr = node_stack->explore_action(*curr, scheduler->get_enabled()); + newcurr = node_stack->explore_action(*curr, scheduler->get_enabled_array()); if (newcurr) { /* First restore type and order in case of RMW operation */ if ((*curr)->is_rmwr()) @@ -805,7 +1034,7 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr) else if (newcurr->is_wait()) newcurr->get_node()->set_misc_max(2); else if (newcurr->is_notify_one()) { - newcurr->get_node()->set_misc_max(condvar_waiters_map->get_safe_ptr(newcurr->get_location())->size()); + newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size()); } return true; /* This was a new ModelAction */ } @@ -827,7 +1056,7 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) { struct std::mutex_state * state = lock->get_state(); if (state->islocked) { //Stick the action in the appropriate waiting queue - lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr); + get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr); return false; } } else if (curr->get_type() == THREAD_JOIN) { @@ -841,6 +1070,16 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) { return true; } +/** + * Stores the ModelAction for the current thread action. Call this + * immediately before switching from user- to system-context to pass + * data between them. + * @param act The ModelAction created by the user-thread action + */ +void ModelChecker::set_current_action(ModelAction *act) { + priv->current_action = act; +} + /** * This is the heart of the model checker routine. It performs model-checking * actions corresponding to a given "current action." Among other processes, it @@ -880,7 +1119,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(); @@ -961,7 +1200,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) { @@ -971,44 +1211,67 @@ bool ModelChecker::promises_expired() { return false; } -/** @return whether the current partial trace must be a prefix of a - * feasible trace. */ -bool ModelChecker::isfeasibleprefix() { - return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible(); +/** + * This is the strongest feasibility check available. + * @return whether the current trace (partial or complete) must be a prefix of + * a feasible trace. + */ +bool ModelChecker::isfeasibleprefix() const +{ + return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq(); } -/** @return whether the current partial trace is feasible. */ -bool ModelChecker::isfeasible() { +/** + * Returns whether the current completed trace is feasible, except for pending + * release sequences. + */ +bool ModelChecker::is_feasible_prefix_ignore_relseq() const +{ + if (DBG_ENABLED() && promises->size() != 0) + DEBUG("Infeasible: unrevolved promises\n"); + + return !is_infeasible() && promises->size() == 0; +} + +/** + * 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() { +/** + * 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(); -} - -/** Returns whether the current completed trace is feasible. */ -bool ModelChecker::isfinalfeasible() { - if (DBG_ENABLED() && promises->size() != 0) - DEBUG("Infeasible: unrevolved promises\n"); - - return isfeasible() && promises->size() == 0; + return mo_graph->checkForCycles() || priv->failed_promise || + priv->too_many_reads || priv->bad_synchronization || + promises_expired(); } /** Close out a RMWR by converting previous RMWR into a RMW or READ. */ @@ -1040,9 +1303,9 @@ 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 = obj_thrd_map->get_safe_ptr(curr->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); int tid = id_to_int(curr->get_tid()); /* Skip checks */ @@ -1083,7 +1346,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) @@ -1108,7 +1371,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { } } if (feasiblewrite) { - too_many_reads = true; + priv->too_many_reads = true; return; } } @@ -1134,7 +1397,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { */ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf) { - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; bool added = false; ASSERT(curr->is_read()); @@ -1193,7 +1456,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf */ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf) { - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; ASSERT(curr->is_read()); @@ -1264,7 +1527,7 @@ void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelActio */ bool ModelChecker::w_modification_order(ModelAction *curr) { - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; bool added = false; ASSERT(curr->is_write()); @@ -1272,7 +1535,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr) if (curr->is_seqcst()) { /* We have to at least see the last sequentially consistent write, so we are initialized. */ - ModelAction *last_seq_cst = get_last_seq_cst(curr); + ModelAction *last_seq_cst = get_last_seq_cst_write(curr); if (last_seq_cst != NULL) { mo_graph->addEdge(last_seq_cst, curr); added = true; @@ -1343,8 +1606,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); } @@ -1386,7 +1649,7 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, con */ bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader) { - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location()); unsigned int i; /* Iterate over all threads */ for (i = 0; i < thrd_lists->size(); i++) { @@ -1478,7 +1741,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, /* else relaxed write; check modification order for contiguous subsequence * -> rf must be same thread as release */ int tid = id_to_int(rf->get_tid()); - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(rf->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location()); action_list_t *list = &(*thrd_lists)[tid]; action_list_t::const_reverse_iterator rit; @@ -1513,7 +1776,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, ModelAction *last = get_last_action(int_to_id(i)); Thread *th = get_thread(int_to_id(i)); if ((last && rf->happens_before(last)) || - !scheduler->is_enabled(th) || + !is_enabled(th) || th->is_complete()) future_ordered = true; @@ -1657,9 +1920,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; } @@ -1676,9 +1937,9 @@ void ModelChecker::add_action_to_lists(ModelAction *act) int tid = id_to_int(act->get_tid()); action_trace->push_back(act); - obj_map->get_safe_ptr(act->get_location())->push_back(act); + get_safe_ptr_action(obj_map, act->get_location())->push_back(act); - std::vector *vec = obj_thrd_map->get_safe_ptr(act->get_location()); + std::vector *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location()); if (tid >= (int)vec->size()) vec->resize(priv->next_thread_id); (*vec)[tid].push_back(act); @@ -1689,9 +1950,9 @@ void ModelChecker::add_action_to_lists(ModelAction *act) if (act->is_wait()) { void *mutex_loc=(void *) act->get_value(); - obj_map->get_safe_ptr(mutex_loc)->push_back(act); + get_safe_ptr_action(obj_map, mutex_loc)->push_back(act); - std::vector *vec = obj_thrd_map->get_safe_ptr(mutex_loc); + std::vector *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc); if (tid >= (int)vec->size()) vec->resize(priv->next_thread_id); (*vec)[tid].push_back(act); @@ -1724,10 +1985,10 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid) const * check * @return The last seq_cst write */ -ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const +ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const { void *location = curr->get_location(); - action_list_t *list = obj_map->get_safe_ptr(location); + action_list_t *list = get_safe_ptr_action(obj_map, location); /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */ action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) @@ -1747,7 +2008,7 @@ ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const { void *location = curr->get_location(); - action_list_t *list = obj_map->get_safe_ptr(location); + action_list_t *list = get_safe_ptr_action(obj_map, location); /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */ action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) @@ -1756,7 +2017,7 @@ ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const return NULL; } -ModelAction * ModelChecker::get_parent_action(thread_id_t tid) +ModelAction * ModelChecker::get_parent_action(thread_id_t tid) const { ModelAction *parent = get_last_action(tid); if (!parent) @@ -1769,7 +2030,7 @@ ModelAction * ModelChecker::get_parent_action(thread_id_t tid) * @param tid The thread whose clock vector we want * @return Desired clock vector */ -ClockVector * ModelChecker::get_cv(thread_id_t tid) +ClockVector * ModelChecker::get_cv(thread_id_t tid) const { return get_parent_action(tid)->get_cv(); } @@ -1852,7 +2113,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; } } @@ -1863,7 +2124,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; } } @@ -1914,12 +2175,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; } } @@ -1930,7 +2191,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; } } @@ -1969,7 +2230,7 @@ void ModelChecker::compute_relseq_breakwrites(ModelAction *curr) */ void ModelChecker::build_reads_from_past(ModelAction *curr) { - std::vector *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location()); + std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; ASSERT(curr->is_read()); @@ -1979,7 +2240,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) bool initialized = false; if (curr->is_seqcst()) { - last_seq_cst = get_last_seq_cst(curr); + last_seq_cst = get_last_seq_cst_write(curr); /* We have to at least see the last sequentially consistent write, so we are initialized. */ if (last_seq_cst != NULL) @@ -2018,18 +2279,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"); } } @@ -2049,20 +2307,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 @@ -2093,26 +2353,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"); + if (!isfeasibleprefix()) + model_print("INFEASIBLE EXECUTION!\n"); + print_list(action_trace, stats.num_total); + model_print("\n"); } /** @@ -2155,6 +2411,26 @@ Thread * ModelChecker::get_thread(ModelAction *act) const return get_thread(act->get_tid()); } +/** + * @brief Check if a Thread is currently enabled + * @param t The Thread to check + * @return True if the Thread is currently enabled + */ +bool ModelChecker::is_enabled(Thread *t) const +{ + return scheduler->is_enabled(t); +} + +/** + * @brief Check if a Thread is currently enabled + * @param tid The ID of the Thread to check + * @return True if the Thread is currently enabled + */ +bool ModelChecker::is_enabled(thread_id_t tid) const +{ + return scheduler->is_enabled(tid); +} + /** * Switch from a user-context to the "master thread" context (a.k.a. system * context). This switch is made with the intention of exploring a particular @@ -2200,8 +2476,12 @@ 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(); + return false; + } if (params.bound != 0) { if (priv->used_sequence_numbers > params.bound) { @@ -2222,8 +2502,8 @@ bool ModelChecker::take_step() { * (4) no pending promises */ if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) && - isfinalfeasible() && !unrealizedraces.empty()) { - printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n", + is_feasible_prefix_ignore_relseq() && !unrealizedraces.empty()) { + 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, @@ -2250,9 +2530,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(); }