model: stash actions for lazy release-seq checking

[model-checker.git] / model.cc

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);
        }
 }