X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=7df70eebbe271c88486a4c85e4289217f1a40e4b;hb=262fab229626c8504297467fc7b5a04f60b7c530;hp=32be0538a9077d17951911cb01be66accacbb266;hpb=9cfaad02da50095ae169b8fd30ee3148bf88b282;p=model-checker.git

diff --git a/model.cc b/model.cc
index 32be053..7df70ee 100644
--- a/model.cc
+++ b/model.cc
@@ -1051,6 +1051,37 @@ 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 and writer do not cross any promises
+ * 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
+{
+	if (promises->empty())
+		return true;
+	for(int i=promises->size()-1;i>=0;i--) {
+		ModelAction *pr=(*promises)[i]->get_reader(0);
+		//reader is after promise...doesn't cross any promise
+		if (*reader > *pr)
+			return true;
+		//writer is after promise, reader before...bad...
+		if (*writer > *pr)
+			return false;
+	}
+	return true;
+}
+
 /**
  * @brief Add a future value to a reader
  *
@@ -1104,19 +1135,27 @@ 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()) {
-		for (unsigned int i = 0; i < futurevalues->size(); i++) {
-			struct PendingFutureValue pfv = (*futurevalues)[i];
+	/* Check the pending future values */
+	for (int i = (int)futurevalues->size() - 1; i >= 0; i--) {
+		struct PendingFutureValue pfv = (*futurevalues)[i];
+		if (promises_may_allow(pfv.writer, pfv.reader)) {
 			add_future_value(pfv.writer, pfv.reader);
+			futurevalues->erase(futurevalues->begin() + i);
 		}
-		futurevalues->clear();
 	}
 
 	mo_graph->commitChanges();