X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=nodestack.cc;h=f0d79245cd8aa2e648a5071f50e66e48f5bdc3d9;hb=05d91de8ac8098425d51e9af2704eb91e04a7f9b;hp=06259b91c54964ba4c094af50347c11a23d9cb41;hpb=fe7b400edb33255770fb47ad520afbd05d13a231;p=model-checker.git diff --git a/nodestack.cc b/nodestack.cc index 06259b9..f0d7924 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -91,7 +91,7 @@ void Node::print() if (action) action->print(); else - printf("******** empty action ********\n"); + model_print("******** empty action ********\n"); } /** @brief Prints info about may_read_from set */ @@ -105,11 +105,14 @@ 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) { +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) + if (promises[i] == PROMISE_IGNORE) { promises[i] = PROMISE_UNFULFILLED; + if (is_rmw) + promises[i] |= PROMISE_RMW; + } } /** @@ -117,8 +120,9 @@ void Node::set_promise(unsigned int i) { * @param i The promise index. * @return true if the promise should be satisfied by the given model action. */ -bool Node::get_promise(unsigned int i) { - return (i < promises.size()) && (promises[i] == PROMISE_FULFILLED); +bool Node::get_promise(unsigned int i) const +{ + return (i < promises.size()) && ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED); } /** @@ -127,16 +131,27 @@ bool Node::get_promise(unsigned int i) { */ bool Node::increment_promise() { DBG(); - + unsigned int rmw_count=0; + for (unsigned int i = 0; i < promises.size(); i++) { + if (promises[i]==(PROMISE_RMW|PROMISE_FULFILLED)) + rmw_count++; + } + for (unsigned int i = 0; i < promises.size(); i++) { - if (promises[i] == PROMISE_UNFULFILLED) { - promises[i] = PROMISE_FULFILLED; + if ((promises[i] & PROMISE_MASK) == PROMISE_UNFULFILLED) { + if ((rmw_count > 0) && (promises[i] & PROMISE_RMW)) { + //sending our value to two rmws... not going to work..try next combination + continue; + } + promises[i] = (promises[i] & PROMISE_RMW) |PROMISE_FULFILLED; while (i > 0) { i--; - if (promises[i] == PROMISE_FULFILLED) - promises[i] = PROMISE_UNFULFILLED; + if ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED) + promises[i] = (promises[i] & PROMISE_RMW) | PROMISE_UNFULFILLED; } return true; + } else if (promises[i] == (PROMISE_RMW|PROMISE_FULFILLED)) { + rmw_count--; } } return false; @@ -146,10 +161,17 @@ bool Node::increment_promise() { * Returns whether the promise set is empty. * @return true if we have explored all promise combinations. */ -bool Node::promise_empty() { - for (unsigned int i = 0; i < promises.size();i++) - if (promises[i] == PROMISE_UNFULFILLED) +bool Node::promise_empty() const +{ + bool fulfilledrmw=false; + for (int i = promises.size()-1 ; i>=0; i--) { + if (promises[i]==PROMISE_UNFULFILLED) + return false; + if (!fulfilledrmw && ((promises[i]&PROMISE_MASK)==PROMISE_UNFULFILLED)) return false; + if (promises[i]==(PROMISE_FULFILLED|PROMISE_RMW)) + fulfilledrmw=true; + } return true; } @@ -158,7 +180,8 @@ void Node::set_misc_max(int i) { misc_max=i; } -int Node::get_misc() { +int Node::get_misc() const +{ return misc_index; } @@ -166,32 +189,46 @@ bool Node::increment_misc() { return (misc_index=misc_max; } /** - * Adds a value from a weakly ordered future write to backtrack to. + * 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(uint64_t value, modelclock_t expiration) { - int suitableindex=-1; + 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].expiration>=expiration) + if (expiration <= future_values[i].expiration) return false; - if (future_index < ((int) i)) { - suitableindex=i; - } + idx = i; } } - - if (suitableindex!=-1) { - future_values[suitableindex].expiration=expiration; + 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; } - struct future_value newfv={value, expiration}; + + /* Limit the size of the future-values set */ + if (model->params.maxfuturevalues > 0 && + (int)future_values.size() >= model->params.maxfuturevalues) + return false; + + struct future_value newfv = {value, expiration}; future_values.push_back(newfv); return true; } @@ -200,7 +237,8 @@ bool Node::add_future_value(uint64_t value, modelclock_t expiration) { * 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() { +bool Node::future_value_empty() const +{ return ((future_index + 1) >= ((int)future_values.size())); } @@ -211,7 +249,7 @@ bool Node::future_value_empty() { * @return true if this thread choice has been explored already, false * otherwise */ -bool Node::has_been_explored(thread_id_t tid) +bool Node::has_been_explored(thread_id_t tid) const { int id = id_to_int(tid); return explored_children[id]; @@ -221,7 +259,7 @@ bool Node::has_been_explored(thread_id_t tid) * Checks if the backtracking set is empty. * @return true if the backtracking set is empty */ -bool Node::backtrack_empty() +bool Node::backtrack_empty() const { return (numBacktracks == 0); } @@ -230,7 +268,8 @@ bool Node::backtrack_empty() * Checks whether the readsfrom set for this node is empty. * @return true if the readsfrom set is empty. */ -bool Node::read_from_empty() { +bool Node::read_from_empty() const +{ return ((read_from_index+1) >= may_read_from.size()); } @@ -262,6 +301,7 @@ void Node::explore_child(ModelAction *act, enabled_type_t * is_enabled) bool Node::set_backtrack(thread_id_t id) { int i = id_to_int(id); + ASSERT(i<((int)backtrack.size())); if (backtrack[i]) return false; backtrack[i] = true; @@ -284,19 +324,28 @@ thread_id_t Node::get_next_backtrack() return int_to_id(i); } -bool Node::is_enabled(Thread *t) +bool Node::is_enabled(Thread *t) const { int thread_id=id_to_int(t->get_id()); return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED); } -bool Node::is_enabled(thread_id_t tid) +enabled_type_t Node::enabled_status(thread_id_t tid) const +{ + int thread_id = id_to_int(tid); + if (thread_id < num_threads) + return enabled_array[thread_id]; + else + return THREAD_DISABLED; +} + +bool Node::is_enabled(thread_id_t tid) const { int thread_id=id_to_int(tid); return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED); } -bool Node::has_priority(thread_id_t tid) +bool Node::has_priority(thread_id_t tid) const { return fairness[id_to_int(tid)].priority; } @@ -315,18 +364,21 @@ void Node::add_read_from(const ModelAction *act) * where this->action is a 'read'. * @return The first element in future_values */ -uint64_t Node::get_future_value() { +uint64_t Node::get_future_value() const +{ ASSERT(future_index >= 0 && future_index<((int)future_values.size())); return future_values[future_index].value; } -modelclock_t Node::get_future_value_expiration() { +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() { +int Node::get_read_from_size() const +{ return may_read_from.size(); } @@ -339,7 +391,8 @@ const ModelAction * Node::get_read_from_at(int i) { * where this->action is a 'read'. * @return The first element in may_read_from */ -const ModelAction * Node::get_read_from() { +const ModelAction * Node::get_read_from() const +{ if (read_from_index < may_read_from.size()) return may_read_from[read_from_index]; else @@ -394,7 +447,7 @@ void Node::add_relseq_break(const ModelAction *write) * @return A write that may break the release sequence. If NULL, that means * the release sequence should not be broken. */ -const ModelAction * Node::get_relseq_break() +const ModelAction * Node::get_relseq_break() const { if (relseq_break_index < (int)relseq_break_writes.size()) return relseq_break_writes[relseq_break_index]; @@ -422,13 +475,15 @@ bool Node::increment_relseq_break() * @return True if all writes that may break the release sequence have been * explored */ -bool Node::relseq_break_empty() { +bool Node::relseq_break_empty() const +{ return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size())); } 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--; @@ -450,16 +505,16 @@ NodeStack::~NodeStack() delete node_list[i]; } -void NodeStack::print() +void NodeStack::print() const { - printf("............................................\n"); - printf("NodeStack printing node_list:\n"); + model_print("............................................\n"); + model_print("NodeStack printing node_list:\n"); for (unsigned int it = 0; it < node_list.size(); it++) { if (it == this->iter) - printf("vvv following action is the current iterator vvv\n"); + model_print("vvv following action is the current iterator vvv\n"); node_list[it]->print(); } - printf("............................................\n"); + model_print("............................................\n"); } /** Note: The is_enabled set contains what actions were enabled when @@ -505,14 +560,14 @@ void NodeStack::pop_restofstack(int numAhead) node_list.resize(it); } -Node * NodeStack::get_head() +Node * NodeStack::get_head() const { if (node_list.empty()) return NULL; return node_list[iter]; } -Node * NodeStack::get_next() +Node * NodeStack::get_next() const { if (node_list.empty()) { DEBUG("Empty\n");