X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=model.cc;h=5a1f3992343bc4376fc1c0570832efe9e6bc43d9;hp=24eb83dbbc6515cb4c24730e27ee94c4c949afbe;hb=57f11820dd7dc4c3b95459a8de99305ac31f88bf;hpb=0997f5bf1b28a79066ed4abfed57f14419ee44d3

diff --git a/model.cc b/model.cc
index 24eb83db..5a1f3992 100644
--- a/model.cc
+++ b/model.cc
@@ -263,10 +263,6 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 			/* The next node will read from a different value. */
 			tid = next->get_tid();
 			node_stack->pop_restofstack(2);
-		} else if (nextnode->increment_future_value()) {
-			/* The next node will try to read from a different future value. */
-			tid = next->get_tid();
-			node_stack->pop_restofstack(2);
 		} else if (nextnode->increment_relseq_break()) {
 			/* The next node will try to resolve a release sequence differently */
 			tid = next->get_tid();
@@ -487,8 +483,16 @@ void ModelChecker::record_stats()
 		stats.num_buggy_executions++;
 	else if (is_complete_execution())
 		stats.num_complete++;
-	else
+	else {
 		stats.num_redundant++;
+
+		/**
+		 * @todo We can violate this ASSERT() when fairness/sleep sets
+		 * conflict to cause an execution to terminate, e.g. with:
+		 * Scheduler: [0: disabled][1: disabled][2: sleep][3: current, enabled]
+		 */
+		//ASSERT(scheduler->all_threads_sleeping());
+	}
 }
 
 /** @brief Print execution stats */
@@ -842,42 +846,56 @@ ModelAction * ModelChecker::get_next_backtrack()
 }
 
 /**
- * Processes a read or rmw model action.
+ * Processes a read model action.
  * @param curr is the read model action to process.
- * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
  * @return True if processing this read updates the mo_graph.
  */
-bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
+bool ModelChecker::process_read(ModelAction *curr)
 {
+	Node *node = curr->get_node();
 	uint64_t value = VALUE_NONE;
-	bool updated = false;
 	while (true) {
-		const ModelAction *reads_from = curr->get_node()->get_read_from();
-		if (reads_from != NULL) {
-			mo_graph->startChanges();
+		bool updated = false;
+		switch (node->get_read_from_status()) {
+		case READ_FROM_PAST: {
+			const ModelAction *rf = node->get_read_from_past();
+			ASSERT(rf);
 
-			value = reads_from->get_value();
-			bool r_status = false;
+			mo_graph->startChanges();
 
-			if (!second_part_of_rmw) {
-				check_recency(curr, reads_from);
-				r_status = r_modification_order(curr, reads_from);
-			}
+			ASSERT(!is_infeasible());
+			if (!check_recency(curr, rf))
+				priv->too_many_reads = true;
+			updated = r_modification_order(curr, rf);
 
-			if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
+			if (is_infeasible() && node->increment_read_from()) {
 				mo_graph->rollbackChanges();
 				priv->too_many_reads = false;
 				continue;
 			}
 
-			read_from(curr, reads_from);
+			value = rf->get_value();
+			read_from(curr, rf);
 			mo_graph->commitChanges();
 			mo_check_promises(curr, true);
 
-			updated |= r_status;
-		} else if (!second_part_of_rmw) {
+			break;
+		}
+		case READ_FROM_PROMISE: {
+			Promise *promise = curr->get_node()->get_read_from_promise();
+			promise->add_reader(curr);
+			value = promise->get_value();
+			curr->set_read_from_promise(promise);
+			mo_graph->startChanges();
+			if (!check_recency(curr, promise))
+				priv->too_many_reads = true;
+			updated = r_modification_order(curr, promise);
+			mo_graph->commitChanges();
+			break;
+		}
+		case READ_FROM_FUTURE: {
 			/* Read from future value */
-			struct future_value fv = curr->get_node()->get_future_value();
+			struct future_value fv = node->get_future_value();
 			Promise *promise = new Promise(curr, fv);
 			value = fv.value;
 			curr->set_read_from_promise(promise);
@@ -885,6 +903,10 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 			mo_graph->startChanges();
 			updated = r_modification_order(curr, promise);
 			mo_graph->commitChanges();
+			break;
+		}
+		default:
+			ASSERT(false);
 		}
 		get_thread(curr)->set_return_value(value);
 		return updated;
@@ -1010,7 +1032,7 @@ void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *read
 			write_thread = write_thread->get_parent();
 
 		struct future_value fv = {
-			writer->get_value(),
+			writer->get_write_value(),
 			writer->get_seq_number() + params.maxfuturedelay,
 			write_thread->get_id(),
 		};
@@ -1026,8 +1048,26 @@ void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *read
  */
 bool ModelChecker::process_write(ModelAction *curr)
 {
-	bool updated_mod_order = w_modification_order(curr);
-	bool updated_promises = resolve_promises(curr);
+	/* Readers to which we may send our future value */
+	std::vector< ModelAction *, ModelAlloc<ModelAction *> > send_fv;
+
+	bool updated_mod_order = w_modification_order(curr, &send_fv);
+	int promise_idx = get_promise_to_resolve(curr);
+	const ModelAction *earliest_promise_reader;
+	bool updated_promises = false;
+
+	if (promise_idx >= 0) {
+		earliest_promise_reader = (*promises)[promise_idx]->get_reader(0);
+		updated_promises = resolve_promise(curr, promise_idx);
+	} else
+		earliest_promise_reader = NULL;
+
+	/* Don't send future values to reads after the Promise we resolve */
+	for (unsigned int i = 0; i < send_fv.size(); i++) {
+		ModelAction *read = send_fv[i];
+		if (!earliest_promise_reader || *read < *earliest_promise_reader)
+			futurevalues->push_back(PendingFutureValue(curr, read));
+	}
 
 	if (promises->size() == 0) {
 		for (unsigned int i = 0; i < futurevalues->size(); i++) {
@@ -1312,8 +1352,9 @@ bool ModelChecker::initialize_curr_action(ModelAction **curr)
  */
 bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
 {
+	ASSERT(rf);
 	act->set_read_from(rf);
-	if (rf != NULL && act->is_acquire()) {
+	if (act->is_acquire()) {
 		rel_heads_list_t release_heads;
 		get_release_seq_heads(act, act, &release_heads);
 		int num_heads = release_heads.size();
@@ -1327,6 +1368,35 @@ bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
 	return false;
 }
 
+/**
+ * Check promises and eliminate potentially-satisfying threads when a thread is
+ * blocked (e.g., join, lock). A thread which is waiting on another thread can
+ * no longer satisfy a promise generated from that thread.
+ *
+ * @param blocker The thread on which a thread is waiting
+ * @param waiting The waiting thread
+ */
+void ModelChecker::thread_blocking_check_promises(Thread *blocker, Thread *waiting)
+{
+	for (unsigned int i = 0; i < promises->size(); i++) {
+		Promise *promise = (*promises)[i];
+		if (!promise->thread_is_available(waiting->get_id()))
+			continue;
+		for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+			ModelAction *reader = promise->get_reader(j);
+			if (reader->get_tid() != blocker->get_id())
+				continue;
+			if (promise->eliminate_thread(waiting->get_id())) {
+				/* Promise has failed */
+				priv->failed_promise = true;
+			} else {
+				/* Only eliminate the 'waiting' thread once */
+				return;
+			}
+		}
+	}
+}
+
 /**
  * @brief Check whether a model action is enabled.
  *
@@ -1350,6 +1420,7 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
 		Thread *blocking = (Thread *)curr->get_location();
 		if (!blocking->is_complete()) {
 			blocking->push_wait_list(curr);
+			thread_blocking_check_promises(blocking, get_thread(curr));
 			return false;
 		}
 	}
@@ -1412,7 +1483,7 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr)
 			if (process_thread_action(curr))
 				update_all = true;
 
-			if (act->is_read() && process_read(act, second_part_of_rmw))
+			if (act->is_read() && !second_part_of_rmw && process_read(act))
 				update = true;
 
 			if (act->is_write() && process_write(act))
@@ -1453,7 +1524,7 @@ ModelAction * ModelChecker::check_current_action(ModelAction *curr)
 				}
 			}
 			if (act->is_write()) {
-				if (w_modification_order(act))
+				if (w_modification_order(act, NULL))
 					updated = true;
 			}
 			mo_graph->commitChanges();
@@ -1481,7 +1552,6 @@ void ModelChecker::check_curr_backtracking(ModelAction *curr)
 	if ((parnode && !parnode->backtrack_empty()) ||
 			 !currnode->misc_empty() ||
 			 !currnode->read_from_empty() ||
-			 !currnode->future_value_empty() ||
 			 !currnode->promise_empty() ||
 			 !currnode->relseq_break_empty()) {
 		set_latest_backtrack(curr);
@@ -1574,6 +1644,33 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
 	return lastread;
 }
 
+template <typename T, typename U>
+bool ModelChecker::should_read_instead(const ModelAction *curr, const T *rf, const U *other_rf) const
+{
+	/* Need a different write/promise */
+	if (other_rf->equals(rf))
+		return false;
+
+	/* Only look for "newer" writes/promises */
+	if (!mo_graph->checkReachable(rf, other_rf))
+		return false;
+
+	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+	action_list_t *list = &(*thrd_lists)[id_to_int(curr->get_tid())];
+	action_list_t::reverse_iterator rit = list->rbegin();
+	ASSERT((*rit) == curr);
+	/* Skip past curr */
+	rit++;
+
+	/* Does this write/promise work for everyone? */
+	for (int i = 0; i < params.maxreads; i++, rit++) {
+		ModelAction *act = *rit;
+		if (!act->may_read_from(other_rf))
+			return false;
+	}
+	return true;
+}
+
 /**
  * Checks whether a thread has read from the same write for too many times
  * without seeing the effects of a later write.
@@ -1584,83 +1681,58 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
  * 3) that other write must have been in the reads_from set for maxreads times.
  *
  * If so, we decide that the execution is no longer feasible.
+ *
+ * @param curr The current action. Must be a read.
+ * @param rf The ModelAction/Promise from which we might read.
+ * @return True if the read should succeed; false otherwise
  */
-void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
+template <typename T>
+bool ModelChecker::check_recency(ModelAction *curr, const T *rf) const
 {
-	if (params.maxreads != 0) {
-		if (curr->get_node()->get_read_from_size() <= 1)
-			return;
-		//Must make sure that execution is currently feasible...  We could
-		//accidentally clear by rolling back
-		if (is_infeasible())
-			return;
-		std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
-		int tid = id_to_int(curr->get_tid());
-
-		/* Skip checks */
-		if ((int)thrd_lists->size() <= tid)
-			return;
-		action_list_t *list = &(*thrd_lists)[tid];
-
-		action_list_t::reverse_iterator rit = list->rbegin();
-		/* Skip past curr */
-		for (; (*rit) != curr; rit++)
-			;
-		/* go past curr now */
-		rit++;
-
-		action_list_t::reverse_iterator ritcopy = rit;
-		//See if we have enough reads from the same value
-		int count = 0;
-		for (; count < params.maxreads; rit++, count++) {
-			if (rit == list->rend())
-				return;
-			ModelAction *act = *rit;
-			if (!act->is_read())
-				return;
-
-			if (act->get_reads_from() != rf)
-				return;
-			if (act->get_node()->get_read_from_size() <= 1)
-				return;
-		}
-		for (int i = 0; i < curr->get_node()->get_read_from_size(); i++) {
-			/* Get write */
-			const ModelAction *write = curr->get_node()->get_read_from_at(i);
-
-			/* Need a different write */
-			if (write == rf)
-				continue;
-
-			/* Test to see whether this is a feasible write to read from */
-			/** NOTE: all members of read-from set should be
-			 *  feasible, so we no longer check it here **/
-
-			rit = ritcopy;
+	if (!params.maxreads)
+		return true;
 
-			bool feasiblewrite = true;
-			//new we need to see if this write works for everyone
+	//NOTE: Next check is just optimization, not really necessary....
+	if (curr->get_node()->get_read_from_past_size() +
+			curr->get_node()->get_read_from_promise_size() <= 1)
+		return true;
 
-			for (int loop = count; loop > 0; loop--, rit++) {
-				ModelAction *act = *rit;
-				bool foundvalue = false;
-				for (int j = 0; j < act->get_node()->get_read_from_size(); j++) {
-					if (act->get_node()->get_read_from_at(j) == write) {
-						foundvalue = true;
-						break;
-					}
-				}
-				if (!foundvalue) {
-					feasiblewrite = false;
-					break;
-				}
-			}
-			if (feasiblewrite) {
-				priv->too_many_reads = true;
-				return;
-			}
-		}
+	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+	int tid = id_to_int(curr->get_tid());
+	ASSERT(tid < (int)thrd_lists->size());
+	action_list_t *list = &(*thrd_lists)[tid];
+	action_list_t::reverse_iterator rit = list->rbegin();
+	ASSERT((*rit) == curr);
+	/* Skip past curr */
+	rit++;
+
+	action_list_t::reverse_iterator ritcopy = rit;
+	/* See if we have enough reads from the same value */
+	for (int count = 0; count < params.maxreads; ritcopy++, count++) {
+		if (ritcopy == list->rend())
+			return true;
+		ModelAction *act = *ritcopy;
+		if (!act->is_read())
+			return true;
+		if (act->get_reads_from_promise() && !act->get_reads_from_promise()->equals(rf))
+			return true;
+		if (act->get_reads_from() && !act->get_reads_from()->equals(rf))
+			return true;
+		if (act->get_node()->get_read_from_past_size() +
+				act->get_node()->get_read_from_promise_size() <= 1)
+			return true;
 	}
+	for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
+		const ModelAction *write = curr->get_node()->get_read_from_past(i);
+		if (should_read_instead(curr, rf, write))
+			return false; /* liveness failure */
+	}
+	for (int i = 0; i < curr->get_node()->get_read_from_promise_size(); i++) {
+		const Promise *promise = curr->get_node()->get_read_from_promise(i);
+		if (should_read_instead(curr, rf, promise))
+			return false; /* liveness failure */
+	}
+	return true;
 }
 
 /**
@@ -1740,13 +1812,13 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 						added = mo_graph->addEdge(act, rf) || added;
 					}
 				} else {
-					const ModelAction *prevreadfrom = act->get_reads_from();
-					//if the previous read is unresolved, keep going...
-					if (prevreadfrom == NULL)
-						continue;
-
-					if (!prevreadfrom->equals(rf)) {
-						added = mo_graph->addEdge(prevreadfrom, rf) || added;
+					const ModelAction *prevrf = act->get_reads_from();
+					const Promise *prevrf_promise = act->get_reads_from_promise();
+					if (prevrf) {
+						if (!prevrf->equals(rf))
+							added = mo_graph->addEdge(prevrf, rf) || added;
+					} else if (!prevrf_promise->equals(rf)) {
+						added = mo_graph->addEdge(prevrf_promise, rf) || added;
 					}
 				}
 				break;
@@ -1785,9 +1857,11 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
  * (II) Sending the write back to non-synchronizing reads.
  *
  * @param curr The current action. Must be a write.
+ * @param send_fv A vector for stashing reads to which we may pass our future
+ * value. If NULL, then don't record any future values.
  * @return True if modification order edges were added; false otherwise
  */
-bool ModelChecker::w_modification_order(ModelAction *curr)
+bool ModelChecker::w_modification_order(ModelAction *curr, std::vector< ModelAction *, ModelAlloc<ModelAction *> > *send_fv)
 {
 	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
 	unsigned int i;
@@ -1880,9 +1954,9 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
 				   pendingfuturevalue.
 
 				 */
-				if (thin_air_constraint_may_allow(curr, act)) {
+				if (send_fv && thin_air_constraint_may_allow(curr, act)) {
 					if (!is_infeasible())
-						futurevalues->push_back(PendingFutureValue(curr, act));
+						send_fv->push_back(act);
 					else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from())
 						add_future_value(curr, act);
 				}
@@ -2404,42 +2478,49 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) const
 }
 
 /**
- * Resolve a set of Promises with a current write. The set is provided in the
- * Node corresponding to @a write.
+ * @brief Find the promise, if any to resolve for the current action
+ * @param curr The current ModelAction. Should be a write.
+ * @return The (non-negative) index for the Promise to resolve, if any;
+ * otherwise -1
+ */
+int ModelChecker::get_promise_to_resolve(const ModelAction *curr) const
+{
+	for (unsigned int i = 0; i < promises->size(); i++)
+		if (curr->get_node()->get_promise(i))
+			return i;
+	return -1;
+}
+
+/**
+ * Resolve a Promise with a current write.
  * @param write The ModelAction that is fulfilling Promises
- * @return True if promises were resolved; false otherwise
+ * @param promise_idx The index corresponding to the promise
+ * @return True if the Promise was successfully resolved; false otherwise
  */
-bool ModelChecker::resolve_promises(ModelAction *write)
+bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx)
 {
-	bool haveResolved = false;
 	std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
-	promise_list_t mustResolve, resolved;
+	promise_list_t mustResolve;
+	Promise *promise = (*promises)[promise_idx];
 
-	for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
-		Promise *promise = (*promises)[promise_index];
-		if (write->get_node()->get_promise(i)) {
-			ModelAction *read = promise->get_action();
-			read_from(read, write);
-			//Make sure the promise's value matches the write's value
-			ASSERT(promise->is_compatible(write));
-			mo_graph->resolvePromise(read, write, &mustResolve);
+	for (unsigned int i = 0; i < promise->get_num_readers(); i++) {
+		ModelAction *read = promise->get_reader(i);
+		read_from(read, write);
+		actions_to_check.push_back(read);
+	}
+	/* Make sure the promise's value matches the write's value */
+	ASSERT(promise->is_compatible(write) && promise->same_value(write));
+	mo_graph->resolvePromise(promise, write, &mustResolve);
 
-			resolved.push_back(promise);
-			promises->erase(promises->begin() + promise_index);
-			actions_to_check.push_back(read);
+	promises->erase(promises->begin() + promise_idx);
 
-			haveResolved = true;
-		} else
-			promise_index++;
-	}
+	/** @todo simplify the 'mustResolve' stuff */
+	ASSERT(mustResolve.size() <= 1);
+
+	if (!mustResolve.empty() && mustResolve[0] != promise)
+		priv->failed_promise = true;
+	delete promise;
 
-	for (unsigned int i = 0; i < mustResolve.size(); i++) {
-		if (std::find(resolved.begin(), resolved.end(), mustResolve[i])
-				== resolved.end())
-			priv->failed_promise = true;
-	}
-	for (unsigned int i = 0; i < resolved.size(); i++)
-		delete resolved[i];
 	//Check whether reading these writes has made threads unable to
 	//resolve promises
 
@@ -2448,7 +2529,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 		mo_check_promises(read, true);
 	}
 
-	return haveResolved;
+	return true;
 }
 
 /**
@@ -2461,15 +2542,20 @@ void ModelChecker::compute_promises(ModelAction *curr)
 {
 	for (unsigned int i = 0; i < promises->size(); i++) {
 		Promise *promise = (*promises)[i];
-		const ModelAction *act = promise->get_action();
-		if (!act->happens_before(curr) &&
-				act->is_read() &&
-				!act->could_synchronize_with(curr) &&
-				!act->same_thread(curr) &&
-				act->get_location() == curr->get_location() &&
-				promise->get_value() == curr->get_value()) {
-			curr->get_node()->set_promise(i, act->is_rmw());
+		if (!promise->is_compatible(curr) || !promise->same_value(curr))
+			continue;
+
+		bool satisfy = true;
+		for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+			const ModelAction *act = promise->get_reader(j);
+			if (act->happens_before(curr) ||
+					act->could_synchronize_with(curr)) {
+				satisfy = false;
+				break;
+			}
 		}
+		if (satisfy)
+			curr->get_node()->set_promise(i);
 	}
 }
 
@@ -2478,13 +2564,17 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec
 {
 	for (unsigned int i = 0; i < promises->size(); i++) {
 		Promise *promise = (*promises)[i];
-		const ModelAction *act = promise->get_action();
-		if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
-				merge_cv->synchronized_since(act)) {
-			if (promise->eliminate_thread(tid)) {
-				//Promise has failed
-				priv->failed_promise = true;
-				return;
+		if (!promise->thread_is_available(tid))
+			continue;
+		for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+			const ModelAction *act = promise->get_reader(j);
+			if ((!old_cv || !old_cv->synchronized_since(act)) &&
+					merge_cv->synchronized_since(act)) {
+				if (promise->eliminate_thread(tid)) {
+					/* Promise has failed */
+					priv->failed_promise = true;
+					return;
+				}
 			}
 		}
 	}
