X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.cc;h=9c0df20b5de89bd2876cde69ca281502506f4709;hb=3f77119600ac3aa246258dec2776056d09f8e4e0;hp=2f99aef24639a9cf128f5083362596aaf0c374e5;hpb=8ea66f246f18e3a92e279a9ba49c29beb2d8ef52;p=model-checker.git diff --git a/nodestack.cc b/nodestack.cc index 2f99aef..9c0df20 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -1,3 +1,6 @@ +#define __STDC_FORMAT_MACROS +#include + #include #include "nodestack.h" @@ -5,6 +8,7 @@ #include "common.h" #include "model.h" #include "threads-model.h" +#include "modeltypes.h" /** * @brief Node constructor @@ -41,13 +45,13 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) ASSERT(act); act->set_node(this); int currtid = id_to_int(act->get_tid()); - int prevtid = (prevfairness != NULL) ? id_to_int(prevfairness->action->get_tid()) : 0; + int prevtid = prevfairness ? id_to_int(prevfairness->action->get_tid()) : 0; if (model->params.fairwindow != 0) { - for (int i = 0; i < nthreads; i++) { + for (int i = 0; i < num_threads; i++) { ASSERT(i < ((int)fairness.size())); struct fairness_info *fi = &fairness[i]; - struct fairness_info *prevfi = (par != NULL) && (i < par->get_num_threads()) ? &par->fairness[i] : NULL; + struct fairness_info *prevfi = (parent && i < parent->get_num_threads()) ? &parent->fairness[i] : NULL; if (prevfi) { *fi = *prevfi; } @@ -86,12 +90,24 @@ Node::~Node() } /** Prints debugging info for the ModelAction associated with this Node */ -void Node::print() +void Node::print() const { action->print(); - model_print(" backtrack: %s\n", backtrack_empty() ? "empty" : "non-empty"); - model_print(" future values: %s\n", future_value_empty() ? "empty" : "non-empty"); - model_print(" read-from: %s\n", read_from_empty() ? "empty" : "non-empty"); + model_print(" backtrack: %s", backtrack_empty() ? "empty" : "non-empty "); + for (int i = 0; i < (int)backtrack.size(); i++) + 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_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("\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"); @@ -108,7 +124,8 @@ void Node::print_may_read_from() * Sets a promise to explore meeting with the given node. * @param i is the promise index. */ -void Node::set_promise(unsigned int i, bool is_rmw) { +void Node::set_promise(unsigned int i, bool is_rmw) +{ if (i >= promises.size()) promises.resize(i + 1, PROMISE_IGNORE); if (promises[i] == PROMISE_IGNORE) { @@ -132,7 +149,8 @@ bool Node::get_promise(unsigned int i) const * Increments to the next combination of promises. * @return true if we have a valid combination. */ -bool Node::increment_promise() { +bool Node::increment_promise() +{ DBG(); unsigned int rmw_count = 0; for (unsigned int i = 0; i < promises.size(); i++) { @@ -146,7 +164,7 @@ bool Node::increment_promise() { //sending our value to two rmws... not going to work..try next combination continue; } - promises[i] = (promises[i] & PROMISE_RMW) |PROMISE_FULFILLED; + promises[i] = (promises[i] & PROMISE_RMW) | PROMISE_FULFILLED; while (i > 0) { i--; if ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED) @@ -170,15 +188,14 @@ bool Node::promise_empty() const for (int i = promises.size() - 1; i >= 0; i--) { if (promises[i] == PROMISE_UNFULFILLED) return false; - if (!fulfilledrmw && ((promises[i]&PROMISE_MASK) == PROMISE_UNFULFILLED)) + if (!fulfilledrmw && ((promises[i] & PROMISE_MASK) == PROMISE_UNFULFILLED)) return false; - if (promises[i] == (PROMISE_FULFILLED|PROMISE_RMW)) + if (promises[i] == (PROMISE_FULFILLED | PROMISE_RMW)) fulfilledrmw = true; } return true; } - void Node::set_misc_max(int i) { misc_max = i; @@ -189,7 +206,8 @@ int Node::get_misc() const return misc_index; } -bool Node::increment_misc() { +bool Node::increment_misc() +{ return (misc_index < misc_max) && ((++misc_index) < misc_max); } @@ -198,7 +216,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 @@ -209,10 +226,14 @@ bool Node::misc_empty() const * @param value is the value to backtrack to. * @return True if the future value was successully added; false otherwise */ -bool Node::add_future_value(uint64_t value, modelclock_t expiration) { +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) { + if (future_values[i].value == value && future_values[i].tid == tid) { if (expiration <= future_values[i].expiration) return false; idx = i; @@ -232,8 +253,7 @@ bool Node::add_future_value(uint64_t value, modelclock_t expiration) { (int)future_values.size() >= model->params.maxfuturevalues) return false; - struct future_value newfv = {value, expiration}; - future_values.push_back(newfv); + future_values.push_back(fv); return true; } @@ -328,6 +348,14 @@ thread_id_t Node::get_next_backtrack() return int_to_id(i); } +void Node::clear_backtracking() +{ + for (unsigned int i = 0; i < backtrack.size(); i++) + backtrack[i] = false; + for (unsigned int i = 0; i < explored_children.size(); i++) + explored_children[i] = false; +} + bool Node::is_enabled(Thread *t) const { int thread_id = id_to_int(t->get_id()); @@ -364,23 +392,16 @@ void Node::add_read_from(const ModelAction *act) } /** - * Gets the next 'future_value' value from this Node. Only valid for a node - * where this->action is a 'read'. + * 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 */ -uint64_t Node::get_future_value() const +struct future_value Node::get_future_value() const { ASSERT(future_index >= 0 && future_index < ((int)future_values.size())); - return future_values[future_index].value; + return future_values[future_index]; } -modelclock_t Node::get_future_value_expiration() const -{ - ASSERT(future_index >= 0 && future_index < ((int)future_values.size())); - return future_values[future_index].expiration; -} - - int Node::get_read_from_size() const { return may_read_from.size(); @@ -408,7 +429,8 @@ 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() +{ DBG(); promises.clear(); if (read_from_index < may_read_from.size()) { @@ -422,7 +444,8 @@ bool Node::increment_read_from() { * Increments the index into the future_values set to explore the next item. * @return Returns false if we have explored all values. */ -bool Node::increment_future_value() { +bool Node::increment_future_value() +{ DBG(); promises.clear(); if (future_index < ((int)future_values.size())) { @@ -541,7 +564,11 @@ ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_ena if (model->params.fairwindow != 0 && head_idx > (int)model->params.fairwindow) prevfairness = node_list[head_idx - model->params.fairwindow]; } - node_list.push_back(new Node(act, head, model->get_num_threads(), prevfairness)); + + int next_threads = model->get_num_threads(); + if (act->get_type() == THREAD_CREATE) + next_threads++; + node_list.push_back(new Node(act, head, next_threads, prevfairness)); total_nodes++; head_idx++; return NULL; @@ -562,6 +589,7 @@ void NodeStack::pop_restofstack(int numAhead) for (unsigned int i = it; i < node_list.size(); i++) delete node_list[i]; node_list.resize(it); + node_list.back()->clear_backtracking(); } Node * NodeStack::get_head() const