X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.cc;h=b2ef73cac30108fab56745f89b0542a186fc6410;hb=09c3eb5539455e82dcb357fbce82bf5974c3a37c;hp=ccf79e40ea99b3726cbe092e6f0942b7659c61cb;hpb=46c83c24286f22d49b1e7879925869304c4bdf7a;p=model-checker.git

diff --git a/nodestack.cc b/nodestack.cc
index ccf79e4..b2ef73c 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -8,6 +8,7 @@
 #include "common.h"
 #include "model.h"
 #include "threads-model.h"
+#include "modeltypes.h"
 
 /**
  * @brief Node constructor
@@ -89,7 +90,7 @@ Node::~Node()
 }
 
 /** Prints debugging info for the ModelAction associated with this Node */
-void Node::print()
+void Node::print() const
 {
 	action->print();
 	model_print("          backtrack: %s", backtrack_empty() ? "empty" : "non-empty ");
@@ -163,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)
@@ -187,15 +188,14 @@ 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;
 }
 
-
 void Node::set_misc_max(int i)
 {
 	misc_max = i;
@@ -216,7 +216,6 @@ bool Node::misc_empty() const
 	return (misc_index + 1) >= misc_max;
 }
 
-
 /**
  * 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
@@ -227,11 +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(uint64_t value, modelclock_t expiration)
+bool Node::add_future_value(struct future_value& fv)
 {
+	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(uint64_t value, 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;
 }
 
@@ -383,23 +384,16 @@ void Node::add_read_from(const ModelAction *act)
 }
 
 /**
- * Gets the next 'future_value' value from this Node. Only valid for a node
- * where this->action is a 'read'.
+ * Gets the next 'future_value' from this Node. Only valid for a node where
+ * this->action is a 'read'.
  * @return The first element in future_values
  */
-uint64_t Node::get_future_value() const
+struct future_value Node::get_future_value() const
 {
 	ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
-	return future_values[future_index].value;
+	return future_values[future_index];
 }
 
-modelclock_t Node::get_future_value_expiration() const
-{
-	ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
-	return future_values[future_index].expiration;
-}
-
-
 int Node::get_read_from_size() const
 {
 	return may_read_from.size();
@@ -562,7 +556,11 @@ ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_ena
 		if (model->params.fairwindow != 0 && head_idx > (int)model->params.fairwindow)
 			prevfairness = node_list[head_idx - model->params.fairwindow];
 	}
-	node_list.push_back(new Node(act, head, model->get_num_threads(), prevfairness));
+
+	int next_threads = model->get_num_threads();
+	if (act->get_type() == THREAD_CREATE)
+		next_threads++;
+	node_list.push_back(new Node(act, head, next_threads, prevfairness));
 	total_nodes++;
 	head_idx++;
 	return NULL;