From: Brian Demsky <bdemsky@uci.edu>
Date: Thu, 13 Sep 2012 03:35:47 +0000 (-0700)
Subject: separate out rmw actions
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=0cb05db166b91ab2820fd8c58b6903ca3a455e04;p=cdsspec-compiler.git

separate out rmw actions
make sure we don't insert promises twice for a node
---

diff --git a/Makefile b/Makefile
index 2acdbc7..67b6e6d 100644
--- a/Makefile
+++ b/Makefile
@@ -25,7 +25,7 @@ include $(DEPS)
 debug: CPPFLAGS += -DCONFIG_DEBUG
 debug: all
 
-mac: CPPFLAGS += -D_XOPEN_SOURCE -DMAC
+mac: CPPFLAGS += -D_XOPEN_SOURCE -DMAC -DCONFIG_DEBUG
 mac: LDFLAGS=-ldl
 mac: SHARED=-Wl,-undefined,dynamic_lookup -dynamiclib
 mac: all
diff --git a/cyclegraph.cc b/cyclegraph.cc
index f519dac..2bac4de 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -5,7 +5,9 @@
 /** Initializes a CycleGraph object. */
 CycleGraph::CycleGraph() :
 	hasCycles(false),
-	oldCycles(false)
+	oldCycles(false),
+	hasRMWViolation(false),
+	oldRMWViolation(false)
 {
 }
 
@@ -77,7 +79,7 @@ void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
 
 	/* Two RMW actions cannot read from the same write. */
 	if (fromnode->setRMW(rmwnode)) {
-		hasCycles=true;
+		hasRMWViolation=true;
 	} else {
 		rmwrollbackvector.push_back(fromnode);
 	}
@@ -144,6 +146,7 @@ void CycleGraph::startChanges() {
 	ASSERT(rollbackvector.size()==0);
 	ASSERT(rmwrollbackvector.size()==0);
 	ASSERT(oldCycles==hasCycles);
+	ASSERT(oldRMWViolation==hasRMWViolation);
 }
 
 /** Commit changes to the cyclegraph. */
@@ -151,6 +154,7 @@ void CycleGraph::commitChanges() {
 	rollbackvector.resize(0);
 	rmwrollbackvector.resize(0);
 	oldCycles=hasCycles;
+	oldRMWViolation=hasRMWViolation;
 }
 
 /** Rollback changes to the previous commit. */
@@ -164,6 +168,7 @@ void CycleGraph::rollbackChanges() {
 	}
 
 	hasCycles = oldCycles;
+	hasRMWViolation = oldRMWViolation;
 	rollbackvector.resize(0);
 	rmwrollbackvector.resize(0);
 }
@@ -173,6 +178,10 @@ bool CycleGraph::checkForCycles() {
 	return hasCycles;
 }
 
+bool CycleGraph::checkForRMWViolation() {
+	return hasRMWViolation;
+}
+
 /**
  * Constructor for a CycleNode.
  * @param modelaction The ModelAction for this node
diff --git a/cyclegraph.h b/cyclegraph.h
index 8a9bf7c..013a11a 100644
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -19,6 +19,7 @@ class CycleGraph {
 	~CycleGraph();
 	void addEdge(const ModelAction *from, const ModelAction *to);
 	bool checkForCycles();
+	bool checkForRMWViolation();
 	void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
 
 	bool checkReachable(const ModelAction *from, const ModelAction *to);
@@ -36,9 +37,11 @@ class CycleGraph {
 
 	/** @brief A flag: true if this graph contains cycles */
 	bool hasCycles;
-
 	bool oldCycles;
 
+	bool hasRMWViolation;
+	bool oldRMWViolation;
+
 	std::vector<CycleNode *> rollbackvector;
 	std::vector<CycleNode *> rmwrollbackvector;
 };
diff --git a/model.cc b/model.cc
index cc464a2..bd4ade2 100644
--- a/model.cc
+++ b/model.cc
@@ -291,7 +291,7 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
 
 			mo_graph->commitChanges();
 			updated |= r_status;
