X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=nodestack.cc;h=00cc30f8d7efb22cf9e5b110d4628ac83db55e0f;hp=10115af6090f964793132e2656ecc9941f07cdc1;hb=9eee54de6cd97a5a58f3185de0c4635123d398b2;hpb=ee745811958143fe03e854709a649c2954dd6d16

diff --git a/nodestack.cc b/nodestack.cc
index 10115af..00cc30f 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -24,8 +24,9 @@
  * @param nthreads The number of threads which exist at this point in the
  * execution trace.
  */
-Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
-	: action(act),
+Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) :
+	read_from_status(READ_FROM_PAST),
+	action(act),
 	parent(par),
 	num_threads(nthreads),
 	explored_children(num_threads),
@@ -35,8 +36,12 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
 	enabled_array(NULL),
 	read_from_past(),
 	read_from_past_idx(0),
+	read_from_promises(),
+	read_from_promise_idx(-1),
 	future_values(),
 	future_index(-1),
+	resolve_promise(),
+	resolve_promise_idx(-1),
 	relseq_break_writes(),
 	relseq_break_index(0),
 	misc_index(0),
@@ -98,83 +103,65 @@ void Node::print() const
 		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_past_empty() ? "empty" : "non-empty ");
+	model_print("          read from past: %s", read_from_past_empty() ? "empty" : "non-empty ");
 	for (int i = read_from_past_idx + 1; i < (int)read_from_past.size(); i++)
 		model_print("[%d]", read_from_past[i]->get_seq_number());
 	model_print("\n");
 
+	model_print("          read-from promises: %s", read_from_promise_empty() ? "empty" : "non-empty ");
+	for (int i = read_from_promise_idx + 1; i < (int)read_from_promises.size(); i++)
+		model_print("[%d]", read_from_promises[i]->get_seq_number());
+	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("          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 read_from_past set */
-void Node::print_read_from_past()
-{
-	for (unsigned int i = 0; i < read_from_past.size(); i++)
-		read_from_past[i]->print();
-}
+/*********************************** promise **********************************/
 
 /**
  * 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)
-{
-	if (i >= promises.size())
-		promises.resize(i + 1, PROMISE_IGNORE);
-	if (promises[i] == PROMISE_IGNORE) {
-		promises[i] = PROMISE_UNFULFILLED;
-		if (is_rmw)
-			promises[i] |= PROMISE_RMW;
-	}
+void Node::set_promise(unsigned int i)
+{
+	if (i >= resolve_promise.size())
+		resolve_promise.resize(i + 1, false);
+	resolve_promise[i] = true;
 }
 
 /**
  * Looks up whether a given promise should be satisfied by this node.
  * @param i The promise index.
- * @return true if the promise should be satisfied by the given model action.
+ * @return true if the promise should be satisfied by the given ModelAction.
  */
 bool Node::get_promise(unsigned int i) const
 {
-	return (i < promises.size()) && ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED);
+	return (i < resolve_promise.size()) && (int)i == resolve_promise_idx;
 }
 
 /**
- * Increments to the next combination of promises.
+ * Increments to the next promise to resolve.
  * @return true if we have a valid combination.
  */
 bool Node::increment_promise()
 {
 	DBG();
-	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 ((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_MASK) == PROMISE_FULFILLED)
-					promises[i] = (promises[i] & PROMISE_RMW) | PROMISE_UNFULFILLED;
-			}
+	if (resolve_promise.empty())
+		return false;
+	int prev_idx = resolve_promise_idx;
+	resolve_promise_idx++;
+	for ( ; resolve_promise_idx < (int)resolve_promise.size(); resolve_promise_idx++)
+		if (resolve_promise[resolve_promise_idx])
 			return true;
-		} else if (promises[i] == (PROMISE_RMW|PROMISE_FULFILLED)) {
-			rmw_count--;
-		}
-	}
+	resolve_promise_idx = prev_idx;
 	return false;
 }
 
@@ -184,18 +171,21 @@ bool Node::increment_promise()
  */
 bool Node::promise_empty() const
 {
-	bool fulfilledrmw = false;
-	for (int i = promises.size() - 1; i >= 0; i--) {
-		if (promises[i] == PROMISE_UNFULFILLED)
+	for (int i = resolve_promise_idx + 1; i < (int)resolve_promise.size(); i++)
+		if (i >= 0 && resolve_promise[i])
 			return false;
-		if (!fulfilledrmw && ((promises[i] & PROMISE_MASK) == PROMISE_UNFULFILLED))
-			return false;
-		if (promises[i] == (PROMISE_FULFILLED | PROMISE_RMW))
-			fulfilledrmw = true;
-	}
 	return true;
 }
 
