From: Brian Norris <banorris@uci.edu>
Date: Fri, 24 Aug 2012 00:50:21 +0000 (-0700)
Subject: model: report status of resolved promises
X-Git-Tag: pldi2013~248
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=775ba9f4b05d1a09295b0551c5efbd814b8e15aa;p=model-checker.git

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.
---

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);