From dbee0c57f6edff31aafb79d6e956f1408bbb8fb8 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Mon, 25 Feb 2013 17:04:13 -0800
Subject: [PATCH] model: promises: eliminate threads when they "join"
A thread that joins with another thread can no longer satisfy a promise
from that thread.
---
model.cc | 25 +++++++++++++++++++++++++
model.h | 4 +++-
2 files changed, 28 insertions(+), 1 deletion(-)
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;
--
2.34.1