change func_atomics and work_list to vectors

diff --git a/execution.cc b/execution.cc
index d75499f1349a4e24c69a1c01c90aa8bb599240d5..af98c2f32619364df8bf27520ad2de2244ce7bad 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -14,6 +14,7 @@
 #include "datarace.h"
 #include "threads-model.h"
 #include "bugmessage.h"
+#include "history.h"
 #include "fuzzer.h"
 
 #define INITIAL_THREAD_ID       0
@@ -64,7 +65,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack
        thrd_last_fence_release(),
        node_stack(node_stack),
        priv(new struct model_snapshot_members ()),
-                        mo_graph(new CycleGraph()),
+       mo_graph(new CycleGraph()),
        fuzzer(new Fuzzer())
 {
        /* Initialize a model-checker thread, for special ModelActions */
@@ -388,10 +389,7 @@ bool ModelExecution::process_mutex(ModelAction *curr)
  */
 void ModelExecution::process_write(ModelAction *curr)
 {
-
        w_modification_order(curr);
-
-
        get_thread(curr)->set_return_value(VALUE_NONE);
 }
 
@@ -1631,6 +1629,9 @@ Thread * ModelExecution::take_step(ModelAction *curr)
        curr = check_current_action(curr);
        ASSERT(curr);
 
+       // model_print("poitner loc: %p, thread: %d, type: %d, order: %d, position: %s\n", curr, curr->get_tid(), curr->get_type(), curr->get_mo(), curr->get_position() );
+       model->get_history()->add_func_atomic( curr, curr_thrd->get_id() );
+
        if (curr_thrd->is_blocked() || curr_thrd->is_complete())
                scheduler->remove_thread(curr_thrd);
 

diff --git a/history.cc b/history.cc
index ca52209d6ff17b5a95ebe29a6cfaecb546e2de89..f757a5d75dfa4ecd84fd8704402240c02e44b5c1 100644 (file)
--- a/history.cc
+++ b/history.cc
@@ -2,29 +2,41 @@
 #include "history.h"
 #include "action.h"
 
+HistoryNode::HistoryNode(ModelAction *act) :
+       action(act)
+{
+       ASSERT(act);
+       this->position = act->get_position();
+}
+
+/** @brief Constructor */
 ModelHistory::ModelHistory() :
-       func_id(1), /* function id starts with 1 */
+       func_counter(0), /* function id starts with 0 */
        func_map(),
-       func_history(),
-       work_list()
+       func_atomics(),
+       work_list(2)    /* we have at least two threads */
 {}
 
 void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
 {
-       if ( !work_list.contains(tid) ) {
-               // This thread has not been pushed to work_list
-               SnapList<uint32_t> * func_list = new SnapList<uint32_t>();
-               func_list->push_back(func_id);
-               work_list.put(tid, func_list);
-       } else {
-               SnapList<uint32_t> * func_list = work_list.get(tid);
-               func_list->push_back(func_id);
+//     model_print("entering function: %d\n", func_id);
+
+       uint32_t id = id_to_int(tid);
+       if ( work_list.size() <= id )
+               work_list.resize( id + 1 );
+
+       func_id_list_t * func_list = work_list[id];
+       if (func_list == NULL) {
+               func_list = new func_id_list_t();
+               work_list[id] = func_list;
        }
+
+       func_list->push_back(func_id);
 }
 
 void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid)
 {
-       SnapList<uint32_t> * func_list = work_list.get(tid);
+       func_id_list_t * func_list = work_list[ id_to_int(tid) ];
        uint32_t last_func_id = func_list->back();
 
        if (last_func_id == func_id) {
@@ -33,4 +45,49 @@ void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid)
                model_print("trying to exit with a wrong function id\n");
                model_print("--- last_func: %d, func_id: %d\n", last_func_id, func_id);
        }
+
+//     model_print("exiting function: %d\n", func_id);
+}
+
+void ModelHistory::add_func_atomic(ModelAction *act, thread_id_t tid) {
+       /* return if thread i has not entered any function or has exited
+          from all functions */
+       uint32_t id = id_to_int(tid);
+       if ( work_list.size() <= id )
+               return;
+       else if (work_list[id] == NULL)
+               return;
+
+       /* get the function id that thread i is currently in */
+       func_id_list_t * func_list = work_list[id];
+       uint32_t func_id = func_list->back();
+
+       if ( func_atomics.size() <= func_id )
+               func_atomics.resize( func_id + 1 );
+
+       action_mlist_t * atomic_list = func_atomics[func_id];
+       if (atomic_list == NULL) {
+               atomic_list = new action_mlist_t();
+               func_atomics[func_id] = atomic_list;
+       }
+
+       atomic_list->push_back(act);
+
+       model_print("func id: %d, added atomic acts: %d\n", func_id, act->get_type());
+}
+
+void ModelHistory::print() {
+       for (uint32_t i = 0; i < func_atomics.size(); i++ ) {
+               action_mlist_t * atomic_list = func_atomics[i];
+
+               if (atomic_list == NULL)
+                       continue;
+
+               model_print("function with id: %d has following actions\n", i);
+               action_mlist_t::iterator it;
+               for (it = atomic_list->begin(); it != atomic_list->end(); it++) {
+                       const ModelAction *act = *it;
+                       act->print();
+               }
+       }
 }

