From 718fed530a17d55ab479921e8dffebea4f98cbdf Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
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