bug fix...recompute promises of RMW actions at divergence points

diff --git a/model.cc b/model.cc
index 47c6cdb92d442f0b0f460e353e9d25c93cfb6dc7..62e75205e4ee9681bcef321856c744978c9cc5c1 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -525,7 +525,9 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
        if (curr->is_rmwc() || curr->is_rmw()) {
                newcurr = process_rmw(curr);
                delete curr;
        if (curr->is_rmwc() || curr->is_rmw()) {
                newcurr = process_rmw(curr);
                delete curr;

-               compute_promises(newcurr);
+
+               if (newcurr->is_rmw())
+                       compute_promises(newcurr);

                return newcurr;
        }
 
                return newcurr;
        }
 


@@ -542,8 +544,9 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
                delete curr;
 
                /* If we have diverged, we need to reset the clock vector. */
                delete curr;
 
                /* If we have diverged, we need to reset the clock vector. */

-               if (diverge == NULL)
+               if (diverge == NULL) {

                        newcurr->create_cv(get_parent_action(newcurr->get_tid()));
                        newcurr->create_cv(get_parent_action(newcurr->get_tid()));

+               }

        } else {
                newcurr = curr;
                /*
        } else {
                newcurr = curr;
                /*


@@ -1436,6 +1439,8 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                        //Next fix up the modification order for actions that happened
                        //after the read.
                        post_r_modification_order(read, write);
                        //Next fix up the modification order for actions that happened
                        //after the read.
                        post_r_modification_order(read, write);

+                       //Make sure the promise's value matches the write's value
+                       ASSERT(promise->get_value() == write->get_value());

 
                        promises->erase(promises->begin() + promise_index);
                        resolved = true;
 
                        promises->erase(promises->begin() + promise_index);
                        resolved = true;


@@ -1642,6 +1647,7 @@ bool ModelChecker::take_step() {
 
                        priv->nextThread = check_current_action(priv->current_action);
                        priv->current_action = NULL;
 
                        priv->nextThread = check_current_action(priv->current_action);
                        priv->current_action = NULL;

+

                        if (curr->is_blocked() || curr->is_complete())
                                scheduler->remove_thread(curr);
                } else {
                        if (curr->is_blocked() || curr->is_complete())
                                scheduler->remove_thread(curr);
                } else {

diff --git a/nodestack.cc b/nodestack.cc
index 85bbf7169248f42e580f0ff2fc6373a4b723ba96..136e3a2eb4a2f72325db5e95e5fc9205160450b2 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -324,7 +324,7 @@ const ModelAction * Node::get_read_from() {
  */
 bool Node::increment_read_from() {
        DBG();
  */
 bool Node::increment_read_from() {
        DBG();

-
+       promises.clear();

        read_from_index++;
        return (read_from_index < may_read_from.size());
 }
        read_from_index++;
        return (read_from_index < may_read_from.size());
 }


@@ -335,7 +335,7 @@ bool Node::increment_read_from() {
  */
 bool Node::increment_future_value() {
        DBG();
  */
 bool Node::increment_future_value() {
        DBG();

-
+       promises.clear();

        future_index++;
        return (future_index < future_values.size());
 }
        future_index++;
        return (future_index < future_values.size());
 }