X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=40b25d0d635a32a5fdd2832001c638c3ee1986fc;hb=ffb2033ac6b31407810703b65ae0fbaeb9c0da59;hp=97df9a2dbba274857e85e6be417489c776e82024;hpb=f10dc6ce67a97ab18423e7cedaa24961bf0d80dc;p=model-checker.git diff --git a/model.cc b/model.cc index 97df9a2..40b25d0 100644 --- a/model.cc +++ b/model.cc @@ -738,8 +738,7 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) struct future_value fv = curr->get_node()->get_future_value(); value = fv.value; curr->set_read_from(NULL); - Promise *valuepromise = new Promise(curr, value, fv.expiration); - promises->push_back(valuepromise); + promises->push_back(new Promise(curr, fv)); } get_thread(curr)->set_return_value(value); return updated; @@ -856,10 +855,14 @@ bool ModelChecker::process_mutex(ModelAction *curr) 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) && - reader->get_node()->add_future_value(writer, - writer->get_seq_number() + params.maxfuturedelay)) - set_latest_backtrack(reader); + 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); + } } /** @@ -2379,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; @@ -2388,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. * @@ -2419,11 +2427,11 @@ 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 read The ModelAction that reads a promised write, or NULL otherwise. + * @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, const ModelAction *read) { @@ -2432,24 +2440,24 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write, 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 + // 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 + // The pwrite cannot happen before the promise if (write->happens_before(act) && (write != act)) { priv->failed_promise = true; return; } } - + if (mo_graph->checkPromise(write, promise)) { priv->failed_promise = true; return; @@ -2457,12 +2465,12 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write, } } - //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; } @@ -2683,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()); }