From 6014243b7130f34b7ffd1098da225b0b8de5c328 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Sat, 25 Jan 2014 14:11:22 -0800 Subject: [PATCH] Bug fix for broken treatment of promises + coherence based pruning to regain pruning lost by bug fix --- cyclegraph.cc | 5 ++--- execution.cc | 62 +++++++++++++++++++++++++++++++++++++++++++++------ execution.h | 2 +- promise.cc | 15 +++++++++++++ promise.h | 4 ++++ 5 files changed, 77 insertions(+), 11 deletions(-) diff --git a/cyclegraph.cc b/cyclegraph.cc index 7e5e956..def51f9 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -456,9 +456,8 @@ bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) cons if (node->getPromise() == promise) return true; - if (!node->is_promise() && - promise->eliminate_thread(node->getAction()->get_tid())) - return true; + if (!node->is_promise()) + promise->eliminate_thread(node->getAction()->get_tid()); for (unsigned int i = 0; i < node->getNumEdges(); i++) { CycleNode *next = node->getEdge(i); diff --git a/execution.cc b/execution.cc index 53aa521..3a630d7 100644 --- a/execution.cc +++ b/execution.cc @@ -30,6 +30,7 @@ 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), @@ -47,6 +48,7 @@ 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 */ @@ -1375,7 +1377,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]"); @@ -1397,7 +1399,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 +1413,9 @@ bool ModelExecution::is_infeasible() const { return mo_graph->checkForCycles() || priv->no_valid_reads || - priv->failed_promise || priv->too_many_reads || priv->bad_synchronization || + priv->hard_failed_promise || promises_expired(); } @@ -1769,7 +1772,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 +1795,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. */ @@ -2353,7 +2401,7 @@ bool ModelExecution::resolve_promise(ModelAction *write, Promise *promise, /* 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 @@ -2465,7 +2513,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; @@ -2477,7 +2525,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; } } diff --git a/execution.h b/execution.h index 9c9c1ca..2ca2513 100644 --- a/execution.h +++ b/execution.h @@ -187,7 +187,7 @@ private: void propagate_clockvector(ModelAction *acquire, work_queue_t *work); bool resolve_release_sequences(void *location, work_queue_t *work_queue); void add_future_value(const ModelAction *writer, ModelAction *reader); - + bool check_coherence_promise(const ModelAction *write, const ModelAction *read); ModelAction * get_uninitialized_action(const ModelAction *curr) const; action_list_t action_trace; diff --git a/promise.cc b/promise.cc index 3a38384..a98403b 100644 --- a/promise.cc +++ b/promise.cc @@ -16,6 +16,7 @@ Promise::Promise(const ModelExecution *execution, ModelAction *read, struct future_value fv) : execution(execution), num_available_threads(0), + num_was_available_threads(0), fv(fv), readers(1, read), write(NULL) @@ -82,6 +83,12 @@ void Promise::add_thread(thread_id_t tid) available_thread[id] = true; num_available_threads++; } + if (id >= was_available_thread.size()) + was_available_thread.resize(id + 1, false); + if (!was_available_thread[id]) { + was_available_thread[id] = true; + num_was_available_threads++; + } } /** @@ -100,6 +107,14 @@ bool Promise::thread_is_available(thread_id_t tid) const return available_thread[id]; } +bool Promise::thread_was_available(thread_id_t tid) const +{ + unsigned int id = id_to_int(tid); + if (id >= was_available_thread.size()) + return false; + return was_available_thread[id]; +} + /** * @brief Get an upper bound on the number of available threads * diff --git a/promise.h b/promise.h index 84d5aa4..e306e14 100644 --- a/promise.h +++ b/promise.h @@ -31,11 +31,13 @@ class Promise { bool eliminate_thread(thread_id_t tid); void add_thread(thread_id_t tid); bool thread_is_available(thread_id_t tid) const; + bool thread_was_available(thread_id_t tid) const; unsigned int max_available_thread_idx() const; bool has_failed() const; void set_write(const ModelAction *act) { write = act; } const ModelAction * get_write() const { return write; } int get_num_available_threads() const { return num_available_threads; } + int get_num_was_available_threads() const { return num_was_available_threads; } bool is_compatible(const ModelAction *act) const; bool is_compatible_exclusive(const ModelAction *act) const; bool same_value(const ModelAction *write) const; @@ -60,8 +62,10 @@ class Promise { /** @brief Thread ID(s) for thread(s) that potentially can satisfy this * promise */ SnapVector available_thread; + SnapVector was_available_thread; int num_available_threads; + int num_was_available_threads; const future_value fv; -- 2.34.1