From 7bd9b5a1446863dc1a9de9683476f5a480dfba91 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Tue, 26 Feb 2013 11:13:10 -0800
Subject: [PATCH] nodestack: add read_from_promises backtracking

This is just the basic framework for now. I still need to hook it up for
actual use in ModelChecker.
---
 nodestack.cc | 59 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 nodestack.h  |  9 ++++++++
 2 files changed, 68 insertions(+)

diff --git a/nodestack.cc b/nodestack.cc
index 730c7024..3cde3456 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -36,6 +36,8 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) :
 	enabled_array(NULL),
 	read_from_past(),
 	read_from_past_idx(0),
+	read_from_promises(),
+	read_from_promise_idx(-1),
 	future_values(),
 	future_index(-1),
 	relseq_break_writes(),
@@ -105,6 +107,11 @@ void Node::print() const
 		model_print("[%d]", read_from_past[i]->get_seq_number());
 	model_print("\n");
 
+	model_print("          read-from promises: %s", read_from_promise_empty() ? "empty" : "non-empty ");
+	for (int i = read_from_promise_idx + 1; i < (int)read_from_promises.size(); i++)
+		model_print("[%d]", read_from_promises[i]->get_seq_number());
+	model_print("\n");
+
 	model_print("          future values: %s", future_value_empty() ? "empty" : "non-empty ");
 	for (int i = future_index + 1; i < (int)future_values.size(); i++)
 		model_print("[%#" PRIx64 "]", future_values[i].value);
@@ -342,6 +349,9 @@ bool Node::increment_read_from()
 	if (increment_read_from_past()) {
 	       read_from_status = READ_FROM_PAST;
 	       return true;
+	} else if (increment_read_from_promise()) {
+		read_from_status = READ_FROM_PROMISE;
+		return true;
 	} else if (increment_future_value()) {
 		read_from_status = READ_FROM_FUTURE;
 		return true;
@@ -436,6 +446,55 @@ bool Node::increment_read_from_past()
 
 /************************** end read from past ********************************/
 
+/***************************** read_from_promises *****************************/
+
+/**
+ * Add an action to the read_from_promises set.
+ * @param reader The read which generated the Promise; we use the ModelAction
+ * instead of the Promise because the Promise does not last across executions
+ */
+void Node::add_read_from_promise(const ModelAction *reader)
+{
+	read_from_promises.push_back(reader);
+}
+
+/**
+ * Gets the next 'read-from-promise' from this Node. Only valid for a node
+ * where this->action is a 'read'.
+ * @return The current element in read_from_promises
+ */
+const Promise * Node::get_read_from_promise() const
+{
+	if (read_from_promise_idx < 0 || read_from_promise_idx >= ((int)read_from_promises.size()))
+		return NULL;
+	return read_from_promises[read_from_promise_idx]->get_reads_from_promise();
+}
+
+/**
+ * Checks whether the read_from_promises set for this node is empty.
+ * @return true if the read_from_promises set is empty.
+ */
+bool Node::read_from_promise_empty() const
+{
+	return ((read_from_promise_idx + 1) >= ((int)read_from_promises.size()));
+}
+
+/**
+ * Increments the index into the read_from_promises set to explore the next item.
+ * @return Returns false if we have explored all promises.
+ */
+bool Node::increment_read_from_promise()
+{
+	DBG();
+	if (read_from_promise_idx < ((int)read_from_promises.size())) {
+		read_from_promise_idx++;
+		return (read_from_promise_idx < ((int)read_from_promises.size()));
+	}
+	return false;
+}
+
+/************************* end read_from_promises *****************************/
+
 /****************************** future values *********************************/
 
 /**
diff --git a/nodestack.h b/nodestack.h
index a857084b..8a20c45c 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -40,6 +40,7 @@ struct fairness_info {
 
 typedef enum {
 	READ_FROM_PAST,
+	READ_FROM_PROMISE,
 	READ_FROM_FUTURE,
 	READ_FROM_NONE,
 } read_from_type_t;
@@ -89,6 +90,9 @@ public:
 	const ModelAction * get_read_from_past(int i) const;
 	int get_read_from_past_size() const;
 
+	void add_read_from_promise(const ModelAction *reader);
+	const Promise * get_read_from_promise() const;
+
 	bool add_future_value(struct future_value fv);
 	struct future_value get_future_value() const;
 
@@ -116,6 +120,8 @@ private:
 
 	bool read_from_past_empty() const;
 	bool increment_read_from_past();
+	bool read_from_promise_empty() const;
+	bool increment_read_from_promise();
 	bool future_value_empty() const;
 	bool increment_future_value();
 	read_from_type_t read_from_status;
@@ -136,6 +142,9 @@ private:
 	std::vector< const ModelAction *, ModelAlloc< const ModelAction * > > read_from_past;
 	unsigned int read_from_past_idx;
 
+	std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > read_from_promises;
+	int read_from_promise_idx;
+
 	std::vector< struct future_value, ModelAlloc<struct future_value> > future_values;
 	std::vector< promise_t, ModelAlloc<promise_t> > promises;
 	int future_index;
-- 
2.34.1