X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=62e75205e4ee9681bcef321856c744978c9cc5c1;hp=47c6cdb92d442f0b0f460e353e9d25c93cfb6dc7;hb=718fed530a17d55ab479921e8dffebea4f98cbdf;hpb=d6def735e3fb70267ca802f3b1909e7ace6e4507

diff --git a/model.cc b/model.cc
index 47c6cdb9..62e75205 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 {