X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=24eb83dbbc6515cb4c24730e27ee94c4c949afbe;hb=0997f5bf1b28a79066ed4abfed57f14419ee44d3;hp=0bccd833ff843e40fd700f8ea3f198b1a2f4e065;hpb=8d9a43be3bc794d7c9096dbda88640eb2fa99ee6;p=model-checker.git diff --git a/model.cc b/model.cc index 0bccd83..24eb83d 100644 --- a/model.cc +++ b/model.cc @@ -282,6 +282,8 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) earliest_diverge = prevnode->get_action(); } } + /* Start the round robin scheduler from this thread id */ + scheduler->set_scheduler_thread(tid); /* The correct sleep set is in the parent node. */ execute_sleep_set(); @@ -313,14 +315,41 @@ void ModelChecker::execute_sleep_set() } } +/** + * @brief Should the current action wake up a given thread? + * + * @param curr The current action + * @param thread The thread that we might wake up + * @return True, if we should wake up the sleeping thread; false otherwise + */ +bool ModelChecker::should_wake_up(const ModelAction *curr, const Thread *thread) const +{ + const ModelAction *asleep = thread->get_pending(); + /* Don't allow partial RMW to wake anyone up */ + if (curr->is_rmwr()) + return false; + /* Synchronizing actions may have been backtracked */ + if (asleep->could_synchronize_with(curr)) + return true; + /* All acquire/release fences and fence-acquire/store-release */ + if (asleep->is_fence() && asleep->is_acquire() && curr->is_release()) + return true; + /* Fence-release + store can awake load-acquire on the same location */ + if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) { + ModelAction *fence_release = get_last_fence_release(curr->get_tid()); + if (fence_release && *(get_last_action(thread->get_id())) < *fence_release) + return true; + } + return false; +} + 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 + if (should_wake_up(curr, thr)) + /* Remove this thread from sleep set */ scheduler->remove_sleep(thr); } } @@ -545,25 +574,118 @@ bool ModelChecker::next_execution() return true; } -ModelAction * ModelChecker::get_last_conflict(ModelAction *act) +/** + * @brief Find the last fence-related backtracking conflict for a ModelAction + * + * This function performs the search for the most recent conflicting action + * against which we should perform backtracking, as affected by fence + * operations. This includes pairs of potentially-synchronizing actions which + * occur due to fence-acquire or fence-release, and hence should be explored in + * the opposite execution order. + * + * @param act The current action + * @return The most recent action which conflicts with act due to fences + */ +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; + + /* Skip past the release */ + action_list_t *list = action_trace; + action_list_t::reverse_iterator rit; + for (rit = list->rbegin(); rit != list->rend(); rit++) + if (*rit == last_release) + break; + ASSERT(rit != list->rend()); + + /* Find a prior: + * load-acquire + * or + * load --sb-> fence-acquire */ + 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; + for ( ; 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; +} + +/** + * @brief Find the last backtracking conflict for a ModelAction + * + * This function performs the search for the most recent conflicting action + * against which we should perform backtracking. This primary includes pairs of + * synchronizing actions which should be explored in the opposite execution + * order. + * + * @param act The current action + * @return The most recent action which conflicts with act + */ +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: { @@ -991,7 +1113,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr) case THREAD_CREATE: { thrd_t *thrd = (thrd_t *)curr->get_location(); struct thread_params *params = (struct thread_params *)curr->get_value(); - Thread *th = new Thread(thrd, params->func, params->arg); + Thread *th = new Thread(thrd, params->func, params->arg, get_thread(curr)); add_thread(th); th->set_creation(curr); /* Promises can be satisfied by children */ @@ -1273,7 +1395,7 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr) /* Build may_read_from set for newly-created actions */ if (newly_explored && curr->is_read()) - build_reads_from_past(curr); + build_may_read_from(curr); /* Initialize work_queue with the "current action" work */ work_queue_t work_queue(1, CheckCurrWorkEntry(curr)); @@ -1870,7 +1992,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()) @@ -1890,8 +2012,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 */ @@ -2450,12 +2570,12 @@ void ModelChecker::compute_relseq_breakwrites(ModelAction *curr) /** * Build up an initial set of all past writes that this 'read' action may read - * from. This set is determined by the clock vector's "happens before" - * relationship. + * from, as well as any previously-observed future values that must still be valid. + * * @param curr is the current ModelAction that we are exploring; it must be a * 'read' operation. */ -void ModelChecker::build_reads_from_past(ModelAction *curr) +void ModelChecker::build_may_read_from(ModelAction *curr) { std::vector *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location()); unsigned int i; @@ -2500,8 +2620,25 @@ void ModelChecker::build_reads_from_past(ModelAction *curr) break; } } + + /* Inherit existing, promised future values */ + for (i = 0; i < promises->size(); i++) { + const Promise *promise = (*promises)[i]; + const ModelAction *promise_read = promise->get_action(); + if (promise_read->same_var(curr)) { + /* Only add feasible future-values */ + mo_graph->startChanges(); + r_modification_order(curr, promise); + if (!is_infeasible()) { + const struct future_value fv = promise->get_fv(); + curr->get_node()->add_future_value(fv); + } + mo_graph->rollbackChanges(); + } + } + /* We may find no valid may-read-from only if the execution is doomed */ - if (!curr->get_node()->get_read_from_size()) { + if (!curr->get_node()->get_read_from_size() && curr->get_node()->future_value_empty()) { priv->no_valid_reads = true; set_assert(); } @@ -2517,7 +2654,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; @@ -2526,13 +2663,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; } /**