From: Brian Norris <banorris@uci.edu>
Date: Tue, 26 Feb 2013 01:04:13 +0000 (-0800)
Subject: model: promises: eliminate threads when they "join"
X-Git-Tag: oopsla2013~218
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;ds=sidebyside;h=dbee0c57f6edff31aafb79d6e956f1408bbb8fb8;p=model-checker.git

model: promises: eliminate threads when they "join"

A thread that joins with another thread can no longer satisfy a promise
from that thread.
---

diff --git a/model.cc b/model.cc
index 9e064ea..94bc58b 100644
--- a/model.cc
+++ b/model.cc
@@ -1327,6 +1327,30 @@ bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
 	return false;
 }
 
+/**
+ * Check promises and eliminate potentially-satisfying threads when a thread is
+ * blocked (e.g., join, lock). A thread which is waiting on another thread can
+ * no longer satisfy a promise generated from that thread.
+ *
+ * @param blocker The thread on which a thread is waiting
+ * @param waiting The waiting thread
+ */
+void ModelChecker::thread_blocking_check_promises(Thread *blocker, Thread *waiting)
+{
+	for (unsigned int i = 0; i < promises->size(); i++) {
+		Promise *promise = (*promises)[i];
+		ModelAction *reader = promise->get_action();
+		if (reader->get_tid() != blocker->get_id())
+			continue;
+		if (!promise->thread_is_available(waiting->get_id()))
+			continue;
+		if (promise->eliminate_thread(waiting->get_id())) {
+			/* Promise has failed */
+			priv->failed_promise = true;
+		}
+	}
+}
+
 /**
  * @brief Check whether a model action is enabled.
  *
@@ -1350,6 +1374,7 @@ bool ModelChecker::check_action_enabled(ModelAction *curr) {
 		Thread *blocking = (Thread *)curr->get_location();
 		if (!blocking->is_complete()) {
 			blocking->push_wait_list(curr);
+			thread_blocking_check_promises(blocking, get_thread(curr));
 			return false;
 		}
 	}
diff --git a/model.h b/model.h
index ee9d2c7..783f7a6 100644
--- a/model.h
+++ b/model.h
@@ -126,7 +126,6 @@ public:
 	ClockVector * get_cv(thread_id_t tid) const;
 	ModelAction * get_parent_action(thread_id_t tid) const;
 	void check_promises_thread_disabled();
-	void mo_check_promises(const ModelAction *act, bool is_read_check);
 	void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv);
 	bool isfeasibleprefix() const;
 
@@ -179,6 +178,9 @@ private:
 	void compute_promises(ModelAction *curr);
 	void compute_relseq_breakwrites(ModelAction *curr);
 
+	void mo_check_promises(const ModelAction *act, bool is_read_check);
+	void thread_blocking_check_promises(Thread *blocker, Thread *waiting);
+
 	void check_curr_backtracking(ModelAction *curr);
 	void add_action_to_lists(ModelAction *act);
 	ModelAction * get_last_action(thread_id_t tid) const;