From 8c9713418515a44e0a96cadabca0feececf962b3 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Wed, 27 Feb 2013 15:13:17 -0800 Subject: [PATCH] promise: record multiple readers in the same Promise This requires more adjustments throughout ModelChecker. --- cyclegraph.cc | 2 +- model.cc | 81 +++++++++++++++++++++++++++++++++------------------ promise.cc | 31 ++++++++++++++++++-- promise.h | 8 +++-- 4 files changed, 86 insertions(+), 36 deletions(-) diff --git a/cyclegraph.cc b/cyclegraph.cc index 1dbb12d9..67552e00 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -320,7 +320,7 @@ static void print_node(const CycleNode *node, FILE *file, int label) modelclock_t idx; if (node->is_promise()) { const Promise *promise = node->getPromise(); - idx = promise->get_action()->get_seq_number(); + idx = promise->get_reader(0)->get_seq_number(); fprintf(file, "P%u", idx); if (label) { int first = 1; diff --git a/model.cc b/model.cc index 44fba7ea..38d63a2f 100644 --- a/model.cc +++ b/model.cc @@ -873,6 +873,7 @@ bool ModelChecker::process_read(ModelAction *curr) } case READ_FROM_PROMISE: { Promise *promise = curr->get_node()->get_read_from_promise(); + promise->add_reader(curr); value = promise->get_value(); curr->set_read_from_promise(promise); mo_graph->startChanges(); @@ -1348,14 +1349,19 @@ void ModelChecker::thread_blocking_check_promises(Thread *blocker, Thread *waiti { for (unsigned int i = 0; i < promises->size(); i++) { Promise *promise = (*promises)[i]; - ModelAction *reader = promise->get_action(); - if (reader->get_tid() != blocker->get_id()) - continue; if (!promise->thread_is_available(waiting->get_id())) continue; - if (promise->eliminate_thread(waiting->get_id())) { - /* Promise has failed */ - priv->failed_promise = true; + for (unsigned int j = 0; j < promise->get_num_readers(); j++) { + ModelAction *reader = promise->get_reader(j); + if (reader->get_tid() != blocker->get_id()) + continue; + if (promise->eliminate_thread(waiting->get_id())) { + /* Promise has failed */ + priv->failed_promise = true; + } else { + /* Only eliminate the 'waiting' thread once */ + return; + } } } } @@ -2451,15 +2457,17 @@ bool ModelChecker::resolve_promises(ModelAction *write) for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) { Promise *promise = (*promises)[promise_index]; if (write->get_node()->get_promise(i)) { - ModelAction *read = promise->get_action(); - read_from(read, write); + for (unsigned int j = 0; j < promise->get_num_readers(); j++) { + ModelAction *read = promise->get_reader(j); + read_from(read, write); + actions_to_check.push_back(read); + } //Make sure the promise's value matches the write's value ASSERT(promise->is_compatible(write)); mo_graph->resolvePromise(promise, write, &mustResolve); resolved.push_back(promise); promises->erase(promises->begin() + promise_index); - actions_to_check.push_back(read); haveResolved = true; } else @@ -2494,14 +2502,20 @@ void ModelChecker::compute_promises(ModelAction *curr) { for (unsigned int i = 0; i < promises->size(); i++) { Promise *promise = (*promises)[i]; - const ModelAction *act = promise->get_action(); - ASSERT(act->is_read()); - if (!act->happens_before(curr) && - !act->could_synchronize_with(curr) && - promise->is_compatible(curr) && - promise->get_value() == curr->get_value()) { - curr->get_node()->set_promise(i); + if (!promise->is_compatible(curr) || promise->get_value() != curr->get_value()) + continue; + + bool satisfy = true; + for (unsigned int j = 0; j < promise->get_num_readers(); j++) { + const ModelAction *act = promise->get_reader(j); + if (act->happens_before(curr) || + act->could_synchronize_with(curr)) { + satisfy = false; + break; + } } + if (satisfy) + curr->get_node()->set_promise(i); } } @@ -2510,13 +2524,17 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec { for (unsigned int i = 0; i < promises->size(); i++) { Promise *promise = (*promises)[i]; - const ModelAction *act = promise->get_action(); - if ((old_cv == NULL || !old_cv->synchronized_since(act)) && - merge_cv->synchronized_since(act)) { - if (promise->eliminate_thread(tid)) { - //Promise has failed - priv->failed_promise = true; - return; + if (!promise->thread_is_available(tid)) + continue; + for (unsigned int j = 0; j < promise->get_num_readers(); j++) { + const ModelAction *act = promise->get_reader(j); + if ((!old_cv || !old_cv->synchronized_since(act)) && + merge_cv->synchronized_since(act)) { + if (promise->eliminate_thread(tid)) { + /* Promise has failed */ + priv->failed_promise = true; + return; + } } } } @@ -2553,15 +2571,20 @@ void ModelChecker::mo_check_promises(const ModelAction *act, bool is_read_check) for (unsigned int i = 0; i < promises->size(); i++) { Promise *promise = (*promises)[i]; - const ModelAction *pread = promise->get_action(); // Is this promise on the same location? - if (!pread->same_var(write)) + if (promise->get_value() != write->get_value()) continue; - if (pread->happens_before(act) && mo_graph->checkPromise(write, promise)) { - priv->failed_promise = true; - return; + for (unsigned int j = 0; j < promise->get_num_readers(); j++) { + const ModelAction *pread = promise->get_reader(j); + if (!pread->happens_before(act)) + continue; + if (mo_graph->checkPromise(write, promise)) { + priv->failed_promise = true; + return; + } + break; } // Don't do any lookups twice for the same thread @@ -2656,7 +2679,7 @@ void ModelChecker::build_may_read_from(ModelAction *curr) /* Inherit existing, promised future values */ for (i = 0; i < promises->size(); i++) { const Promise *promise = (*promises)[i]; - const ModelAction *promise_read = promise->get_action(); + const ModelAction *promise_read = promise->get_reader(0); if (promise_read->same_var(curr)) { /* Only add feasible future-values */ mo_graph->startChanges(); diff --git a/promise.cc b/promise.cc index 86c3c584..23b92cd4 100644 --- a/promise.cc +++ b/promise.cc @@ -15,13 +15,38 @@ Promise::Promise(ModelAction *read, struct future_value fv) : num_available_threads(0), fv(fv), - read(read), + readers(1, read), write(NULL) { add_thread(fv.tid); eliminate_thread(read->get_tid()); } +/** + * Add a reader that reads from this Promise. Must be added in an order + * consistent with execution order. + * + * @param reader The ModelAction that reads from this promise. Must be a read. + * @return True if this new reader has invalidated the promise; false otherwise + */ +bool Promise::add_reader(ModelAction *reader) +{ + readers.push_back(reader); + return eliminate_thread(reader->get_tid()); +} + +/** + * Access a reader that read from this Promise. Readers must be inserted in + * order by execution order, so they can be returned in this order. + * + * @param i The index of the reader to return + * @return The i'th reader of this Promise + */ +ModelAction * Promise::get_reader(unsigned int i) const +{ + return i < readers.size() ? readers[i] : NULL; +} + /** * Eliminate a thread which no longer can satisfy this promise. Once all * enabled threads have been eliminated, this promise is unresolvable. @@ -76,7 +101,7 @@ bool Promise::thread_is_available(thread_id_t tid) const /** @brief Print debug info about the Promise */ void Promise::print() const { - model_print("Promised value %#" PRIx64 ", read from thread %d, available threads to resolve: ", fv.value, id_to_int(read->get_tid())); + model_print("Promised value %#" PRIx64 ", first read from thread %d, available threads to resolve: ", fv.value, id_to_int(get_reader(0)->get_tid())); for (unsigned int i = 0; i < available_thread.size(); i++) if (available_thread[i]) model_print("[%d]", i); @@ -102,7 +127,7 @@ bool Promise::has_failed() const */ bool Promise::is_compatible(const ModelAction *act) const { - return thread_is_available(act->get_tid()) && read->same_var(act); + return thread_is_available(act->get_tid()) && get_reader(0)->same_var(act); } /** diff --git a/promise.h b/promise.h index c131d743..5ea7dc58 100644 --- a/promise.h +++ b/promise.h @@ -24,7 +24,9 @@ struct future_value { class Promise { public: Promise(ModelAction *read, struct future_value fv); - ModelAction * get_action() const { return read; } + bool add_reader(ModelAction *reader); + ModelAction * get_reader(unsigned int i) const; + unsigned int get_num_readers() const { return readers.size(); } bool eliminate_thread(thread_id_t tid); void add_thread(thread_id_t tid); bool thread_is_available(thread_id_t tid) const; @@ -54,8 +56,8 @@ class Promise { const future_value fv; - /** @brief The action which reads a promised value */ - ModelAction * const read; + /** @brief The action(s) which read the promised future value */ + std::vector< ModelAction *, SnapshotAlloc > readers; const ModelAction *write; }; -- 2.34.1