-		} else {
+		} else if (!second_part_of_rmw) {
 			/* Read from future value */
 			value = curr->get_node()->get_future_value();
 			modelclock_t expiration = curr->get_node()->get_future_value_expiration();
@@ -454,6 +454,11 @@ bool ModelChecker::isfeasibleprefix() {
 
 /** @returns whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
+	return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
+}
+
+/** @returns whether the current partial trace is feasible. */
+bool ModelChecker::isfeasibleotherthanRMW() {
 	return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
 }
 
@@ -704,9 +709,14 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 				   =>
 				   that read could potentially read from our write.
 				 */
-				if (isfeasible() && act->get_node()->add_future_value(curr->get_value(), curr->get_seq_number()+params.maxfuturedelay) &&
-						(!priv->next_backtrack || *act > *priv->next_backtrack))
-					priv->next_backtrack = act;
+				if (thin_air_constraint_may_allow(curr, act)) {
+					if (isfeasible() ||
+							(curr->is_rmw() && act->is_rmw() && curr->get_reads_from()==act->get_reads_from() && isfeasibleotherthanRMW())) {
+						if (act->get_node()->add_future_value(curr->get_value(), curr->get_seq_number()+params.maxfuturedelay) &&
+								(!priv->next_backtrack || *act > *priv->next_backtrack))
+							priv->next_backtrack = act;
+					}
+				}
 			}
 		}
 	}
@@ -714,6 +724,29 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 	return added;
 }
 
+/** Arbitrary reads from the future are not allowed.  Section 29.3
+ * part 9 places some constraints.  This method checks one result of constraint
+ * constraint.  Others require compiler support. */
+
+bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader) {
+	if (!writer->is_rmw())
+		return true;
+
+	if (!reader->is_rmw())
+		return true;
+
+	for(const ModelAction *search=writer->get_reads_from();search!=NULL;search=search->get_reads_from()) {
+		if (search==reader)
+			return false;
+		if (search->get_tid()==reader->get_tid()&&
+				search->happens_before(reader))
+			break;
+	}
+
+	return true;
+}
+
+
 /**
  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
  * The ModelAction under consideration is expected to be taking part in
@@ -988,6 +1021,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid)
 bool ModelChecker::resolve_promises(ModelAction *write)
 {
 	bool resolved = false;
+
 	for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
 		Promise *promise = (*promises)[promise_index];
 		if (write->get_node()->get_promise(i)) {
@@ -1003,7 +1037,6 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 		} else
 			promise_index++;
 	}
-
 	return resolved;
 }
 
@@ -1193,6 +1226,7 @@ bool ModelChecker::take_step() {
 	if (curr) {
 		if (curr->get_state() == THREAD_READY) {
 			ASSERT(priv->current_action);
+
 			priv->nextThread = check_current_action(priv->current_action);
 			priv->current_action = NULL;
 			if (!curr->is_blocked() && !curr->is_complete())
diff --git a/model.h b/model.h
index bcb9d61..fec8d1f 100644
--- a/model.h
+++ b/model.h
@@ -75,11 +75,11 @@ public:
 	ModelAction * get_parent_action(thread_id_t tid);
 	bool next_execution();
 	bool isfeasible();
+	bool isfeasibleotherthanRMW();
 	bool isfinalfeasible();
 	void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
 	void get_release_seq_heads(ModelAction *act,
 	                std::vector<const ModelAction *> *release_heads);
-
 	void finish_execution();
 	bool isfeasibleprefix();
 	void set_assert() {asserted=true;}
@@ -88,7 +88,8 @@ public:
 private:
 	/** The scheduler to use: tracks the running/ready Threads */
 	Scheduler *scheduler;
-
+	
+	bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
 	bool has_asserted() {return asserted;}
 	void reset_asserted() {asserted=false;}
 	int num_executions;