X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=nodestack.cc;h=addf93f67469f1cd7f96a15ffad8ec5551cb1c1b;hp=2e5a04c20cfaa5cf3dd6b73602302bf368c3c995;hb=482c7447dd2f63823eb969c37dd6fb4e22991fde;hpb=2d9c8d86e9a5050786c5f83ab6f18cd583984279

diff --git a/nodestack.cc b/nodestack.cc
index 2e5a04c..addf93f 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -1,3 +1,6 @@
+#define __STDC_FORMAT_MACROS
+#include <inttypes.h>
+
 #include <string.h>
 
 #include "nodestack.h"
@@ -5,6 +8,7 @@
 #include "common.h"
 #include "model.h"
 #include "threads-model.h"
+#include "modeltypes.h"
 
 /**
  * @brief Node constructor
@@ -38,41 +42,40 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
 	misc_index(0),
 	misc_max(0)
 {
-	if (act) {
-		act->set_node(this);
-		int currtid = id_to_int(act->get_tid());
-		int prevtid = (prevfairness != NULL) ? id_to_int(prevfairness->action->get_tid()) : 0;
-
-		if (model->params.fairwindow != 0) {
-			for (int i = 0; i < nthreads; i++) {
-				ASSERT(i < ((int)fairness.size()));
-				struct fairness_info *fi = &fairness[i];
-				struct fairness_info *prevfi = (par != NULL) && (i < par->get_num_threads()) ? &par->fairness[i] : NULL;
-				if (prevfi) {
-					*fi = *prevfi;
-				}
-				if (parent && parent->is_enabled(int_to_id(i))) {
-					fi->enabled_count++;
-				}
-				if (i == currtid) {
-					fi->turns++;
-					fi->priority = false;
-				}
-				/* Do window processing */
-				if (prevfairness != NULL) {
-					if (prevfairness->parent->is_enabled(int_to_id(i)))
-						fi->enabled_count--;
-					if (i == prevtid) {
-						fi->turns--;
-					}
-					/* Need full window to start evaluating
-					 * conditions
-					 * If we meet the enabled count and
-					 * have no turns, give us priority */
-					if ((fi->enabled_count >= model->params.enabledcount) &&
-							(fi->turns == 0))
-						fi->priority = true;
+	ASSERT(act);
+	act->set_node(this);
+	int currtid = id_to_int(act->get_tid());
+	int prevtid = prevfairness ? id_to_int(prevfairness->action->get_tid()) : 0;
+
+	if (model->params.fairwindow != 0) {
+		for (int i = 0; i < num_threads; i++) {
+			ASSERT(i < ((int)fairness.size()));
+			struct fairness_info *fi = &fairness[i];
+			struct fairness_info *prevfi = (parent && i < parent->get_num_threads()) ? &parent->fairness[i] : NULL;
+			if (prevfi) {
+				*fi = *prevfi;
+			}
+			if (parent && parent->is_enabled(int_to_id(i))) {
+				fi->enabled_count++;
+			}
+			if (i == currtid) {
+				fi->turns++;
+				fi->priority = false;
+			}
+			/* Do window processing */
+			if (prevfairness != NULL) {
+				if (prevfairness->parent->is_enabled(int_to_id(i)))
+					fi->enabled_count--;
+				if (i == prevtid) {
+					fi->turns--;
 				}
+				/* Need full window to start evaluating
+				 * conditions
+				 * If we meet the enabled count and have no
+				 * turns, give us priority */
+				if ((fi->enabled_count >= model->params.enabledcount) &&
+						(fi->turns == 0))
+					fi->priority = true;
 			}
 		}
 	}
@@ -81,25 +84,33 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
 /** @brief Node desctructor */
 Node::~Node()
 {
-	if (action)
-		delete action;
+	delete action;
 	if (enabled_array)
 		model_free(enabled_array);
 }
 
 /** Prints debugging info for the ModelAction associated with this Node */
-void Node::print()
+void Node::print() const
 {
-	if (action) {
-		action->print();
-		model_print("          backtrack: %s\n", backtrack_empty() ? "empty" : "non-empty");
-		model_print("          future values: %s\n", future_value_empty() ? "empty" : "non-empty");
-		model_print("          read-from: %s\n", read_from_empty() ? "empty" : "non-empty");
-		model_print("          promises: %s\n", promise_empty() ? "empty" : "non-empty");
-		model_print("          misc: %s\n", misc_empty() ? "empty" : "non-empty");
-		model_print("          rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty");
-	} else
-		model_print("******** empty action ********\n");
+	action->print();
+	model_print("          backtrack: %s", backtrack_empty() ? "empty" : "non-empty ");
+	for (int i = 0; i < (int)backtrack.size(); i++)
+		if (backtrack[i] == true)
+			model_print("[%d]", i);
+	model_print("\n");
+	model_print("          future values: %s", future_value_empty() ? "empty" : "non-empty ");
+	for (int i = future_index + 1; i < (int)future_values.size(); i++)
+		model_print("[%#" PRIx64 "]", future_values[i].value);
+	model_print("\n");
+
+	model_print("          read-from: %s", read_from_empty() ? "empty" : "non-empty ");
+	for (int i = read_from_index + 1; i < (int)may_read_from.size(); i++)
+		model_print("[%d]", may_read_from[i]->get_seq_number());
+	model_print("\n");
+
+	model_print("          promises: %s\n", promise_empty() ? "empty" : "non-empty");
+	model_print("          misc: %s\n", misc_empty() ? "empty" : "non-empty");
+	model_print("          rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty");
 }
 
 /** @brief Prints info about may_read_from set */
@@ -113,7 +124,8 @@ 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, bool is_rmw) {
+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) {
@@ -137,7 +149,8 @@ bool Node::get_promise(unsigned int i) const
  * Increments to the next combination of promises.
  * @return true if we have a valid combination.
  */
-bool Node::increment_promise() {
+bool Node::increment_promise()
+{
 	DBG();
 	unsigned int rmw_count = 0;
 	for (unsigned int i = 0; i < promises.size(); i++) {
@@ -151,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)
@@ -175,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;
@@ -194,7 +206,8 @@ int Node::get_misc() const
 	return misc_index;
 }
 
-bool Node::increment_misc() {
+bool Node::increment_misc()
+{
 	return (misc_index < misc_max) && ((++misc_index) < misc_max);
 }
 
@@ -203,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
@@ -214,10 +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;
@@ -237,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;
 }
 
@@ -369,29 +384,23 @@ 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
-{
-	ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
-	return future_values[future_index].value;
-}
-
-modelclock_t Node::get_future_value_expiration() const
+struct future_value Node::get_future_value() const
 {
 	ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
-	return future_values[future_index].expiration;
+	return future_values[future_index];
 }
 
-
 int Node::get_read_from_size() const
 {
 	return may_read_from.size();
 }
 
-const ModelAction * Node::get_read_from_at(int i) {
+const ModelAction * Node::get_read_from_at(int i) const
+{
 	return may_read_from[i];
 }
 
@@ -412,7 +421,8 @@ const ModelAction * Node::get_read_from() const
  * Increments the index into the readsfrom set to explore the next item.
  * @return Returns false if we have explored all items.
  */
-bool Node::increment_read_from() {
+bool Node::increment_read_from()
+{
 	DBG();
 	promises.clear();
 	if (read_from_index < may_read_from.size()) {
@@ -426,7 +436,8 @@ bool Node::increment_read_from() {
  * Increments the index into the future_values set to explore the next item.
  * @return Returns false if we have explored all values.
  */
-bool Node::increment_future_value() {
+bool Node::increment_future_value()
+{
 	DBG();
 	promises.clear();
 	if (future_index < ((int)future_values.size())) {