From 775ba9f4b05d1a09295b0551c5efbd814b8e15aa Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 23 Aug 2012 17:50:21 -0700 Subject: [PATCH] model: report status of resolved promises The rest of the model checker needs to know when promises are added, so add a return status as a boolean. --- model.cc | 6 +++++- model.h | 2 +- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/model.cc b/model.cc index bd0c3dc..bd4496b 100644 --- a/model.cc +++ b/model.cc @@ -696,9 +696,11 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) * Resolve a set of Promises with a current write. The set is provided in the * Node corresponding to @a write. * @param write The ModelAction that is fulfilling Promises + * @return True if promises were resolved; false otherwise */ -void ModelChecker::resolve_promises(ModelAction *write) +bool ModelChecker::resolve_promises(ModelAction *write) { + bool resolved = false; 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)) { @@ -707,9 +709,11 @@ void ModelChecker::resolve_promises(ModelAction *write) r_modification_order(read, write); post_r_modification_order(read, write); promises->erase(promises->begin() + promise_index); + resolved = true; } else promise_index++; } + return resolved; } /** diff --git a/model.h b/model.h index dea744c..0666472 100644 --- a/model.h +++ b/model.h @@ -93,7 +93,7 @@ private: thread_id_t get_next_replay_thread(); ModelAction * get_next_backtrack(); void reset_to_initial_state(); - void resolve_promises(ModelAction *curr); + bool resolve_promises(ModelAction *curr); void compute_promises(ModelAction *curr); void add_action_to_lists(ModelAction *act); -- 2.34.1