+/** @brief Clear any promise-resolution information for this Node */
+void Node::clear_promise_resolutions()
+{
+	resolve_promise.clear();
+	resolve_promise_idx = -1;
+}
+
+/******************************* end promise **********************************/
+
 void Node::set_misc_max(int i)
 {
 	misc_max = i;
@@ -216,56 +206,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
- * 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(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 && future_values[i].tid == tid) {
-			if (expiration <= future_values[i].expiration)
-				return false;
-			idx = i;
-		}
-	}
-	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;
-	}
-
-	/* Limit the size of the future-values set */
-	if (model->params.maxfuturevalues > 0 &&
-			(int)future_values.size() >= model->params.maxfuturevalues)
-		return false;
-
-	future_values.push_back(fv);
-	return true;
-}
-
-/**
- * Checks whether the future_values set for this node is empty.
- * @return true if the future_values set is empty.
- */
-bool Node::future_value_empty() const
-{
-	return ((future_index + 1) >= ((int)future_values.size()));
-}
-
 /**
  * Checks if the Thread associated with this thread ID has been explored from
  * this Node already.
@@ -288,15 +228,6 @@ bool Node::backtrack_empty() const
 	return (numBacktracks == 0);
 }
 
-/**
- * Checks whether the readsfrom set for this node is empty.
- * @return true if the readsfrom set is empty.
- */
-bool Node::read_from_past_empty() const
-{
-	return ((read_from_past_idx + 1) >= read_from_past.size());
-}
-
 /**
  * Mark the appropriate backtracking information for exploring a thread choice.
  * @param act The ModelAction to explore
@@ -354,6 +285,7 @@ void Node::clear_backtracking()
 		backtrack[i] = false;
 	for (unsigned int i = 0; i < explored_children.size(); i++)
 		explored_children[i] = false;
+	numBacktracks = 0;
 }
 
 bool Node::is_enabled(Thread *t) const
@@ -382,34 +314,81 @@ bool Node::has_priority(thread_id_t tid) const
 	return fairness[id_to_int(tid)].priority;
 }
 
+/*********************************** read from ********************************/
+
 /**
- * Add an action to the read_from_past set.
- * @param act is the action to add
+ * Get the current state of the may-read-from set iteration
+ * @return The read-from type we should currently be checking (past or future)
  */
-void Node::add_read_from_past(const ModelAction *act)
+read_from_type_t Node::get_read_from_status()
 {
-	read_from_past.push_back(act);
+	if (read_from_status == READ_FROM_PAST && read_from_past.empty())
+		increment_read_from();
+	return read_from_status;
 }
 
 /**
- * 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
+ * Iterate one step in the may-read-from iteration. This includes a step in
+ * reading from the either the past or the future.
+ * @return True if there is a new read-from to explore; false otherwise
  */
-struct future_value Node::get_future_value() const
+bool Node::increment_read_from()
+{
+	clear_promise_resolutions();
+	if (increment_read_from_past()) {
+	       read_from_status = READ_FROM_PAST;
+	       return true;
+	} else if (increment_read_from_promise()) {
+		read_from_status = READ_FROM_PROMISE;
+		return true;
+	} else if (increment_future_value()) {
+		read_from_status = READ_FROM_FUTURE;
+		return true;
+	}
+	read_from_status = READ_FROM_NONE;
+	return false;
+}
+
+/**
+ * @return True if there are any new read-froms to explore
+ */
+bool Node::read_from_empty() const
 {
-	ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
-	return future_values[future_index];
+	return read_from_past_empty() &&
+		read_from_promise_empty() &&
+		future_value_empty();
 }
 
-int Node::get_read_from_past_size() const
+/**
+ * Get the total size of the may-read-from set, including both past and future
+ * values
+ * @return The size of may-read-from
+ */
+unsigned int Node::read_from_size() const
 {
-	return read_from_past.size();
+	return read_from_past.size() +
+		read_from_promises.size() +
+		future_values.size();
 }
 
