X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=59f148ef0f6c4a7b316a970bb1024d9e6aa0ed9a;hb=247e28f81f258c3c380be00a89430186f8ac11ed;hp=726901b2c07fcf9bb9f44317ca644a565c6dc8d6;hpb=bf7f7645131e1143b7ece3a74a827ace0c7a7304;p=model-checker.git

diff --git a/model.cc b/model.cc
index 726901b..59f148e 100644
--- a/model.cc
+++ b/model.cc
@@ -250,36 +250,37 @@ ModelAction * ModelChecker::get_next_backtrack()
 void ModelChecker::check_current_action(void)
 {
 	ModelAction *curr = this->current_action;
-	ModelAction *tmp;
-	current_action = NULL;
+	bool already_added = false;
+	this->current_action = NULL;
 	if (!curr) {
 		DEBUG("trying to push NULL action...\n");
 		return;
 	}
 
-	if (curr->is_rmw()) {
-		//We have a RMW action
-		process_rmw(curr);
-		//Force the current thread to continue since the RMW should be atomic
-		nextThread = thread_current()->get_id();
-		delete curr;
-		return;
-	}
-
-	tmp = node_stack->explore_action(curr);
-	if (tmp) {
-		/* Discard duplicate ModelAction; use action from NodeStack */
+	if (curr->is_rmwc()||curr->is_rmw()) {
+		ModelAction *tmp=process_rmw(curr);
+		already_added = true;
 		delete curr;
-		curr = tmp;
+		curr=tmp;
 	} else {
-		/*
-		 * Perform one-time actions when pushing new ModelAction onto
-		 * NodeStack
-		 */
-		curr->create_cv(get_parent_action(curr->get_tid()));
-		/* Build may_read_from set */
-		if (curr->is_read())
-			build_reads_from_past(curr);
+		ModelAction * tmp = node_stack->explore_action(curr);
+		if (tmp) {
+			/* Discard duplicate ModelAction; use action from NodeStack */
+			/* First restore type and order in case of RMW operation */
+			if (curr->is_rmwr())
+				tmp->copy_typeandorder(curr);
+			delete curr;
+			curr = tmp;
+		} else {
+			/*
+			 * Perform one-time actions when pushing new ModelAction onto
+			 * NodeStack
+			 */
+			curr->create_cv(get_parent_action(curr->get_tid()));
+			/* Build may_read_from set */
+			if (curr->is_read())
+				build_reads_from_past(curr);
+		}
 	}
 
 	/* Assign 'creation' parent */
@@ -288,21 +289,6 @@ void ModelChecker::check_current_action(void)
 		th->set_creation(curr);
 	}
 
-	/* Is there a better interface for setting the next thread rather
-		 than this field/convoluted approach?  Perhaps like just returning
-		 it or something? */
-
-	nextThread = get_next_replay_thread();
-
-	Node *currnode = curr->get_node();
-	Node *parnode = currnode->get_parent();
-
-	if (!parnode->backtrack_empty()||!currnode->readsfrom_empty())
-		if (!next_backtrack || *curr > *next_backtrack)
-			next_backtrack = curr;
-
-	set_backtracking(curr);
-
 	/* Assign reads_from values */
 	Thread *th = get_thread(curr->get_tid());
 	uint64_t value = VALUE_NONE;
@@ -318,8 +304,30 @@ void ModelChecker::check_current_action(void)
 
 	th->set_return_value(value);
 
-	/* Add action to list last.  */
-	add_action_to_lists(curr);
+	/* Add action to list.  */
+	if (!already_added)
+		add_action_to_lists(curr);
+
+	/* Do not split atomic actions. */
+	if (curr->is_rmwr()) {
+		nextThread = thread_current()->get_id();
+		return;
+	}
+
+	/* Is there a better interface for setting the next thread rather
+		 than this field/convoluted approach?  Perhaps like just returning
+		 it or something? */
+
+	nextThread = get_next_replay_thread();
+
+	Node *currnode = curr->get_node();
+	Node *parnode = currnode->get_parent();
+
+	if (!parnode->backtrack_empty()||!currnode->readsfrom_empty())
+		if (!next_backtrack || *curr > *next_backtrack)
+			next_backtrack = curr;
+
+	set_backtracking(curr);
 }
 
 /** @returns whether the current trace is feasible. */
@@ -327,12 +335,14 @@ bool ModelChecker::isfeasible() {
 	return !cyclegraph->checkForCycles();
 }
 
-/** Process a RMW by converting previous read into a RMW. */
-void ModelChecker::process_rmw(ModelAction * act) {
+/** Close out a RMWR by converting previous RMWR into a RMW or READ. */
+ModelAction * ModelChecker::process_rmw(ModelAction * act) {
 	int tid = id_to_int(act->get_tid());
 	ModelAction *lastread=get_last_action(tid);
-	lastread->upgrade_rmw(act);
-	cyclegraph->addRMWEdge(lastread->get_reads_from(),lastread);
+	lastread->process_rmw(act);
+	if (act->is_rmw())
+		cyclegraph->addRMWEdge(lastread, lastread->get_reads_from());
+	return lastread;
 }
 
 /**