@@ -2521,15 +2611,20 @@ void ModelChecker::mo_check_promises(const ModelAction *act, bool is_read_check)
 
 	for (unsigned int i = 0; i < promises->size(); i++) {
 		Promise *promise = (*promises)[i];
-		const ModelAction *pread = promise->get_action();
 
 		// Is this promise on the same location?
-		if (!pread->same_var(write))
+		if (!promise->same_location(write))
 			continue;
 
-		if (pread->happens_before(act) && mo_graph->checkPromise(write, promise)) {
-			priv->failed_promise = true;
-			return;
+		for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+			const ModelAction *pread = promise->get_reader(j);
+			if (!pread->happens_before(act))
+			       continue;
+			if (mo_graph->checkPromise(write, promise)) {
+				priv->failed_promise = true;
+				return;
+			}
+			break;
 		}
 
 		// Don't do any lookups twice for the same thread
@@ -2611,7 +2706,7 @@ void ModelChecker::build_may_read_from(ModelAction *curr)
 				mo_graph->startChanges();
 				r_modification_order(curr, act);
 				if (!is_infeasible())
-					curr->get_node()->add_read_from(act);
+					curr->get_node()->add_read_from_past(act);
 				mo_graph->rollbackChanges();
 			}
 
@@ -2624,21 +2719,19 @@ void ModelChecker::build_may_read_from(ModelAction *curr)
 	/* Inherit existing, promised future values */
 	for (i = 0; i < promises->size(); i++) {
 		const Promise *promise = (*promises)[i];
-		const ModelAction *promise_read = promise->get_action();
+		const ModelAction *promise_read = promise->get_reader(0);
 		if (promise_read->same_var(curr)) {
 			/* Only add feasible future-values */
 			mo_graph->startChanges();
 			r_modification_order(curr, promise);
-			if (!is_infeasible()) {
-				const struct future_value fv = promise->get_fv();
-				curr->get_node()->add_future_value(fv);
-			}
+			if (!is_infeasible())
+				curr->get_node()->add_read_from_promise(promise_read);
 			mo_graph->rollbackChanges();
 		}
 	}
 
 	/* We may find no valid may-read-from only if the execution is doomed */
