utilize SnapshotAlloc STL allocator

diff --git a/action.h b/action.h
index 65b060f6c1941b33720a3f9b572a9f2e7c0c8e31..96b791ee50bb12695de577b21f75e8926347103b 100644 (file)
--- a/action.h
+++ b/action.h
@@ -157,6 +157,6 @@ private:
        ClockVector *cv;
 };
 
-typedef std::list<ModelAction *> action_list_t;
+typedef std::list< ModelAction *, SnapshotAlloc<ModelAction *> > action_list_t;
 
 #endif /* __ACTION_H__ */

diff --git a/model.cc b/model.cc
index 31e0694e459b018da371ae4ff8c484369582f49d..538b4a9e37c35a32c69bef58cd21eeadf0ad663c 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -32,10 +32,10 @@ ModelChecker::ModelChecker(struct model_params params) :
        obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
        lock_waiters_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 *>()),
-       futurevalues(new std::vector<struct PendingFutureValue>()),
-       pending_rel_seqs(new std::vector<struct release_seq *>()),
-       thrd_last_action(new std::vector<ModelAction *>(1)),
+       promises(new std::vector< Promise *, SnapshotAlloc<Promise *> >()),
+       futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
+       pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
+       thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
        node_stack(new NodeStack()),
        mo_graph(new CycleGraph()),
        failed_promise(false),
@@ -1478,7 +1478,7 @@ void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *rel
 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
 {
        bool updated = false;
-       std::vector<struct release_seq *>::iterator it = pending_rel_seqs->begin();
+       std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
        while (it != pending_rel_seqs->end()) {
                struct release_seq *pending = *it;
                ModelAction *act = pending->acquire;

diff --git a/model.h b/model.h
index 7bc3585d8562eeff369cf307b81751781e381f6b..1bd32a1fffcb926449f2b5fc7a11f7d74410cf34 100644 (file)
--- a/model.h
+++ b/model.h
@@ -186,8 +186,8 @@ private:
        HashTable<const void *, action_list_t, uintptr_t, 4> *lock_waiters_map;
 
        HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 > *obj_thrd_map;
-       std::vector<Promise *> *promises;
-       std::vector<struct PendingFutureValue> *futurevalues;
+       std::vector< Promise *, SnapshotAlloc<Promise *> > *promises;
+       std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> > *futurevalues;
 
        /**
         * List of pending release sequences. Release sequences might be
@@ -195,9 +195,9 @@ private:
         * are established. Each entry in the list may only be partially
         * filled, depending on its pending status.
         */
-       std::vector<struct release_seq *> *pending_rel_seqs;
+       std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> > *pending_rel_seqs;
 
-       std::vector<ModelAction *> *thrd_last_action;
+       std::vector< ModelAction *, SnapshotAlloc<ModelAction *> > *thrd_last_action;
        NodeStack *node_stack;
 
        /** Private data members that should be snapshotted. They are grouped

diff --git a/threads.h b/threads.h
index 7f005c078c0c126edfcb5f48af6f220a65b3798b..9fecdfd3c7466398c85ec3dfafebb314d5887bfa 100644 (file)
--- a/threads.h
+++ b/threads.h
@@ -126,7 +126,7 @@ private:
         * list is used for thread joins, where another Thread waits for this
         * Thread to complete
         */
-       std::vector<ModelAction *> wait_list;
+       std::vector< ModelAction *, SnapshotAlloc<ModelAction *> > wait_list;
 
        /**
         * The value returned by the last action in this thread