X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.cc;h=b9142435c5267f276d10ed9b9c5c315801bfd6f7;hb=02558d484765370cd00ff15008412aa4a15eea11;hp=3cde3456bb9363bc08f2549035166b6f7fe3bd15;hpb=7bd9b5a1446863dc1a9de9683476f5a480dfba91;p=model-checker.git

diff --git a/nodestack.cc b/nodestack.cc
index 3cde345..b914243 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -27,6 +27,7 @@
 Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) :
 	read_from_status(READ_FROM_PAST),
 	action(act),
+	uninit_action(NULL),
 	parent(par),
 	num_threads(nthreads),
 	explored_children(num_threads),
@@ -40,10 +41,13 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) :
 	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),
-	misc_max(0)
+	misc_max(0),
+	yield_data(NULL)
 {
 	ASSERT(act);
 	act->set_node(this);
@@ -84,18 +88,82 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) :
 	}
 }
 
+int Node::get_yield_data(int tid1, int tid2) const {
+	if (tid1<num_threads && tid2 < num_threads)
+		return yield_data[YIELD_INDEX(tid1,tid2,num_threads)];
+	else
+		return YIELD_S | YIELD_D;
+}
+
+void Node::update_yield(Scheduler * scheduler) {
+	if (yield_data==NULL)
+		yield_data=(int *) model_calloc(1, sizeof(int)*num_threads*num_threads);
+	//handle base case
+	if (parent == NULL) {
+		for(int i = 0; i < num_threads*num_threads; i++) {
+			yield_data[i] = YIELD_S | YIELD_D;
+		}
+		return;
+	}
+	int curr_tid=id_to_int(action->get_tid());
+
+	for(int u = 0; u < num_threads; u++) {
+		for(int v = 0; v < num_threads; v++) {
+			int yield_state=parent->get_yield_data(u, v);
+			bool next_enabled=scheduler->is_enabled(int_to_id(v));
+			bool curr_enabled=parent->is_enabled(int_to_id(v));
+			if (!next_enabled) {
+				//Compute intersection of ES and E
+				yield_state&=~YIELD_E;
+				//Check to see if we disabled the thread
+				if (u==curr_tid && curr_enabled)
+					yield_state|=YIELD_D;
+			}
+			yield_data[YIELD_INDEX(u, v, num_threads)]=yield_state;
+		}
+		yield_data[YIELD_INDEX(u, curr_tid, num_threads)]=(yield_data[YIELD_INDEX(u, curr_tid, num_threads)]&~YIELD_P)|YIELD_S;
+	}
+	//handle curr.yield(t) part of computation
+	if (action->is_yield()) {
+		for(int v = 0; v < num_threads; v++) {
+			int yield_state=yield_data[YIELD_INDEX(curr_tid, v, num_threads)];
+			if ((yield_state & (YIELD_E | YIELD_D)) && (!(yield_state & YIELD_S)))
+				yield_state |= YIELD_P;
+			yield_state &= YIELD_P;
+			if (scheduler->is_enabled(int_to_id(v))) {
+				yield_state|=YIELD_E;
+			}
+			yield_data[YIELD_INDEX(curr_tid, v, num_threads)]=yield_state;
+		}
+	}
+}
+
 /** @brief Node desctructor */
 Node::~Node()
 {
 	delete action;
+	if (uninit_action)
+		delete uninit_action;
 	if (enabled_array)
 		model_free(enabled_array);
+	if (yield_data)
+		model_free(yield_data);
 }
 
 /** Prints debugging info for the ModelAction associated with this Node */
 void Node::print() const
 {
 	action->print();
+	model_print("          thread status: ");
+	if (enabled_array) {
+		for (int i = 0; i < num_threads; i++) {
+			char str[20];
+			enabled_type_to_string(enabled_array[i], str);
+			model_print("[%d: %s]", i, str);
+		}
+		model_print("\n");
+	} else
+		model_print("(info not available)\n");
 	model_print("          backtrack: %s", backtrack_empty() ? "empty" : "non-empty ");
 	for (int i = 0; i < (int)backtrack.size(); i++)
 		if (backtrack[i] == true)
@@ -122,61 +190,44 @@ void Node::print() const
 	model_print("          rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty");
 }
 
+/*********************************** 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;
 }
 
@@ -186,18 +237,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)
-			return false;
-		if (!fulfilledrmw && ((promises[i] & PROMISE_MASK) == PROMISE_UNFULFILLED))
+	for (int i = resolve_promise_idx + 1; i < (int)resolve_promise.size(); i++)
+		if (i >= 0 && resolve_promise[i])
 			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;
@@ -297,6 +351,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
@@ -325,6 +380,11 @@ bool Node::has_priority(thread_id_t tid) const
 	return fairness[id_to_int(tid)].priority;
 }
 
+bool Node::has_priority_over(thread_id_t tid1, thread_id_t tid2) const
+{
+	return get_yield_data(id_to_int(tid1), id_to_int(tid2)) & YIELD_P;
+}
+
 /*********************************** read from ********************************/
 
 /**
@@ -345,7 +405,7 @@ read_from_type_t Node::get_read_from_status()
  */
 bool Node::increment_read_from()
 {
-	promises.clear();
+	clear_promise_resolutions();
 	if (increment_read_from_past()) {
 	       read_from_status = READ_FROM_PAST;
 	       return true;
@@ -365,7 +425,9 @@ bool Node::increment_read_from()
  */
 bool Node::read_from_empty() const
 {
-	return read_from_past_empty() && future_value_empty();
+	return read_from_past_empty() &&
+		read_from_promise_empty() &&
+		future_value_empty();
 }
 
 /**
@@ -375,7 +437,9 @@ bool Node::read_from_empty() const
  */
 unsigned int Node::read_from_size() const
 {
-	return read_from_past.size() + future_values.size();
+	return read_from_past.size() +
+		read_from_promises.size() +
+		future_values.size();
 }
 
 /******************************* end read from ********************************/
@@ -463,13 +527,30 @@ void Node::add_read_from_promise(const ModelAction *reader)
  * where this->action is a 'read'.
  * @return The current element in read_from_promises
  */
-const Promise * Node::get_read_from_promise() const
+Promise * Node::get_read_from_promise() const
 {
-	if (read_from_promise_idx < 0 || read_from_promise_idx >= ((int)read_from_promises.size()))
-		return NULL;
+	ASSERT(read_from_promise_idx >= 0 && read_from_promise_idx < ((int)read_from_promises.size()));
 	return read_from_promises[read_from_promise_idx]->get_reads_from_promise();
 }
 
+/**
+ * Gets a particular 'read-from-promise' form this Node. Only vlaid for a node
+ * where this->action is a 'read'.
+ * @param i The index of the Promise to get
+ * @return The Promise at index i, if the Promise is still available; NULL
+ * otherwise
+ */
+Promise * Node::get_read_from_promise(int i) const
+{
+	return read_from_promises[i]->get_reads_from_promise();
+}
+
+/** @return The size of the read-from-promise set */
+int Node::get_read_from_promise_size() const
+{
+	return read_from_promises.size();
+}
+
 /**
  * Checks whether the read_from_promises set for this node is empty.
  * @return true if the read_from_promises set is empty.
@@ -610,7 +691,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()));