Move data structures from execution.h to history.h

diff --git a/execution.cc b/execution.cc
index 3c2edafaf03bea96f467aff2f35c8976862ce1db..7b8461226a8860d60a0311c2fa2538607c9b1363 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -64,8 +64,6 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        priv(new struct model_snapshot_members ()),
        mo_graph(new CycleGraph()),
        fuzzer(new NewFuzzer()),
-       thrd_func_list(),
-       thrd_func_act_lists(),
        isfinished(false)
 {
        /* Initialize a model-checker thread, for special ModelActions */

diff --git a/execution.h b/execution.h
index 5493489126a7d30a101e4400e9289acfe130ff4a..e25a72e9b697401b60dd5951aa7ef96cc0e390b6 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -85,9 +85,6 @@ public:
        HashTable<pthread_mutex_t *, cdsc::snapmutex *, uintptr_t, 4> * getMutexMap() {return &mutex_map;}
        ModelAction * check_current_action(ModelAction *curr);
 
-       SnapVector<func_id_list_t> * get_thrd_func_list() { return &thrd_func_list; }
-       SnapVector<uint32_t> * get_thrd_last_entered_func() { return &thrd_last_entered_func; }
-       SnapVector< SnapList<action_list_t *> *> * get_thrd_func_act_lists() { return &thrd_func_act_lists; }
        bool isFinished() {return isfinished;}
        void setFinished() {isfinished = true;}
 
@@ -203,20 +200,6 @@ private:
        Thread * action_select_next_thread(const ModelAction *curr) const;
        bool paused_by_fuzzer(const ModelAction * act) const;
 
-       /* thrd_func_list stores a list of function ids for each thread.
-        * Each element in thrd_func_list stores the functions that
-        * thread i has entered and yet to exit from
-        *
-        * This data structure is handled by ModelHistory
-        */
-       SnapVector<func_id_list_t> thrd_func_list;
-       SnapVector<uint32_t> thrd_last_entered_func;
-
-       /* Keeps track of atomic actions that thread i has performed in some
-        * function. Index of SnapVector is thread id. SnapList simulates
-        * the call stack.
-        */
-       SnapVector< SnapList<action_list_t *> *> thrd_func_act_lists;
        bool isfinished;
 };
 

diff --git a/history.cc b/history.cc
index 67f873b67b282d3d98e45c4d45d90f77a58821f1..f1060ca996e7949214d200e59aa0aa2c1b5a5dd0 100644 (file)
--- a/history.cc
+++ b/history.cc
@@ -23,6 +23,9 @@ ModelHistory::ModelHistory() :
        loc_rd_func_nodes_map = new HashTable<void *, SnapVector<FuncNode *> *, uintptr_t, 0>();
        loc_wr_func_nodes_map = new HashTable<void *, SnapVector<FuncNode *> *, uintptr_t, 0>();
        loc_waiting_writes_map = new HashTable<void *, SnapVector<ConcretePredicate *> *, uintptr_t, 0>();
+       thrd_func_act_lists = new SnapVector< SnapList<action_list_t *> *>();
+       thrd_func_list = new SnapVector<func_id_list_t>();
+       thrd_last_entered_func = new SnapVector<uint32_t>();
        thrd_waiting_write = new SnapVector<ConcretePredicate *>();
        thrd_wait_obj = new SnapVector<WaitObj *>();
        func_inst_act_maps = new HashTable<uint32_t, SnapVector<inst_act_map_t *> *, int, 0>(128);
@@ -38,14 +41,8 @@ ModelHistory::~ModelHistory()
 void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
 {
        //model_print("thread %d entering func %d\n", tid, func_id);
-       ModelExecution * execution = model->get_execution();
        uint id = id_to_int(tid);
 
-       SnapVector<func_id_list_t> * thrd_func_list = execution->get_thrd_func_list();
-       SnapVector< SnapList<action_list_t *> *> *
-               thrd_func_act_lists = execution->get_thrd_func_act_lists();
-       SnapVector<uint32_t> * thrd_last_entered_func = execution->get_thrd_last_entered_func();
-
        if ( thrd_func_list->size() <= id ) {
                uint oldsize = thrd_func_list->size();
                thrd_func_list->resize( id + 1 );
@@ -88,11 +85,7 @@ void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
 /* @param func_id a non-zero value */
 void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid)
 {
-       ModelExecution * execution = model->get_execution();
        uint32_t id = id_to_int(tid);
-       SnapVector<func_id_list_t> * thrd_func_list = execution->get_thrd_func_list();
-       SnapVector< SnapList<action_list_t *> *> *
-               thrd_func_act_lists = execution->get_thrd_func_act_lists();
 
        SnapList<action_list_t *> * func_act_lists = (*thrd_func_act_lists)[id];
        uint32_t last_func_id = (*thrd_func_list)[id].back();
@@ -147,11 +140,6 @@ void ModelHistory::resize_func_nodes(uint32_t new_size)
 
 void ModelHistory::process_action(ModelAction *act, thread_id_t tid)
 {
-       ModelExecution * execution = model->get_execution();
-       SnapVector<func_id_list_t> * thrd_func_list = execution->get_thrd_func_list();
-       SnapVector< SnapList<action_list_t *> *> *
-               thrd_func_act_lists = execution->get_thrd_func_act_lists();
-
        uint32_t thread_id = id_to_int(tid);
        /* Return if thread tid has not entered any function that contains atomics */
        if ( thrd_func_list->size() <= thread_id )
@@ -235,7 +223,6 @@ FuncNode * ModelHistory::get_func_node(uint32_t func_id)
 FuncNode * ModelHistory::get_curr_func_node(thread_id_t tid)
 {
        int thread_id = id_to_int(tid);
-       SnapVector<func_id_list_t> * thrd_func_list =  model->get_execution()->get_thrd_func_list();
        uint32_t func_id = (*thrd_func_list)[thread_id].back();
 
        if (func_id != 0) {

diff --git a/history.h b/history.h
index 4795eb53e4cae374027cccf6592eb68549dbc0f4..f06c2e44e46cb189c34d06f870063a75a0dcd772 100644 (file)
--- a/history.h
+++ b/history.h
@@ -73,6 +73,20 @@ private:
        HashTable<void *, SnapVector<FuncNode *> *, uintptr_t, 0> * loc_wr_func_nodes_map;
 
        HashTable<void *, SnapVector<ConcretePredicate *> *, uintptr_t, 0> * loc_waiting_writes_map;
+
+       /* Keeps track of atomic actions that thread i has performed in some
+        * function. Index of SnapVector is thread id. SnapList simulates
+        * the call stack.
+        */
+       SnapVector< SnapList<action_list_t *> *> * thrd_func_act_lists;
+
+       /* thrd_func_list stores a list of function ids for each thread.
+        * Each element in thrd_func_list stores the functions that
+        * thread i has entered and yet to exit from
+        */
+       SnapVector<func_id_list_t> * thrd_func_list;
+       SnapVector<uint32_t> * thrd_last_entered_func;
+
        /* The write values each paused thread is waiting for */
        SnapVector<ConcretePredicate *> * thrd_waiting_write;
        SnapVector<WaitObj *> * thrd_wait_obj;
@@ -84,6 +98,7 @@ private:
        bool skip_action(ModelAction * act, SnapList<ModelAction *> * curr_act_list);
        void monitor_waiting_thread(uint32_t func_id, thread_id_t tid);
        void monitor_waiting_thread_counter(thread_id_t tid);
+
 };
 
 #endif /* __HISTORY_H__ */