From: Brian Norris <banorris@uci.edu>
Date: Thu, 24 Jan 2013 03:00:49 +0000 (-0800)
Subject: promise: bugfix - a disabled thread should not be eliminated
X-Git-Tag: oopsla2013~324
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=7823790c1d16dc687bf4bb3d6e3c6de5eb9f6366

promise: bugfix - a disabled thread should not be eliminated

Because we now only consider a subset of threads for satisfying
promises, we can have a disabled thread that still may satisfy a
promise; it could simply synchronize with another unrelated thread, then
continue to generate a write that can resolve the promise.

As a side effect, this change makes "has_failed()" much simpler.
---

diff --git a/promise.cc b/promise.cc
index e3b8d65..2bd6637 100644
--- a/promise.cc
+++ b/promise.cc
@@ -74,11 +74,5 @@ void Promise::print() const
  */
 bool Promise::has_failed() const
 {
-	for (unsigned int i = 0; i < available_thread.size(); i++) {
-		thread_id_t tid = int_to_id(i);
-		if (thread_is_available(tid) && model->is_enabled(tid))
-			return false;
-	}
-	ASSERT(num_available_threads == 0);
-	return true;
+	return num_available_threads == 0;
 }