X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=nodestack.cc;h=b2ef73cac30108fab56745f89b0542a186fc6410;hp=d4c97652b3c08084d3b08be614638dd054f54913;hb=fcae856e66379752f8d227784d28c424206ab0c1;hpb=ac8e176cd4a8756244c12dbbcaf961d27bfc8a74 diff --git a/nodestack.cc b/nodestack.cc index d4c9765..b2ef73c 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"); @@ -148,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) @@ -172,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; @@ -201,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 @@ -212,11 +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; @@ -236,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; } @@ -368,23 +384,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(); @@ -547,7 +556,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;