Revamp obj_map for just what it is used for

diff --git a/execution.cc b/execution.cc
index 6d435dec095c4185a6b0dbbf89923a70431f3e73..3c2edafaf03bea96f467aff2f35c8976862ce1db 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -1110,11 +1110,10 @@ void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
        int tid = id_to_int(act->get_tid());
        ModelAction *uninit = NULL;
        int uninit_id = -1;
-       action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
-       if (list->empty() && act->is_atomic_var()) {
+       SnapVector<action_list_t> *objvec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
+       if (objvec->empty() && act->is_atomic_var()) {
                uninit = get_uninitialized_action(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());
                if ((int)vec->size() <= uninit_id) {
                        int oldsize = (int) vec->size();
@@ -1159,8 +1158,10 @@ void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
 void ModelExecution::add_action_to_lists(ModelAction *act)
 {
        int tid = id_to_int(act->get_tid());
-       action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
-       list->push_back(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->push_back(act);
+       }
 
        // Update action trace, a total order of all actions
        action_trace.push_back(act);
@@ -1249,9 +1250,6 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
        int tid = id_to_int(act->get_tid());
        insertIntoActionListAndSetCV(&action_trace, act);
 
-       action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
-       insertIntoActionList(list, 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());
        if (tid >= (int)vec->size()) {

diff --git a/execution.h b/execution.h
index a8ab02cc8bad2c548f7cf071095898034f63b581..4a453bb24650ff2f3878dfc2cd07ac491119b997 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -97,34 +97,20 @@ public:
 #endif
        SNAPSHOTALLOC
 private:
-#ifdef TLS
-       pthread_key_t pthreadkey;
-#endif
        int get_execution_number() const;
-
-       ModelChecker *model;
-
-       struct model_params * params;
-
-       /** The scheduler to use: tracks the running/ready Threads */
-       Scheduler * const scheduler;
-
        bool mo_may_allow(const ModelAction *writer, const ModelAction *reader);
        bool should_wake_up(const ModelAction *curr, const Thread *thread) const;
        void wake_up_sleeping_actions(ModelAction *curr);
        modelclock_t get_next_seq_num();
-
        bool next_execution();
        bool initialize_curr_action(ModelAction **curr);
        bool process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set);
        void process_write(ModelAction *curr);
        bool process_fence(ModelAction *curr);
        bool process_mutex(ModelAction *curr);
-
        void process_thread_action(ModelAction *curr);
        void read_from(ModelAction *act, ModelAction *rf);
        bool synchronize(const ModelAction *first, ModelAction *second);
-
        void add_uninit_action_to_lists(ModelAction *act);
        void add_action_to_lists(ModelAction *act);
        void add_normal_write_to_lists(ModelAction *act);
@@ -135,20 +121,30 @@ private:
        ModelAction * get_last_unlock(ModelAction *curr) const;
        SnapVector<ModelAction *> * build_may_read_from(ModelAction *curr);
        ModelAction * process_rmw(ModelAction *curr);
-
        bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> *priorset, bool *canprune, bool check_only = false);
        void w_modification_order(ModelAction *curr);
        ClockVector * get_hb_from_write(ModelAction *rf) const;
        ModelAction * get_uninitialized_action(ModelAction *curr) const;
        ModelAction * convertNonAtomicStore(void*);
 
+#ifdef TLS
+       pthread_key_t pthreadkey;
+#endif
+       ModelChecker *model;
+       struct model_params * params;
+
+       /** The scheduler to use: tracks the running/ready Threads */
+       Scheduler * const scheduler;
+
        action_list_t action_trace;
        SnapVector<Thread *> thread_map;
        SnapVector<Thread *> pthread_map;
        uint32_t pthread_counter;
 
        /** Per-object list of actions. Maps an object (i.e., memory location)
-        * to a trace of all actions performed on the object. */
+        * 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;
 
        /** Per-object list of actions. Maps an object (i.e., memory location)