model: stash actions for lazy release-seq checking

Build up lists of actions to lazily check for new release sequence
developments.

diff --git a/model.cc b/model.cc
index fc93296a2524f4d2edc741e36f54dff24eb881e2..d2e4d9b1f70a092cfd2700faa1ab1d99f3d5c1a9 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -31,6 +31,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
        obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
        promises(new std::vector<Promise *>()),
+       lazy_sync_with_release(new HashTable<void *, std::list<ModelAction *>, uintptr_t, 4>()),
        thrd_last_action(new std::vector<ModelAction *>(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<ModelAction *> *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 7dc6ed6cb78574596488ecfb53fad221cf1436f1..7d5489eaadd5fc0c6c3f6995831122830ba0c44b 100644 (file)
--- a/model.h
+++ b/model.h
@@ -122,6 +122,16 @@ private:
 
        HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 > *obj_thrd_map;
        std::vector<Promise *> *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<void *, std::list<ModelAction *>, uintptr_t, 4> *lazy_sync_with_release;
+
        std::vector<ModelAction *> *thrd_last_action;
        NodeStack *node_stack;
        ModelAction *next_backtrack;