X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=nodestack.cc;h=bacd067dcb4b8277408e2efd5685fc27bac8e2da;hp=131b06ca6fe1d190ed56f74577676cc81cc3b069;hb=a65e234b607444355eb6e34097ee55ba93d4c01b;hpb=e356dc963edf27f8a97b1ae3d39e276723aa5968 diff --git a/nodestack.cc b/nodestack.cc index 131b06c..bacd067 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -6,9 +6,10 @@ #include "nodestack.h" #include "action.h" #include "common.h" -#include "model.h" #include "threads-model.h" #include "modeltypes.h" +#include "execution.h" +#include "params.h" /** * @brief Node constructor @@ -18,15 +19,19 @@ * as an empty stub, to represent the first thread "choice") and up to one * parent. * + * @param params The model-checker parameters * @param act The ModelAction to associate with this Node. May be NULL. * @param par The parent Node in the NodeStack. May be NULL if there is no * parent. * @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) : +Node::Node(const struct model_params *params, ModelAction *act, Node *par, + int nthreads, Node *prevfairness) : read_from_status(READ_FROM_PAST), action(act), + params(params), + uninit_action(NULL), parent(par), num_threads(nthreads), explored_children(num_threads), @@ -45,14 +50,15 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) : relseq_break_writes(), relseq_break_index(0), misc_index(0), - misc_max(0) + misc_max(0), + yield_data(NULL) { ASSERT(act); act->set_node(this); int currtid = id_to_int(act->get_tid()); int prevtid = prevfairness ? id_to_int(prevfairness->action->get_tid()) : 0; - if (model->params.fairwindow != 0) { + if (get_params()->fairwindow != 0) { for (int i = 0; i < num_threads; i++) { ASSERT(i < ((int)fairness.size())); struct fairness_info *fi = &fairness[i]; @@ -78,7 +84,7 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) : * conditions * If we meet the enabled count and have no * turns, give us priority */ - if ((fi->enabled_count >= model->params.enabledcount) && + if ((fi->enabled_count >= get_params()->enabledcount) && (fi->turns == 0)) fi->priority = true; } @@ -86,18 +92,82 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) : } } +int Node::get_yield_data(int tid1, int tid2) const { + if (tid1get_tid()); + + for(int u = 0; u < num_threads; u++) { + for(int v = 0; v < num_threads; v++) { + int yield_state=parent->get_yield_data(u, v); + bool next_enabled=scheduler->is_enabled(int_to_id(v)); + bool curr_enabled=parent->is_enabled(int_to_id(v)); + if (!next_enabled) { + //Compute intersection of ES and E + yield_state&=~YIELD_E; + //Check to see if we disabled the thread + if (u==curr_tid && curr_enabled) + yield_state|=YIELD_D; + } + yield_data[YIELD_INDEX(u, v, num_threads)]=yield_state; + } + yield_data[YIELD_INDEX(u, curr_tid, num_threads)]=(yield_data[YIELD_INDEX(u, curr_tid, num_threads)]&~YIELD_P)|YIELD_S; + } + //handle curr.yield(t) part of computation + if (action->is_yield()) { + for(int v = 0; v < num_threads; v++) { + int yield_state=yield_data[YIELD_INDEX(curr_tid, v, num_threads)]; + if ((yield_state & (YIELD_E | YIELD_D)) && (!(yield_state & YIELD_S))) + yield_state |= YIELD_P; + yield_state &= YIELD_P; + if (scheduler->is_enabled(int_to_id(v))) { + yield_state|=YIELD_E; + } + yield_data[YIELD_INDEX(curr_tid, v, num_threads)]=yield_state; + } + } +} + /** @brief Node desctructor */ Node::~Node() { delete action; + if (uninit_action) + delete uninit_action; if (enabled_array) model_free(enabled_array); + if (yield_data) + model_free(yield_data); } /** Prints debugging info for the ModelAction associated with this Node */ void Node::print() const { action->print(); + model_print(" thread status: "); + if (enabled_array) { + for (int i = 0; i < num_threads; i++) { + char str[20]; + enabled_type_to_string(enabled_array[i], str); + model_print("[%d: %s]", i, str); + } + model_print("\n"); + } else + model_print("(info not available)\n"); model_print(" backtrack: %s", backtrack_empty() ? "empty" : "non-empty "); for (int i = 0; i < (int)backtrack.size(); i++) if (backtrack[i] == true) @@ -124,87 +194,7 @@ void Node::print() const model_print(" rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty"); } -/*********************************** promise **********************************/ - -/** - * Sets a promise to explore meeting with the given node. - * @param i is the promise index. - */ -void Node::set_promise(unsigned int i) -{ - if (i >= resolve_promise.size()) - resolve_promise.resize(i + 1, false); - resolve_promise[i] = true; -} - -/** - * Looks up whether a given promise should be satisfied by this node. - * @param i The promise index. - * @return true if the promise should be satisfied by the given ModelAction. - */ -bool Node::get_promise(unsigned int i) const -{ - return (i < resolve_promise.size()) && (int)i == resolve_promise_idx; -} - -/** - * Increments to the next promise to resolve. - * @return true if we have a valid combination. - */ -bool Node::increment_promise() -{ - DBG(); - if (resolve_promise.empty()) - return false; - int prev_idx = resolve_promise_idx; - resolve_promise_idx++; - for ( ; resolve_promise_idx < (int)resolve_promise.size(); resolve_promise_idx++) - if (resolve_promise[resolve_promise_idx]) - return true; - resolve_promise_idx = prev_idx; - return false; -} - -/** - * Returns whether the promise set is empty. - * @return true if we have explored all promise combinations. - */ -bool Node::promise_empty() const -{ - for (int i = resolve_promise_idx + 1; i < (int)resolve_promise.size(); i++) - if (i >= 0 && resolve_promise[i]) - return false; - return true; -} - -/** @brief Clear any promise-resolution information for this Node */ -void Node::clear_promise_resolutions() -{ - resolve_promise.clear(); - resolve_promise_idx = -1; -} - -/******************************* end promise **********************************/ - -void Node::set_misc_max(int i) -{ - misc_max = i; -} - -int Node::get_misc() const -{ - return misc_index; -} - -bool Node::increment_misc() -{ - return (misc_index < misc_max) && ((++misc_index) < misc_max); -} - -bool Node::misc_empty() const -{ - return (misc_index + 1) >= misc_max; -} +/****************************** threads backtracking **************************/ /** * Checks if the Thread associated with this thread ID has been explored from @@ -228,6 +218,17 @@ bool Node::backtrack_empty() const return (numBacktracks == 0); } +void Node::explore(thread_id_t tid) +{ + int i = id_to_int(tid); + ASSERT(i < ((int)backtrack.size())); + if (backtrack[i]) { + backtrack[i] = false; + numBacktracks--; + } + explored_children[i] = true; +} + /** * Mark the appropriate backtracking information for exploring a thread choice. * @param act The ModelAction to explore @@ -285,6 +286,91 @@ void Node::clear_backtracking() backtrack[i] = false; for (unsigned int i = 0; i < explored_children.size(); i++) explored_children[i] = false; + numBacktracks = 0; +} + +/************************** end threads backtracking **************************/ + +/*********************************** promise **********************************/ + +/** + * Sets a promise to explore meeting with the given node. + * @param i is the promise index. + */ +void Node::set_promise(unsigned int i) +{ + if (i >= resolve_promise.size()) + resolve_promise.resize(i + 1, false); + resolve_promise[i] = true; +} + +/** + * Looks up whether a given promise should be satisfied by this node. + * @param i The promise index. + * @return true if the promise should be satisfied by the given ModelAction. + */ +bool Node::get_promise(unsigned int i) const +{ + return (i < resolve_promise.size()) && (int)i == resolve_promise_idx; +} + +/** + * Increments to the next promise to resolve. + * @return true if we have a valid combination. + */ +bool Node::increment_promise() +{ + DBG(); + if (resolve_promise.empty()) + return false; + int prev_idx = resolve_promise_idx; + resolve_promise_idx++; + for ( ; resolve_promise_idx < (int)resolve_promise.size(); resolve_promise_idx++) + if (resolve_promise[resolve_promise_idx]) + return true; + resolve_promise_idx = prev_idx; + return false; +} + +/** + * Returns whether the promise set is empty. + * @return true if we have explored all promise combinations. + */ +bool Node::promise_empty() const +{ + for (int i = resolve_promise_idx + 1; i < (int)resolve_promise.size(); i++) + if (i >= 0 && resolve_promise[i]) + return false; + return true; +} + +/** @brief Clear any promise-resolution information for this Node */ +void Node::clear_promise_resolutions() +{ + resolve_promise.clear(); + resolve_promise_idx = -1; +} + +/******************************* end promise **********************************/ + +void Node::set_misc_max(int i) +{ + misc_max = i; +} + +int Node::get_misc() const +{ + return misc_index; +} + +bool Node::increment_misc() +{ + return (misc_index < misc_max) && ((++misc_index) < misc_max); +} + +bool Node::misc_empty() const +{ + return (misc_index + 1) >= misc_max; } bool Node::is_enabled(Thread *t) const @@ -313,6 +399,11 @@ bool Node::has_priority(thread_id_t tid) const return fairness[id_to_int(tid)].priority; } +bool Node::has_priority_over(thread_id_t tid1, thread_id_t tid2) const +{ + return get_yield_data(id_to_int(tid1), id_to_int(tid2)) & YIELD_P; +} + /*********************************** read from ********************************/ /** @@ -455,13 +546,30 @@ void Node::add_read_from_promise(const ModelAction *reader) * where this->action is a 'read'. * @return The current element in read_from_promises */ -const Promise * Node::get_read_from_promise() const +Promise * Node::get_read_from_promise() const { - if (read_from_promise_idx < 0 || read_from_promise_idx >= ((int)read_from_promises.size())) - return NULL; + ASSERT(read_from_promise_idx >= 0 && read_from_promise_idx < ((int)read_from_promises.size())); return read_from_promises[read_from_promise_idx]->get_reads_from_promise(); } +/** + * Gets a particular 'read-from-promise' form this Node. Only vlaid for a node + * where this->action is a 'read'. + * @param i The index of the Promise to get + * @return The Promise at index i, if the Promise is still available; NULL + * otherwise + */ +Promise * Node::get_read_from_promise(int i) const +{ + return read_from_promises[i]->get_reads_from_promise(); +} + +/** @return The size of the read-from-promise set */ +int Node::get_read_from_promise_size() const +{ + return read_from_promises.size(); +} + /** * Checks whether the read_from_promises set for this node is empty. * @return true if the read_from_promises set is empty. @@ -516,14 +624,14 @@ bool Node::add_future_value(struct future_value fv) /* 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) { + } else if (idx >= 0 && expiration <= future_values[idx].expiration + get_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) + if (get_params()->maxfuturevalues > 0 && + (int)future_values.size() >= get_params()->maxfuturevalues) return false; future_values.push_back(fv); @@ -566,6 +674,8 @@ bool Node::increment_future_value() /************************** end future values *********************************/ +/*********************** breaking release sequences ***************************/ + /** * Add a write ModelAction to the set of writes that may break the release * sequence. This is used during replay exploration of pending release @@ -618,15 +728,27 @@ bool Node::relseq_break_empty() const return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size())); } -void Node::explore(thread_id_t tid) +/******************* end breaking release sequences ***************************/ + +/** + * Increments some behavior's index, if a new behavior is available + * @return True if there is a new behavior available; otherwise false + */ +bool Node::increment_behaviors() { - int i = id_to_int(tid); - ASSERT(i < ((int)backtrack.size())); - if (backtrack[i]) { - backtrack[i] = false; - numBacktracks--; - } - explored_children[i] = true; + /* satisfy a different misc_index values */ + if (increment_misc()) + return true; + /* satisfy a different set of promises */ + if (increment_promise()) + return true; + /* read from a different value */ + if (increment_read_from()) + return true; + /* resolve a release sequence differently */ + if (increment_relseq_break()) + return true; + return false; } NodeStack::NodeStack() : @@ -643,6 +765,20 @@ NodeStack::~NodeStack() delete node_list[i]; } +/** + * @brief Register the model-checker object with this NodeStack + * @param exec The execution structure for the ModelChecker + */ +void NodeStack::register_engine(const ModelExecution *exec) +{ + this->execution = exec; +} + +const struct model_params * NodeStack::get_params() const +{ + return execution->get_params(); +} + void NodeStack::print() const { model_print("............................................\n"); @@ -671,14 +807,14 @@ ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_ena Node *prevfairness = NULL; if (head) { head->explore_child(act, is_enabled); - if (model->params.fairwindow != 0 && head_idx > (int)model->params.fairwindow) - prevfairness = node_list[head_idx - model->params.fairwindow]; + if (get_params()->fairwindow != 0 && head_idx > (int)get_params()->fairwindow) + prevfairness = node_list[head_idx - get_params()->fairwindow]; } - int next_threads = model->get_num_threads(); + int next_threads = execution->get_num_threads(); if (act->get_type() == THREAD_CREATE) next_threads++; - node_list.push_back(new Node(act, head, next_threads, prevfairness)); + node_list.push_back(new Node(get_params(), act, head, next_threads, prevfairness)); total_nodes++; head_idx++; return NULL; @@ -702,6 +838,16 @@ void NodeStack::pop_restofstack(int numAhead) node_list.back()->clear_backtracking(); } +/** Reset the node stack. */ +void NodeStack::full_reset() +{ + for (unsigned int i = 0; i < node_list.size(); i++) + delete node_list[i]; + node_list.clear(); + reset_execution(); + total_nodes = 1; +} + Node * NodeStack::get_head() const { if (node_list.empty() || head_idx < 0)