From 89bcfc74c2999b15984759e5b0eab4a9c46feaf3 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 1 Mar 2013 19:25:29 -0800 Subject: [PATCH] check_recency: implement loops as function ModelAction::may_read_from() This strange loop makes more sense with a name, associated with the ModelAction class. --- action.cc | 26 ++++++++++++++++++++++++++ action.h | 3 +++ model.cc | 10 +--------- 3 files changed, 30 insertions(+), 9 deletions(-) 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; } -- 2.34.1