X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.cc;h=b4f75e0336a3afdc3978b7ecb086e459423df455;hb=refs%2Ftags%2Fpldi2013;hp=22cc3784a1c75476b15c3e4378677158dc911e95;hpb=023c2e9d75b5f4460d1e079e4915b1c41a8045a4;p=model-checker.git

diff --git a/nodestack.cc b/nodestack.cc
index 22cc378..b4f75e0 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -161,21 +161,14 @@ bool Node::increment_promise() {
  * @return true if we have explored all promise combinations.
  */
 bool Node::promise_empty() {
-	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;
+	bool fulfilledrmw=false;
+	for (int i = promises.size()-1 ; i>=0; i--) {
+		if (promises[i]==PROMISE_UNFULFILLED)
 			return false;
-		} else if (promises[i] == (PROMISE_RMW|PROMISE_FULFILLED)) {
-			rmw_count--;
-		}
+		if (!fulfilledrmw && ((promises[i]&PROMISE_MASK)==PROMISE_UNFULFILLED))
+			return false;
+		if (promises[i]==(PROMISE_FULFILLED|PROMISE_RMW))
+			fulfilledrmw=true;
 	}
 	return true;
 }
@@ -199,26 +192,39 @@ bool Node::misc_empty() {
 
 
 /**
- * Adds a value from a weakly ordered future write to backtrack to.
+ * Adds a value from a weakly ordered future write to backtrack to. This
+ * operation may "fail" if the future value has already been run (within some
+ * sloppiness window of this expiration), or if the futurevalues set has
+ * reached its maximum.
+ * @see model_params.maxfuturevalues
+ *
  * @param value is the value to backtrack to.
+ * @return True if the future value was successully added; false otherwise
  */
 bool Node::add_future_value(uint64_t value, modelclock_t expiration) {
-	int suitableindex=-1;
+	int idx = -1; /* Highest index where value is found */
 	for (unsigned int i = 0; i < future_values.size(); i++) {
 		if (future_values[i].value == value) {
-			if (future_values[i].expiration>=expiration)
+			if (expiration <= future_values[i].expiration)
 				return false;
-			if (future_index < ((int) i)) {
-				suitableindex=i;
-			}
+			idx = i;
 		}
 	}
-
-	if (suitableindex!=-1) {
-		future_values[suitableindex].expiration=expiration;
+	if (idx > future_index) {
+		/* Future value hasn't been explored; update expiration */
+		future_values[idx].expiration = expiration;
 		return true;
+	} else if (idx >= 0 && expiration <= future_values[idx].expiration + model->params.expireslop) {
+		/* Future value has been explored and is within the "sloppy" window */
+		return false;
 	}
-	struct future_value newfv={value, expiration};
+
+	/* Limit the size of the future-values set */
+	if (model->params.maxfuturevalues > 0 &&
+			(int)future_values.size() >= model->params.maxfuturevalues)
+		return false;
+
+	struct future_value newfv = {value, expiration};
 	future_values.push_back(newfv);
 	return true;
 }