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

[model-checker.git] / execution.cc

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),
                next_backtrack(NULL),
                bugs(),
                failed_promise(false),

+               hard_failed_promise(false),

                too_many_reads(false),
                no_valid_reads(false),
                bad_synchronization(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;
        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 */
        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]");
        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]");
                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
 {
  */
 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 ||
 {
        return mo_graph->checkForCycles() ||
                priv->no_valid_reads ||

-               priv->failed_promise ||

                priv->too_many_reads ||
                priv->bad_synchronization ||
                priv->too_many_reads ||
                priv->bad_synchronization ||

+               priv->hard_failed_promise ||

                promises_expired();
 }
 
                promises_expired();
 }
 


@@ -1769,7 +1772,8 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVector<ModelAc
                                   pendingfuturevalue.
 
                                 */
                                   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())
                                        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;
 }
 
        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. */
 /** 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))
        /* 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
 
        /**
         * @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)) {
                        if (!pread->happens_before(act))
                               continue;
                        if (mo_graph->checkPromise(write, promise)) {

-                               priv->failed_promise = true;
+                               priv->hard_failed_promise = true;

                                return;
                        }
                        break;
                                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)) {
 
                if (mo_graph->checkReachable(promise, write)) {
                        if (mo_graph->checkPromise(write, promise)) {

-                               priv->failed_promise = true;
+                               priv->hard_failed_promise = true;

                                return;
                        }
                }
                                return;
                        }
                }