switch to snapshot/modelalloc versions of stl classes

diff --git a/cyclegraph.cc b/cyclegraph.cc
index e96549ff1fddcace369f57102572edf2c6bf9c32..20623347213d0958bfdff79d142595420461b015 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -8,7 +8,7 @@
 /** Initializes a CycleGraph object. */
 CycleGraph::CycleGraph() :
        discovered(new HashTable<const CycleNode *, const CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free>(16)),
-       queue(new std::vector< const CycleNode *, ModelAlloc<const CycleNode *> >()),
+       queue(new model_vector< const CycleNode * >()),
        hasCycles(false),
        oldCycles(false)
 {

diff --git a/cyclegraph.h b/cyclegraph.h
index 25401d9a3d349d07f6c4b11fe4a140e041f82394..d5c6a92af78715de0ff4f2c323a578b7a43f6ff1 100644 (file)
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -9,7 +9,7 @@
 #ifndef __CYCLEGRAPH_H__
 #define __CYCLEGRAPH_H__
 
-#include <vector>
+#include "stl_wrappers.h"
 #include <inttypes.h>
 #include <stdio.h>
 
@@ -21,7 +21,7 @@ class Promise;
 class CycleNode;
 class ModelAction;
 
-typedef std::vector< const Promise *, ModelAlloc<const Promise *> > promise_list_t;
+typedef model_vector< const Promise * > promise_list_t;
 
 /** @brief A graph of Model Actions for tracking cycles. */
 class CycleGraph {
@@ -68,7 +68,7 @@ class CycleGraph {
        bool mergeNodes(CycleNode *node1, CycleNode *node2);
 
        HashTable<const CycleNode *, const CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free> *discovered;
-       std::vector< const CycleNode *, ModelAlloc<const CycleNode *> > * queue;
+       model_vector< const CycleNode * > * queue;
 
 
        /** @brief A table for mapping ModelActions to CycleNodes */

diff --git a/model.cc b/model.cc
index 0122922d376ca03a742f03729585f3c48db7b09a..f492af30d35b39ac00fbb080184cb6ec11b523f7 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -85,12 +85,12 @@ 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>()),
        condvar_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 *, 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)),
-       thrd_last_fence_release(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >()),
+       obj_thrd_map(new HashTable<void *, snap_vector<action_list_t> *, uintptr_t, 4 >()),
+       promises(new snap_vector< Promise * >()),
+       futurevalues(new snap_vector< struct PendingFutureValue >()),
+       pending_rel_seqs(new snap_vector< struct release_seq * >()),
+       thrd_last_action(new snap_vector< ModelAction * >(1)),
+       thrd_last_fence_release(new snap_vector< ModelAction * >()),
        node_stack(new NodeStack()),
        priv(new struct model_snapshot_members()),
        mo_graph(new CycleGraph())
@@ -137,11 +137,11 @@ static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t
        return tmp;
 }
 
