From b77a679eea5ce045bdfb2485625890bf0a087866 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Thu, 21 Mar 2013 16:33:04 -0700
Subject: [PATCH] model: bugfix - send future values more eagerly

This is a bugfix to a pretty big problem with our future value pruning,
where we would hold future values as 'pending' until all pending
promises were resolved. Unfortunately, this is unsound and must be
rewritten.

Now, we allow sending some future values even in presence of promises,
if the value is being sent to a load that is later than the last time a
Promise was created. We have a pseudo-proof that this should be correct.
---
 model.cc | 34 +++++++++++++++++++++++++++++++---
 model.h  |  1 +
 2 files changed, 32 insertions(+), 3 deletions(-)

diff --git a/model.cc b/model.cc
index 32be0538..a9d90914 100644
--- a/model.cc
+++ b/model.cc
@@ -1051,6 +1051,27 @@ bool ModelChecker::process_mutex(ModelAction *curr)
 	return false;
 }
 
+/**
+ * @brief Check if the current pending promises allow a future value to be sent
+ *
+ * If one of the following is true:
+ *  (a) there are no pending promises
+ *  (b) the reader is ordered after the latest Promise creation
+ * Then, it is safe to pass a future value back now.
+ *
+ * Otherwise, we must save the pending future value until (a) or (b) is true
+ *
+ * @param writer The operation which sends the future value. Must be a write.
+ * @param reader The operation which will observe the value. Must be a read.
+ * @return True if the future value can be sent now; false if it must wait.
+ */
+bool ModelChecker::promises_may_allow(const ModelAction *writer,
+		const ModelAction *reader) const
+{
+	return promises->empty() ||
+		*(promises->back()->get_reader(0)) < *reader;
+}
+
 /**
  * @brief Add a future value to a reader
  *
@@ -1104,11 +1125,18 @@ bool ModelChecker::process_write(ModelAction *curr)
 	} 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));
+
+		/* Don't send future values to reads after the Promise we resolve */
+		if (!earliest_promise_reader || *read < *earliest_promise_reader) {
+			/* Check if future value can be sent immediately */
+			if (promises_may_allow(curr, read)) {
+				add_future_value(curr, read);
+			} else {
+				futurevalues->push_back(PendingFutureValue(curr, read));
+			}
+		}
 	}
 
 	if (promises->empty()) {
diff --git a/model.h b/model.h
index 3e9d0643..355764b7 100644
--- a/model.h
+++ b/model.h
@@ -148,6 +148,7 @@ private:
 	bool sleep_can_read_from(ModelAction *curr, const ModelAction *write);
 	bool thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader) const;
 	bool mo_may_allow(const ModelAction *writer, const ModelAction *reader);
+	bool promises_may_allow(const ModelAction *writer, const ModelAction *reader) const;
 	bool has_asserted() const;
 	void set_assert();
 	void set_bad_synchronization();
-- 
2.34.1