model: wake up pending (sleep-set) actions for fences

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index fab1a5994feb96e6ee22c59e941b7fc9550ff041..998059e2451e7e652d2493af3fc6785aad9ba542 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -313,14 +313,41 @@ void ModelChecker::execute_sleep_set()
        }
 }
 
+/**
+ * @brief Should the current action wake up a given thread?
+ *
+ * @param curr The current action
+ * @param thread The thread that we might wake up
+ * @return True, if we should wake up the sleeping thread; false otherwise
+ */
+bool ModelChecker::should_wake_up(const ModelAction *curr, const Thread *thread) const
+{
+       const ModelAction *asleep = thread->get_pending();
+       /* Don't allow partial RMW to wake anyone up */
+       if (curr->is_rmwr())
+               return false;
+       /* Synchronizing actions may have been backtracked */
+       if (asleep->could_synchronize_with(curr))
+               return true;
+       /* All acquire/release fences and fence-acquire/store-release */
+       if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
+               return true;
+       /* Fence-release + store can awake load-acquire on the same location */
+       if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
+               ModelAction *fence_release = get_last_fence_release(curr->get_tid());
+               if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
+                       return true;
+       }
+       return false;
+}
+
 void ModelChecker::wake_up_sleeping_actions(ModelAction *curr)
 {
        for (unsigned int i = 0; i < get_num_threads(); i++) {
                Thread *thr = get_thread(int_to_id(i));
                if (scheduler->is_sleep_set(thr)) {
-                       ModelAction *pending_act = thr->get_pending();
-                       if ((!curr->is_rmwr()) && pending_act->could_synchronize_with(curr))
-                               //Remove this thread from sleep set
+                       if (should_wake_up(curr, thr))
+                               /* Remove this thread from sleep set */
                                scheduler->remove_sleep(thr);
                }
        }
@@ -545,6 +572,18 @@ bool ModelChecker::next_execution()
        return true;
 }
 
+/**
+ * @brief Find the last fence-related backtracking conflict for a ModelAction
+ *
+ * This function performs the search for the most recent conflicting action
+ * against which we should perform backtracking, as affected by fence
+ * operations. This includes pairs of potentially-synchronizing actions which
+ * occur due to fence-acquire or fence-release, and hence should be explored in
+ * the opposite execution order.
+ *
+ * @param act The current action
+ * @return The most recent action which conflicts with act due to fences
+ */
 ModelAction * ModelChecker::get_last_fence_conflict(ModelAction *act) const
 {
        /* Only perform release/acquire fence backtracking for stores */
@@ -560,16 +599,22 @@ ModelAction * ModelChecker::get_last_fence_conflict(ModelAction *act) const
        if (!last_release)
                return NULL;
 
-       std::vector< ModelAction *, ModelAlloc<ModelAction *> > acquire_fences(get_num_threads(), NULL);
-       std::vector< ModelAction *, ModelAlloc<ModelAction *> > prior_loads(get_num_threads(), NULL);
-       bool found_acquire_fences = false;
+       /* Skip past the release */
+       action_list_t *list = action_trace;
+       action_list_t::reverse_iterator rit;
+       for (rit = list->rbegin(); rit != list->rend(); rit++)
+               if (*rit == last_release)
+                       break;
+       ASSERT(rit != list->rend());
+
        /* Find a prior:
         *   load-acquire
         * or
         *   load --sb-> fence-acquire */
-       action_list_t *list = action_trace;
-       action_list_t::reverse_iterator rit;
-       for (rit = list->rbegin(); rit != list->rend(); rit++) {
+       std::vector< ModelAction *, ModelAlloc<ModelAction *> > acquire_fences(get_num_threads(), NULL);
+       std::vector< ModelAction *, ModelAlloc<ModelAction *> > prior_loads(get_num_threads(), NULL);
+       bool found_acquire_fences = false;
+       for ( ; rit != list->rend(); rit++) {
                ModelAction *prev = *rit;
                if (act->same_thread(prev))
                        continue;
@@ -600,6 +645,17 @@ ModelAction * ModelChecker::get_last_fence_conflict(ModelAction *act) const
        return latest_backtrack;
 }
 
+/**
+ * @brief Find the last backtracking conflict for a ModelAction
+ *
+ * This function performs the search for the most recent conflicting action
+ * against which we should perform backtracking. This primary includes pairs of
+ * synchronizing actions which should be explored in the opposite execution
+ * order.
+ *
+ * @param act The current action
+ * @return The most recent action which conflicts with act
+ */
 ModelAction * ModelChecker::get_last_conflict(ModelAction *act) const
 {
        switch (act->get_type()) {