-const ModelAction * Node::get_read_from_past(int i) const
+/******************************* end read from ********************************/
+
+/****************************** read from past ********************************/
+
+/** @brief Prints info about read_from_past set */
+void Node::print_read_from_past()
 {
-	return read_from_past[i];
+	for (unsigned int i = 0; i < read_from_past.size(); i++)
+		read_from_past[i]->print();
+}
+
+/**
+ * Add an action to the read_from_past set.
+ * @param act is the action to add
+ */
+void Node::add_read_from_past(const ModelAction *act)
+{
+	read_from_past.push_back(act);
 }
 
 /**
@@ -425,6 +404,25 @@ const ModelAction * Node::get_read_from_past() const
 		return NULL;
 }
 
+const ModelAction * Node::get_read_from_past(int i) const
+{
+	return read_from_past[i];
+}
+
+int Node::get_read_from_past_size() const
+{
+	return read_from_past.size();
+}
+
+/**
+ * Checks whether the readsfrom set for this node is empty.
+ * @return true if the readsfrom set is empty.
+ */
+bool Node::read_from_past_empty() const
+{
+	return ((read_from_past_idx + 1) >= read_from_past.size());
+}
+
 /**
  * Increments the index into the readsfrom set to explore the next item.
  * @return Returns false if we have explored all items.
@@ -432,7 +430,6 @@ const ModelAction * Node::get_read_from_past() const
 bool Node::increment_read_from_past()
 {
 	DBG();
-	promises.clear();
 	if (read_from_past_idx < read_from_past.size()) {
 		read_from_past_idx++;
 		return read_from_past_idx < read_from_past.size();
@@ -440,6 +437,120 @@ bool Node::increment_read_from_past()
 	return false;
 }
 
+/************************** end read from past ********************************/
+
+/***************************** read_from_promises *****************************/
+
+/**
+ * Add an action to the read_from_promises set.
+ * @param reader The read which generated the Promise; we use the ModelAction
+ * instead of the Promise because the Promise does not last across executions
+ */
+void Node::add_read_from_promise(const ModelAction *reader)
+{
+	read_from_promises.push_back(reader);
+}
+
+/**
+ * Gets the next 'read-from-promise' from this Node. Only valid for a node
+ * where this->action is a 'read'.
+ * @return The current element in read_from_promises
+ */
+Promise * Node::get_read_from_promise() const
+{
+	if (read_from_promise_idx < 0 || read_from_promise_idx >= ((int)read_from_promises.size()))
+		return NULL;
+	return read_from_promises[read_from_promise_idx]->get_reads_from_promise();
+}
+
+/**
+ * Checks whether the read_from_promises set for this node is empty.
+ * @return true if the read_from_promises set is empty.
+ */
+bool Node::read_from_promise_empty() const
+{
+	return ((read_from_promise_idx + 1) >= ((int)read_from_promises.size()));
+}
+
+/**
+ * Increments the index into the read_from_promises set to explore the next item.
+ * @return Returns false if we have explored all promises.
+ */
+bool Node::increment_read_from_promise()
+{
+	DBG();
+	if (read_from_promise_idx < ((int)read_from_promises.size())) {
+		read_from_promise_idx++;
+		return (read_from_promise_idx < ((int)read_from_promises.size()));
+	}
+	return false;
+}
+
+/************************* end read_from_promises *****************************/
+
+/****************************** future values *********************************/
+
+/**
+ * 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(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 && future_values[i].tid == tid) {
+			if (expiration <= future_values[i].expiration)
+				return false;
+			idx = i;
+		}
+	}
+	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;
+	}
+
+	/* Limit the size of the future-values set */
+	if (model->params.maxfuturevalues > 0 &&
+			(int)future_values.size() >= model->params.maxfuturevalues)
+		return false;
+
+	future_values.push_back(fv);
+	return true;
+}
+
+/**
+ * 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
+ */
+struct future_value Node::get_future_value() const
+{
+	ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
+	return future_values[future_index];
+}
+
+/**
+ * Checks whether the future_values set for this node is empty.
+ * @return true if the future_values set is empty.
+ */
+bool Node::future_value_empty() const
+{
+	return ((future_index + 1) >= ((int)future_values.size()));
+}
+
 /**
  * Increments the index into the future_values set to explore the next item.
  * @return Returns false if we have explored all values.
@@ -447,7 +558,6 @@ bool Node::increment_read_from_past()
 bool Node::increment_future_value()
 {
 	DBG();
-	promises.clear();
 	if (future_index < ((int)future_values.size())) {
 		future_index++;
 		return (future_index < ((int)future_values.size()));
@@ -455,6 +565,8 @@ bool Node::increment_future_value()
 	return false;
 }
 
+/************************** end future values *********************************/
+
 /**
  * Add a write ModelAction to the set of writes that may break the release
  * sequence. This is used during replay exploration of pending release
@@ -491,7 +603,6 @@ const ModelAction * Node::get_relseq_break() const
 bool Node::increment_relseq_break()
 {
 	DBG();
-	promises.clear();
 	if (relseq_break_index < ((int)relseq_break_writes.size())) {
 		relseq_break_index++;
 		return (relseq_break_index < ((int)relseq_break_writes.size()));