From: Brian Norris <banorris@uci.edu>
Date: Wed, 23 Jan 2013 19:49:01 +0000 (-0800)
Subject: promise: refactor eliminate_thread()/check_promise()
X-Git-Tag: oopsla2013~339
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=014ccdb9492a8e6f36dadb3a7e0a45e5f3d39bee

promise: refactor eliminate_thread()/check_promise()

eliminate_thread() and check_promise() have near-duplicate code, for
checking if the promise has failed. This change makes them consistent
(check_promise() now knows to eliminate its own thread immediately) and
allows one function to simply call the other.
---

diff --git a/promise.cc b/promise.cc
index 943a0f4..c3aee51 100644
--- a/promise.cc
+++ b/promise.cc
@@ -19,21 +19,15 @@ bool Promise::eliminate_thread(thread_id_t tid)
 		return false;
 
 	synced_thread[id] = true;
-	unsigned int sync_size = synced_thread.size();
-	int promise_tid = id_to_int(read->get_tid());
-	for (unsigned int i = 1; i < model->get_num_threads(); i++) {
-		if ((i >= sync_size || !synced_thread[i]) && ((int)i != promise_tid) && model->is_enabled(int_to_id(i))) {
-			return false;
-		}
-	}
-	return true;
+	return check_promise();
 }
 
 bool Promise::check_promise() const
 {
 	unsigned int sync_size = synced_thread.size();
+	int promise_tid = id_to_int(read->get_tid());
 	for (unsigned int i = 1; i < model->get_num_threads(); i++) {
-		if ((i >= sync_size || !synced_thread[i]) && model->is_enabled(int_to_id(i))) {
+		if ((i >= sync_size || !synced_thread[i]) && ((int)i != promise_tid) && model->is_enabled(int_to_id(i))) {
 			return false;
 		}
 	}