-	if (!curr->get_node()->get_read_from_size() && curr->get_node()->future_value_empty()) {
+	if (!curr->get_node()->read_from_size()) {
 		priv->no_valid_reads = true;
 		set_assert();
 	}
@@ -2646,9 +2739,9 @@ void ModelChecker::build_may_read_from(ModelAction *curr)
 	if (DBG_ENABLED()) {
 		model_print("Reached read action:\n");
 		curr->print();
-		model_print("Printing may_read_from\n");
-		curr->get_node()->print_may_read_from();
-		model_print("End printing may_read_from\n");
+		model_print("Printing read_from_past\n");
+		curr->get_node()->print_read_from_past();
+		model_print("End printing read_from_past\n");
 	}
 }
 
@@ -2709,17 +2802,28 @@ void ModelChecker::dumpGraph(char *filename) const
 	ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
 
 	for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
-		ModelAction *action = *it;
-		if (action->is_read()) {
-			fprintf(file, "N%u [label=\"N%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
-			if (action->get_reads_from() != NULL)
-				fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
+		ModelAction *act = *it;
+		if (act->is_read()) {
+			mo_graph->dot_print_node(file, act);
+			if (act->get_reads_from())
+				mo_graph->dot_print_edge(file,
+						act->get_reads_from(),
+						act,
+						"label=\"rf\", color=red, weight=2");
+			else
+				mo_graph->dot_print_edge(file,
+						act->get_reads_from_promise(),
+						act,
+						"label=\"rf\", color=red");
 		}
-		if (thread_array[action->get_tid()] != NULL) {
-			fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
+		if (thread_array[act->get_tid()]) {
+			mo_graph->dot_print_edge(file,
+					thread_array[id_to_int(act->get_tid())],
+					act,
+					"label=\"sb\", color=blue, weight=400");
 		}
 
-		thread_array[action->get_tid()] = action;
+		thread_array[act->get_tid()] = act;
 	}
 	fprintf(file, "}\n");
 	model_free(thread_array);
@@ -2739,9 +2843,11 @@ void ModelChecker::print_summary() const
 #endif
 
 	model_print("Execution %d:", stats.num_total);
-	if (isfeasibleprefix())
+	if (isfeasibleprefix()) {
+		if (scheduler->all_threads_sleeping())
+			model_print(" SLEEP-SET REDUNDANT");
 		model_print("\n");
-	else
+	} else
 		print_infeasibility(" INFEASIBLE");
 	print_list(action_trace);
 	model_print("\n");
@@ -2787,6 +2893,26 @@ Thread * ModelChecker::get_thread(const ModelAction *act) const
 	return get_thread(act->get_tid());
 }
 
+/**
+ * @brief Get a Promise's "promise number"
+ *
+ * A "promise number" is an index number that is unique to a promise, valid
+ * only for a specific snapshot of an execution trace. Promises may come and go
+ * as they are generated an resolved, so an index only retains meaning for the
+ * current snapshot.
+ *
+ * @param promise The Promise to check
+ * @return The promise index, if the promise still is valid; otherwise -1
+ */
+int ModelChecker::get_promise_number(const Promise *promise) const
+{
+	for (unsigned int i = 0; i < promises->size(); i++)
+		if ((*promises)[i] == promise)
+			return i;
+	/* Not found */
+	return -1;
+}
+
 /**
  * @brief Check if a Thread is currently enabled
  * @param t The Thread to check
@@ -2890,7 +3016,7 @@ void ModelChecker::run()
 {
 	do {
 		thrd_t user_thread;
-		Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL);
+		Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL, NULL);
 		add_thread(t);
 
 		do {