-static std::vector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
+static snap_vector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, snap_vector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
 {
-       std::vector<action_list_t> *tmp = hash->get(ptr);
+       snap_vector<action_list_t> *tmp = hash->get(ptr);
        if (tmp == NULL) {
-               tmp = new std::vector<action_list_t>();
+               tmp = new snap_vector<action_list_t>();
                hash->put(ptr, tmp);
        }
        return tmp;
@@ -1704,7 +1704,7 @@ bool ModelChecker::should_read_instead(const ModelAction *curr, const T *rf, con
        if (!mo_graph->checkReachable(rf, other_rf))
                return false;
 
-       std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+       snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
        action_list_t *list = &(*thrd_lists)[id_to_int(curr->get_tid())];
        action_list_t::reverse_iterator rit = list->rbegin();
        ASSERT((*rit) == curr);
@@ -1747,7 +1747,7 @@ bool ModelChecker::check_recency(ModelAction *curr, const T *rf) const
                        curr->get_node()->get_read_from_promise_size() <= 1)
                return true;
 
-       std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+       snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
        int tid = id_to_int(curr->get_tid());
        ASSERT(tid < (int)thrd_lists->size());
        action_list_t *list = &(*thrd_lists)[tid];
@@ -1805,7 +1805,7 @@ bool ModelChecker::check_recency(ModelAction *curr, const T *rf) const
 template <typename rf_type>
 bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
 {
-       std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+       snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
        unsigned int i;
        bool added = false;
        ASSERT(curr->is_read());
@@ -1913,7 +1913,7 @@ bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
  */
 bool ModelChecker::w_modification_order(ModelAction *curr, std::vector< ModelAction *, ModelAlloc<ModelAction *> > *send_fv)
 {
-       std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+       snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
        unsigned int i;
        bool added = false;
        ASSERT(curr->is_write());
@@ -2057,7 +2057,7 @@ bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, cons
  */
 bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
 {
-       std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
+       snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
        unsigned int i;
        /* Iterate over all threads */
        for (i = 0; i < thrd_lists->size(); i++) {
@@ -2158,7 +2158,7 @@ bool ModelChecker::release_seq_heads(const ModelAction *rf,
                release_heads->push_back(fence_release);
 
        int tid = id_to_int(rf->get_tid());
-       std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
+       snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
        action_list_t *list = &(*thrd_lists)[tid];
        action_list_t::const_reverse_iterator rit;
 
@@ -2301,7 +2301,7 @@ void ModelChecker::get_release_seq_heads(ModelAction *acquire,
 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
 {
        bool updated = false;
-       std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
+       snap_vector< struct release_seq * >::iterator it = pending_rel_seqs->begin();
        while (it != pending_rel_seqs->end()) {
                struct release_seq *pending = *it;
                ModelAction *acquire = pending->acquire;
@@ -2382,7 +2382,7 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
        if (uninit)
                action_trace->push_front(uninit);
 
-       std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
+       snap_vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
        if (tid >= (int)vec->size())
                vec->resize(priv->next_thread_id);
        (*vec)[tid].push_back(act);
@@ -2405,7 +2405,7 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
                void *mutex_loc = (void *) act->get_value();
                get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
 
-               std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
+               snap_vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
                if (tid >= (int)vec->size())
                        vec->resize(priv->next_thread_id);
                (*vec)[tid].push_back(act);
@@ -2724,7 +2724,7 @@ void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
  */
 void ModelChecker::build_may_read_from(ModelAction *curr)
 {
-       std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+       snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
        unsigned int i;
        ASSERT(curr->is_read());
 

diff --git a/model.h b/model.h
index 96c1ec78a60ca343400c309b2e756ae53fb39967..0af3425deefa1743fd03ca99c055678c26f48e22 100644 (file)
--- a/model.h
+++ b/model.h
@@ -5,7 +5,7 @@
 #ifndef __MODEL_H__
 #define __MODEL_H__
 
-#include <vector>
+#include "stl_wrappers.h"
 #include <cstddef>
 #include <ucontext.h>
 #include <inttypes.h>
@@ -27,9 +27,9 @@ class ClockVector;
 struct model_snapshot_members;
 
 /** @brief Shorthand for a list of release sequence heads */
-typedef std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > rel_heads_list_t;
+typedef model_vector< const ModelAction * > rel_heads_list_t;
 
-typedef std::list< ModelAction *, SnapshotAlloc<ModelAction *> > action_list_t;
+typedef snap_list< ModelAction * > action_list_t;
 
 /**
  * Model checker parameter structure. Holds run-time configuration options for
@@ -231,9 +231,9 @@ private:
         * to a trace of all actions performed on the object. */
        HashTable<const void *, action_list_t *, uintptr_t, 4> * const condvar_waiters_map;
 
-       HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4 > * const obj_thrd_map;
-       std::vector< Promise *, SnapshotAlloc<Promise *> > * const promises;
-       std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> > * const futurevalues;
+       HashTable<void *, snap_vector<action_list_t> *, uintptr_t, 4 > * const obj_thrd_map;
+       snap_vector< Promise * > * const promises;
+       snap_vector< struct PendingFutureValue > * const futurevalues;
 
        /**
         * List of pending release sequences. Release sequences might be
@@ -241,10 +241,10 @@ private:
         * are established. Each entry in the list may only be partially
         * filled, depending on its pending status.
         */
-       std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> > * const pending_rel_seqs;
+       snap_vector< struct release_seq * > * const pending_rel_seqs;
 
-       std::vector< ModelAction *, SnapshotAlloc<ModelAction *> > * const thrd_last_action;
-       std::vector< ModelAction *, SnapshotAlloc<ModelAction *> > * const thrd_last_fence_release;
+       snap_vector< ModelAction * > * const thrd_last_action;
+       snap_vector< ModelAction * > * const thrd_last_fence_release;
        NodeStack * const node_stack;
 
        /** Private data members that should be snapshotted. They are grouped

diff --git a/nodestack.h b/nodestack.h
index 8ad329eeaf04f09eb4037c6d9dc6931e8cc1524a..47c0272f95fa917e8710235fa0d56b02194a4d08 100644 (file)
--- a/nodestack.h
+++ b/nodestack.h
@@ -5,7 +5,7 @@
 #ifndef __NODESTACK_H__
 #define __NODESTACK_H__
 
-#include <vector>
+#include "stl_wrappers.h"
 #include <cstddef>
 #include <inttypes.h>
 
@@ -163,7 +163,7 @@ private:
        int * yield_data;
 };
 
-typedef std::vector< Node *, ModelAlloc< Node * > > node_list_t;
+typedef model_vector< Node * > node_list_t;
 
 /**
  * @brief A stack of nodes

diff --git a/stl_wrappers.h b/stl_wrappers.h
new file mode 100644 (file)
index 0000000..061fce0
--- /dev/null
+++ b/stl_wrappers.h
@@ -0,0 +1,40 @@
+#ifndef STL_WRAPPERS_H
+#define STL_WRAPPERS_H
+
+#include <vector>
+#include <list>
+#include "mymemory.h"
+
+template<typename _Tp >
+class snap_vector:public std::vector<_Tp, SnapshotAlloc<_Tp> > {
+ public:
+ snap_vector() : std::vector<_Tp, SnapshotAlloc<_Tp> >() {
+       }
+ snap_vector(int __n) : std::vector<_Tp, SnapshotAlloc<_Tp> >(__n) {
+       }
+
+       SNAPSHOTALLOC
+};
+
+template<typename _Tp >
+class model_vector:public std::vector<_Tp, ModelAlloc<_Tp> > {
+ public:
+       MEMALLOC
+};
+
+template<typename _Tp >
+class snap_list:public std::list<_Tp, SnapshotAlloc<_Tp> > {
+ public:
+       SNAPSHOTALLOC
+};
+
+template<typename _Tp >
+class model_list:public std::list<_Tp, ModelAlloc<_Tp> > {
+ public:
+ model_list() : std::list<_Tp, ModelAlloc<_Tp> >() {
+       }
+ model_list(int __n, _Tp t) : std::list<_Tp, ModelAlloc<_Tp> >(__n, t) {
+       }
+       MEMALLOC
+};
+#endif

diff --git a/workqueue.h b/workqueue.h
index f08f63c783596968e9dd13a5595fa1f23fcd865f..3e2481b97eb2080437beb02e22863db25fdbfac3 100644 (file)
--- a/workqueue.h
+++ b/workqueue.h
@@ -6,7 +6,7 @@
 #ifndef __WORKQUEUE_H__
 #define __WORKQUEUE_H__
 
-#include <list>
+#include "stl_wrappers.h"
 #include "mymemory.h"
 
 class ModelAction;
@@ -102,6 +102,6 @@ class MOEdgeWorkEntry : public WorkQueueEntry {
 };
 
 /** @brief typedef for the work queue type */
-typedef std::list< WorkQueueEntry, ModelAlloc<WorkQueueEntry> > work_queue_t;
+typedef model_list< WorkQueueEntry > work_queue_t;
 
 #endif /* __WORKQUEUE_H__ */