check_recency: implement loops as function ModelAction::may_read_from()
authorBrian Norris <banorris@uci.edu>
Sat, 2 Mar 2013 03:25:29 +0000 (19:25 -0800)
committerBrian Norris <banorris@uci.edu>
Sat, 2 Mar 2013 03:28:33 +0000 (19:28 -0800)
This strange loop makes more sense with a name, associated with the
ModelAction class.

action.cc
action.h
model.cc

index 757b3d1..893c812 100644 (file)
--- 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;
+}
index c546f57..7c9146f 100644 (file)
--- 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:
 
index d523fc2..fba9cf0 100644 (file)
--- 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;
                        }