From: Brian Demsky <bdemsky@uci.edu>
Date: Sun, 9 Sep 2012 09:25:47 +0000 (-0700)
Subject: model: some bug fixes to the model checker
X-Git-Tag: pldi2013~223^2~3
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=d4b8c4bcfb145de476c9473d80653a8849f295ed;hp=de3a9589c278417a95fa49624bbeda538f533b9b

model: some bug fixes to the model checker
---

diff --git a/model.cc b/model.cc
index 36435d9..b5a29dd 100644
--- a/model.cc
+++ b/model.cc
@@ -259,13 +259,13 @@ ModelAction * ModelChecker::get_next_backtrack()
  */
 Thread * ModelChecker::check_current_action(ModelAction *curr)
 {
-	bool already_added = false;
+	bool second_part_of_rmw = false;
 
 	ASSERT(curr);
 
 	if (curr->is_rmwc() || curr->is_rmw()) {
 		ModelAction *tmp = process_rmw(curr);
-		already_added = true;
+		second_part_of_rmw = true;
 		delete curr;
 		curr = tmp;
 	} else {
@@ -330,12 +330,12 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 				value = reads_from->get_value();
 				/* Assign reads_from, perform release/acquire synchronization */
 				curr->read_from(reads_from);
-				if (!already_added)
+				if (!second_part_of_rmw)
 					check_recency(curr,false);
 
 				bool r_status=r_modification_order(curr,reads_from);
 
-				if (!isfeasible()&&(curr->get_node()->increment_read_from()||!curr->get_node()->future_value_empty())) {
+				if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||!curr->get_node()->future_value_empty())) {
 					mo_graph->rollbackChanges();
 					too_many_reads=false;
 					continue;
@@ -366,7 +366,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 	th->set_return_value(value);
 
 	/* Add action to list.  */
-	if (!already_added)
+	if (!second_part_of_rmw)
 		add_action_to_lists(curr);
 
 	Node *currnode = curr->get_node();