From: Brian Norris <banorris@uci.edu>
Date: Sun, 7 Oct 2012 23:12:00 +0000 (-0700)
Subject: nodestack: add release sequence breakage backtracking
X-Git-Tag: pldi2013~97^2~1^2~13
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=4955df9bfa3d2e961024d419069735fd6f25ac67;p=model-checker.git

nodestack: add release sequence breakage backtracking

End-of-execution resolution of release sequences requires a search
procedure in which we test various attempts at breaking our pending
release sequences. This provides the NodeStack infrastructure.
---

diff --git a/nodestack.cc b/nodestack.cc
index 4cf8950..72c8d5c 100644
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -32,7 +32,9 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
 	may_read_from(),
 	read_from_index(0),
 	future_values(),
-	future_index(-1)
+	future_index(-1),
+	relseq_break_writes(),
+	relseq_break_index(0)
 {
 	if (act) {
 		act->set_node(this);
@@ -352,6 +354,58 @@ bool Node::increment_future_value() {
 	return false;
 }
 
+/**
+ * Add a write ModelAction to the set of writes that may break the release
+ * sequence. This is used during replay exploration of pending release
+ * sequences. This Node must correspond to a release sequence fixup action.
+ *
+ * @param write The write that may break the release sequence. NULL means we
+ * allow the release sequence to synchronize.
+ */
+void Node::add_relseq_break(const ModelAction *write)
+{
+	relseq_break_writes.push_back(write);
+}
+
+/**
+ * Get the write that may break the current pending release sequence,
+ * according to the replay / divergence pattern.
+ *
+ * @return A write that may break the release sequence. If NULL, that means
+ * the release sequence should not be broken.
+ */
+const ModelAction * Node::get_relseq_break()
+{
+	if (relseq_break_index < (int)relseq_break_writes.size())
+		return relseq_break_writes[relseq_break_index];
+	else
+		return NULL;
+}
+
+/**
+ * Increments the index into the relseq_break_writes set to explore the next
+ * item.
+ * @return Returns false if we have explored all values.
+ */
+bool Node::increment_relseq_break()
+{
+	DBG();
+	promises.clear();
+	if (relseq_break_index < ((int)relseq_break_writes.size())) {
+		relseq_break_index++;
+		return (relseq_break_index < ((int)relseq_break_writes.size()));
+	}
+	return false;
+}
+
+/**
+ * @return True if all writes that may break the release sequence have been
+ * explored
+ */
+bool Node::relseq_break_empty() {
+	return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size()));
+}
+
 void Node::explore(thread_id_t tid)
 {
 	int i = id_to_int(tid);
diff --git a/nodestack.h b/nodestack.h
index 55deac5..cb281ca 100644
--- a/nodestack.h
+++ b/nodestack.h
@@ -91,6 +91,11 @@ public:
 	bool increment_promise();
 	bool promise_empty();
 
+	void add_relseq_break(const ModelAction *write);
+	const ModelAction * get_relseq_break();
+	bool increment_relseq_break();
+	bool relseq_break_empty();
+
 	void print();
 	void print_may_read_from();
 
@@ -116,6 +121,9 @@ private:
 	std::vector< struct future_value, ModelAlloc<struct future_value> > future_values;
 	std::vector< promise_t, ModelAlloc<promise_t> > promises;
 	int future_index;
+
+	std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > relseq_break_writes;
+	int relseq_break_index;
 };
 
 typedef std::vector< Node *, ModelAlloc< Node * > > node_list_t;