From d63f01d45efd1aedb8aafb7dce7e7c6375fec9e7 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Thu, 13 Dec 2012 14:47:59 -0800
Subject: [PATCH] model: add 'set_latest_backtrack()'

---
 model.cc | 38 +++++++++++++++++++++++++++-----------
 model.h  |  1 +
 2 files changed, 28 insertions(+), 11 deletions(-)

diff --git a/model.cc b/model.cc
index 478d1e3..d6b84c3 100644
--- a/model.cc
+++ b/model.cc
@@ -646,8 +646,7 @@ void ModelChecker::set_backtracking(ModelAction *act)
 				continue;
 		}
 		/* Cache the latest backtracking point */
-		if (!priv->next_backtrack || *prev > *priv->next_backtrack)
-			priv->next_backtrack = prev;
+		set_latest_backtrack(prev);
 
 		/* If this is a new backtracking point, mark the tree */
 		if (!node->set_backtrack(tid))
@@ -662,6 +661,26 @@ void ModelChecker::set_backtracking(ModelAction *act)
 	}
 }
 
+/**
+ * @brief Cache the a backtracking point as the "most recent", if eligible
+ *
+ * Note that this does not prepare the NodeStack for this backtracking
+ * operation, it only caches the action on a per-execution basis
+ *
+ * @param act The operation at which we should explore a different next action
+ * (i.e., backtracking point)
+ * @return True, if this action is now the most recent backtracking point;
+ * false otherwise
+ */
+bool ModelChecker::set_latest_backtrack(ModelAction *act)
+{
+	if (!priv->next_backtrack || *act > *priv->next_backtrack) {
+		priv->next_backtrack = act;
+		return true;
+	}
+	return false;
+}
+
 /**
  * Returns last backtracking point. The model checker will explore a different
  * path for this point in the next execution.
@@ -843,10 +862,9 @@ bool ModelChecker::process_write(ModelAction *curr)
 		for (unsigned int i = 0; i < futurevalues->size(); i++) {
 			struct PendingFutureValue pfv = (*futurevalues)[i];
 			//Do more ambitious checks now that mo is more complete
-			if (mo_may_allow(pfv.writer, pfv.act)&&
-					pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number()+params.maxfuturedelay) &&
-					(!priv->next_backtrack || *pfv.act > *priv->next_backtrack))
-				priv->next_backtrack = pfv.act;
+			if (mo_may_allow(pfv.writer, pfv.act) &&
+					pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number() + params.maxfuturedelay))
+				set_latest_backtrack(pfv.act);
 		}
 		futurevalues->resize(0);
 	}
@@ -1277,15 +1295,13 @@ void ModelChecker::check_curr_backtracking(ModelAction *curr)
 	Node *currnode = curr->get_node();
 	Node *parnode = currnode->get_parent();
 
-	if ((!parnode->backtrack_empty() ||
+	if (!parnode->backtrack_empty() ||
 			 !currnode->misc_empty() ||
 			 !currnode->read_from_empty() ||
 			 !currnode->future_value_empty() ||
 			 !currnode->promise_empty() ||
-			 !currnode->relseq_break_empty())
-			&& (!priv->next_backtrack ||
-					*curr > *priv->next_backtrack)) {
-		priv->next_backtrack = curr;
+			 !currnode->relseq_break_empty()) {
+		set_latest_backtrack(curr);
 	}
 }
 
diff --git a/model.h b/model.h
index 8345678..5f62ff8 100644
--- a/model.h
+++ b/model.h
@@ -165,6 +165,7 @@ private:
 	ModelAction * get_last_conflict(ModelAction *act);
 	void set_backtracking(ModelAction *act);
 	Thread * get_next_thread(ModelAction *curr);
+	bool set_latest_backtrack(ModelAction *act);
 	ModelAction * get_next_backtrack();
 	void reset_to_initial_state();
 	bool resolve_promises(ModelAction *curr);
-- 
2.34.1