From ee745811958143fe03e854709a649c2954dd6d16 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Wed, 27 Feb 2013 17:30:24 -0800 Subject: [PATCH] nodestack: rename 'read_from' to 'read_from_past' One step of re-architecting the reads-from set in NodeStack (i.e., read from past + promised future values + future values). --- model.cc | 30 ++++++++++++++--------------- nodestack.cc | 54 ++++++++++++++++++++++++++-------------------------- nodestack.h | 25 ++++++++++++------------ 3 files changed, 55 insertions(+), 54 deletions(-) diff --git a/model.cc b/model.cc index 417cbc1c..649f3d95 100644 --- a/model.cc +++ b/model.cc @@ -259,7 +259,7 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) /* The next node will try to satisfy a different set of promises. */ tid = next->get_tid(); node_stack->pop_restofstack(2); - } else if (nextnode->increment_read_from()) { + } else if (nextnode->increment_read_from_past()) { /* The next node will read from a different value. */ tid = next->get_tid(); node_stack->pop_restofstack(2); @@ -851,7 +851,7 @@ bool ModelChecker::process_read(ModelAction *curr) uint64_t value = VALUE_NONE; bool updated = false; while (true) { - const ModelAction *reads_from = curr->get_node()->get_read_from(); + const ModelAction *reads_from = curr->get_node()->get_read_from_past(); if (reads_from != NULL) { mo_graph->startChanges(); @@ -860,7 +860,7 @@ bool ModelChecker::process_read(ModelAction *curr) check_recency(curr, reads_from); bool r_status = r_modification_order(curr, reads_from); - if (is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) { + if (is_infeasible() && (curr->get_node()->increment_read_from_past() || curr->get_node()->increment_future_value())) { mo_graph->rollbackChanges(); priv->too_many_reads = false; continue; @@ -1501,7 +1501,7 @@ void ModelChecker::check_curr_backtracking(ModelAction *curr) if ((parnode && !parnode->backtrack_empty()) || !currnode->misc_empty() || - !currnode->read_from_empty() || + !currnode->read_from_past_empty() || !currnode->future_value_empty() || !currnode->promise_empty() || !currnode->relseq_break_empty()) { @@ -1609,7 +1609,7 @@ ModelAction * ModelChecker::process_rmw(ModelAction *act) { void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) { if (params.maxreads != 0) { - if (curr->get_node()->get_read_from_size() <= 1) + 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 @@ -1642,12 +1642,12 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) if (act->get_reads_from() != rf) return; - if (act->get_node()->get_read_from_size() <= 1) + if (act->get_node()->get_read_from_past_size() <= 1) return; } - for (int i = 0; i < curr->get_node()->get_read_from_size(); i++) { + for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) { /* Get write */ - const ModelAction *write = curr->get_node()->get_read_from_at(i); + const ModelAction *write = curr->get_node()->get_read_from_past(i); /* Need a different write */ if (write == rf) @@ -1665,8 +1665,8 @@ void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) for (int loop = count; loop > 0; loop--, rit++) { ModelAction *act = *rit; bool foundvalue = false; - for (int j = 0; j < act->get_node()->get_read_from_size(); j++) { - if (act->get_node()->get_read_from_at(j) == write) { + 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; } @@ -2631,7 +2631,7 @@ void ModelChecker::build_may_read_from(ModelAction *curr) mo_graph->startChanges(); r_modification_order(curr, act); if (!is_infeasible()) - curr->get_node()->add_read_from(act); + curr->get_node()->add_read_from_past(act); mo_graph->rollbackChanges(); } @@ -2658,7 +2658,7 @@ void ModelChecker::build_may_read_from(ModelAction *curr) } /* We may find no valid may-read-from only if the execution is doomed */ - if (!curr->get_node()->get_read_from_size() && curr->get_node()->future_value_empty()) { + if (!curr->get_node()->get_read_from_past_size() && curr->get_node()->future_value_empty()) { priv->no_valid_reads = true; set_assert(); } @@ -2666,9 +2666,9 @@ void ModelChecker::build_may_read_from(ModelAction *curr) if (DBG_ENABLED()) { model_print("Reached read action:\n"); curr->print(); - model_print("Printing may_read_from\n"); - curr->get_node()->print_may_read_from(); - model_print("End printing may_read_from\n"); + model_print("Printing read_from_past\n"); + curr->get_node()->print_read_from_past(); + model_print("End printing read_from_past\n"); } } diff --git a/nodestack.cc b/nodestack.cc index 9c0df20b..10115af6 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -33,8 +33,8 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) fairness(num_threads), numBacktracks(0), enabled_array(NULL), - may_read_from(), - read_from_index(0), + read_from_past(), + read_from_past_idx(0), future_values(), future_index(-1), relseq_break_writes(), @@ -103,9 +103,9 @@ void Node::print() const model_print("[%#" PRIx64 "]", future_values[i].value); model_print("\n"); - model_print(" read-from: %s", read_from_empty() ? "empty" : "non-empty "); - for (int i = read_from_index + 1; i < (int)may_read_from.size(); i++) - model_print("[%d]", may_read_from[i]->get_seq_number()); + model_print(" read-from: %s", read_from_past_empty() ? "empty" : "non-empty "); + for (int i = read_from_past_idx + 1; i < (int)read_from_past.size(); i++) + model_print("[%d]", read_from_past[i]->get_seq_number()); model_print("\n"); model_print(" promises: %s\n", promise_empty() ? "empty" : "non-empty"); @@ -113,11 +113,11 @@ void Node::print() const model_print(" rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty"); } -/** @brief Prints info about may_read_from set */ -void Node::print_may_read_from() +/** @brief Prints info about read_from_past set */ +void Node::print_read_from_past() { - for (unsigned int i = 0; i < may_read_from.size(); i++) - may_read_from[i]->print(); + for (unsigned int i = 0; i < read_from_past.size(); i++) + read_from_past[i]->print(); } /** @@ -292,9 +292,9 @@ bool Node::backtrack_empty() const * Checks whether the readsfrom set for this node is empty. * @return true if the readsfrom set is empty. */ -bool Node::read_from_empty() const +bool Node::read_from_past_empty() const { - return ((read_from_index + 1) >= may_read_from.size()); + return ((read_from_past_idx + 1) >= read_from_past.size()); } /** @@ -383,12 +383,12 @@ bool Node::has_priority(thread_id_t tid) const } /** - * Add an action to the may_read_from set. + * Add an action to the read_from_past set. * @param act is the action to add */ -void Node::add_read_from(const ModelAction *act) +void Node::add_read_from_past(const ModelAction *act) { - may_read_from.push_back(act); + read_from_past.push_back(act); } /** @@ -402,25 +402,25 @@ struct future_value Node::get_future_value() const return future_values[future_index]; } -int Node::get_read_from_size() const +int Node::get_read_from_past_size() const { - return may_read_from.size(); + return read_from_past.size(); } -const ModelAction * Node::get_read_from_at(int i) const +const ModelAction * Node::get_read_from_past(int i) const { - return may_read_from[i]; + return read_from_past[i]; } /** - * Gets the next 'may_read_from' action from this Node. Only valid for a node + * Gets the next 'read_from_past' action from this Node. Only valid for a node * where this->action is a 'read'. - * @return The first element in may_read_from + * @return The first element in read_from_past */ -const ModelAction * Node::get_read_from() const +const ModelAction * Node::get_read_from_past() const { - if (read_from_index < may_read_from.size()) - return may_read_from[read_from_index]; + if (read_from_past_idx < read_from_past.size()) + return read_from_past[read_from_past_idx]; else return NULL; } @@ -429,13 +429,13 @@ const ModelAction * Node::get_read_from() const * Increments the index into the readsfrom set to explore the next item. * @return Returns false if we have explored all items. */ -bool Node::increment_read_from() +bool Node::increment_read_from_past() { DBG(); promises.clear(); - if (read_from_index < may_read_from.size()) { - read_from_index++; - return read_from_index < may_read_from.size(); + if (read_from_past_idx < read_from_past.size()) { + read_from_past_idx++; + return read_from_past_idx < read_from_past.size(); } return false; } diff --git a/nodestack.h b/nodestack.h index 941178d7..6200887a 100644 --- a/nodestack.h +++ b/nodestack.h @@ -77,12 +77,12 @@ public: bool increment_future_value(); bool future_value_empty() const; - void add_read_from(const ModelAction *act); - const ModelAction * get_read_from() const; - bool increment_read_from(); - bool read_from_empty() const; - int get_read_from_size() const; - const ModelAction * get_read_from_at(int i) const; + void add_read_from_past(const ModelAction *act); + const ModelAction * get_read_from_past() const; + bool increment_read_from_past(); + bool read_from_past_empty() const; + int get_read_from_past_size() const; + const ModelAction * get_read_from_past(int i) const; void set_promise(unsigned int i, bool is_rmw); bool get_promise(unsigned int i) const; @@ -101,7 +101,7 @@ public: bool relseq_break_empty() const; void print() const; - void print_may_read_from(); + void print_read_from_past(); MEMALLOC private: @@ -116,11 +116,12 @@ private: int numBacktracks; enabled_type_t *enabled_array; - /** The set of ModelActions that this the action at this Node may read - * from. Only meaningful if this Node represents a 'read' action. */ - std::vector< const ModelAction *, ModelAlloc< const ModelAction * > > may_read_from; - - unsigned int read_from_index; + /** + * The set of past ModelActions that this the action at this Node may + * read from. Only meaningful if this Node represents a 'read' action. + */ + std::vector< const ModelAction *, ModelAlloc< const ModelAction * > > read_from_past; + unsigned int read_from_past_idx; std::vector< struct future_value, ModelAlloc > future_values; std::vector< promise_t, ModelAlloc > promises; -- 2.34.1