X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=40b25d0d635a32a5fdd2832001c638c3ee1986fc;hb=ffb2033ac6b31407810703b65ae0fbaeb9c0da59;hp=98df8f316106a5f4cce404f4cada60ee35c5898a;hpb=260b391c9292c9eb48da1033bf4ac1c32ea49f87;p=model-checker.git diff --git a/model.cc b/model.cc index 98df8f3..40b25d0 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 { @@ -730,16 +730,15 @@ 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_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,19 @@ 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)) { + struct future_value fv = { + writer->get_value(), + writer->get_seq_number() + params.maxfuturedelay, + }; + if (reader->get_node()->add_future_value(fv)) + set_latest_backtrack(reader); + } +} + /** * Process a write ModelAction * @param curr The ModelAction to process @@ -866,16 +878,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->resize(0); + 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; @@ -1333,15 +1342,39 @@ 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->checkForRMWViolation()) + ptr += sprintf(ptr, "[RMW atomicity]"); + 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,9 +1386,6 @@ 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(); } @@ -1369,18 +1399,6 @@ bool ModelChecker::is_infeasible() const * */ 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 || promises_expired(); @@ -1773,8 +1791,7 @@ 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())) { - struct PendingFutureValue pfv = {curr, act}; - futurevalues->push_back(pfv); + futurevalues->push_back(PendingFutureValue(curr, act)); } } } @@ -2296,7 +2313,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]; @@ -2317,7 +2334,7 @@ bool ModelChecker::resolve_promises(ModelAction *write) 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 @@ -2327,8 +2344,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; } @@ -2363,7 +2382,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; @@ -2372,29 +2391,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. * @@ -2403,46 +2427,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_eliminated(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; } @@ -2562,13 +2590,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; @@ -2621,9 +2647,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"); } @@ -2662,7 +2691,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()); }