X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=execution.cc;h=2a7e0dadd1e0918ac21b5f43dd4e3608935b8f18;hp=4e154275eac6b42cb4ea805ab9e86bf6a63cd2b5;hb=88fb5522811e0bd481ad3e60b70fe40fbc9c3e0f;hpb=dd1f275d3e8042282bad49cf85fddfc2a5735166 diff --git a/execution.cc b/execution.cc index 4e15427..2a7e0da 100644 --- a/execution.cc +++ b/execution.cc @@ -30,9 +30,11 @@ 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), + bad_sc_read(false), asserted(false) { } @@ -47,10 +49,12 @@ 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 */ bool bad_synchronization; + bool bad_sc_read; bool asserted; SNAPSHOTALLOC @@ -200,6 +204,13 @@ void ModelExecution::set_bad_synchronization() priv->bad_synchronization = true; } +/** @brief Alert the model-checker that an incorrectly-ordered + * synchronization was made */ +void ModelExecution::set_bad_sc_read() +{ + priv->bad_sc_read = true; +} + bool ModelExecution::assert_bug(const char *msg) { priv->bugs.push_back(new bug_message(msg)); @@ -755,12 +766,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. @@ -769,8 +781,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 @@ -817,9 +827,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; @@ -832,7 +843,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; @@ -1272,7 +1283,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)) @@ -1304,6 +1315,12 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (rf) { if (r_modification_order(act, rf)) updated = true; + if (act->is_seqcst()) { + ModelAction *last_sc_write = get_last_seq_cst_write(act); + if (last_sc_write != NULL && rf->happens_before(last_sc_write)) { + set_bad_sc_read(); + } + } } else if (promise) { if (r_modification_order(act, promise)) updated = true; @@ -1375,7 +1392,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]"); @@ -1383,12 +1400,14 @@ void ModelExecution::print_infeasibility(const char *prefix) const ptr += sprintf(ptr, "[no valid reads-from]"); if (priv->bad_synchronization) ptr += sprintf(ptr, "[bad sw ordering]"); + if (priv->bad_sc_read) + ptr += sprintf(ptr, "[bad sc read]"); if (promises_expired()) ptr += sprintf(ptr, "[promise expired]"); 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); } /** @@ -1397,7 +1416,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; + } /** @@ -1410,9 +1430,10 @@ bool ModelExecution::is_infeasible() const { return mo_graph->checkForCycles() || priv->no_valid_reads || - priv->failed_promise || priv->too_many_reads || priv->bad_synchronization || + priv->bad_sc_read || + priv->hard_failed_promise || promises_expired(); } @@ -1613,12 +1634,6 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) } } - /* C++, Section 29.3 statement 3 (second subpoint) */ - if (curr->is_seqcst() && last_sc_write && act == last_sc_write) { - added = mo_graph->addEdge(act, rf) || added; - break; - } - /* * Include at most one act per-thread that "happens * before" curr @@ -1750,9 +1765,10 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVectoraddEdge(act, curr) || added; else if (act->is_read()) { //if previous read accessed a null, just keep going - if (act->get_reads_from() == NULL) - continue; - added = mo_graph->addEdge(act->get_reads_from(), curr) || added; + if (act->get_reads_from() == NULL) { + added = mo_graph->addEdge(act->get_reads_from_promise(), curr) || added; + } else + added = mo_graph->addEdge(act->get_reads_from(), curr) || added; } break; } else if (act->is_read() && !act->could_synchronize_with(curr) && @@ -1769,7 +1785,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()) @@ -1791,6 +1808,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. */ @@ -1819,6 +1880,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) { @@ -2333,21 +2395,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 @@ -2459,7 +2526,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; @@ -2471,7 +2538,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; } } @@ -2624,7 +2691,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; @@ -2635,7 +2704,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 @@ -2689,17 +2758,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++) {