Bug fix for broken treatment of promises + coherence based pruning to regain pruning...

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 7e5e95602408b47f5d4ff5b746e64db88287366f..def51f9671e346251a4f108abe1c78c8d09a8bfe 100644 (file)
--- 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 53aa5212f0b017622d0c284f1cbc765e0620fddd..3a630d777f060cb22598858278044d6e140cfed3 100644 (file)
--- 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<bug_message *> 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, ModelVector<ModelAc
                                   pendingfuturevalue.
 
                                 */
-                               if (send_fv && thin_air_constraint_may_allow(curr, act)) {
+
+                               if (send_fv && thin_air_constraint_may_allow(curr, act) && check_coherence_promise(curr, act)) {
                                        if (!is_infeasible())
                                                send_fv->push_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, ModelVector<ModelAc
        return added;
 }
 
+//This procedure uses cohere to prune future values that are
+//guaranteed to generate a coherence violation.
+//
+//need to see if there is (1) a promise for thread write, (2)
+//the promise is sb before write, (3) the promise can only be
+//resolved by the thread read, and (4) the promise has same
+//location as read/write
+
+bool ModelExecution::check_coherence_promise(const ModelAction * write, const ModelAction *read) {
+       thread_id_t write_tid=write->get_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;j<pr->get_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 9c9c1ca454431dc64a3ee8ddf17cd19d13c8a5d4..2ca25131a013166b7fdc76e53f75afdc4969c888 100644 (file)
--- 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 3a38384721cd3dfdc59b25f59440b432cf62c87b..a98403bbcf10569a91c2929bd17c420f4a3dc5f6 100644 (file)
--- 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 84d5aa49b3af7b8156ef4744e270f128c6a0cabf..e306e14a261aafe8d38b0753524cd194dfc730f0 100644 (file)
--- 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<bool> available_thread;
+       SnapVector<bool> was_available_thread;
 
        int num_available_threads;
+       int num_was_available_threads;
 
        const future_value fv;