towards getting rid of STL

diff --git a/execution.cc b/execution.cc
index 022021cd93c38f018d1bf5eecec63b4cb518e6ac..1691c6434e6025ece00a736a116a4dbf007c5242 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -1101,8 +1101,12 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
                uninit_id = id_to_int(uninit->get_tid());
                list->push_front(uninit);
                SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
                uninit_id = id_to_int(uninit->get_tid());
                list->push_front(uninit);
                SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());

-               if (uninit_id >= (int)vec->size())
-                       vec->resize(uninit_id + 1);
+               if (uninit_id >= (int)vec->size()) {
+                 int oldsize = (int) vec->size();
+                 vec->resize(uninit_id + 1);
+                 for(int i=oldsize; i<uninit_id+1; i++)
+                   new (&vec[i]) action_list_t(); 
+               }

                (*vec)[uninit_id].push_front(uninit);
        }
        list->push_back(act);
                (*vec)[uninit_id].push_front(uninit);
        }
        list->push_back(act);


@@ -1114,8 +1118,12 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
 
        // Update obj_thrd_map, a per location, per thread, order of actions
        SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
 
        // Update obj_thrd_map, a per location, per thread, order of actions
        SnapVector<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);
+       if (tid >= (int)vec->size()) {
+         uint oldsize =vec->size();
+         vec->resize(priv->next_thread_id);
+         for(uint i=oldsize; i<priv->next_thread_id; i++)
+           new (&vec[i]) action_list_t(); 
+       }

        (*vec)[tid].push_back(act);
        if (uninit)
                (*vec)[uninit_id].push_front(uninit);
        (*vec)[tid].push_back(act);
        if (uninit)
                (*vec)[uninit_id].push_front(uninit);


@@ -1139,8 +1147,12 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
                get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
 
                SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
                get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
 
                SnapVector<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);
+               if (tid >= (int)vec->size()) {
+                 uint oldsize = vec->size();
+                 vec->resize(priv->next_thread_id);
+                 for(uint i=oldsize; i<priv->next_thread_id; i++)
+                   new (&vec[i]) action_list_t(); 
+               }

                (*vec)[tid].push_back(act);
        }
 }
                (*vec)[tid].push_back(act);
        }
 }


@@ -1199,8 +1211,12 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
 
        // Update obj_thrd_map, a per location, per thread, order of actions
        SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
 
        // Update obj_thrd_map, a per location, per thread, order of actions
        SnapVector<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);
+       if (tid >= (int)vec->size()) {
+         uint oldsize =vec->size();
+         vec->resize(priv->next_thread_id);
+         for(uint i=oldsize; i<priv->next_thread_id; i++)
+           new (&vec[i]) action_list_t();
+       }

        insertIntoActionList(&(*vec)[tid],act);
 
        // Update thrd_last_action, the last action taken by each thrad
        insertIntoActionList(&(*vec)[tid],act);
 
        // Update thrd_last_action, the last action taken by each thrad


@@ -1212,8 +1228,12 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
 void ModelExecution::add_write_to_lists(ModelAction *write) {
        SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
        int tid = id_to_int(write->get_tid());
 void ModelExecution::add_write_to_lists(ModelAction *write) {
        SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
        int tid = id_to_int(write->get_tid());

-       if (tid >= (int)vec->size())
-               vec->resize(priv->next_thread_id);
+       if (tid >= (int)vec->size()) {
+         uint oldsize =vec->size();
+         vec->resize(priv->next_thread_id);
+         for(uint i=oldsize; i<priv->next_thread_id; i++)
+           new (&vec[i]) action_list_t();
+       }

        (*vec)[tid].push_back(write);
 }
 
        (*vec)[tid].push_back(write);
 }
 

diff --git a/model.cc b/model.cc
index 78729bd38ac4d9da05d25527450f6668f38be997..b0540699aee48bdca071ef1894d9690e7395c38e 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -423,11 +423,10 @@ void ModelChecker::run()
                         * thread which just took a step--plus the first step
                         * for any newly-created thread
                         */
                         * thread which just took a step--plus the first step
                         * for any newly-created thread
                         */

