From a01fa7fb82f22ef8d4787fd5d3ad44598a44f924 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 21 Feb 2013 11:59:50 -0800 Subject: [PATCH] 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'. --- model.cc | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/model.cc b/model.cc index e0edbec..8f0b3ce 100644 --- 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 > acquire_fences(get_num_threads(), NULL); - std::vector< ModelAction *, ModelAlloc > 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 > acquire_fences(get_num_threads(), NULL); + std::vector< ModelAction *, ModelAlloc > 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; -- 2.34.1