From: Brian Norris Date: Thu, 28 Feb 2013 02:48:46 +0000 (-0800) Subject: nodestack: bugfix - rewrite 'may-read-from' and 'future values' as the same set X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=ab9a8cb068ff8fbc2f913c2c4be0fb4cede98743 nodestack: bugfix - rewrite 'may-read-from' and 'future values' as the same set There were some subtle bugs that appeared because of the difficulty in iterating over two separate sets that represent the "read from" set for a particular read. Now, we expose an interface where there's just a single pair of functions 'increment_read_from()' and 'read_from_empty()', for iterating over this set, along with a flag-check 'get_read_from_status()', so that we know where to grab values from (get_read_from_past() or get_future_value()). This also does a lot of code moving and documentation in nodestack.cc, for better readability and organization. --- diff --git a/model.cc b/model.cc index 73bafc00..ced34316 100644 --- a/model.cc +++ b/model.cc @@ -259,14 +259,10 @@ 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_past()) { + } else if (nextnode->increment_read_from()) { /* The next node will read from a different value. */ tid = next->get_tid(); node_stack->pop_restofstack(2); - } else if (nextnode->increment_future_value()) { - /* The next node will try to read from a different future value. */ - tid = next->get_tid(); - node_stack->pop_restofstack(2); } else if (nextnode->increment_relseq_break()) { /* The next node will try to resolve a release sequence differently */ tid = next->get_tid(); @@ -852,16 +848,17 @@ bool ModelChecker::process_read(ModelAction *curr) uint64_t value = VALUE_NONE; bool updated = false; while (true) { - const ModelAction *rf = node->get_read_from_past(); - if (rf != NULL) { - mo_graph->startChanges(); + 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); - if (is_infeasible() && (node->increment_read_from_past() || node->increment_future_value())) { + if (is_infeasible() && node->increment_read_from()) { mo_graph->rollbackChanges(); priv->too_many_reads = false; continue; @@ -872,7 +869,9 @@ bool ModelChecker::process_read(ModelAction *curr) mo_check_promises(curr, true); updated |= r_status; - } else { + break; + } + case READ_FROM_FUTURE: { /* Read from future value */ struct future_value fv = node->get_future_value(); Promise *promise = new Promise(curr, fv); @@ -882,6 +881,10 @@ bool ModelChecker::process_read(ModelAction *curr) mo_graph->startChanges(); updated = r_modification_order(curr, promise); mo_graph->commitChanges(); + break; + } + default: + ASSERT(false); } get_thread(curr)->set_return_value(value); return updated; @@ -1502,8 +1505,7 @@ void ModelChecker::check_curr_backtracking(ModelAction *curr) if ((parnode && !parnode->backtrack_empty()) || !currnode->misc_empty() || - !currnode->read_from_past_empty() || - !currnode->future_value_empty() || + !currnode->read_from_empty() || !currnode->promise_empty() || !currnode->relseq_break_empty()) { set_latest_backtrack(curr); @@ -2659,7 +2661,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_past_size() && curr->get_node()->future_value_empty()) { + if (!curr->get_node()->read_from_size()) { priv->no_valid_reads = true; set_assert(); } diff --git a/nodestack.cc b/nodestack.cc index 10115af6..730c7024 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -24,8 +24,9 @@ * @param nthreads The number of threads which exist at this point in the * execution trace. */ -Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) - : action(act), +Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) : + read_from_status(READ_FROM_PAST), + action(act), parent(par), num_threads(nthreads), explored_children(num_threads), @@ -98,28 +99,22 @@ void Node::print() const if (backtrack[i] == true) model_print("[%d]", i); model_print("\n"); - model_print(" future values: %s", future_value_empty() ? "empty" : "non-empty "); - for (int i = future_index + 1; i < (int)future_values.size(); i++) - model_print("[%#" PRIx64 "]", future_values[i].value); - model_print("\n"); - model_print(" read-from: %s", read_from_past_empty() ? "empty" : "non-empty "); + model_print(" read from past: %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(" future values: %s", future_value_empty() ? "empty" : "non-empty "); + for (int i = future_index + 1; i < (int)future_values.size(); i++) + model_print("[%#" PRIx64 "]", future_values[i].value); + model_print("\n"); + model_print(" promises: %s\n", promise_empty() ? "empty" : "non-empty"); model_print(" misc: %s\n", misc_empty() ? "empty" : "non-empty"); model_print(" rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty"); } -/** @brief Prints info about read_from_past set */ -void Node::print_read_from_past() -{ - for (unsigned int i = 0; i < read_from_past.size(); i++) - read_from_past[i]->print(); -} - /** * Sets a promise to explore meeting with the given node. * @param i is the promise index. @@ -216,56 +211,6 @@ bool Node::misc_empty() const return (misc_index + 1) >= misc_max; } -/** - * Adds a value from a weakly ordered future write to backtrack to. This - * operation may "fail" if the future value has already been run (within some - * sloppiness window of this expiration), or if the futurevalues set has - * reached its maximum. - * @see model_params.maxfuturevalues - * - * @param value is the value to backtrack to. - * @return True if the future value was successully added; false otherwise - */ -bool Node::add_future_value(struct future_value fv) -{ - uint64_t value = fv.value; - modelclock_t expiration = fv.expiration; - thread_id_t tid = fv.tid; - int idx = -1; /* Highest index where value is found */ - for (unsigned int i = 0; i < future_values.size(); i++) { - if (future_values[i].value == value && future_values[i].tid == tid) { - if (expiration <= future_values[i].expiration) - return false; - idx = i; - } - } - if (idx > future_index) { - /* Future value hasn't been explored; update expiration */ - future_values[idx].expiration = expiration; - return true; - } else if (idx >= 0 && expiration <= future_values[idx].expiration + model->params.expireslop) { - /* Future value has been explored and is within the "sloppy" window */ - return false; - } - - /* Limit the size of the future-values set */ - if (model->params.maxfuturevalues > 0 && - (int)future_values.size() >= model->params.maxfuturevalues) - return false; - - future_values.push_back(fv); - return true; -} - -/** - * Checks whether the future_values set for this node is empty. - * @return true if the future_values set is empty. - */ -bool Node::future_value_empty() const -{ - return ((future_index + 1) >= ((int)future_values.size())); -} - /** * Checks if the Thread associated with this thread ID has been explored from * this Node already. @@ -288,15 +233,6 @@ bool Node::backtrack_empty() const return (numBacktracks == 0); } -/** - * Checks whether the readsfrom set for this node is empty. - * @return true if the readsfrom set is empty. - */ -bool Node::read_from_past_empty() const -{ - return ((read_from_past_idx + 1) >= read_from_past.size()); -} - /** * Mark the appropriate backtracking information for exploring a thread choice. * @param act The ModelAction to explore @@ -382,34 +318,74 @@ bool Node::has_priority(thread_id_t tid) const return fairness[id_to_int(tid)].priority; } +/*********************************** read from ********************************/ + /** - * Add an action to the read_from_past set. - * @param act is the action to add + * Get the current state of the may-read-from set iteration + * @return The read-from type we should currently be checking (past or future) */ -void Node::add_read_from_past(const ModelAction *act) +read_from_type_t Node::get_read_from_status() { - read_from_past.push_back(act); + if (read_from_status == READ_FROM_PAST && read_from_past.empty()) + increment_read_from(); + return read_from_status; } /** - * Gets the next 'future_value' from this Node. Only valid for a node where - * this->action is a 'read'. - * @return The first element in future_values + * Iterate one step in the may-read-from iteration. This includes a step in + * reading from the either the past or the future. + * @return True if there is a new read-from to explore; false otherwise */ -struct future_value Node::get_future_value() const +bool Node::increment_read_from() { - ASSERT(future_index >= 0 && future_index < ((int)future_values.size())); - return future_values[future_index]; + promises.clear(); + if (increment_read_from_past()) { + read_from_status = READ_FROM_PAST; + return true; + } else if (increment_future_value()) { + read_from_status = READ_FROM_FUTURE; + return true; + } + read_from_status = READ_FROM_NONE; + return false; } -int Node::get_read_from_past_size() const +/** + * @return True if there are any new read-froms to explore + */ +bool Node::read_from_empty() const { - return read_from_past.size(); + return read_from_past_empty() && future_value_empty(); } -const ModelAction * Node::get_read_from_past(int i) const +/** + * Get the total size of the may-read-from set, including both past and future + * values + * @return The size of may-read-from + */ +unsigned int Node::read_from_size() const { - return read_from_past[i]; + return read_from_past.size() + future_values.size(); +} + +/******************************* end read from ********************************/ + +/****************************** read from past ********************************/ + +/** @brief Prints info about read_from_past set */ +void Node::print_read_from_past() +{ + for (unsigned int i = 0; i < read_from_past.size(); i++) + read_from_past[i]->print(); +} + +/** + * Add an action to the read_from_past set. + * @param act is the action to add + */ +void Node::add_read_from_past(const ModelAction *act) +{ + read_from_past.push_back(act); } /** @@ -425,6 +401,25 @@ const ModelAction * Node::get_read_from_past() const return NULL; } +const ModelAction * Node::get_read_from_past(int i) const +{ + return read_from_past[i]; +} + +int Node::get_read_from_past_size() const +{ + return read_from_past.size(); +} + +/** + * Checks whether the readsfrom set for this node is empty. + * @return true if the readsfrom set is empty. + */ +bool Node::read_from_past_empty() const +{ + return ((read_from_past_idx + 1) >= read_from_past.size()); +} + /** * Increments the index into the readsfrom set to explore the next item. * @return Returns false if we have explored all items. @@ -432,7 +427,6 @@ const ModelAction * Node::get_read_from_past() const bool Node::increment_read_from_past() { DBG(); - promises.clear(); if (read_from_past_idx < read_from_past.size()) { read_from_past_idx++; return read_from_past_idx < read_from_past.size(); @@ -440,6 +434,71 @@ bool Node::increment_read_from_past() return false; } +/************************** end read from past ********************************/ + +/****************************** future values *********************************/ + +/** + * Adds a value from a weakly ordered future write to backtrack to. This + * operation may "fail" if the future value has already been run (within some + * sloppiness window of this expiration), or if the futurevalues set has + * reached its maximum. + * @see model_params.maxfuturevalues + * + * @param value is the value to backtrack to. + * @return True if the future value was successully added; false otherwise + */ +bool Node::add_future_value(struct future_value fv) +{ + uint64_t value = fv.value; + modelclock_t expiration = fv.expiration; + thread_id_t tid = fv.tid; + int idx = -1; /* Highest index where value is found */ + for (unsigned int i = 0; i < future_values.size(); i++) { + if (future_values[i].value == value && future_values[i].tid == tid) { + if (expiration <= future_values[i].expiration) + return false; + idx = i; + } + } + if (idx > future_index) { + /* Future value hasn't been explored; update expiration */ + future_values[idx].expiration = expiration; + return true; + } else if (idx >= 0 && expiration <= future_values[idx].expiration + model->params.expireslop) { + /* Future value has been explored and is within the "sloppy" window */ + return false; + } + + /* Limit the size of the future-values set */ + if (model->params.maxfuturevalues > 0 && + (int)future_values.size() >= model->params.maxfuturevalues) + return false; + + future_values.push_back(fv); + return true; +} + +/** + * Gets the next 'future_value' from this Node. Only valid for a node where + * this->action is a 'read'. + * @return The first element in future_values + */ +struct future_value Node::get_future_value() const +{ + ASSERT(future_index >= 0 && future_index < ((int)future_values.size())); + return future_values[future_index]; +} + +/** + * Checks whether the future_values set for this node is empty. + * @return true if the future_values set is empty. + */ +bool Node::future_value_empty() const +{ + return ((future_index + 1) >= ((int)future_values.size())); +} + /** * Increments the index into the future_values set to explore the next item. * @return Returns false if we have explored all values. @@ -447,7 +506,6 @@ bool Node::increment_read_from_past() bool Node::increment_future_value() { DBG(); - promises.clear(); if (future_index < ((int)future_values.size())) { future_index++; return (future_index < ((int)future_values.size())); @@ -455,6 +513,8 @@ bool Node::increment_future_value() return false; } +/************************** end future values *********************************/ + /** * Add a write ModelAction to the set of writes that may break the release * sequence. This is used during replay exploration of pending release diff --git a/nodestack.h b/nodestack.h index 6200887a..a857084b 100644 --- a/nodestack.h +++ b/nodestack.h @@ -38,6 +38,12 @@ struct fairness_info { bool priority; }; +typedef enum { + READ_FROM_PAST, + READ_FROM_FUTURE, + READ_FROM_NONE, +} read_from_type_t; + /** * @brief A single node in a NodeStack * @@ -72,17 +78,19 @@ public: * occurred previously in the stack. */ Node * get_parent() const { return parent; } - bool add_future_value(struct future_value fv); - struct future_value get_future_value() const; - bool increment_future_value(); - bool future_value_empty() const; + read_from_type_t get_read_from_status(); + bool increment_read_from(); + bool read_from_empty() const; + unsigned int read_from_size() const; + void print_read_from_past(); 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; + int get_read_from_past_size() const; + + bool add_future_value(struct future_value fv); + struct future_value get_future_value() const; void set_promise(unsigned int i, bool is_rmw); bool get_promise(unsigned int i) const; @@ -101,12 +109,17 @@ public: bool relseq_break_empty() const; void print() const; - void print_read_from_past(); MEMALLOC private: void explore(thread_id_t tid); + bool read_from_past_empty() const; + bool increment_read_from_past(); + bool future_value_empty() const; + bool increment_future_value(); + read_from_type_t read_from_status; + ModelAction * const action; Node * const parent; const int num_threads;