From: Brian Norris <banorris@uci.edu>
Date: Sat, 2 Mar 2013 03:25:29 +0000 (-0800)
Subject: check_recency: implement loops as function ModelAction::may_read_from()
X-Git-Tag: oopsla2013~184
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=89bcfc74c2999b15984759e5b0eab4a9c46feaf3

check_recency: implement loops as function ModelAction::may_read_from()

This strange loop makes more sense with a name, associated with the
ModelAction class.
---

diff --git a/action.cc b/action.cc
index 757b3d1..893c812 100644
--- a/action.cc
+++ b/action.cc
@@ -613,3 +613,29 @@ unsigned int ModelAction::hash() const
 		hash ^= reads_from->get_seq_number();
 	return hash;
 }
+
+/**
+ * @brief Checks the NodeStack to see if a ModelAction is in our may-read-from set
+ * @param write The ModelAction to check for
+ * @return True if the ModelAction is found; false otherwise
+ */
+bool ModelAction::may_read_from(const ModelAction *write) const
+{
+	for (int i = 0; i < node->get_read_from_past_size(); i++)
+		if (node->get_read_from_past(i) == write)
+			return true;
+	return false;
+}
+
+/**
+ * @brief Checks the NodeStack to see if a Promise is in our may-read-from set
+ * @param promise The Promise to check for
+ * @return True if the Promise is found; false otherwise
+ */
+bool ModelAction::may_read_from(const Promise *promise) const
+{
+	for (int i = 0; i < node->get_read_from_promise_size(); i++)
+		if (node->get_read_from_promise(i) == promise)
+			return true;
+	return false;
+}
diff --git a/action.h b/action.h
index c546f57..7c9146f 100644
--- a/action.h
+++ b/action.h
@@ -155,6 +155,9 @@ public:
 
 	bool equals(const ModelAction *x) const { return this == x; }
 	bool equals(const Promise *x) const { return false; }
+
+	bool may_read_from(const ModelAction *write) const;
+	bool may_read_from(const Promise *promise) const;
 	MEMALLOC
 private:
 
diff --git a/model.cc b/model.cc
index d523fc2..fba9cf0 100644
--- a/model.cc
+++ b/model.cc
@@ -1704,17 +1704,9 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
 
 		bool feasiblewrite = true;
 		/* now we need to see if this write works for everyone */
-
 		for (int loop = params.maxreads; loop > 0; loop--, ritcopy++) {
 			ModelAction *act = *ritcopy;
-			bool foundvalue = false;
-			for (int j = 0; j < act->get_node()->get_read_from_past_size(); j++) {
-				if (act->get_node()->get_read_from_past(j) == write) {
-					foundvalue = true;
-					break;
-				}
-			}
-			if (!foundvalue) {
+			if (!act->may_read_from(write)) {
 				feasiblewrite = false;
 				break;
 			}