From: Brian Demsky <bdemsky@uci.edu>
Date: Wed, 12 Sep 2012 23:24:07 +0000 (-0700)
Subject: (1) structure code a little better
X-Git-Tag: pldi2013~216
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=a0562e0739fd643fdb2108f784f4722482ea5a4f

(1) structure code a little better
(2) add startChanges to cyclegraph...  This is just to check some assertions that rollback is being used correctly and doesn't rollback unintended changes
---

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 9256deb..f519dac 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -140,6 +140,12 @@ bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
 	return false;
 }
 
+void CycleGraph::startChanges() {
+	ASSERT(rollbackvector.size()==0);
+	ASSERT(rmwrollbackvector.size()==0);
+	ASSERT(oldCycles==hasCycles);
+}
+
 /** Commit changes to the cyclegraph. */
 void CycleGraph::commitChanges() {
 	rollbackvector.resize(0);
diff --git a/cyclegraph.h b/cyclegraph.h
index 0bb01c4..8a9bf7c 100644
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -22,6 +22,7 @@ class CycleGraph {
 	void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
 
 	bool checkReachable(const ModelAction *from, const ModelAction *to);
+	void startChanges();
 	void commitChanges();
 	void rollbackChanges();
 
diff --git a/model.cc b/model.cc
index 9611f2f..cc464a2 100644
--- a/model.cc
+++ b/model.cc
@@ -272,6 +272,8 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
 	while(true) {
 		const ModelAction *reads_from = curr->get_node()->get_read_from();
 		if (reads_from != NULL) {
+			mo_graph->startChanges();
+
 			value = reads_from->get_value();
 				/* Assign reads_from, perform release/acquire synchronization */
 			curr->read_from(reads_from);
@@ -412,23 +414,28 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 	if (!second_part_of_rmw)
 		add_action_to_lists(curr);
 
+	check_curr_backtracking(curr);
+	
+	set_backtracking(curr);
+
+	return get_next_thread(curr);
+}
+
+void ModelChecker::check_curr_backtracking(ModelAction * curr) {
 	Node *currnode = curr->get_node();
 	Node *parnode = currnode->get_parent();
-
+	
 	if ((!parnode->backtrack_empty() ||
-	                !currnode->read_from_empty() ||
-	                !currnode->future_value_empty() ||
-	                !currnode->promise_empty())
-	            && (!priv->next_backtrack ||
-	                *curr > *priv->next_backtrack)) {
+			 !currnode->read_from_empty() ||
+			 !currnode->future_value_empty() ||
+			 !currnode->promise_empty())
+			&& (!priv->next_backtrack ||
+					*curr > *priv->next_backtrack)) {
 		priv->next_backtrack = curr;
 	}
-
-	set_backtracking(curr);
-
-	return get_next_thread(curr);
 }
 
+
 bool ModelChecker::promises_expired() {
 	for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
 		Promise *promise = (*promises)[promise_index];
@@ -529,6 +536,7 @@ void ModelChecker::check_recency(ModelAction *curr, bool already_added) {
 				continue;
 
 			/* Test to see whether this is a feasible write to read from*/
+			mo_graph->startChanges();
 			r_modification_order(curr, write);
 			bool feasiblereadfrom=isfeasible();
 			mo_graph->rollbackChanges();
diff --git a/model.h b/model.h
index 1a2f6a1..bcb9d61 100644
--- a/model.h
+++ b/model.h
@@ -116,6 +116,8 @@ private:
 	bool resolve_promises(ModelAction *curr);
 	void compute_promises(ModelAction *curr);
 
+
+	void check_curr_backtracking(ModelAction * curr);
 	void add_action_to_lists(ModelAction *act);
 	ModelAction * get_last_action(thread_id_t tid);
 	ModelAction * get_last_seq_cst(const void *location);