From: Brian Norris <banorris@uci.edu>
Date: Tue, 12 Feb 2013 18:42:17 +0000 (-0800)
Subject: model: prune may-read-from set early
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=f2a0c8a2e1073829d963f7f8dbc1e5a0bb6172d3

model: prune may-read-from set early

It helps to prune the may-read-from set (according to modification order
constraints) as we build it. This prevents unnecessary backtracking and
provides a significant (linear) speedup in model-checking speed.

Note that this now allows us to assume that at any point in an
execution, any selection from the may-read-from set is feasible.
---

diff --git a/model.cc b/model.cc
index ef9bed30..cbf1f331 100644
--- a/model.cc
+++ b/model.cc
@@ -48,6 +48,7 @@ struct model_snapshot_members {
 		stats(),
 		failed_promise(false),
 		too_many_reads(false),
+		no_valid_reads(false),
 		bad_synchronization(false),
 		asserted(false)
 	{ }
@@ -66,6 +67,7 @@ struct model_snapshot_members {
 	struct execution_stats stats;
 	bool failed_promise;
 	bool too_many_reads;
+	bool no_valid_reads;
 	/** @brief Incorrectly-ordered synchronization was made */
 	bool bad_synchronization;
 	bool asserted;
@@ -1387,6 +1389,8 @@ void ModelChecker::print_infeasibility(const char *prefix) const
 		ptr += sprintf(ptr, "[failed promise]");
 	if (priv->too_many_reads)
 		ptr += sprintf(ptr, "[too many reads]");
+	if (priv->no_valid_reads)
+		ptr += sprintf(ptr, "[no valid reads-from]");
 	if (priv->bad_synchronization)
 		ptr += sprintf(ptr, "[bad sw ordering]");
 	if (promises_expired())
@@ -1415,6 +1419,7 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const
 bool ModelChecker::is_infeasible() const
 {
 	return mo_graph->checkForCycles() ||
+		priv->no_valid_reads ||
 		priv->failed_promise ||
 		priv->too_many_reads ||
 		priv->bad_synchronization ||
@@ -1494,13 +1499,9 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 				continue;
 
 			/* Test to see whether this is a feasible write to read from */
-			mo_graph->startChanges();
-			r_modification_order(curr, write);
-			bool feasiblereadfrom = !is_infeasible();
-			mo_graph->rollbackChanges();
+			/** NOTE: all members of read-from set should be
+			 *  feasible, so we no longer check it here **/
 
-			if (!feasiblereadfrom)
-				continue;
 			rit = ritcopy;
 
 			bool feasiblewrite = true;
@@ -2473,14 +2474,25 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
 			else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
 				allow_read = false;
 
-			if (allow_read)
-				curr->get_node()->add_read_from(act);
+			if (allow_read) {
+				/* Only add feasible reads */
+				mo_graph->startChanges();
+				r_modification_order(curr, act);
+				if (!is_infeasible())
+					curr->get_node()->add_read_from(act);
+				mo_graph->rollbackChanges();
+			}
 
 			/* Include at most one act per-thread that "happens before" curr */
 			if (act->happens_before(curr))
 				break;
 		}
 	}
+	/* We may find no valid may-read-from only if the execution is doomed */
+	if (!curr->get_node()->get_read_from_size()) {
+		priv->no_valid_reads = true;
+		set_assert();
+	}
 
 	if (DBG_ENABLED()) {
 		model_print("Reached read action:\n");