From: Brian Norris <banorris@uci.edu>
Date: Wed, 23 Jan 2013 20:36:28 +0000 (-0800)
Subject: promise: rename has_sync_thread() -> thread_is_eliminated()
X-Git-Tag: oopsla2013~337
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=c49d1c1de40847e0133b61137422005ec1cc69fd

promise: rename has_sync_thread() -> thread_is_eliminated()

This function doesn't actually check for synchronization; there are
numerous ways to be eliminated.
---

diff --git a/model.cc b/model.cc
index 0964ae7..ac88933 100644
--- a/model.cc
+++ b/model.cc
@@ -2459,7 +2459,7 @@ void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write,
 		}
 
 		//Don't do any lookups twice for the same thread
-		if (promise->has_sync_thread(tid))
+		if (promise->thread_is_eliminated(tid))
 			continue;
 
 		if (promise->get_write() && mo_graph->checkReachable(promise->get_write(), write)) {
diff --git a/promise.cc b/promise.cc
index 7b11002..3b2aa96 100644
--- a/promise.cc
+++ b/promise.cc
@@ -13,12 +13,12 @@
 bool Promise::eliminate_thread(thread_id_t tid)
 {
 	unsigned int id = id_to_int(tid);
-	if (id >= synced_thread.size())
-		synced_thread.resize(id + 1, false);
-	if (synced_thread[id])
+	if (id >= eliminated_thread.size())
+		eliminated_thread.resize(id + 1, false);
+	if (eliminated_thread[id])
 		return false;
 
-	synced_thread[id] = true;
+	eliminated_thread[id] = true;
 	return has_failed();
 }
 
@@ -30,10 +30,10 @@ bool Promise::eliminate_thread(thread_id_t tid)
  */
 bool Promise::has_failed() const
 {
-	unsigned int sync_size = synced_thread.size();
+	unsigned int size = eliminated_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))) {
+		if ((i >= size || !eliminated_thread[i]) && ((int)i != promise_tid) && model->is_enabled(int_to_id(i))) {
 			return false;
 		}
 	}
diff --git a/promise.h b/promise.h
index f30779c..9fd6552 100644
--- a/promise.h
+++ b/promise.h
@@ -32,11 +32,18 @@ class Promise {
 	ModelAction * get_action() const { return read; }
 	bool eliminate_thread(thread_id_t tid);
 
-	bool has_sync_thread(thread_id_t tid) {
+	/**
+	 * Check if a thread has already been eliminated from resolving this
+	 * promise
+	 * @param tid Thread ID of the thread to check
+	 * @return True if the thread is already eliminated; false otherwise
+	 */
+	bool thread_is_eliminated(thread_id_t tid) const
+	{
 		unsigned int id = id_to_int(tid);
-		if (id >= synced_thread.size())
+		if (id >= eliminated_thread.size())
 			return false;
-		return synced_thread[id];
+		return eliminated_thread[id];
 	}
 
 	bool has_failed() const;
@@ -46,7 +53,7 @@ class Promise {
 
 	SNAPSHOTALLOC
  private:
-	std::vector<bool> synced_thread;
+	std::vector<bool> eliminated_thread;
 	const uint64_t value;
 	const modelclock_t expiration;
 	ModelAction * const read;