From: Brian Norris <banorris@uci.edu>
Date: Thu, 21 Mar 2013 23:24:47 +0000 (-0700)
Subject: model: refactor add_future_value, add documentation
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=9cfaad02da50095ae169b8fd30ee3148bf88b282

model: refactor add_future_value, add documentation
---

diff --git a/model.cc b/model.cc
index 7ce959e9..32be0538 100644
--- a/model.cc
+++ b/model.cc
@@ -1051,25 +1051,35 @@ bool ModelChecker::process_mutex(ModelAction *curr)
 	return false;
 }
 
+/**
+ * @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);
 }
 
 /**