model: only backtrack fences when acquire is before release

Because there are up to 4 actions involved in this search for a
"conflict" (load, fence-acquire, fence-release, store), I overlooked the
fact that we only need to backtrack when the release comes after acquire
in the execution order. This fix skips past the 'release' action before
we begin searching for the 'acquire'.

diff --git a/model.cc b/model.cc
index e0edbec091bcba052b926c560dec5a306fe8bee4..8f0b3ce443c4bf9d18eedbf524cd2d6e3c7b91fe 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -572,16 +572,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;