edits

diff --git a/action.cc b/action.cc
index d90a94ee48211ddb17e9a3f26cafcb4e56ca9e55..9905ab2bf11bbd50e601f6157b04ee69480d99c6 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -38,6 +38,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),

+       action_ref(NULL),

        value(value),
        type(type),
        order(order),
        value(value),
        type(type),
        order(order),


@@ -69,6 +70,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, uint64_t value,
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),

+       action_ref(NULL),

        value(value),
        type(type),
        order(order),
        value(value),
        type(type),
        order(order),


@@ -99,6 +101,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),

+       action_ref(NULL),

        value(value),
        type(type),
        order(order),
        value(value),
        type(type),
        order(order),


@@ -133,6 +136,7 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),

+       action_ref(NULL),

        value(value),
        type(type),
        order(order),
        value(value),
        type(type),
        order(order),


@@ -168,6 +172,7 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),

+       action_ref(NULL),

        value(value),
        type(type),
        order(order),
        value(value),
        type(type),
        order(order),

diff --git a/action.h b/action.h
index c5ba6d7dda9f9593a315a26c3d1da336a50b5a0f..fbf566fb7a8f61497284c6ab1e826dd39b0f44e0 100644 (file)
--- a/action.h
+++ b/action.h
@@ -193,6 +193,9 @@ public:
        Thread * thread_operand;
        void set_thread_operand(Thread *th) { thread_operand = th; }
 
        Thread * thread_operand;
        void set_thread_operand(Thread *th) { thread_operand = th; }
 

+       void setActionRef(sllnode<ModelAction *> *ref) { action_ref = ref; }
+       sllnode<ModelAction *> * getActionRef() { return action_ref; }
+

        SNAPSHOTALLOC
 private:
        const char * get_type_str() const;
        SNAPSHOTALLOC
 private:
        const char * get_type_str() const;


@@ -227,6 +230,7 @@ private:
         */
        ClockVector *cv;
        ClockVector *rf_cv;
         */
        ClockVector *cv;
        ClockVector *rf_cv;

+       sllnode<ModelAction *> * action_ref;

 
        /** @brief The value written (for write or RMW; undefined for read) */
        uint64_t value;
 
        /** @brief The value written (for write or RMW; undefined for read) */
        uint64_t value;

diff --git a/actionlist.cc b/actionlist.cc
index 0dc8bc89661db7556d4fdc00344f8811d81be927..4a24ba9952a32bffbefdbdf418a031d6ac1db412 100644 (file)
--- a/actionlist.cc
+++ b/actionlist.cc
@@ -246,3 +246,16 @@ void actionlist::clear() {
 bool actionlist::isEmpty() {
        return root.count == 0;
 }
 bool actionlist::isEmpty() {
        return root.count == 0;
 }

+
+/**
+ * Fix the parent pointer of root when root address changes (possible
+ * due to vector<action_list_t> resize)
+ */
+void actionlist::fixupParent()
+{
+       for (int i = 0; i < ALLNODESIZE; i++) {
+               allnode * child = root.children[i];
+               if (child != NULL && child->parent != &root)
+                       child->parent = &root;
+       }
+}

diff --git a/actionlist.h b/actionlist.h
index 20f93fc953b9c27472df84c7de15cc53f66800e7..ee0a144590fb8fd6ed146c025eab2e10c8984409 100644 (file)
--- a/actionlist.h
+++ b/actionlist.h
@@ -41,6 +41,7 @@ public:
        uint size() {return _size;}
        sllnode<ModelAction *> * begin() {return head;}
        sllnode<ModelAction *> * end() {return tail;}
        uint size() {return _size;}
        sllnode<ModelAction *> * begin() {return head;}
        sllnode<ModelAction *> * end() {return tail;}

+       void fixupParent();

 
        SNAPSHOTALLOC;
 
 
        SNAPSHOTALLOC;
 

diff --git a/execution.cc b/execution.cc
index 9c3b4afa2986fac9ecce604e9de9394ebca6f3eb..04314d194c17058713d1107911b7377b692c5a25 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -98,36 +98,50 @@ int ModelExecution::get_execution_number() const
        return model->get_execution_number();
 }
 
        return model->get_execution_number();
 }
 

-static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
+static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)

 {
 {

-       action_list_t *tmp = hash->get(ptr);
+       SnapVector<action_list_t> *tmp = hash->get(ptr);

        if (tmp == NULL) {
        if (tmp == NULL) {

-               tmp = new action_list_t();
+               tmp = new SnapVector<action_list_t>();

                hash->put(ptr, tmp);
        }
        return tmp;
 }
 
                hash->put(ptr, tmp);
        }
        return tmp;
 }
 

