From: Brian Norris <banorris@uci.edu>
Date: Sun, 7 Oct 2012 23:18:07 +0000 (-0700)
Subject: model: wire up rest of release seq. resolution backtracking
X-Git-Tag: pldi2013~97^2~1^2~12
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=27a6b2d336785fa3d30d937a397242c0a6823cfc;p=model-checker.git

model: wire up rest of release seq. resolution backtracking

I still need to actually initiate the special ModelAction fixups.
---

diff --git a/model.cc b/model.cc
index 6eaf656..e46a18c 100644
--- a/model.cc
+++ b/model.cc
@@ -163,6 +163,10 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr)
 			/* The next node will try to read from a different future value. */
 			tid = next->get_tid();
 			node_stack->pop_restofstack(2);
+		} else if (nextnode->increment_relseq_break()) {
+			/* The next node will try to resolve a release sequence differently */
+			tid = next->get_tid();
+			node_stack->pop_restofstack(2);
 		} else {
 			/* Make a different thread execute for next step */
 			Node *node = nextnode->get_parent();
@@ -591,6 +595,8 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr)
 		 */
 		if (newcurr->is_write())
 			compute_promises(newcurr);
+		else if (newcurr->is_relseq_fixup())
+			compute_relseq_breakwrites(newcurr);
 	}
 	return newcurr;
 }
@@ -740,7 +746,8 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) {
 	if ((!parnode->backtrack_empty() ||
 			 !currnode->read_from_empty() ||
 			 !currnode->future_value_empty() ||
-			 !currnode->promise_empty())
+			 !currnode->promise_empty() ||
+			 !currnode->relseq_break_empty())
 			&& (!priv->next_backtrack ||
 					*curr > *priv->next_backtrack)) {
 		priv->next_backtrack = curr;
@@ -1652,6 +1659,29 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write)
 	}
 }
 
+/**
+ * Compute the set of writes that may break the current pending release
+ * sequence. This information is extracted from previou release sequence
+ * calculations.
+ *
+ * @param curr The current ModelAction. Must be a release sequence fixup
+ * action.
+ */
+void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
+{
+	if (pending_rel_seqs->empty())
+		return;
+
+	struct release_seq *pending = pending_rel_seqs->back();
+	for (unsigned int i = 0; i < pending->writes.size(); i++) {
+		const ModelAction *write = pending->writes[i];
+		curr->get_node()->add_relseq_break(write);
+	}
+
+	/* NULL means don't break the sequence; just synchronize */
+	curr->get_node()->add_relseq_break(NULL);
+}
+
 /**
  * Build up an initial set of all past writes that this 'read' action may read
  * from. This set is determined by the clock vector's "happens before"
diff --git a/model.h b/model.h
index d5dc422..a8268cf 100644
--- a/model.h
+++ b/model.h
@@ -152,6 +152,7 @@ private:
 	void reset_to_initial_state();
 	bool resolve_promises(ModelAction *curr);
 	void compute_promises(ModelAction *curr);
+	void compute_relseq_breakwrites(ModelAction *curr);
 
 	void check_curr_backtracking(ModelAction * curr);
 	void add_action_to_lists(ModelAction *act);