-                       ModelAction * pending;

                        for (unsigned int i = 0;i < get_num_threads();i++) {
                                thread_id_t tid = int_to_id(i);
                                Thread *thr = get_thread(tid);
                        for (unsigned int i = 0;i < get_num_threads();i++) {
                                thread_id_t tid = int_to_id(i);
                                Thread *thr = get_thread(tid);

-                               if (!thr->is_model_thread() && !thr->is_complete() && ((!(pending=thr->get_pending())) || is_nonsc_write(pending)) ) {
+                               if (!thr->is_model_thread() && !thr->is_complete() && (!thr->get_pending())) {

                                        switch_from_master(thr);        // L: context swapped, and action type of thr changed.
                                        if (thr->is_waiting_on(thr))
                                                assert_bug("Deadlock detected (thread %u)", i);
                                        switch_from_master(thr);        // L: context swapped, and action type of thr changed.
                                        if (thr->is_waiting_on(thr))
                                                assert_bug("Deadlock detected (thread %u)", i);

diff --git a/stl-model.h b/stl-model.h
index 30a9b8c69872f9122e7494bcf28a5962ab2d4ab1..24ed29a6ddd33306dff6d0d1543f61b7b6c23ebf 100644 (file)
--- a/stl-model.h
+++ b/stl-model.h
@@ -5,39 +5,228 @@
 #include "mymemory.h"
 
 template<typename _Tp>
 #include "mymemory.h"
 
 template<typename _Tp>

-class ModelList : public std::list<_Tp, ModelAlloc<_Tp> >
-{
-public:
-       typedef std::list< _Tp, ModelAlloc<_Tp> > list;
-
-       ModelList() :
-               list()
-       { }
-
-       ModelList(size_t n, const _Tp& val = _Tp()) :
-               list(n, val)
-       { }
-
-       MEMALLOC
+class mllnode {
+ public:
+  _Tp getVal() {return val;}
+  mllnode<_Tp> * getNext() {return next;}
+  mllnode<_Tp> * getPrev() {return prev;}
+  MEMALLOC;
+  
+ private:
+  mllnode<_Tp> * next;
+  mllnode<_Tp> * prev;
+  _Tp val;
+  friend class ModelList;

 };
 
 template<typename _Tp>
 };
 
 template<typename _Tp>

-class SnapList : public std::list<_Tp, SnapshotAlloc<_Tp> >
+class ModelList

 {
 {

-public:
-       typedef std::list<_Tp, SnapshotAlloc<_Tp> > list;
-
-       SnapList() :
-               list()
-       { }
+public:  
+ ModelList() : head(NULL),
+    tail(NULL) {
+  }
+
+  void push_front(_Tp val) {
+    mllnode<_Tp> * tmp = new mllnode<_Tp>();
+    tmp->prev = NULL;
+    tmp->next = head;
+    tmp->val = val;
+    if (head == NULL)
+      tail = tmp;
+    else
+      head->prev = tmp;
+    head = tmp;
+  }
+
+  void push_back(_Tp val) {
+    mllnode<_Tp> * tmp = new mllnode<_Tp>();
+    tmp->prev = tail;
+    tmp->next = NULL;
+    tmp->val = val;
+    if (tail == NULL)
+      head = tmp;
+    else tail->next = tmp;
+    tail = tmp;
+  }
+
+  void insertAfter(mllnode<_Tp> * node, _Tp val) {
+    mllnode<_Tp> *tmp = new mllnode<_Tp>();
+    tmp->val = val;
+    tmp->prev = node;
+    tmp->next = node->next;
+    node->next = tmp;
+    if (tmp->next == NULL) {
+      tail = tmp;
+    } else {
+      tmp->next->prev = tmp;
+    }
+  }
+
+  void insertBefore(mllnode<_Tp> * node, _Tp val) {
+    mllnode<_Tp> *tmp = new mllnode<_Tp>();
+    tmp->val = val;
+    tmp->next = node;
+    tmp->prev = node->prev;
+    node->prev = tmp;
+    if (tmp->prev == NULL) {
+      head = tmp;
+    } else {
+      tmp->prev->next = tmp;
+    }
+  }
+  
+  void erase(mllnode<_Tp> * node) {
+    if (head == node) {
+      head = node->next;
+    } else {
+      node->prev->next = node->next;
+    }
+
+    if (tail == node) {
+      tail = node->prev;
+    } else {
+      tail->next->prev = node->prev;
+    }
+    
+    delete node;
+  }
+  
+  mllnode<_Tp> begin() {
+    return head;
+  }
+
+  mllnode<_Tp> end() {
+    return tail;
+  }
+  
+  _Tp front() {
+    return head->val;
+  }
+
+  _Tp back() {
+    return tail->val;
+  }
+  
+  
+  MEMALLOC;
+ private:
+  mllnode<_Tp> *head;
+  mllnode<_Tp> *tail;
+};

 
 

-       SnapList(size_t n, const _Tp& val = _Tp()) :
-               list(n, val)
-       { }
+template<typename _Tp>
+class sllnode {
+ public:
+  _Tp getVal() {return val;}
+  sllnode<_Tp> * getNext() {return next;}
+  sllnode<_Tp> * getPrev() {return prev;}
+  SNAPSHOTALLOC;
+  
+ private:
+  sllnode<_Tp> * next;
+  sllnode<_Tp> * prev;
+  _Tp val;
+  friend class SnapList;
+};

 
 

-       SNAPSHOTALLOC
+template<typename _Tp>
+class SnapList
+{
+public:  
+ SnapList() : head(NULL),
+    tail(NULL) {
+  }
+
+  void push_front(_Tp val) {
+    sllnode<_Tp> * tmp = new sllnode<_Tp>();
+    tmp->prev = NULL;
+    tmp->next = head;
+    tmp->val = val;
+    if (head == NULL)
+      tail = tmp;
+    else
+      head->prev = tmp;
+    head = tmp;
+  }
+
+  void push_back(_Tp val) {
+    sllnode<_Tp> * tmp = new sllnode<_Tp>();
+    tmp->prev = tail;
+    tmp->next = NULL;
+    tmp->val = val;
+    if (tail == NULL)
+      head = tmp;
+    else tail->next = tmp;
+    tail = tmp;
+  }
+
+  void insertAfter(sllnode<_Tp> * node, _Tp val) {
+    sllnode<_Tp> *tmp = new sllnode<_Tp>();
+    tmp->val = val;
+    tmp->prev = node;
+    tmp->next = node->next;
+    node->next = tmp;
+    if (tmp->next == NULL) {
+      tail = tmp;
+    } else {
+      tmp->next->prev = tmp;
+    }
+  }
+
+  void insertBefore(sllnode<_Tp> * node, _Tp val) {
+    sllnode<_Tp> *tmp = new sllnode<_Tp>();
+    tmp->val = val;
+    tmp->next = node;
+    tmp->prev = node->prev;
+    node->prev = tmp;
+    if (tmp->prev == NULL) {
+      head = tmp;
+    } else {
+      tmp->prev->next = tmp;
+    }
+  }
+  
+  void erase(sllnode<_Tp> * node) {
+    if (head == node) {
+      head = node->next;
+    } else {
+      node->prev->next = node->next;
+    }
+
+    if (tail == node) {
+      tail = node->prev;
+    } else {
+      tail->next->prev = node->prev;
+    }
+    
+    delete node;
+  }
+  
+  sllnode<_Tp> begin() {
+    return head;
+  }
+
+  sllnode<_Tp> end() {
+    return tail;
+  }
+  
+  _Tp front() {
+    return head->val;
+  }
+
+  _Tp back() {
+    return tail->val;
+  }
+  
+  
+  SNAPSHOTALLOC;
+ private:
+  sllnode<_Tp> *head;
+  sllnode<_Tp> *tail;

 };
 
 };
 

+

 #define VECTOR_DEFCAP 8
 
 typedef unsigned int uint;
 #define VECTOR_DEFCAP 8
 
 typedef unsigned int uint;