X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=7df70eebbe271c88486a4c85e4289217f1a40e4b;hb=262fab229626c8504297467fc7b5a04f60b7c530;hp=780633e3e6a0d4ec0f0778c09cf3403c130175e8;hpb=4dd0204b6013e344a8728d27448cbf32f50825b6;p=model-checker.git

diff --git a/model.cc b/model.cc
index 780633e..7df70ee 100644
--- a/model.cc
+++ b/model.cc
@@ -1051,25 +1051,66 @@ 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
+ *
+ * This function performs a few additional checks to ensure that the future
+ * value can be feasibly observed by the reader
+ *
+ * @param writer The operation whose value is sent. Must be a write.
+ * @param reader The read operation which may read the future value. Must be a read.
+ */
 void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader)
 {
 	/* Do more ambitious checks now that mo is more complete */
-	if (mo_may_allow(writer, reader)) {
-		Node *node = reader->get_node();
-
-		/* Find an ancestor thread which exists at the time of the reader */
-		Thread *write_thread = get_thread(writer);
-		while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
-			write_thread = write_thread->get_parent();
-
-		struct future_value fv = {
-			writer->get_write_value(),
-			writer->get_seq_number() + params.maxfuturedelay,
-			write_thread->get_id(),
-		};
-		if (node->add_future_value(fv))
-			set_latest_backtrack(reader);
-	}
+	if (!mo_may_allow(writer, reader))
+		return;
+
+	Node *node = reader->get_node();
+
+	/* Find an ancestor thread which exists at the time of the reader */
+	Thread *write_thread = get_thread(writer);
+	while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
+		write_thread = write_thread->get_parent();
+
+	struct future_value fv = {
+		writer->get_write_value(),
+		writer->get_seq_number() + params.maxfuturedelay,
+		write_thread->get_id(),
+	};
+	if (node->add_future_value(fv))
+		set_latest_backtrack(reader);
 }
 
 /**
@@ -1094,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];
-			add_future_value(pfv.writer, pfv.act);
+	/* 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();
@@ -2049,7 +2098,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr, ModelVector<ModelActi
 /** Arbitrary reads from the future are not allowed.  Section 29.3
  * part 9 places some constraints.  This method checks one result of constraint
  * constraint.  Others require compiler support. */
-bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader)
+bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader) const
 {
 	if (!writer->is_rmw())
 		return true;