From a98cefb336e2b2298e9205f09f37612d03db3d9e Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Wed, 22 Aug 2012 19:16:58 -0700 Subject: [PATCH] model: stash actions for lazy release-seq checking Build up lists of actions to lazily check for new release sequence developments. --- model.cc | 8 +++++++- model.h | 10 ++++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) diff --git a/model.cc b/model.cc index fc93296..d2e4d9b 100644 --- a/model.cc +++ b/model.cc @@ -31,6 +31,7 @@ ModelChecker::ModelChecker(struct model_params params) : obj_map(new HashTable()), obj_thrd_map(new HashTable, uintptr_t, 4 >()), promises(new std::vector()), + lazy_sync_with_release(new HashTable, uintptr_t, 4>()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), next_backtrack(NULL), @@ -54,6 +55,8 @@ ModelChecker::~ModelChecker() delete (*promises)[i]; delete promises; + delete lazy_sync_with_release; + delete thrd_last_action; delete node_stack; delete scheduler; @@ -637,7 +640,10 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, bool complete; complete = release_seq_head(rf, release_heads); if (!complete) { - /** @todo complete lazy checking */ + /* add act to 'lazy checking' list */ + std::list *list; + list = lazy_sync_with_release->get_safe_ptr(act->get_location()); + list->push_back(act); } } diff --git a/model.h b/model.h index 7dc6ed6..7d5489e 100644 --- a/model.h +++ b/model.h @@ -122,6 +122,16 @@ private: HashTable, uintptr_t, 4 > *obj_thrd_map; std::vector *promises; + + /** + * Collection of lists of objects that might synchronize with one or + * more release sequence. Release sequences might be determined lazily + * as promises are fulfilled and modification orders are established. + * This structure maps its lists by object location. Each ModelAction + * in the lists should be an acquire operation. + */ + HashTable, uintptr_t, 4> *lazy_sync_with_release; + std::vector *thrd_last_action; NodeStack *node_stack; ModelAction *next_backtrack; -- 2.34.1