From: Brian Norris <banorris@uci.edu>
Date: Sat, 2 Mar 2013 08:26:51 +0000 (-0800)
Subject: check_recency: return a boolean status
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=c8de5897b0c8caaab3a695dd677acd38770e48b3;ds=sidebyside

check_recency: return a boolean status

The output of check_recency is actually a boolean (failure => "too many
reads"), so make that explicit.

Also, rework a little more logic to make the structure a little more
obvious.
---

diff --git a/model.cc b/model.cc
index 36c23bf1..a0df0876 100644
--- a/model.cc
+++ b/model.cc
@@ -854,17 +854,19 @@ bool ModelChecker::process_read(ModelAction *curr)
 {
 	Node *node = curr->get_node();
 	uint64_t value = VALUE_NONE;
-	bool updated = false;
 	while (true) {
+		bool updated = false;
 		switch (node->get_read_from_status()) {
 		case READ_FROM_PAST: {
 			const ModelAction *rf = node->get_read_from_past();
 			ASSERT(rf);
 
 			mo_graph->startChanges();
-			value = rf->get_value();
-			check_recency(curr, rf);
-			bool r_status = r_modification_order(curr, rf);
+
+			ASSERT(!is_infeasible());
+			if (!check_recency(curr, rf))
+				priv->too_many_reads = true;
+			updated = r_modification_order(curr, rf);
 
 			if (is_infeasible() && node->increment_read_from()) {
 				mo_graph->rollbackChanges();
@@ -872,11 +874,11 @@ bool ModelChecker::process_read(ModelAction *curr)
 				continue;
 			}
 
+			value = rf->get_value();
 			read_from(curr, rf);
 			mo_graph->commitChanges();
 			mo_check_promises(curr, true);
 
-			updated |= r_status;
 			break;
 		}
 		case READ_FROM_PROMISE: {
@@ -1650,19 +1652,19 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) {
  * 3) that other write must have been in the reads_from set for maxreads times.
  *
  * If so, we decide that the execution is no longer feasible.
+ *
+ * @param curr The current action. Must be a read.
+ * @param rf The store from which we might read.
+ * @return True if the read should succeed; false otherwise
  */
-void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
+bool ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) const
 {
 	if (!params.maxreads)
-		return;
+		return true;
 
 	//NOTE: Next check is just optimization, not really necessary....
 	if (curr->get_node()->get_read_from_past_size() <= 1)
-		return;
-	/* Must make sure that execution is currently feasible...  We could
-	 * accidentally clear by rolling back */
-	if (is_infeasible())
-		return;
+		return true;
 
 	std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
 	int tid = id_to_int(curr->get_tid());
@@ -1677,14 +1679,14 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 	/* See if we have enough reads from the same value */
 	for (int count = 0; count < params.maxreads; ritcopy++, count++) {
 		if (ritcopy == list->rend())
-			return;
+			return true;
 		ModelAction *act = *ritcopy;
 		if (!act->is_read())
-			return;
+			return true;
 		if (act->get_reads_from() != rf)
-			return;
+			return true;
 		if (act->get_node()->get_read_from_past_size() <= 1)
-			return;
+			return true;
 	}
 	for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
 		/* Get write */
@@ -1709,11 +1711,10 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 				break;
 			}
 		}
-		if (feasiblewrite) {
-			priv->too_many_reads = true;
-			return;
-		}
+		if (feasiblewrite)
+			return false;
 	}
+	return true;
 }
 
 /**
diff --git a/model.h b/model.h
index 412543db..115d9445 100644
--- a/model.h
+++ b/model.h
@@ -167,7 +167,7 @@ private:
 
 	Thread * take_step(ModelAction *curr);
 
-	void check_recency(ModelAction *curr, const ModelAction *rf);
+	bool check_recency(ModelAction *curr, const ModelAction *rf) const;
 	ModelAction * get_last_fence_conflict(ModelAction *act) const;
 	ModelAction * get_last_conflict(ModelAction *act) const;
 	void set_backtracking(ModelAction *act);