-static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
+static simple_action_list_t * get_safe_ptr_action(HashTable<const void *, simple_action_list_t *, uintptr_t, 2> * hash, void * ptr)

 {
 {

-       SnapVector<action_list_t> *tmp = hash->get(ptr);
+       simple_action_list_t *tmp = hash->get(ptr);

        if (tmp == NULL) {
        if (tmp == NULL) {

-               tmp = new SnapVector<action_list_t>();
+               tmp = new simple_action_list_t();

                hash->put(ptr, tmp);
        }
        return tmp;
 }
 
                hash->put(ptr, tmp);
        }
        return tmp;
 }
 

-static simple_action_list_t * get_safe_ptr_action(HashTable<const void *, simple_action_list_t *, uintptr_t, 2> * hash, void * ptr)
+static SnapVector<simple_action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<simple_action_list_t> *, uintptr_t, 2> * hash, void * ptr)

 {
 {

-       simple_action_list_t *tmp = hash->get(ptr);
+       SnapVector<simple_action_list_t> *tmp = hash->get(ptr);

        if (tmp == NULL) {
        if (tmp == NULL) {

-               tmp = new simple_action_list_t();
+               tmp = new SnapVector<simple_action_list_t>();

                hash->put(ptr, tmp);
        }
        return tmp;
 }
 
                hash->put(ptr, tmp);
        }
        return tmp;
 }
 

+/**
+ * When vectors of action lists are reallocated due to resize, the root address of
+ * action lists may change. Hence we need to fix the parent pointer of the children
+ * of root.
+ */
+static void fixup_action_list (SnapVector<action_list_t> * vec)
+{
+       for (uint i = 0; i < vec->size(); i++) {
+               action_list_t * list = &(*vec)[i];
+               if (list != NULL)
+                       list->fixupParent();
+       }
+}
+

 /** @return a thread ID for a new Thread */
 thread_id_t ModelExecution::get_next_id()
 {
 /** @return a thread ID for a new Thread */
 thread_id_t ModelExecution::get_next_id()
 {


@@ -814,6 +828,8 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *
                thrd_lists->resize(priv->next_thread_id);
                for(uint i = oldsize;i < priv->next_thread_id;i++)
                        new (&(*thrd_lists)[i]) action_list_t();
                thrd_lists->resize(priv->next_thread_id);
                for(uint i = oldsize;i < priv->next_thread_id;i++)
                        new (&(*thrd_lists)[i]) action_list_t();

+
+               fixup_action_list(thrd_lists);

        }
 
        ModelAction *prev_same_thread = NULL;
        }
 
        ModelAction *prev_same_thread = NULL;


@@ -1134,8 +1150,8 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
 {
        int tid = id_to_int(act->get_tid());
        if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
 {
        int tid = id_to_int(act->get_tid());
        if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {

-               action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
-               list->addAction(act);
+               simple_action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+               act->setActionRef(list->add_back(act));

        }
 
        // Update action trace, a total order of all actions
        }
 
        // Update action trace, a total order of all actions


@@ -1149,6 +1165,8 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
                vec->resize(priv->next_thread_id);
                for(uint i = oldsize;i < priv->next_thread_id;i++)
                        new (&(*vec)[i]) action_list_t();
                vec->resize(priv->next_thread_id);
                for(uint i = oldsize;i < priv->next_thread_id;i++)
                        new (&(*vec)[i]) action_list_t();

+
+               fixup_action_list(vec);

        }
        if (!canprune && (act->is_read() || act->is_write()))
                (*vec)[tid].addAction(act);
        }
        if (!canprune && (act->is_read() || act->is_write()))
                (*vec)[tid].addAction(act);


@@ -1167,7 +1185,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
 
        if (act->is_wait()) {
                void *mutex_loc = (void *) act->get_value();
 
        if (act->is_wait()) {
                void *mutex_loc = (void *) act->get_value();

-               get_safe_ptr_action(&obj_map, mutex_loc)->addAction(act);
+               act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act));

        }
 }
 
        }
 }
 


@@ -1200,6 +1218,8 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
                vec->resize(priv->next_thread_id);
                for(uint i=oldsize;i<priv->next_thread_id;i++)
                        new (&(*vec)[i]) action_list_t();
                vec->resize(priv->next_thread_id);
                for(uint i=oldsize;i<priv->next_thread_id;i++)
                        new (&(*vec)[i]) action_list_t();

+
+               fixup_action_list(vec);

        }
        insertIntoActionList(&(*vec)[tid],act);
 
        }
        insertIntoActionList(&(*vec)[tid],act);
 


@@ -1211,15 +1231,15 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
 
 
 void ModelExecution::add_write_to_lists(ModelAction *write) {
 
 
 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());
+       SnapVector<simple_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()) {
                uint oldsize =vec->size();
                vec->resize(priv->next_thread_id);
                for(uint i=oldsize;i<priv->next_thread_id;i++)
        int tid = id_to_int(write->get_tid());
        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();
+                       new (&(*vec)[i]) simple_action_list_t();

        }
        }

