From 6caada76d7318c7853dd334bccbfed0367c242ec Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 1 Mar 2013 16:13:25 -0800 Subject: [PATCH] model: we only resolve one promise at a time --- model.cc | 75 +++++++++++++++++++++++++++++++------------------------- model.h | 3 ++- 2 files changed, 44 insertions(+), 34 deletions(-) diff --git a/model.cc b/model.cc index 9135e5c..618b37e 100644 --- a/model.cc +++ b/model.cc @@ -1045,7 +1045,11 @@ void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *read bool ModelChecker::process_write(ModelAction *curr) { bool updated_mod_order = w_modification_order(curr); - bool updated_promises = resolve_promises(curr); + int promise_idx = get_promise_to_resolve(curr); + bool updated_promises = false; + + if (promise_idx >= 0) + updated_promises = resolve_promise(curr, promise_idx); if (promises->size() == 0) { for (unsigned int i = 0; i < futurevalues->size(); i++) { @@ -2452,44 +2456,49 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) const } /** - * Resolve a set of Promises with a current write. The set is provided in the - * Node corresponding to @a write. + * @brief Find the promise, if any to resolve for the current action + * @param curr The current ModelAction. Should be a write. + * @return The (non-negative) index for the Promise to resolve, if any; + * otherwise -1 + */ +int ModelChecker::get_promise_to_resolve(const ModelAction *curr) const +{ + for (unsigned int i = 0; i < promises->size(); i++) + if (curr->get_node()->get_promise(i)) + return i; + return -1; +} + +/** + * Resolve a Promise with a current write. * @param write The ModelAction that is fulfilling Promises - * @return True if promises were resolved; false otherwise + * @param promise_idx The index corresponding to the promise + * @return True if the Promise was successfully resolved; false otherwise */ -bool ModelChecker::resolve_promises(ModelAction *write) +bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx) { - bool haveResolved = false; std::vector< ModelAction *, ModelAlloc > actions_to_check; - promise_list_t mustResolve, resolved; - - 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)) { - for (unsigned int j = 0; j < promise->get_num_readers(); j++) { - ModelAction *read = promise->get_reader(j); - read_from(read, write); - actions_to_check.push_back(read); - } - //Make sure the promise's value matches the write's value - ASSERT(promise->is_compatible(write)); - mo_graph->resolvePromise(promise, write, &mustResolve); - - resolved.push_back(promise); - promises->erase(promises->begin() + promise_index); + promise_list_t mustResolve; + Promise *promise = (*promises)[promise_idx]; - haveResolved = true; - } else - promise_index++; + for (unsigned int i = 0; i < promise->get_num_readers(); i++) { + ModelAction *read = promise->get_reader(i); + read_from(read, write); + actions_to_check.push_back(read); } + /* Make sure the promise's value matches the write's value */ + ASSERT(promise->is_compatible(write) && promise->same_value(write)); + mo_graph->resolvePromise(promise, write, &mustResolve); + + promises->erase(promises->begin() + promise_idx); + + /** @todo simplify the 'mustResolve' stuff */ + ASSERT(mustResolve.size() <= 1); + + if (!mustResolve.empty() && mustResolve[0] != promise) + priv->failed_promise = true; + delete promise; - for (unsigned int i = 0; i < mustResolve.size(); i++) { - if (std::find(resolved.begin(), resolved.end(), mustResolve[i]) - == resolved.end()) - priv->failed_promise = true; - } - for (unsigned int i = 0; i < resolved.size(); i++) - delete resolved[i]; //Check whether reading these writes has made threads unable to //resolve promises @@ -2498,7 +2507,7 @@ bool ModelChecker::resolve_promises(ModelAction *write) mo_check_promises(read, true); } - return haveResolved; + return true; } /** diff --git a/model.h b/model.h index e92137d..fe76d7f 100644 --- a/model.h +++ b/model.h @@ -175,7 +175,8 @@ private: bool set_latest_backtrack(ModelAction *act); ModelAction * get_next_backtrack(); void reset_to_initial_state(); - bool resolve_promises(ModelAction *curr); + int get_promise_to_resolve(const ModelAction *curr) const; + bool resolve_promise(ModelAction *curr, unsigned int promise_idx); void compute_promises(ModelAction *curr); void compute_relseq_breakwrites(ModelAction *curr); -- 2.34.1