X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=fab1a5994feb96e6ee22c59e941b7fc9550ff041;hp=70732868bd3114825f3ccc8c2db51bb57e339a92;hb=5fa2efec1354b2781ff0b29460ec8e9b8fa75991;hpb=b3786419ac8bbc47f33038b1d6c595a70490e634 diff --git a/model.cc b/model.cc index 70732868..fab1a599 100644 --- a/model.cc +++ b/model.cc @@ -211,11 +211,14 @@ Node * ModelChecker::get_curr_node() const * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be * followed by a THREAD_START, or it can enforce execution replay/backtracking. * The model-checker may have no preference regarding the next thread (i.e., - * when exploring a new execution ordering), in which case this will return - * NULL. - * @param curr The current ModelAction. This action might guide the choice of - * next thread. - * @return The next thread to run. If the model-checker has no preference, NULL. + * when exploring a new execution ordering), in which case we defer to the + * scheduler. + * + * @param curr Optional: The current ModelAction. Only used if non-NULL and it + * might guide the choice of next thread (i.e., THREAD_CREATE should be + * followed by THREAD_START, or ATOMIC_RMWR followed by ATOMIC_{RMW,RMWC}) + * @return The next chosen thread to run, if any exist. Or else if no threads + * remain to be executed, return NULL. */ Thread * ModelChecker::get_next_thread(ModelAction *curr) { @@ -229,9 +232,12 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) return curr->get_thread_operand(); } - /* Have we completed exploring the preselected path? */ + /* + * Have we completed exploring the preselected path? Then let the + * scheduler decide + */ if (diverge == NULL) - return NULL; + return scheduler->select_next_thread(); /* Else, we are trying to replay an execution */ ModelAction *next = node_stack->get_next()->get_action(); @@ -539,25 +545,89 @@ bool ModelChecker::next_execution() return true; } -ModelAction * ModelChecker::get_last_conflict(ModelAction *act) +ModelAction * ModelChecker::get_last_fence_conflict(ModelAction *act) const +{ + /* Only perform release/acquire fence backtracking for stores */ + if (!act->is_write()) + return NULL; + + /* Find a fence-release (or, act is a release) */ + ModelAction *last_release; + if (act->is_release()) + last_release = act; + else + last_release = get_last_fence_release(act->get_tid()); + if (!last_release) + return NULL; + + std::vector< ModelAction *, ModelAlloc > acquire_fences(get_num_threads(), NULL); + std::vector< ModelAction *, ModelAlloc > prior_loads(get_num_threads(), NULL); + bool found_acquire_fences = false; + /* Find a prior: + * load-acquire + * or + * load --sb-> fence-acquire */ + action_list_t *list = action_trace; + action_list_t::reverse_iterator rit; + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *prev = *rit; + if (act->same_thread(prev)) + continue; + + int tid = id_to_int(prev->get_tid()); + + if (prev->is_read() && act->same_var(prev)) { + if (prev->is_acquire()) { + /* Found most recent load-acquire, don't need + * to search for more fences */ + if (!found_acquire_fences) + return NULL; + } else { + prior_loads[tid] = prev; + } + } + if (prev->is_acquire() && prev->is_fence() && !acquire_fences[tid]) { + found_acquire_fences = true; + acquire_fences[tid] = prev; + } + } + + ModelAction *latest_backtrack = NULL; + for (unsigned int i = 0; i < acquire_fences.size(); i++) + if (acquire_fences[i] && prior_loads[i]) + if (!latest_backtrack || *latest_backtrack < *acquire_fences[i]) + latest_backtrack = acquire_fences[i]; + return latest_backtrack; +} + +ModelAction * ModelChecker::get_last_conflict(ModelAction *act) const { switch (act->get_type()) { - case ATOMIC_FENCE: + /* case ATOMIC_FENCE: fences don't directly cause backtracking */ case ATOMIC_READ: case ATOMIC_WRITE: case ATOMIC_RMW: { - /* Optimization: relaxed operations don't need backtracking */ - if (act->is_relaxed()) - return NULL; + ModelAction *ret = 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; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; - if (prev->could_synchronize_with(act)) - return prev; + if (prev->could_synchronize_with(act)) { + ret = prev; + break; + } } - break; + + ModelAction *ret2 = get_last_fence_conflict(act); + if (!ret2) + return ret; + if (!ret) + return ret2; + if (*ret < *ret2) + return ret2; + return ret; } case ATOMIC_LOCK: case ATOMIC_TRYLOCK: { @@ -1864,7 +1934,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, if (mo_graph->checkForCycles()) return false; - while (rf) { + for ( ; rf != NULL; rf = rf->get_reads_from()) { ASSERT(rf->is_write()); if (rf->is_release()) @@ -1884,8 +1954,6 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf, /* acq_rel RMW is a sufficient stopping condition */ if (rf->is_acquire() && rf->is_release()) return true; /* complete */ - - rf = rf->get_reads_from(); }; if (!rf) { /* read from future: need to settle this later */ @@ -2511,7 +2579,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *write) { - while (true) { + for ( ; write != NULL; write = write->get_reads_from()) { /* UNINIT actions don't have a Node, and they never sleep */ if (write->is_uninitialized()) return true; @@ -2520,13 +2588,10 @@ bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *wri bool thread_sleep = prevnode->enabled_status(curr->get_tid()) == THREAD_SLEEP_SET; if (write->is_release() && thread_sleep) return true; - if (!write->is_rmw()) { + if (!write->is_rmw()) return false; - } - if (write->get_reads_from() == NULL) - return true; - write = write->get_reads_from(); } + return true; } /** @@ -2732,10 +2797,6 @@ Thread * ModelChecker::take_step(ModelAction *curr) scheduler->remove_thread(curr_thrd); Thread *next_thrd = get_next_thread(curr); - /* Only ask for the next thread from Scheduler if we haven't chosen one - * already */ - if (!next_thrd) - next_thrd = scheduler->select_next_thread(); DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1, next_thrd ? id_to_int(next_thrd->get_id()) : -1); @@ -2805,5 +2866,6 @@ void ModelChecker::run() }; } while (next_execution()); + model_print("******* Model-checking complete: *******\n"); print_stats(); }