edits
authorweiyu <weiyuluo1232@gmail.com>
Thu, 16 Apr 2020 23:55:45 +0000 (16:55 -0700)
committerweiyu <weiyuluo1232@gmail.com>
Thu, 16 Apr 2020 23:55:45 +0000 (16:55 -0700)
action.cc
action.h
actionlist.cc
actionlist.h
execution.cc
execution.h

index d90a94e..9905ab2 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),
+       action_ref(NULL),
        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),
+       action_ref(NULL),
        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),
+       action_ref(NULL),
        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),
+       action_ref(NULL),
        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),
+       action_ref(NULL),
        value(value),
        type(type),
        order(order),
index c5ba6d7..fbf566f 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; }
 
+       void setActionRef(sllnode<ModelAction *> *ref) { action_ref = ref; }
+       sllnode<ModelAction *> * getActionRef() { return action_ref; }
+
        SNAPSHOTALLOC
 private:
        const char * get_type_str() const;
@@ -227,6 +230,7 @@ private:
         */
        ClockVector *cv;
        ClockVector *rf_cv;
+       sllnode<ModelAction *> * action_ref;
 
        /** @brief The value written (for write or RMW; undefined for read) */
        uint64_t value;
index 0dc8bc8..4a24ba9 100644 (file)
@@ -246,3 +246,16 @@ void actionlist::clear() {
 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;
+       }
+}
index 20f93fc..ee0a144 100644 (file)
@@ -41,6 +41,7 @@ public:
        uint size() {return _size;}
        sllnode<ModelAction *> * begin() {return head;}
        sllnode<ModelAction *> * end() {return tail;}
+       void fixupParent();
 
        SNAPSHOTALLOC;
 
index 9c3b4af..04314d1 100644 (file)
@@ -98,36 +98,50 @@ int ModelExecution::get_execution_number() const
        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) {
-               tmp = new action_list_t();
+               tmp = new SnapVector<action_list_t>();
                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) {
-               tmp = new SnapVector<action_list_t>();
+               tmp = new simple_action_list_t();
                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) {
-               tmp = new simple_action_list_t();
+               tmp = new SnapVector<simple_action_list_t>();
                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()
 {
@@ -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();
+
+               fixup_action_list(thrd_lists);
        }
 
        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()) {
-               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
@@ -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();
+
+               fixup_action_list(vec);
        }
        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();
-               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();
+
+               fixup_action_list(vec);
        }
        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) {
-       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++)
-                       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 */
-       action_list_t *list = obj_map.get(FENCE_LOCATION);
+       simple_action_list_t *list = obj_map.get(FENCE_LOCATION);
 
        if (!list)
                return NULL;
@@ -1311,7 +1331,7 @@ ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
 {
        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;
 
@@ -1367,7 +1387,7 @@ bool valequals(uint64_t val1, uint64_t val2, int size) {
  */
 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());
 
@@ -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 */
-                       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();
@@ -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()) {
-               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()) {
-               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()) {
-               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) {
index 0c401b1..5cd5446 100644 (file)
@@ -146,7 +146,7 @@ private:
         * 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. */
@@ -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_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;