From 88ccfdff63126a0fa70c094c7ed7e66f68e1b861 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Tue, 14 Aug 2012 17:37:32 -0700 Subject: [PATCH] action: utilize release sequence(s) for synchronization Instead of checking only the trivial release sequence (i.e., a read-acquire reads directly from a write-release) for establishing synchronization, make use of the ModelChecker's more complete 'get_release_seq_head()' functionality, then loop through all release heads and synchronize with each. This is necessary because a read-acquire may synchronize with more than one store-release. Note that this step only implements support based on present knowledge. The incomplete knowledge of the modification order, as given in mo_graph, as well as "reading from the future" may require lazy checking. --- action.cc | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/action.cc b/action.cc index 5124780..b435524 100644 --- a/action.cc +++ b/action.cc @@ -1,6 +1,7 @@ #include #define __STDC_FORMAT_MACROS #include +#include #include "model.h" #include "action.h" @@ -166,8 +167,11 @@ void ModelAction::read_from(const ModelAction *act) { ASSERT(cv); reads_from = act; - if (act!=NULL && act->is_release() && this->is_acquire()) { - synchronize_with(act); + if (act != NULL && this->is_acquire()) { + std::vector release_heads; + model->get_release_seq_heads(this, &release_heads); + for (unsigned int i = 0; i < release_heads.size(); i++) + synchronize_with(release_heads[i]); } } -- 2.34.1