From 7ba211ec7d1cacbaa3ef2027f1a0f534888f1708 Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Tue, 2 Oct 2012 00:29:10 -0700
Subject: [PATCH] Fixed bug breaking our consolidation of future values...

---
 model.cc     | 11 ++++++++++-
 model.h      |  1 +
 nodestack.cc | 16 +++++++++++-----
 nodestack.h  |  2 +-
 4 files changed, 23 insertions(+), 7 deletions(-)

diff --git a/model.cc b/model.cc
index a22e0214..0665ff49 100644
--- a/model.cc
+++ b/model.cc
@@ -25,6 +25,7 @@ ModelChecker::ModelChecker(struct model_params params) :
 	num_executions(0),
 	num_feasible_executions(0),
 	diverge(NULL),
+	earliest_diverge(NULL),
 	action_trace(new action_list_t()),
 	thread_map(new HashTable<int, Thread *, int>()),
 	obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
@@ -180,8 +181,13 @@ bool ModelChecker::next_execution()
 	DBG();
 
 	num_executions++;
-	if (isfinalfeasible())
+	if (isfinalfeasible()) {
+		printf("Earliest divergence point since last feasible execution:\n");
+		earliest_diverge->print();
+
+		earliest_diverge = NULL;
 		num_feasible_executions++;
+	}
 
 	if (isfinalfeasible() || DBG_ENABLED())
 		print_summary();
@@ -189,6 +195,9 @@ bool ModelChecker::next_execution()
 	if ((diverge = get_next_backtrack()) == NULL)
 		return false;
 
+	if (earliest_diverge == NULL || *diverge < *earliest_diverge)
+		earliest_diverge=diverge;
+
 	if (DBG_ENABLED()) {
 		printf("Next execution will diverge at:\n");
 		diverge->print();
diff --git a/model.h b/model.h
index 4b9e3ff5..073b96b9 100644
--- a/model.h
+++ b/model.h
@@ -151,6 +151,7 @@ private:
 	void do_complete_join(ModelAction *join);
 
 	ModelAction *diverge;
+	ModelAction *earliest_diverge;
 
 	ucontext_t system_context;
 	action_list_t *action_trace;
diff --git a/nodestack.cc b/nodestack.cc
index 23611f97..533f75a7 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -158,7 +158,7 @@ bool Node::add_future_value(uint64_t value, modelclock_t expiration) {
 		if (future_values[i].value == value) {
 			if (future_values[i].expiration>=expiration)
 				return false;
-			if (future_index < i) {
+			if (future_index < ((int) i)) {
 				suitableindex=i;
 			}
 		}
@@ -325,8 +325,11 @@ const ModelAction * Node::get_read_from() {
 bool Node::increment_read_from() {
 	DBG();
 	promises.clear();
-	read_from_index++;
-	return (read_from_index < may_read_from.size());
+	if ((read_from_index+1) < may_read_from.size()) {
+		read_from_index++;
+		return true;
+	}
+	return false;
 }
 
 /**
@@ -336,8 +339,11 @@ bool Node::increment_read_from() {
 bool Node::increment_future_value() {
 	DBG();
 	promises.clear();
-	future_index++;
-	return (future_index < future_values.size());
+	if ((future_index+1) < future_values.size()) {
+		future_index++;
+		return true;
+	}
+	return false;
 }
 
 void Node::explore(thread_id_t tid)
diff --git a/nodestack.h b/nodestack.h
index 1f7d3e4a..7402aa57 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -112,7 +112,7 @@ private:
 
 	std::vector< struct future_value, MyAlloc<struct future_value> > future_values;
 	std::vector< promise_t, MyAlloc<promise_t> > promises;
-	unsigned int future_index;
+	int future_index;
 };
 
 typedef std::vector< Node *, MyAlloc< Node * > > node_list_t;
-- 
2.34.1