From: Brian Norris <banorris@uci.edu>
Date: Thu, 21 Mar 2013 23:33:04 +0000 (-0700)
Subject: model: bugfix - send future values more eagerly
X-Git-Tag: oopsla2013~128
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;ds=sidebyside;h=b77a679eea5ce045bdfb2485625890bf0a087866;p=model-checker.git

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.
---

diff --git a/model.cc b/model.cc
index 32be053..a9d9091 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 3e9d064..355764b 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();