diff --git a/history.h b/history.h
index fff5712629057311811bebde6401a42f57bf56db..03a8985292aa65cd97a56dc00fa3213fa86ae762 100644 (file)
--- a/history.h
+++ b/history.h
@@ -1,39 +1,54 @@
 #include "stl-model.h"
 #include "common.h"
 #include "hashtable.h"
-#include "modeltypes.h"
+#include "threads-model.h"
 
 /* forward declaration */
 class ModelAction;
 
-typedef ModelList<ModelAction *> action_mlist_t;
+typedef ModelList<const ModelAction *> action_mlist_t;
+typedef SnapList<uint32_t> func_id_list_t;
+
+class HistoryNode {
+public: 
+       HistoryNode(ModelAction *act);
+       ~HistoryNode();
+
+       ModelAction * get_action() const { return action; }
+       const char * get_position() const { return position; }
+private:
+       ModelAction * const action;
+       const char * position;
+};
 
 class ModelHistory {
 public:
        ModelHistory();
-       
+       ~ModelHistory();
+
        void enter_function(const uint32_t func_id, thread_id_t tid);
        void exit_function(const uint32_t func_id, thread_id_t tid);
 
-        uint32_t get_func_counter() { return func_id; }
-        void incr_func_counter() { func_id++; }
+        uint32_t get_func_counter() { return func_counter; }
+        void incr_func_counter() { func_counter++; }
+
+       void add_func_atomic(ModelAction *act, thread_id_t tid);
 
         HashTable<const char *, uint32_t, uintptr_t, 4> * getFuncMap() { return &func_map; }
-       HashTable<uint32_t, action_mlist_t *, uintptr_t, 4> * getFuncHistory() { return &func_history; }
+       ModelVector< action_mlist_t * > * getFuncAtomics() { return &func_atomics; }
 
        void print();
-
 private:
-       uint32_t func_id;
+       uint32_t func_counter;
 
         /* map function names to integer ids */ 
         HashTable<const char *, uint32_t, uintptr_t, 4> func_map;
 
-       HashTable<uint32_t, action_mlist_t *, uintptr_t, 4> func_history;
+       ModelVector< action_mlist_t * > func_atomics;
 
-       /* work_list stores a list of function ids for each thread
-        * SnapList<uint32_t> is intended to be used as a stack storing
+       /* Work_list stores a list of function ids for each thread. 
+        * Each element in work_list is intended to be used as a stack storing
         * the functions that thread i has entered and yet to exit from 
         */
-       HashTable<thread_id_t, SnapList<uint32_t> *, uintptr_t, 4> work_list;
+       SnapVector< func_id_list_t * > work_list;
 };