X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=e39266d41218feecb14d4fde94701c22cd2040d3;hp=bc17a882c56f38c7bab1a71064f584ca285e6171;hb=d3dffe991352938e5c2ab738ce70e3ec0f069d5f;hpb=73de022597f45a327075153343c13af0bbe9ad0a diff --git a/model.cc b/model.cc index bc17a882..e39266d4 100644 --- a/model.cc +++ b/model.cc @@ -614,7 +614,7 @@ void ModelChecker::set_backtracking(ModelAction *act) Node *node = prev->get_node()->get_parent(); int low_tid, high_tid; - if (node->is_enabled(t)) { + if (node->enabled_status(t->get_id()) == THREAD_ENABLED) { low_tid = id_to_int(act->get_tid()); high_tid = low_tid + 1; } else { @@ -721,7 +721,6 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) r_status = r_modification_order(curr, reads_from); } - if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) { mo_graph->rollbackChanges(); priv->too_many_reads = false; @@ -730,16 +729,16 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) read_from(curr, reads_from); mo_graph->commitChanges(); - mo_check_promises(curr->get_tid(), reads_from); + mo_check_promises(curr->get_tid(), reads_from, NULL); updated |= r_status; } else if (!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(); + struct future_value fv = curr->get_node()->get_future_value(); + value = fv.value; + curr->set_value(fv.value); curr->set_read_from(NULL); - Promise *valuepromise = new Promise(curr, value, expiration); - promises->push_back(valuepromise); + promises->push_back(new Promise(curr, fv)); } get_thread(curr)->set_return_value(value); return updated; @@ -853,6 +852,27 @@ bool ModelChecker::process_mutex(ModelAction *curr) return false; } +void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader) +{ + /* Do more ambitious checks now that mo is more complete */ + if (mo_may_allow(writer, reader)) { + Node *node = reader->get_node(); + + /* Find an ancestor thread which exists at the time of the reader */ + Thread *write_thread = get_thread(writer); + while (id_to_int(write_thread->get_id()) >= node->get_num_threads()) + write_thread = write_thread->get_parent(); + + struct future_value fv = { + writer->get_value(), + writer->get_seq_number() + params.maxfuturedelay, + write_thread->get_id(), + }; + if (node->add_future_value(fv)) + set_latest_backtrack(reader); + } +} + /** * Process a write ModelAction * @param curr The ModelAction to process @@ -866,16 +886,13 @@ bool ModelChecker::process_write(ModelAction *curr) if (promises->size() == 0) { for (unsigned int i = 0; i < futurevalues->size(); i++) { struct PendingFutureValue pfv = (*futurevalues)[i]; - //Do more ambitious checks now that mo is more complete - if (mo_may_allow(pfv.writer, pfv.act) && - pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number() + params.maxfuturedelay)) - set_latest_backtrack(pfv.act); + add_future_value(pfv.writer, pfv.act); } futurevalues->clear(); } mo_graph->commitChanges(); - mo_check_promises(curr->get_tid(), curr); + mo_check_promises(curr->get_tid(), curr, NULL); get_thread(curr)->set_return_value(VALUE_NONE); return updated_mod_order || updated_promises; @@ -950,6 +967,12 @@ bool ModelChecker::process_thread_action(ModelAction *curr) case THREAD_CREATE: { Thread *th = curr->get_thread_operand(); th->set_creation(curr); + /* Promises can be satisfied by children */ + for (unsigned int i = 0; i < promises->size(); i++) { + Promise *promise = (*promises)[i]; + if (promise->thread_is_available(curr->get_tid())) + promise->add_thread(th->get_id()); + } break; } case THREAD_JOIN: { @@ -966,6 +989,13 @@ bool ModelChecker::process_thread_action(ModelAction *curr) scheduler->wake(get_thread(act)); } th->complete(); + /* Completed thread can't satisfy promises */ + for (unsigned int i = 0; i < promises->size(); i++) { + Promise *promise = (*promises)[i]; + if (promise->thread_is_available(th->get_id())) + if (promise->eliminate_thread(th->get_id())) + priv->failed_promise = true; + } updated = true; /* trigger rel-seq checks */ break; } @@ -1333,15 +1363,37 @@ bool ModelChecker::isfeasibleprefix() const return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq(); } +/** + * Print disagnostic information about an infeasible execution + * @param prefix A string to prefix the output with; if NULL, then a default + * message prefix will be provided + */ +void ModelChecker::print_infeasibility(const char *prefix) const +{ + char buf[100]; + char *ptr = buf; + if (mo_graph->checkForCycles()) + ptr += sprintf(ptr, "[mo cycle]"); + if (priv->failed_promise) + ptr += sprintf(ptr, "[failed promise]"); + if (priv->too_many_reads) + ptr += sprintf(ptr, "[too many reads]"); + if (priv->bad_synchronization) + ptr += sprintf(ptr, "[bad sw ordering]"); + 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); +} + /** * 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; } @@ -1353,36 +1405,10 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const */ bool ModelChecker::is_infeasible() const { - if (DBG_ENABLED() && mo_graph->checkForRMWViolation()) - DEBUG("Infeasible: RMW violation\n"); - - return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW(); -} - -/** - * 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 (priv->failed_promise) - DEBUG("Infeasible: failed promise\n"); - if (priv->too_many_reads) - DEBUG("Infeasible: too many reads\n"); - if (priv->bad_synchronization) - DEBUG("Infeasible: bad synchronization ordering\n"); - if (promises_expired()) - DEBUG("Infeasible: promises expired\n"); - } - return mo_graph->checkForCycles() || priv->failed_promise || - priv->too_many_reads || priv->bad_synchronization || + return mo_graph->checkForCycles() || + priv->failed_promise || + priv->too_many_reads || + priv->bad_synchronization || promises_expired(); } @@ -1771,10 +1797,10 @@ bool ModelChecker::w_modification_order(ModelAction *curr) */ if (thin_air_constraint_may_allow(curr, act)) { - if (!is_infeasible() || - (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) { + if (!is_infeasible()) futurevalues->push_back(PendingFutureValue(curr, act)); - } + else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from()) + add_future_value(curr, act); } } } @@ -2295,7 +2321,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) const bool ModelChecker::resolve_promises(ModelAction *write) { bool resolved = false; - std::vector< thread_id_t, ModelAlloc > threads_to_check; + std::vector< ModelAction *, ModelAlloc > actions_to_check; for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) { Promise *promise = (*promises)[promise_index]; @@ -2313,10 +2339,10 @@ bool ModelChecker::resolve_promises(ModelAction *write) post_r_modification_order(read, write); //Make sure the promise's value matches the write's value ASSERT(promise->get_value() == write->get_value()); - delete(promise); + delete promise; promises->erase(promises->begin() + promise_index); - threads_to_check.push_back(read->get_tid()); + actions_to_check.push_back(read); resolved = true; } else @@ -2326,8 +2352,10 @@ bool ModelChecker::resolve_promises(ModelAction *write) //Check whether reading these writes has made threads unable to //resolve promises - for (unsigned int i = 0; i < threads_to_check.size(); i++) - mo_check_promises(threads_to_check[i], write); + for (unsigned int i = 0; i < actions_to_check.size(); i++) { + ModelAction *read=actions_to_check[i]; + mo_check_promises(read->get_tid(), write, read); + } return resolved; } @@ -2362,7 +2390,7 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec const ModelAction *act = promise->get_action(); if ((old_cv == NULL || !old_cv->synchronized_since(act)) && merge_cv->synchronized_since(act)) { - if (promise->increment_threads(tid)) { + if (promise->eliminate_thread(tid)) { //Promise has failed priv->failed_promise = true; return; @@ -2371,29 +2399,34 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec } } -void ModelChecker::check_promises_thread_disabled() { +void ModelChecker::check_promises_thread_disabled() +{ for (unsigned int i = 0; i < promises->size(); i++) { Promise *promise = (*promises)[i]; - if (promise->check_promise()) { + if (promise->has_failed()) { priv->failed_promise = true; return; } } } -/** Checks promises in response to addition to modification order for threads. +/** + * @brief Checks promises in response to addition to modification order for + * threads. + * * Definitions: + * * pthread is the thread that performed the read that created the promise * * pread is the read that created the promise * * pwrite is either the first write to same location as pread by - * pthread that is sequenced after pread or the value read by the - * first read to the same lcoation as pread by pthread that is - * sequenced after pread.. + * pthread that is sequenced after pread or the write read by the + * first read to the same location as pread by pthread that is + * sequenced after pread. * - * 1. If tid=pthread, then we check what other threads are reachable - * through the mode order starting with pwrite. Those threads cannot + * 1. If tid=pthread, then we check what other threads are reachable + * through the mod order starting with pwrite. Those threads cannot * perform a write that will resolve the promise due to modification * order constraints. * @@ -2402,46 +2435,50 @@ void ModelChecker::check_promises_thread_disabled() { * cannot perform a future write that will resolve the promise due to * modificatin order constraints. * - * @param tid The thread that either read from the model action - * write, or actually did the model action write. + * @param tid The thread that either read from the model action write, or + * actually did the model action write. * - * @param write The ModelAction representing the relevant write. + * @param write The ModelAction representing the relevant write. + * @param read The ModelAction that reads a promised write, or NULL otherwise. */ -void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) +void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write, const ModelAction *read) { void *location = write->get_location(); for (unsigned int i = 0; i < promises->size(); i++) { Promise *promise = (*promises)[i]; const ModelAction *act = promise->get_action(); - //Is this promise on the same location? + // Is this promise on the same location? if (act->get_location() != location) continue; - //same thread as the promise + // same thread as the promise if (act->get_tid() == tid) { + // make sure that the reader of this write happens after the promise + if ((read == NULL) || (promise->get_action()->happens_before(read))) { + // do we have a pwrite for the promise, if not, set it + if (promise->get_write() == NULL) { + promise->set_write(write); + // The pwrite cannot happen before the promise + if (write->happens_before(act) && (write != act)) { + priv->failed_promise = true; + return; + } + } - //do we have a pwrite for the promise, if not, set it - if (promise->get_write() == NULL) { - promise->set_write(write); - //The pwrite cannot happen before the promise - if (write->happens_before(act) && (write != act)) { + if (mo_graph->checkPromise(write, promise)) { priv->failed_promise = true; return; } } - if (mo_graph->checkPromise(write, promise)) { - priv->failed_promise = true; - return; - } } - //Don't do any lookups twice for the same thread - if (promise->has_sync_thread(tid)) + // Don't do any lookups twice for the same thread + if (!promise->thread_is_available(tid)) continue; if (promise->get_write() && mo_graph->checkReachable(promise->get_write(), write)) { - if (promise->increment_threads(tid)) { + if (promise->eliminate_thread(tid)) { priv->failed_promise = true; return; } @@ -2561,13 +2598,11 @@ ModelAction * ModelChecker::new_uninitialized_action(void *location) const return act; } -static void print_list(action_list_t *list, int exec_num = -1) +static void print_list(action_list_t *list) { action_list_t::iterator it; model_print("---------------------------------------------------------------------\n"); - if (exec_num >= 0) - model_print("Execution %d:\n", exec_num); unsigned int hash = 0; @@ -2612,7 +2647,6 @@ void ModelChecker::dumpGraph(char *filename) const void ModelChecker::print_summary() const { #if SUPPORT_MOD_ORDER_DUMP - scheduler->print(); char buffername[100]; sprintf(buffername, "exec%04u", stats.num_total); mo_graph->dumpGraphToFile(buffername); @@ -2620,9 +2654,12 @@ void ModelChecker::print_summary() const dumpGraph(buffername); #endif - if (!isfeasibleprefix()) - model_print("INFEASIBLE EXECUTION!\n"); - print_list(action_trace, stats.num_total); + model_print("Execution %d:", stats.num_total); + if (isfeasibleprefix()) + model_print("\n"); + else + print_infeasibility(" INFEASIBLE"); + print_list(action_trace); model_print("\n"); } @@ -2661,7 +2698,7 @@ Thread * ModelChecker::get_thread(thread_id_t tid) const * @param act The ModelAction * @return A Thread reference */ -Thread * ModelChecker::get_thread(ModelAction *act) const +Thread * ModelChecker::get_thread(const ModelAction *act) const { return get_thread(act->get_tid()); }