X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=nodestack.cc;h=addf93f67469f1cd7f96a15ffad8ec5551cb1c1b;hp=404339b6ebcf033b96b55f6b66aa4832c4dc1259;hb=24d17393dc45f60f6f6660159f2f329d1cc5d15a;hpb=3f24c24a6fd349da74351946477b85d807709410

diff --git a/nodestack.cc b/nodestack.cc
index 404339b..addf93f 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -164,7 +164,7 @@ bool Node::increment_promise()
 				//sending our value to two rmws... not going to work..try next combination
 				continue;
 			}
-			promises[i] = (promises[i] & PROMISE_RMW) |PROMISE_FULFILLED;
+			promises[i] = (promises[i] & PROMISE_RMW) | PROMISE_FULFILLED;
 			while (i > 0) {
 				i--;
 				if ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED)
@@ -188,9 +188,9 @@ bool Node::promise_empty() const
 	for (int i = promises.size() - 1; i >= 0; i--) {
 		if (promises[i] == PROMISE_UNFULFILLED)
 			return false;
-		if (!fulfilledrmw && ((promises[i]&PROMISE_MASK) == PROMISE_UNFULFILLED))
+		if (!fulfilledrmw && ((promises[i] & PROMISE_MASK) == PROMISE_UNFULFILLED))
 			return false;
-		if (promises[i] == (PROMISE_FULFILLED|PROMISE_RMW))
+		if (promises[i] == (PROMISE_FULFILLED | PROMISE_RMW))
 			fulfilledrmw = true;
 	}
 	return true;
@@ -226,12 +226,14 @@ bool Node::misc_empty() const
  * @param value is the value to backtrack to.
  * @return True if the future value was successully added; false otherwise
  */
-bool Node::add_future_value(const ModelAction *writer, modelclock_t expiration)
+bool Node::add_future_value(struct future_value& fv)
 {
-	uint64_t value = writer->get_value();
+	uint64_t value = fv.value;
+	modelclock_t expiration = fv.expiration;
+	thread_id_t tid = fv.tid;
 	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].value == value && future_values[i].tid == tid) {
 			if (expiration <= future_values[i].expiration)
 				return false;
 			idx = i;
@@ -251,8 +253,7 @@ bool Node::add_future_value(const ModelAction *writer, modelclock_t expiration)
 			(int)future_values.size() >= model->params.maxfuturevalues)
 		return false;
 
-	struct future_value newfv = {value, expiration};
-	future_values.push_back(newfv);
+	future_values.push_back(fv);
 	return true;
 }