From 718fed530a17d55ab479921e8dffebea4f98cbdf Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Mon, 1 Oct 2012 15:17:11 -0700 Subject: [PATCH] bug fix...recompute promises of RMW actions at divergence points --- model.cc | 10 ++++++++-- nodestack.cc | 4 ++-- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/model.cc b/model.cc index 47c6cdb..62e7520 100644 --- 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; - compute_promises(newcurr); + + if (newcurr->is_rmw()) + compute_promises(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. */ - if (diverge == NULL) + if (diverge == NULL) { newcurr->create_cv(get_parent_action(newcurr->get_tid())); + } } 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); + //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; @@ -1642,6 +1647,7 @@ bool ModelChecker::take_step() { priv->nextThread = check_current_action(priv->current_action); priv->current_action = NULL; + if (curr->is_blocked() || curr->is_complete()) scheduler->remove_thread(curr); } else { diff --git a/nodestack.cc b/nodestack.cc index 85bbf71..136e3a2 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -324,7 +324,7 @@ const ModelAction * Node::get_read_from() { */ bool Node::increment_read_from() { DBG(); - + promises.clear(); 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(); - + promises.clear(); future_index++; return (future_index < future_values.size()); } -- 2.34.1