From: Brian Demsky <bdemsky@uci.edu>
Date: Sat, 3 Nov 2012 09:41:00 +0000 (-0700)
Subject: optimization - a given write can resolve at most one promise from a rmw
X-Git-Tag: pldi2013~13^2~5
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=023c2e9d75b5f4460d1e079e4915b1c41a8045a4;hp=202542965363285e68bb33654a62fe816c69b176

optimization - a given write can resolve at most one promise from a rmw
---

diff --git a/model.cc b/model.cc
index 1ec7273..1e730d7 100644
--- a/model.cc
+++ b/model.cc
@@ -1839,7 +1839,7 @@ void ModelChecker::compute_promises(ModelAction *curr)
 				!act->same_thread(curr) &&
 				act->get_location() == curr->get_location() &&
 				promise->get_value() == curr->get_value()) {
-			curr->get_node()->set_promise(i);
+			curr->get_node()->set_promise(i, act->is_rmw());
 		}
 	}
 }
diff --git a/nodestack.cc b/nodestack.cc
index d08fa5c..22cc378 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -105,11 +105,14 @@ void Node::print_may_read_from()
  * Sets a promise to explore meeting with the given node.
  * @param i is the promise index.
  */
-void Node::set_promise(unsigned int i) {
+void Node::set_promise(unsigned int i, bool is_rmw) {
 	if (i >= promises.size())
 		promises.resize(i + 1, PROMISE_IGNORE);
-	if (promises[i] == PROMISE_IGNORE)
+	if (promises[i] == PROMISE_IGNORE) {
 		promises[i] = PROMISE_UNFULFILLED;
+		if (is_rmw)
+			promises[i] |= PROMISE_RMW;
+	}
 }
 
 /**
@@ -118,7 +121,7 @@ void Node::set_promise(unsigned int i) {
  * @return true if the promise should be satisfied by the given model action.
  */
 bool Node::get_promise(unsigned int i) {
-	return (i < promises.size()) && (promises[i] == PROMISE_FULFILLED);
+	return (i < promises.size()) && ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED);
 }
 
 /**
@@ -127,16 +130,27 @@ bool Node::get_promise(unsigned int i) {
  */
 bool Node::increment_promise() {
 	DBG();
-
+	unsigned int rmw_count=0;
 	for (unsigned int i = 0; i < promises.size(); i++) {
-		if (promises[i] == PROMISE_UNFULFILLED) {
-			promises[i] = PROMISE_FULFILLED;
+		if (promises[i]==(PROMISE_RMW|PROMISE_FULFILLED))
+			rmw_count++;
+	}
+	
+	for (unsigned int i = 0; i < promises.size(); i++) {
+		if ((promises[i] & PROMISE_MASK) == PROMISE_UNFULFILLED) {
+			if ((rmw_count > 0) && (promises[i] & PROMISE_RMW)) {
+				//sending our value to two rmws... not going to work..try next combination
+				continue;
+			}
+			promises[i] = (promises[i] & PROMISE_RMW) |PROMISE_FULFILLED;
 			while (i > 0) {
 				i--;
-				if (promises[i] == PROMISE_FULFILLED)
-					promises[i] = PROMISE_UNFULFILLED;
+				if ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED)
+					promises[i] = (promises[i] & PROMISE_RMW) | PROMISE_UNFULFILLED;
 			}
 			return true;
+		} else if (promises[i] == (PROMISE_RMW|PROMISE_FULFILLED)) {
+			rmw_count--;
 		}
 	}
 	return false;
@@ -147,9 +161,22 @@ bool Node::increment_promise() {
  * @return true if we have explored all promise combinations.
  */
 bool Node::promise_empty() {
-	for (unsigned int i = 0; i < promises.size();i++)
-		if (promises[i] == PROMISE_UNFULFILLED)
+	unsigned int rmw_count=0;
+	for (unsigned int i = 0; i < promises.size(); i++) {
+		if (promises[i]==(PROMISE_RMW|PROMISE_FULFILLED))
+			rmw_count++;
+	}
+
+	for (unsigned int i = 0; i < promises.size();i++) {
+		if ((promises[i]& PROMISE_MASK) == PROMISE_UNFULFILLED) {
+			//if this isn't a feasible option, keep going
+			if ((rmw_count > 0)&&(promises[i] & PROMISE_RMW))
+				continue;
 			return false;
+		} else if (promises[i] == (PROMISE_RMW|PROMISE_FULFILLED)) {
+			rmw_count--;
+		}
+	}
 	return true;
 }
 
diff --git a/nodestack.h b/nodestack.h
index 648ef4d..986b9c9 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -24,11 +24,14 @@ class Thread;
  * <li>@b fulfilled: satisfied by this Node's ModelAction under the current
  * configuration.</li></ol>
  */
-typedef enum {
-	PROMISE_IGNORE = 0, /**< This promise is inapplicable; ignore it */
-	PROMISE_UNFULFILLED, /**< This promise is applicable but unfulfilled */
-	PROMISE_FULFILLED /**< This promise is applicable and fulfilled */
-} promise_t;
+
+#define	PROMISE_IGNORE 0 /**< This promise is inapplicable; ignore it */
+#define	PROMISE_UNFULFILLED 1 /**< This promise is applicable but unfulfilled */
+#define	PROMISE_FULFILLED 2 /**< This promise is applicable and fulfilled */
+#define PROMISE_MASK 0xf
+#define PROMISE_RMW 0x10
+
+typedef int promise_t;
 
 struct future_value {
 	uint64_t value;
@@ -88,7 +91,7 @@ public:
 	int get_read_from_size();
 	const ModelAction * get_read_from_at(int i);
 
-	void set_promise(unsigned int i);
+	void set_promise(unsigned int i, bool is_rmw);
 	bool get_promise(unsigned int i);
 	bool increment_promise();
 	bool promise_empty();