From: Brian Norris Date: Wed, 22 Aug 2012 23:02:48 +0000 (-0700) Subject: nodestack, model: use uniform spacing, style X-Git-Tag: pldi2013~258 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=637cffd1718142edc63a984ab9818a6eadc54e4b;ds=sidebyside nodestack, model: use uniform spacing, style --- diff --git a/model.cc b/model.cc index dabdda7..531ef7e 100644 --- a/model.cc +++ b/model.cc @@ -564,22 +564,22 @@ ModelAction * ModelChecker::get_parent_action(thread_id_t tid) * @param tid The thread whose clock vector we want * @return Desired clock vector */ -ClockVector * ModelChecker::get_cv(thread_id_t tid) { +ClockVector * ModelChecker::get_cv(thread_id_t tid) +{ return get_parent_action(tid)->get_cv(); } - /** Resolve the given promises. */ - -void ModelChecker::resolve_promises(ModelAction *write) { - for (unsigned int i = 0, promise_index = 0;promise_indexsize(); i++) { - Promise * promise = (*promises)[promise_index]; +void ModelChecker::resolve_promises(ModelAction *write) +{ + for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) { + Promise *promise = (*promises)[promise_index]; if (write->get_node()->get_promise(i)) { - ModelAction * read = promise->get_action(); + ModelAction *read = promise->get_action(); read->read_from(write); r_modification_order(read, write); post_r_modification_order(read, write); - promises->erase(promises->begin()+promise_index); + promises->erase(promises->begin() + promise_index); } else promise_index++; } @@ -587,15 +587,15 @@ void ModelChecker::resolve_promises(ModelAction *write) { /** Compute the set of promises that could potentially be satisfied by * this action. */ - -void ModelChecker::compute_promises(ModelAction *curr) { - for (unsigned int i = 0;isize();i++) { - Promise * promise = (*promises)[i]; - const ModelAction * act = promise->get_action(); - if (!act->happens_before(curr)&& - act->is_read()&& - !act->is_synchronizing(curr)&& - !act->same_thread(curr)&& +void ModelChecker::compute_promises(ModelAction *curr) +{ + for (unsigned int i = 0; i < promises->size(); i++) { + Promise *promise = (*promises)[i]; + const ModelAction *act = promise->get_action(); + if (!act->happens_before(curr) && + act->is_read() && + !act->is_synchronizing(curr) && + !act->same_thread(curr) && promise->get_value() == curr->get_value()) { curr->get_node()->set_promise(i); } @@ -603,12 +603,12 @@ void ModelChecker::compute_promises(ModelAction *curr) { } /** Checks promises in response to change in ClockVector Threads. */ - -void ModelChecker::check_promises(ClockVector *old_cv, ClockVector * merge_cv) { - for (unsigned int i = 0;isize();i++) { - Promise * promise = (*promises)[i]; - const ModelAction * act = promise->get_action(); - if ((old_cv == NULL||!old_cv->synchronized_since(act))&& +void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv) +{ + for (unsigned int i = 0; i < promises->size(); i++) { + Promise *promise = (*promises)[i]; + const ModelAction *act = promise->get_action(); + if ((old_cv == NULL || !old_cv->synchronized_since(act)) && merge_cv->synchronized_since(act)) { //This thread is no longer able to send values back to satisfy the promise int num_synchronized_threads = promise->increment_threads(); diff --git a/nodestack.cc b/nodestack.cc index 47f724d..5c54475 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -61,9 +61,9 @@ void Node::print_may_read_from() * @param i is the promise index. */ void Node::set_promise(unsigned int i) { - if (i>=promises.size()) - promises.resize(i+1,0); - promises[i]=1; + if (i >= promises.size()) + promises.resize(i + 1, 0); + promises[i] = 1; } /** @@ -72,7 +72,7 @@ void Node::set_promise(unsigned int i) { * @return true if the promise should be satisfied by the given model action. */ bool Node::get_promise(unsigned int i) { - return (i0) { + for (unsigned int i = 0; i < promises.size(); i++) { + if (promises[i] == 1) { + promises[i] = 2; + while (i > 0) { i--; - if (promises[i]==2) - promises[i]=1; + if (promises[i] == 2) + promises[i] = 1; } return true; } @@ -99,8 +99,8 @@ bool Node::increment_promise() { * @return true if we have explored all promise combinations. */ bool Node::promise_empty() { - for (unsigned int i=0;i=future_values.size()); + return ((future_index + 1) >= future_values.size()); } /** @@ -153,7 +153,7 @@ bool Node::backtrack_empty() * @return true if the readsfrom set is empty. */ bool Node::read_from_empty() { - return ((read_from_index+1)>=may_read_from.size()); + return ((read_from_index+1) >= may_read_from.size()); } /** @@ -227,7 +227,7 @@ uint64_t Node::get_future_value() { * @return The first element in may_read_from */ const ModelAction * Node::get_read_from() { - if (read_from_index