Revert "switch to snapshot/modelalloc versions of stl classes"

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index f492af30d35b39ac00fbb080184cb6ec11b523f7..0122922d376ca03a742f03729585f3c48db7b09a 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 *, 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 * >()),
+       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 *> >()),
        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 snap_vector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, snap_vector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
+static std::vector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
 {
-       snap_vector<action_list_t> *tmp = hash->get(ptr);
+       std::vector<action_list_t> *tmp = hash->get(ptr);
        if (tmp == NULL) {
-               tmp = new snap_vector<action_list_t>();
+               tmp = new std::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;
 
-       snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+       std::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;
 
-       snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+       std::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)
 {
-       snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+       std::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)
 {
-       snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+       std::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)
 {
-       snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
+       std::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());
-       snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
+       std::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;
-       snap_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 *acquire = pending->acquire;
@@ -2382,7 +2382,7 @@ void ModelChecker::add_action_to_lists(ModelAction *act)
        if (uninit)
                action_trace->push_front(uninit);
 
-       snap_vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
+       std::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);
 
-               snap_vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
+               std::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)
 {
-       snap_vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+       std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
        unsigned int i;
        ASSERT(curr->is_read());