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 9e064ea2c76bbebbe02fb03fcdf0bbf47a57dfb3..94bc58b6c5a010254ac34a509afe1a135fa1247d 100644 (file)
--- 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 ee9d2c71280175e4dfe0380380b0839cfaa599f5..783f7a6623df79d89d9611214393098e95484a9a 100644 (file)
--- 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;