X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=4ae69665e4b84e3b04c2e852a120e85271c9c3c0;hb=20c377062e4cfe1c12d517c059822229bacc8c20;hp=417cbc1cf05ee95dffb3bb37180f56fd9d0bcd9e;hpb=61d1e3ae29b690f69cf77c5a6f836fb36507a694;p=model-checker.git

diff --git a/model.cc b/model.cc
index 417cbc1..4ae6966 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 */
@@ -848,32 +852,46 @@ ModelAction * ModelChecker::get_next_backtrack()
  */
 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();
-
-			value = reads_from->get_value();
+		switch (node->get_read_from_status()) {
+		case READ_FROM_PAST: {
+			const ModelAction *rf = node->get_read_from_past();
+			ASSERT(rf);
 
-			check_recency(curr, reads_from);
-			bool r_status = r_modification_order(curr, reads_from);
+			mo_graph->startChanges();
+			value = rf->get_value();
+			check_recency(curr, rf);
+			bool r_status = r_modification_order(curr, rf);
 
-			if (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);
+			read_from(curr, rf);
 			mo_graph->commitChanges();
 			mo_check_promises(curr, true);
 
 			updated |= r_status;
-		} else {
+			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();
+			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);
@@ -881,6 +899,10 @@ bool ModelChecker::process_read(ModelAction *curr)
 			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;
@@ -1006,7 +1028,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(),
 		};
@@ -1022,8 +1044,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++) {
@@ -1308,8 +1348,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();
@@ -1335,14 +1376,19 @@ void ModelChecker::thread_blocking_check_promises(Thread *blocker, Thread *waiti
 {
 	for (unsigned int i = 0; i < promises->size(); i++) {
 		Promise *promise = (*promises)[i];
-		ModelAction *reader = promise->get_action();
-		if (reader->get_tid() != blocker->get_id())
-			continue;
 		if (!promise->thread_is_available(waiting->get_id()))
 			continue;
-		if (promise->eliminate_thread(waiting->get_id())) {
-			/* Promise has failed */
-			priv->failed_promise = true;
+		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;
+			}
 		}
 	}
 }
@@ -1474,7 +1520,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();
@@ -1502,7 +1548,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);
@@ -1608,79 +1653,82 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
  */
 void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 {
-	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());
+	if (!params.maxreads)
+		return;
 
-		/* Skip checks */
-		if ((int)thrd_lists->size() <= tid)
-			return;
-		action_list_t *list = &(*thrd_lists)[tid];
+	//NOTE: Next check is just optimization, not really necessary....
+	if (curr->get_node()->get_read_from_past_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());
 
-		action_list_t::reverse_iterator rit = list->rbegin();
-		/* Skip past curr */
-		for (; (*rit) != curr; rit++)
-			;
-		/* go past curr now */
-		rit++;
+	//NOTE: this check seems left over from previous approach that added action to list late in the game...should be safe to remove
+	/* Skip checks */
+	if ((int)thrd_lists->size() <= tid)
+		return;
+	action_list_t *list = &(*thrd_lists)[tid];
 
-		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;
+	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 */
+	for (int count = 0; count < params.maxreads; ritcopy++, count++) {
+		if (ritcopy == list->rend())
+			return;
+		ModelAction *act = *ritcopy;
+		if (!act->is_read())
+			return;
+		if (act->get_reads_from() != rf)
+			return;
+		if (act->get_node()->get_read_from_past_size() <= 1)
+			return;
+	}
+	for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
+		/* Get write */
+		const ModelAction *write = curr->get_node()->get_read_from_past(i);
 
-			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;
 
-			/* Need a different write */
-			if (write == rf)
-				continue;
+		//NOTE: SHOULD MAKE SURE write is MOd after rf
 
-			/* 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 **/
+		/* 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;
+		ritcopy = rit;
 
-			bool feasiblewrite = true;
-			//new we need to see if this write works for everyone
+		bool feasiblewrite = true;
+		/* now we need to see if this write works for everyone */
 
-			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;
+		for (int loop = params.maxreads; loop > 0; loop--, ritcopy++) {
+			ModelAction *act = *ritcopy;
+			bool foundvalue = false;
+			for (int j = 0; j < act->get_node()->get_read_from_past_size(); j++) {
+				if (act->get_node()->get_read_from_past(j) == write) {
+					foundvalue = true;
 					break;
 				}
 			}
-			if (feasiblewrite) {
-				priv->too_many_reads = true;
-				return;
+			if (!foundvalue) {
+				feasiblewrite = false;
+				break;
 			}
 		}
+		if (feasiblewrite) {
+			priv->too_many_reads = true;
+			return;
+		}
 	}
 }
 
@@ -1806,9 +1854,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;
@@ -1901,9 +1951,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);
 				}
@@ -2425,42 +2475,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(promise, 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
 
@@ -2469,7 +2526,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 		mo_check_promises(read, true);
 	}
 
-	return haveResolved;
+	return true;
 }
 
 /**
@@ -2482,14 +2539,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();
-		ASSERT(act->is_read());
-		if (!act->happens_before(curr) &&
-				!act->could_synchronize_with(curr) &&
-				promise->is_compatible(curr) &&
-				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);
 	}
 }
 
@@ -2498,13 +2561,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;
+				}
 			}
 		}
 	}
@@ -2541,15 +2608,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
@@ -2631,7 +2703,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();
 			}
 
@@ -2644,21 +2716,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();
 	}
@@ -2666,9 +2736,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");
 	}
 }
 
@@ -2729,17 +2799,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);
@@ -2759,9 +2840,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");
@@ -2807,6 +2890,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