-       (*vec)[tid].addAction(write);
+       write->setActionRef((*vec)[tid].add_back(write));

 }
 
 /**
 }
 
 /**


@@ -1275,7 +1295,7 @@ ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
 {
        /* All fences should have location FENCE_LOCATION */
 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
 {
        /* All fences should have location FENCE_LOCATION */

-       action_list_t *list = obj_map.get(FENCE_LOCATION);
+       simple_action_list_t *list = obj_map.get(FENCE_LOCATION);

 
        if (!list)
                return NULL;
 
        if (!list)
                return NULL;


@@ -1311,7 +1331,7 @@ ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
 {
        void *location = curr->get_location();
 
 {
        void *location = curr->get_location();
 

-       action_list_t *list = obj_map.get(location);
+       simple_action_list_t *list = obj_map.get(location);

        if (list == NULL)
                return NULL;
 
        if (list == NULL)
                return NULL;
 


@@ -1367,7 +1387,7 @@ bool valequals(uint64_t val1, uint64_t val2, int size) {
  */
 SnapVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *curr)
 {
  */
 SnapVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *curr)
 {

-       SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
+       SnapVector<simple_action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());

        unsigned int i;
        ASSERT(curr->is_read());
 
        unsigned int i;
        ASSERT(curr->is_read());
 


@@ -1382,7 +1402,7 @@ SnapVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *cu
        if (thrd_lists != NULL)
                for (i = 0;i < thrd_lists->size();i++) {
                        /* Iterate over actions in thread, starting from most recent */
        if (thrd_lists != NULL)
                for (i = 0;i < thrd_lists->size();i++) {
                        /* Iterate over actions in thread, starting from most recent */

-                       action_list_t *list = &(*thrd_lists)[i];
+                       simple_action_list_t *list = &(*thrd_lists)[i];

                        sllnode<ModelAction *> * rit;
                        for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
                                ModelAction *act = rit->getVal();
                        sllnode<ModelAction *> * rit;
                        for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
                                ModelAction *act = rit->getVal();


@@ -1684,14 +1704,23 @@ void ModelExecution::removeAction(ModelAction *act) {
                (*vec)[act->get_tid()].removeAction(act);
        }
        if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
                (*vec)[act->get_tid()].removeAction(act);
        }
        if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {

-               action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
-               list->removeAction(act);
+               sllnode<ModelAction *> * listref = act->getActionRef();
+               if (listref != NULL) {
+                       simple_action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+                       list->erase(listref);
+               }

        } else if (act->is_wait()) {
        } else if (act->is_wait()) {

-               void *mutex_loc = (void *) act->get_value();
-               get_safe_ptr_action(&obj_map, mutex_loc)->removeAction(act);
+               sllnode<ModelAction *> * listref = act->getActionRef();
+               if (listref != NULL) {
+                       void *mutex_loc = (void *) act->get_value();
+                       get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref);
+               }

        } else if (act->is_free()) {
        } else if (act->is_free()) {

-               SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
-               (*vec)[act->get_tid()].removeAction(act);
+               sllnode<ModelAction *> * listref = act->getActionRef();
+               if (listref != NULL) {
+                       SnapVector<simple_action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
+                       (*vec)[act->get_tid()].erase(listref);
+               }

 
                //Clear it from last_sc_map
                if (obj_last_sc_map.get(act->get_location()) == act) {
 
                //Clear it from last_sc_map
                if (obj_last_sc_map.get(act->get_location()) == act) {

diff --git a/execution.h b/execution.h
index 0c401b19b59084609a2fe12b1cbb565a736cfbac..5cd54469c6d3c920b1fda9ab7cecc54ca2de4f29 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -146,7 +146,7 @@ private:
         * to a trace of all actions performed on the object.
         * Used only for SC fences, unlocks, & wait.
         */
         * to a trace of all actions performed on the object.
         * Used only for SC fences, unlocks, & wait.
         */

-       HashTable<const void *, action_list_t *, uintptr_t, 2> obj_map;
+       HashTable<const void *, simple_action_list_t *, uintptr_t, 2> obj_map;

 
        /** Per-object list of actions. Maps an object (i.e., memory location)
         * to a trace of all actions performed on the object. */
 
        /** Per-object list of actions. Maps an object (i.e., memory location)
         * to a trace of all actions performed on the object. */


@@ -156,7 +156,7 @@ private:
        HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> obj_thrd_map;
 
        /** Per-object list of writes that each thread performed. */
        HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> obj_thrd_map;
 
        /** Per-object list of writes that each thread performed. */

-       HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> obj_wr_thrd_map;
+       HashTable<const void *, SnapVector<simple_action_list_t> *, uintptr_t, 2> obj_wr_thrd_map;

 
        HashTable<const void *, ModelAction *, uintptr_t, 4> obj_last_sc_map;
 
 
        HashTable<const void *, ModelAction *, uintptr_t, 4> obj_last_sc_map;