X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=execution.cc;h=3a630d777f060cb22598858278044d6e140cfed3;hp=3c6d0d7588dc2ff33984a94577b34de37bfdac2f;hb=6014243b7130f34b7ffd1098da225b0b8de5c328;hpb=dd34ddf490dd97c2c202092c8fa44064a07f8c4f diff --git a/execution.cc b/execution.cc index 3c6d0d7..3a630d7 100644 --- a/execution.cc +++ b/execution.cc @@ -30,6 +30,7 @@ struct model_snapshot_members { next_backtrack(NULL), bugs(), failed_promise(false), + hard_failed_promise(false), too_many_reads(false), no_valid_reads(false), bad_synchronization(false), @@ -47,6 +48,7 @@ struct model_snapshot_members { ModelAction *next_backtrack; SnapVector bugs; bool failed_promise; + bool hard_failed_promise; bool too_many_reads; bool no_valid_reads; /** @brief Incorrectly-ordered synchronization was made */ @@ -58,7 +60,7 @@ struct model_snapshot_members { /** @brief Constructor */ ModelExecution::ModelExecution(ModelChecker *m, - struct model_params *params, + const struct model_params *params, Scheduler *scheduler, NodeStack *node_stack) : model(m), @@ -66,7 +68,7 @@ ModelExecution::ModelExecution(ModelChecker *m, scheduler(scheduler), action_trace(), thread_map(2), /* We'll always need at least 2 threads */ - obj_map(new HashTable()), + obj_map(), condvar_waiters_map(), obj_thrd_map(), promises(), @@ -82,6 +84,7 @@ ModelExecution::ModelExecution(ModelChecker *m, model_thread = new Thread(get_next_id()); add_thread(model_thread); scheduler->register_engine(this); + node_stack->register_engine(this); } /** @brief Destructor */ @@ -90,8 +93,6 @@ ModelExecution::~ModelExecution() for (unsigned int i = 0; i < get_num_threads(); i++) delete get_thread(int_to_id(i)); - delete obj_map; - for (unsigned int i = 0; i < promises.size(); i++) delete promises[i]; @@ -265,6 +266,28 @@ bool ModelExecution::is_deadlocked() const return blocking_threads; } +/** + * @brief Check if we are yield-blocked + * + * A program can be "yield-blocked" if all threads are ready to execute a + * yield. + * + * @return True if the program is yield-blocked; false otherwise + */ +bool ModelExecution::is_yieldblocked() const +{ + if (!params->yieldblock) + return false; + + for (unsigned int i = 0; i < get_num_threads(); i++) { + thread_id_t tid = int_to_id(i); + Thread *t = get_thread(tid); + if (t->get_pending() && t->get_pending()->is_yield()) + return true; + } + return false; +} + /** * Check if this is a complete execution. That is, have all thread completed * execution (rather than exiting because sleep sets have forced a redundant @@ -274,6 +297,8 @@ bool ModelExecution::is_deadlocked() const */ bool ModelExecution::is_complete_execution() const { + if (is_yieldblocked()) + return false; for (unsigned int i = 0; i < get_num_threads(); i++) if (is_enabled(int_to_id(i))) return false; @@ -367,17 +392,22 @@ ModelAction * ModelExecution::get_last_fence_conflict(ModelAction *act) const ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const { switch (act->get_type()) { - /* case ATOMIC_FENCE: fences don't directly cause backtracking */ + case ATOMIC_FENCE: + /* Only seq-cst fences can (directly) cause backtracking */ + if (!act->is_seqcst()) + break; case ATOMIC_READ: case ATOMIC_WRITE: case ATOMIC_RMW: { 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 *list = obj_map.get(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; + if (prev == act) + continue; if (prev->could_synchronize_with(act)) { ret = prev; break; @@ -396,7 +426,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const case ATOMIC_LOCK: case ATOMIC_TRYLOCK: { /* linear search: from most recent to oldest */ - action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + action_list_t *list = obj_map.get(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -407,7 +437,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const } case ATOMIC_UNLOCK: { /* linear search: from most recent to oldest */ - action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + action_list_t *list = obj_map.get(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -418,7 +448,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const } case ATOMIC_WAIT: { /* linear search: from most recent to oldest */ - action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + action_list_t *list = obj_map.get(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -433,7 +463,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const case ATOMIC_NOTIFY_ALL: case ATOMIC_NOTIFY_ONE: { /* linear search: from most recent to oldest */ - action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + action_list_t *list = obj_map.get(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -727,12 +757,13 @@ bool ModelExecution::process_mutex(ModelAction *curr) /** * @brief Check if the current pending promises allow a future value to be sent * - * If one of the following is true: - * (a) there are no pending promises - * (b) the reader and writer do not cross any promises - * Then, it is safe to pass a future value back now. + * It is unsafe to pass a future value back if there exists a pending promise Pr + * such that: * - * Otherwise, we must save the pending future value until (a) or (b) is true + * reader --exec-> Pr --exec-> writer + * + * If such Pr exists, we must save the pending future value until Pr is + * resolved. * * @param writer The operation which sends the future value. Must be a write. * @param reader The operation which will observe the value. Must be a read. @@ -741,8 +772,6 @@ bool ModelExecution::process_mutex(ModelAction *curr) bool ModelExecution::promises_may_allow(const ModelAction *writer, const ModelAction *reader) const { - if (promises.empty()) - return true; for (int i = promises.size() - 1; i >= 0; i--) { ModelAction *pr = promises[i]->get_reader(0); //reader is after promise...doesn't cross any promise @@ -789,9 +818,10 @@ void ModelExecution::add_future_value(const ModelAction *writer, ModelAction *re /** * Process a write ModelAction * @param curr The ModelAction to process + * @param work The work queue, for adding fixup work * @return True if the mo_graph was updated or promises were resolved */ -bool ModelExecution::process_write(ModelAction *curr) +bool ModelExecution::process_write(ModelAction *curr, work_queue_t *work) { /* Readers to which we may send our future value */ ModelVector send_fv; @@ -804,7 +834,7 @@ bool ModelExecution::process_write(ModelAction *curr) if (promise) { earliest_promise_reader = promise->get_reader(0); - updated_promises = resolve_promise(curr, promise); + updated_promises = resolve_promise(curr, promise, work); } else earliest_promise_reader = NULL; @@ -997,21 +1027,9 @@ void ModelExecution::process_relseq_fixup(ModelAction *curr, work_queue_t *work_ /* Must synchronize */ if (!synchronize(release, acquire)) return; - /* Re-check all pending release sequences */ - work_queue->push_back(CheckRelSeqWorkEntry(NULL)); - /* Re-check act for mo_graph edges */ - work_queue->push_back(MOEdgeWorkEntry(acquire)); - - /* propagate synchronization to later actions */ - action_list_t::reverse_iterator rit = action_trace.rbegin(); - for (; (*rit) != acquire; rit++) { - ModelAction *propagate = *rit; - if (acquire->happens_before(propagate)) { - synchronize(acquire, propagate); - /* Re-check 'propagate' for mo_graph edges */ - work_queue->push_back(MOEdgeWorkEntry(propagate)); - } - } + + /* Propagate the changed clock vector */ + propagate_clockvector(acquire, work_queue); } else { /* Break release sequence with new edges: * release --mo--> write --mo--> rf */ @@ -1177,9 +1195,10 @@ void ModelExecution::thread_blocking_check_promises(Thread *blocker, Thread *wai /** * @brief Check whether a model action is enabled. * - * Checks whether a lock or join operation would be successful (i.e., is the - * lock already locked, or is the joined thread already complete). If not, put - * the action in a waiter list. + * Checks whether an operation would be successful (i.e., is a lock already + * locked, or is the joined thread already complete). + * + * For yield-blocking, yields are never enabled. * * @param curr is the ModelAction to check whether it is enabled. * @return a bool that indicates whether the action is enabled. @@ -1196,6 +1215,8 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) { thread_blocking_check_promises(blocking, get_thread(curr)); return false; } + } else if (params->yieldblock && curr->is_yield()) { + return false; } return true; @@ -1210,7 +1231,7 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) { * * @param curr The current action to process * @return The ModelAction that is actually executed; may be different than - * curr; may be NULL, if the current action is not enabled to run + * curr */ ModelAction * ModelExecution::check_current_action(ModelAction *curr) { @@ -1253,7 +1274,7 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (act->is_read() && !second_part_of_rmw && process_read(act)) update = true; - if (act->is_write() && process_write(act)) + if (act->is_write() && process_write(act, &work_queue)) update = true; if (act->is_fence() && process_fence(act)) @@ -1356,7 +1377,7 @@ void ModelExecution::print_infeasibility(const char *prefix) const char *ptr = buf; if (mo_graph->checkForCycles()) ptr += sprintf(ptr, "[mo cycle]"); - if (priv->failed_promise) + if (priv->failed_promise || priv->hard_failed_promise) ptr += sprintf(ptr, "[failed promise]"); if (priv->too_many_reads) ptr += sprintf(ptr, "[too many reads]"); @@ -1369,7 +1390,7 @@ void ModelExecution::print_infeasibility(const char *prefix) const if (promises.size() != 0) ptr += sprintf(ptr, "[unresolved promise]"); if (ptr != buf) - model_print("%s: %s\n", prefix ? prefix : "Infeasible", buf); + model_print("%s: %s", prefix ? prefix : "Infeasible", buf); } /** @@ -1378,7 +1399,8 @@ void ModelExecution::print_infeasibility(const char *prefix) const */ bool ModelExecution::is_feasible_prefix_ignore_relseq() const { - return !is_infeasible() && promises.size() == 0; + return !is_infeasible() && promises.size() == 0 && ! priv->failed_promise; + } /** @@ -1391,9 +1413,9 @@ bool ModelExecution::is_infeasible() const { return mo_graph->checkForCycles() || priv->no_valid_reads || - priv->failed_promise || priv->too_many_reads || priv->bad_synchronization || + priv->hard_failed_promise || promises_expired(); } @@ -1750,7 +1772,8 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVectorpush_back(act); else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from()) @@ -1772,6 +1795,50 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVectorget_tid(); + for(unsigned int i = promises.size(); i>0; i--) { + Promise *pr=promises[i-1]; + if (!pr->same_location(write)) + continue; + //the reading thread is the only thread that can resolve the promise + if (pr->get_num_was_available_threads()==1 && pr->thread_was_available(read->get_tid())) { + for(unsigned int j=0;jget_num_readers();j++) { + ModelAction *prreader=pr->get_reader(j); + //the writing thread reads from the promise before the write + if (prreader->get_tid()==write_tid && + (*prreader)<(*write)) { + if ((*read)>(*prreader)) { + //check that we don't have a read between the read and promise + //from the same thread as read + bool okay=false; + for(const ModelAction *tmp=read;tmp!=prreader;) { + tmp=tmp->get_node()->get_parent()->get_action(); + if (tmp->is_read() && tmp->same_thread(read)) { + okay=true; + break; + } + } + if (okay) + continue; + } + return false; + } + } + } + } + return true; +} + + /** Arbitrary reads from the future are not allowed. Section 29.3 * part 9 places some constraints. This method checks one result of constraint * constraint. Others require compiler support. */ @@ -1800,6 +1867,7 @@ bool ModelExecution::thin_air_constraint_may_allow(const ModelAction *writer, co * require compiler support): * * If X --hb-> Y --mo-> Z, then X should not read from Z. + * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z. */ bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader) { @@ -2031,6 +2099,37 @@ void ModelExecution::get_release_seq_heads(ModelAction *acquire, } } +/** + * @brief Propagate a modified clock vector to actions later in the execution + * order + * + * After an acquire operation lazily completes a release-sequence + * synchronization, we must update all clock vectors for operations later than + * the acquire in the execution order. + * + * @param acquire The ModelAction whose clock vector must be propagated + * @param work The work queue to which we can add work items, if this + * propagation triggers more updates (e.g., to the modification order) + */ +void ModelExecution::propagate_clockvector(ModelAction *acquire, work_queue_t *work) +{ + /* Re-check all pending release sequences */ + work->push_back(CheckRelSeqWorkEntry(NULL)); + /* Re-check read-acquire for mo_graph edges */ + work->push_back(MOEdgeWorkEntry(acquire)); + + /* propagate synchronization to later actions */ + action_list_t::reverse_iterator rit = action_trace.rbegin(); + for (; (*rit) != acquire; rit++) { + ModelAction *propagate = *rit; + if (acquire->happens_before(propagate)) { + synchronize(acquire, propagate); + /* Re-check 'propagate' for mo_graph edges */ + work->push_back(MOEdgeWorkEntry(propagate)); + } + } +} + /** * Attempt to resolve all stashed operations that might synchronize with a * release sequence for a given location. This implements the "lazy" portion of @@ -2069,22 +2168,8 @@ bool ModelExecution::resolve_release_sequences(void *location, work_queue_t *wor updated = true; if (updated) { - /* Re-check all pending release sequences */ - work_queue->push_back(CheckRelSeqWorkEntry(NULL)); - /* 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) != acquire; rit++) { - ModelAction *propagate = *rit; - if (acquire->happens_before(propagate)) { - synchronize(acquire, propagate); - /* Re-check 'propagate' for mo_graph edges */ - work_queue->push_back(MOEdgeWorkEntry(propagate)); - } - } + /* Propagate the changed clock vector */ + propagate_clockvector(acquire, work_queue); } if (complete) { it = pending_rel_seqs.erase(it); @@ -2112,7 +2197,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act) int tid = id_to_int(act->get_tid()); ModelAction *uninit = NULL; int uninit_id = -1; - action_list_t *list = get_safe_ptr_action(obj_map, act->get_location()); + action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location()); if (list->empty() && act->is_atomic_var()) { uninit = get_uninitialized_action(act); uninit_id = id_to_int(uninit->get_tid()); @@ -2145,7 +2230,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act) if (act->is_wait()) { void *mutex_loc = (void *) act->get_value(); - get_safe_ptr_action(obj_map, mutex_loc)->push_back(act); + get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act); SnapVector *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc); if (tid >= (int)vec->size()) @@ -2193,7 +2278,7 @@ ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const { void *location = curr->get_location(); - action_list_t *list = get_safe_ptr_action(obj_map, location); + action_list_t *list = obj_map.get(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) != curr; rit++) @@ -2216,7 +2301,11 @@ ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const { /* All fences should have location FENCE_LOCATION */ - action_list_t *list = get_safe_ptr_action(obj_map, FENCE_LOCATION); + action_list_t *list = obj_map.get(FENCE_LOCATION); + + if (!list) + return NULL; + action_list_t::reverse_iterator rit = list->rbegin(); if (before_fence) { @@ -2245,7 +2334,7 @@ ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const Mode ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const { void *location = curr->get_location(); - action_list_t *list = get_safe_ptr_action(obj_map, location); + action_list_t *list = obj_map.get(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++) @@ -2293,21 +2382,26 @@ Promise * ModelExecution::pop_promise_to_resolve(const ModelAction *curr) * Resolve a Promise with a current write. * @param write The ModelAction that is fulfilling Promises * @param promise The Promise to resolve + * @param work The work queue, for adding new fixup work * @return True if the Promise was successfully resolved; false otherwise */ -bool ModelExecution::resolve_promise(ModelAction *write, Promise *promise) +bool ModelExecution::resolve_promise(ModelAction *write, Promise *promise, + work_queue_t *work) { ModelVector actions_to_check; for (unsigned int i = 0; i < promise->get_num_readers(); i++) { ModelAction *read = promise->get_reader(i); - read_from(read, write); + if (read_from(read, write)) { + /* Propagate the changed clock vector */ + propagate_clockvector(read, work); + } actions_to_check.push_back(read); } /* Make sure the promise's value matches the write's value */ ASSERT(promise->is_compatible(write) && promise->same_value(write)); if (!mo_graph->resolvePromise(promise, write)) - priv->failed_promise = true; + priv->hard_failed_promise = true; /** * @todo It is possible to end up in an inconsistent state, where a @@ -2419,7 +2513,7 @@ void ModelExecution::mo_check_promises(const ModelAction *act, bool is_read_chec if (!pread->happens_before(act)) continue; if (mo_graph->checkPromise(write, promise)) { - priv->failed_promise = true; + priv->hard_failed_promise = true; return; } break; @@ -2431,7 +2525,7 @@ void ModelExecution::mo_check_promises(const ModelAction *act, bool is_read_chec if (mo_graph->checkReachable(promise, write)) { if (mo_graph->checkPromise(write, promise)) { - priv->failed_promise = true; + priv->hard_failed_promise = true; return; } } @@ -2584,7 +2678,9 @@ static void print_list(const action_list_t *list) { action_list_t::const_iterator it; - model_print("---------------------------------------------------------------------\n"); + model_print("------------------------------------------------------------------------------------\n"); + model_print("# t Action type MO Location Value Rf CV\n"); + model_print("------------------------------------------------------------------------------------\n"); unsigned int hash = 0; @@ -2595,7 +2691,7 @@ static void print_list(const action_list_t *list) hash = hash^(hash<<3)^((*it)->hash()); } model_print("HASH %u\n", hash); - model_print("---------------------------------------------------------------------\n"); + model_print("------------------------------------------------------------------------------------\n"); } #if SUPPORT_MOD_ORDER_DUMP @@ -2608,7 +2704,7 @@ void ModelExecution::dumpGraph(char *filename) const mo_graph->dumpNodes(file); ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads()); - for (action_list_t::iterator it = action_trace.begin(); it != action_trace.end(); it++) { + for (action_list_t::const_iterator it = action_trace.begin(); it != action_trace.end(); it++) { ModelAction *act = *it; if (act->is_read()) { mo_graph->dot_print_node(file, act); @@ -2649,15 +2745,21 @@ void ModelExecution::print_summary() const dumpGraph(buffername); #endif - model_print("Execution %d:", get_execution_number()); + model_print("Execution trace %d:", get_execution_number()); if (isfeasibleprefix()) { + if (is_yieldblocked()) + model_print(" YIELD BLOCKED"); if (scheduler->all_threads_sleeping()) model_print(" SLEEP-SET REDUNDANT"); - model_print("\n"); + if (have_bug_reports()) + model_print(" DETECTED BUG(S)"); } else print_infeasibility(" INFEASIBLE"); + model_print("\n"); + print_list(&action_trace); model_print("\n"); + if (!promises.empty()) { model_print("Pending promises:\n"); for (unsigned int i = 0; i < promises.size(); i++) { @@ -2808,7 +2910,7 @@ void ModelExecution::fixup_release_sequences() { while (!pending_rel_seqs.empty() && is_feasible_prefix_ignore_relseq() && - !unrealizedraces.empty()) { + haveUnrealizedRaces()) { model_print("*** WARNING: release sequence fixup action " "(%zu pending release seuqence(s)) ***\n", pending_rel_seqs.size());