X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=7bff598f974e762daecc27d7d58926bdfa466d68;hb=67cae4edb16c1c432b26bedcc9e19dae6dc37b1b;hp=05e767981554a0c301169905a95ea5081d3cb8c0;hpb=19bf5b6e02169d18d1481876e50bfca7a29f4034;p=model-checker.git diff --git a/model.cc b/model.cc index 05e7679..7bff598 100644 --- a/model.cc +++ b/model.cc @@ -1,6 +1,7 @@ #include #include #include +#include #include "model.h" #include "action.h" @@ -13,6 +14,7 @@ #include "promise.h" #include "datarace.h" #include "threads-model.h" +#include "output.h" #define INITIAL_THREAD_ID 0 @@ -27,7 +29,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 +38,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 +66,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 */ @@ -62,18 +92,11 @@ ModelChecker::ModelChecker(struct model_params params) : 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)), + thrd_last_fence_release(new std::vector< ModelAction *, SnapshotAlloc >()), 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); @@ -99,14 +122,11 @@ ModelChecker::~ModelChecker() delete pending_rel_seqs; delete thrd_last_action; + delete thrd_last_fence_release; 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 +155,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); } @@ -155,7 +175,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(); } @@ -166,7 +186,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(); } @@ -266,8 +287,7 @@ void ModelChecker::execute_sleep_set() { for(unsigned int i=0;iget_enabled(thr) == THREAD_SLEEP_SET && - thr->get_pending() == NULL ) { + if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) { thr->set_state(THREAD_RUNNING); scheduler->next_thread(thr); Thread::swap(&system_context, thr); @@ -278,20 +298,36 @@ void ModelChecker::execute_sleep_set() { priv->current_action = NULL; } -void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) { - for(unsigned int i=0;iget_enabled(thr) == THREAD_SLEEP_SET ) { - ModelAction *pending_act=thr->get_pending(); - if ((!curr->is_rmwr())&&pending_act->could_synchronize_with(curr)) { +void ModelChecker::wake_up_sleeping_actions(ModelAction *curr) +{ + for (unsigned int i = 0; i < get_num_threads(); i++) { + Thread *thr = get_thread(int_to_id(i)); + if (scheduler->is_sleep_set(thr)) { + ModelAction *pending_act = thr->get_pending(); + if ((!curr->is_rmwr()) && pending_act->could_synchronize_with(curr)) //Remove this thread from sleep set scheduler->remove_sleep(thr); - } } } } +/** @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 +409,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++) @@ -390,22 +426,52 @@ void ModelChecker::print_bugs() const void ModelChecker::record_stats() { stats.num_total++; - if (!isfinalfeasible()) + 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 { - 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 +484,34 @@ void ModelChecker::print_stats() const 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()); - 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(); } @@ -458,9 +522,13 @@ bool ModelChecker::next_execution() ModelAction * ModelChecker::get_last_conflict(ModelAction *act) { switch (act->get_type()) { + case ATOMIC_FENCE: 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,13 +698,13 @@ 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; } - curr->read_from(reads_from); + read_from(curr, reads_from); mo_graph->commitChanges(); mo_check_promises(curr->get_tid(), reads_from); @@ -645,7 +713,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) /* Read from future value */ value = curr->get_node()->get_future_value(); modelclock_t expiration = curr->get_node()->get_future_value_expiration(); - curr->read_from(NULL); + curr->set_read_from(NULL); Promise *valuepromise = new Promise(curr, value, expiration); promises->push_back(valuepromise); } @@ -789,6 +857,56 @@ bool ModelChecker::process_write(ModelAction *curr) return updated_mod_order || updated_promises; } +/** + * Process a fence ModelAction + * @param curr The ModelAction to process + * @return True if synchronization was updated + */ +bool ModelChecker::process_fence(ModelAction *curr) +{ + /* + * fence-relaxed: no-op + * fence-release: only log the occurence (not in this function), for + * use in later synchronization + * fence-acquire (this function): search for hypothetical release + * sequences + */ + bool updated = false; + if (curr->is_acquire()) { + action_list_t *list = action_trace; + action_list_t::reverse_iterator rit; + /* Find X : is_read(X) && X --sb-> curr */ + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *act = *rit; + if (act == curr) + continue; + if (act->get_tid() != curr->get_tid()) + continue; + /* Stop at the beginning of the thread */ + if (act->is_thread_start()) + break; + /* Stop once we reach a prior fence-acquire */ + if (act->is_fence() && act->is_acquire()) + break; + if (!act->is_read()) + continue; + /* read-acquire will find its own release sequences */ + if (act->is_acquire()) + continue; + + /* Establish hypothetical release sequences */ + rel_heads_list_t release_heads; + get_release_seq_heads(curr, act, &release_heads); + for (unsigned int i = 0; i < release_heads.size(); i++) + if (!curr->synchronize_with(release_heads[i])) + set_bad_synchronization(); + if (release_heads.size() != 0) + updated = true; + } + } + return updated; +} + /** * @brief Process the current action for thread-related activity * @@ -935,7 +1053,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()) @@ -957,6 +1075,10 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr) /* Always compute new clock vector */ newcurr->create_cv(get_parent_action(newcurr->get_tid())); + + /* Assign most recent release fence */ + newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid())); + /* * Perform one-time actions when pushing new ModelAction onto * NodeStack @@ -974,6 +1096,34 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr) } } +/** + * @brief Establish reads-from relation between two actions + * + * Perform basic operations involved with establishing a concrete rf relation, + * including setting the ModelAction data and checking for release sequences. + * + * @param act The action that is reading (must be a read) + * @param rf The action from which we are reading (must be a write) + * + * @return True if this read established synchronization + */ +bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf) +{ + act->set_read_from(rf); + if (rf != NULL && act->is_acquire()) { + rel_heads_list_t release_heads; + get_release_seq_heads(act, act, &release_heads); + int num_heads = release_heads.size(); + for (unsigned int i = 0; i < release_heads.size(); i++) + if (!act->synchronize_with(release_heads[i])) { + set_bad_synchronization(); + num_heads--; + } + return num_heads > 0; + } + return false; +} + /** * @brief Check whether a model action is enabled. * @@ -1072,6 +1222,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) if (act->is_write() && process_write(act)) update = true; + if (act->is_fence() && process_fence(act)) + update_all = true; + if (act->is_mutex_op() && process_mutex(act)) update_all = true; @@ -1145,48 +1298,67 @@ bool ModelChecker::promises_expired() const return false; } -/** @return whether the current partial trace must be a prefix of a - * feasible trace. */ +/** + * 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 promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible(); + return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq(); } -/** @return whether the current partial trace is feasible. */ -bool ModelChecker::isfeasible() const +/** + * 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() 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(); -} - -/** Returns whether the current completed trace is feasible. */ -bool ModelChecker::isfinalfeasible() const -{ - 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. */ @@ -1218,7 +1390,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 +1433,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 +1458,7 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { } } if (feasiblewrite) { - too_many_reads = true; + priv->too_many_reads = true; return; } } @@ -1317,14 +1489,51 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf bool added = false; ASSERT(curr->is_read()); + /* Last SC fence in the current thread */ + ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL); + /* Iterate over all threads */ for (i = 0; i < thrd_lists->size(); i++) { + /* Last SC fence in thread i */ + ModelAction *last_sc_fence_thread_local = NULL; + if (int_to_id((int)i) != curr->get_tid()) + last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL); + + /* Last SC fence in thread i, before last SC fence in current thread */ + ModelAction *last_sc_fence_thread_before = NULL; + if (last_sc_fence_local) + last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local); + /* Iterate over actions in thread, starting from most recent */ action_list_t *list = &(*thrd_lists)[i]; action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *act = *rit; + if (act->is_write() && act != rf && act != curr) { + /* C++, Section 29.3 statement 5 */ + if (curr->is_seqcst() && last_sc_fence_thread_local && + *act < *last_sc_fence_thread_local) { + mo_graph->addEdge(act, rf); + added = true; + break; + } + /* C++, Section 29.3 statement 4 */ + else if (act->is_seqcst() && last_sc_fence_local && + *act < *last_sc_fence_local) { + mo_graph->addEdge(act, rf); + added = true; + break; + } + /* C++, Section 29.3 statement 6 */ + else if (last_sc_fence_thread_before && + *act < *last_sc_fence_thread_before) { + mo_graph->addEdge(act, rf); + added = true; + break; + } + } + /* * Include at most one act per-thread that "happens * before" curr. Don't consider reflexively. @@ -1450,15 +1659,23 @@ 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; } } + /* Last SC fence in the current thread */ + ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL); + /* Iterate over all threads */ for (i = 0; i < thrd_lists->size(); i++) { + /* Last SC fence in thread i, before last SC fence in current thread */ + ModelAction *last_sc_fence_thread_before = NULL; + if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid()) + last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local); + /* Iterate over actions in thread, starting from most recent */ action_list_t *list = &(*thrd_lists)[i]; action_list_t::reverse_iterator rit; @@ -1485,6 +1702,14 @@ bool ModelChecker::w_modification_order(ModelAction *curr) continue; } + /* C++, Section 29.3 statement 7 */ + if (last_sc_fence_thread_before && act->is_write() && + *act < *last_sc_fence_thread_before) { + mo_graph->addEdge(act, curr); + added = true; + break; + } + /* * Include at most one act per-thread that "happens * before" curr @@ -1521,8 +1746,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); } @@ -1628,6 +1853,8 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, if (rf->is_release()) release_heads->push_back(rf); + else if (rf->get_last_fence_release()) + release_heads->push_back(rf->get_last_fence_release()); if (!rf->is_rmw()) break; /* End of RMW chain */ @@ -1653,8 +1880,17 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, if (rf->is_release()) return true; /* complete */ - /* else relaxed write; check modification order for contiguous subsequence - * -> rf must be same thread as release */ + /* else relaxed write + * - check for fence-release in the same thread (29.8, stmt. 3) + * - check modification order for contiguous subsequence + * -> rf must be same thread as release */ + + const ModelAction *fence_release = rf->get_last_fence_release(); + /* Synchronize with a fence-release unconditionally; we don't need to + * find any more "contiguous subsequence..." for it */ + if (fence_release) + release_heads->push_back(fence_release); + int tid = id_to_int(rf->get_tid()); std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location()); action_list_t *list = &(*thrd_lists)[tid]; @@ -1664,14 +1900,21 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, rit = std::find(list->rbegin(), list->rend(), rf); ASSERT(rit != list->rend()); - /* Find the last write/release */ - for (; rit != list->rend(); rit++) + /* Find the last {write,fence}-release */ + for (; rit != list->rend(); rit++) { + if (fence_release && *(*rit) < *fence_release) + break; if ((*rit)->is_release()) break; + } if (rit == list->rend()) { /* No write-release in this thread */ return true; /* complete */ - } + } else if (fence_release && *(*rit) < *fence_release) { + /* The fence-release is more recent (and so, "stronger") than + * the most recent write-release */ + return true; /* complete */ + } /* else, need to establish contiguous release sequence */ ModelAction *release = *rit; ASSERT(rf->same_thread(release)); @@ -1744,22 +1987,29 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, } /** - * A public interface for getting the release sequence head(s) with which a + * An interface for getting the release sequence head(s) with which a * given ModelAction must synchronize. This function only returns a non-empty * result when it can locate a release sequence head with certainty. Otherwise, * it may mark the internal state of the ModelChecker so that it will handle - * the release sequence at a later time, causing @a act to update its + * the release sequence at a later time, causing @a acquire to update its * synchronization at some later point in execution. - * @param act The 'acquire' action that may read from a release sequence + * + * @param acquire The 'acquire' action that may synchronize with a release + * sequence + * @param read The read action that may read from a release sequence; this may + * be the same as acquire, or else an earlier action in the same thread (i.e., + * when 'acquire' is a fence-acquire) * @param release_heads A pass-by-reference return parameter. Will be filled * with the head(s) of the release sequence(s), if they exists with certainty. * @see ModelChecker::release_seq_heads */ -void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads) +void ModelChecker::get_release_seq_heads(ModelAction *acquire, + ModelAction *read, rel_heads_list_t *release_heads) { - const ModelAction *rf = act->get_reads_from(); + const ModelAction *rf = read->get_reads_from(); struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq)); - sequence->acquire = act; + sequence->acquire = acquire; + sequence->read = read; if (!release_seq_heads(rf, release_heads, sequence)) { /* add act to 'lazy checking' list */ @@ -1788,21 +2038,22 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ std::vector< struct release_seq *, SnapshotAlloc >::iterator it = pending_rel_seqs->begin(); while (it != pending_rel_seqs->end()) { struct release_seq *pending = *it; - ModelAction *act = pending->acquire; + ModelAction *acquire = pending->acquire; + const ModelAction *read = pending->read; /* Only resolve sequences on the given location, if provided */ - if (location && act->get_location() != location) { + if (location && read->get_location() != location) { it++; continue; } - const ModelAction *rf = act->get_reads_from(); + const ModelAction *rf = read->get_reads_from(); rel_heads_list_t release_heads; bool complete; complete = release_seq_heads(rf, &release_heads, pending); for (unsigned int i = 0; i < release_heads.size(); i++) { - if (!act->has_synchronized_with(release_heads[i])) { - if (act->synchronize_with(release_heads[i])) + if (!acquire->has_synchronized_with(release_heads[i])) { + if (acquire->synchronize_with(release_heads[i])) updated = true; else set_bad_synchronization(); @@ -1812,15 +2063,16 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ if (updated) { /* Re-check all pending release sequences */ work_queue->push_back(CheckRelSeqWorkEntry(NULL)); - /* Re-check act for mo_graph edges */ - work_queue->push_back(MOEdgeWorkEntry(act)); + /* Re-check read-acquire for mo_graph edges */ + if (acquire->is_read()) + work_queue->push_back(MOEdgeWorkEntry(acquire)); /* propagate synchronization to later actions */ action_list_t::reverse_iterator rit = action_trace->rbegin(); - for (; (*rit) != act; rit++) { + for (; (*rit) != acquire; rit++) { ModelAction *propagate = *rit; - if (act->happens_before(propagate)) { - propagate->synchronize_with(act); + if (acquire->happens_before(propagate)) { + propagate->synchronize_with(acquire); /* Re-check 'propagate' for mo_graph edges */ work_queue->push_back(MOEdgeWorkEntry(propagate)); } @@ -1850,18 +2102,38 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_ void ModelChecker::add_action_to_lists(ModelAction *act) { int tid = id_to_int(act->get_tid()); - action_trace->push_back(act); + ModelAction *uninit = NULL; + int uninit_id = -1; + action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + if (list->empty()) { + uninit = new_uninitialized_action(act->get_location()); + uninit_id = id_to_int(uninit->get_tid()); + list->push_back(uninit); + } + list->push_back(act); - get_safe_ptr_action(obj_map, act->get_location())->push_back(act); + action_trace->push_back(act); + if (uninit) + action_trace->push_front(uninit); 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); + if (uninit) + (*vec)[uninit_id].push_front(uninit); if ((int)thrd_last_action->size() <= tid) thrd_last_action->resize(get_num_threads()); (*thrd_last_action)[tid] = act; + if (uninit) + (*thrd_last_action)[uninit_id] = uninit; + + if (act->is_fence() && act->is_release()) { + if ((int)thrd_last_fence_release->size() <= tid) + thrd_last_fence_release->resize(get_num_threads()); + (*thrd_last_fence_release)[tid] = act; + } if (act->is_wait()) { void *mutex_loc=(void *) act->get_value(); @@ -1871,10 +2143,6 @@ void ModelChecker::add_action_to_lists(ModelAction *act) if (tid >= (int)vec->size()) vec->resize(priv->next_thread_id); (*vec)[tid].push_back(act); - - if ((int)thrd_last_action->size() <= tid) - thrd_last_action->resize(get_num_threads()); - (*thrd_last_action)[tid] = act; } } @@ -1892,6 +2160,20 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid) const return NULL; } +/** + * @brief Get the last fence release performed by a particular Thread + * @param tid The thread ID of the Thread in question + * @return The last fence release in the thread, if one exists; NULL otherwise + */ +ModelAction * ModelChecker::get_last_fence_release(thread_id_t tid) const +{ + int threadid = id_to_int(tid); + if (threadid < (int)thrd_last_fence_release->size()) + return (*thrd_last_fence_release)[id_to_int(tid)]; + else + return NULL; +} + /** * Gets the last memory_order_seq_cst write (in the total global sequence) * performed on a particular object (i.e., memory location), not including the @@ -1900,7 +2182,7 @@ 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 = get_safe_ptr_action(obj_map, location); @@ -1912,6 +2194,35 @@ ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const return NULL; } +/** + * Gets the last memory_order_seq_cst fence (in the total global sequence) + * performed in a particular thread, prior to a particular fence. + * @param tid The ID of the thread to check + * @param before_fence The fence from which to begin the search; if NULL, then + * search for the most recent fence in the thread. + * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL + */ +ModelAction * ModelChecker::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const +{ + /* All fences should have NULL location */ + action_list_t *list = get_safe_ptr_action(obj_map, NULL); + action_list_t::reverse_iterator rit = list->rbegin(); + + if (before_fence) { + for (; rit != list->rend(); rit++) + if (*rit == before_fence) + break; + + ASSERT(*rit == before_fence); + rit++; + } + + for (; rit != list->rend(); rit++) + if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst()) + return *rit; + return NULL; +} + /** * Gets the last unlock operation performed on a particular mutex (i.e., memory * location). This function identifies the mutex according to the current @@ -1932,7 +2243,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) @@ -1945,7 +2256,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(); } @@ -1968,7 +2279,7 @@ bool ModelChecker::resolve_promises(ModelAction *write) if (read->is_rmw()) { mo_graph->addRMWEdge(write, read); } - read->read_from(write); + read_from(read, write); //First fix up the modification order for actions that happened //before the read r_modification_order(read, write); @@ -2028,7 +2339,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 +2350,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 +2401,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 +2417,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; } } @@ -2149,18 +2460,10 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) unsigned int i; ASSERT(curr->is_read()); - ModelAction *last_seq_cst = NULL; - - /* Track whether this object has been initialized */ - bool initialized = false; + ModelAction *last_sc_write = NULL; - if (curr->is_seqcst()) { - last_seq_cst = get_last_seq_cst(curr); - /* We have to at least see the last sequentially consistent write, - so we are initialized. */ - if (last_seq_cst != NULL) - initialized = true; - } + if (curr->is_seqcst()) + last_sc_write = get_last_seq_cst_write(curr); /* Iterate over all threads */ for (i = 0; i < thrd_lists->size(); i++) { @@ -2175,39 +2478,42 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) continue; /* Don't consider more than one seq_cst write if we are a seq_cst read. */ - if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) { - if (!curr->get_sleep_flag() || curr->is_seqcst() || sleep_can_read_from(curr, act)) { - DEBUG("Adding action to may_read_from:\n"); - if (DBG_ENABLED()) { - act->print(); - curr->print(); - } - curr->get_node()->add_read_from(act); + bool allow_read = true; + + if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write) + allow_read = false; + else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act)) + allow_read = false; + + if (allow_read) { + DEBUG("Adding action to may_read_from:\n"); + if (DBG_ENABLED()) { + act->print(); + curr->print(); } + curr->get_node()->add_read_from(act); } /* Include at most one act per-thread that "happens before" curr */ - if (act->happens_before(curr)) { - initialized = true; + if (act->happens_before(curr)) break; - } } } - if (!initialized) - assert_bug("May read from uninitialized atomic"); - - if (DBG_ENABLED() || !initialized) { - printf("Reached read action:\n"); + if (DBG_ENABLED()) { + 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"); } } bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) { - while(true) { + while (true) { + /* UNINIT actions don't have a Node, and they never sleep */ + if (write->is_uninitialized()) + return true; Node *prevnode=write->get_node()->get_parent(); bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET; @@ -2222,20 +2528,35 @@ bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *wr } } -static void print_list(action_list_t *list) +/** + * @brief Create a new action representing an uninitialized atomic + * @param location The memory location of the atomic object + * @return A pointer to a new ModelAction + */ +ModelAction * ModelChecker::new_uninitialized_action(void *location) const +{ + ModelAction *act = (ModelAction *)snapshot_malloc(sizeof(class ModelAction)); + act = new (act) ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, location, 0, model_thread); + act->create_cv(NULL); + return act; +} + +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 +2587,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(); @@ -2277,10 +2599,10 @@ void ModelChecker::print_summary() 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"); } /** @@ -2388,7 +2710,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(); @@ -2414,8 +2736,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, @@ -2442,9 +2764,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(); }