add a data structrue to keep track of the run-time position in the predicate tree...

diff --git a/funcinst.h b/funcinst.h
index 9aec00f6cc3ae74880c4fc3af6a47cec5df28dd3..95d92ff3e9580921dafd10e324b5d79b51f77d0c 100644 (file)
--- a/funcinst.h
+++ b/funcinst.h
@@ -17,7 +17,7 @@ public:
 
        void * get_location() const { return location; }
        void set_location(void * loc) { location = loc; }
-       void reset_location() { location = NULL; }
+       void unset_location() { location = NULL; }
 
        action_type get_type() const { return type; }
        memory_order get_mo() const { return order; }

diff --git a/funcnode.cc b/funcnode.cc
index 6402a9aee732fd7c71de36284246e7619c2759a2..f4c6c9864c957f85bd6e87cf17aa5f46d0feeb27 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -8,19 +8,20 @@ FuncNode::FuncNode(ModelHistory * history) :
        inst_list(),
        entry_insts(),
 //     thrd_read_map(),
-       action_list_buffer()
+       action_list_buffer(),
+       predicate_tree_position()
 {
        predicate_tree_entry = new Predicate(NULL, true);
        predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true);
 
-       // memory will be reclaimed after each execution
+       // memories that are reclaimed after each execution
        read_locations = new loc_set_t();
        val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0>();
        loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
-       values_may_read_from = new value_set_t();
+       //values_may_read_from = new value_set_t();
 }
 
-/* Reallocate some snapshotted memories when new executions start */
+/* Reallocate snapshotted memories when new executions start */
 void FuncNode::set_new_exec_flag()
 {
 //     for (uint i = 0; i < thrd_read_map.size(); i++)
@@ -28,13 +29,13 @@ void FuncNode::set_new_exec_flag()
 
        for (mllnode<FuncInst *> * it = inst_list.begin(); it != NULL; it = it->getNext()) {
                FuncInst * inst = it->getVal();
-               inst->reset_location();
+               inst->unset_location();
        }
 
        read_locations = new loc_set_t();
        val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0>();
        loc_may_equal_map = new HashTable<void *, loc_set_t *, uintptr_t, 0>();
-       values_may_read_from = new value_set_t();
+       //values_may_read_from = new value_set_t();
 }
 
 /* Check whether FuncInst with the same type, position, and location
@@ -163,13 +164,13 @@ void FuncNode::update_tree(action_list_t * act_list)
                }
        }
 
-       model_print("function %s\n", func_name);
+//     model_print("function %s\n", func_name);
 //     print_val_loc_map();
 
        update_inst_tree(&inst_list);
        update_predicate_tree(&read_act_list);
 
-       print_predicate_tree();
+//     print_predicate_tree();
 }
 
 /** 
@@ -207,7 +208,7 @@ void FuncNode::update_inst_tree(func_inst_list_t * inst_list)
 
 /* @param tid thread id
  * Store the values read by atomic read actions into thrd_read_map */
-void FuncNode::store_read(ModelAction * act, uint32_t tid)
+void FuncNode::store_read(ModelAction * act, thread_id_t tid)
 {
 /*
        ASSERT(act);
@@ -228,7 +229,7 @@ void FuncNode::store_read(ModelAction * act, uint32_t tid)
 */
 }
 
-uint64_t FuncNode::query_last_read(void * location, uint32_t tid)
+uint64_t FuncNode::query_last_read(void * location, thread_id_t tid)
 {
 /*
        if (thrd_read_map.size() <= tid)
@@ -249,7 +250,7 @@ uint64_t FuncNode::query_last_read(void * location, uint32_t tid)
  * Reset read map for a thread. This function shall only be called
  * when a thread exits a function
  */
-void FuncNode::clear_read_map(uint32_t tid)
+void FuncNode::clear_read_map(thread_id_t tid)
 {
 /*
        if (thrd_read_map.size() <= tid)
@@ -521,7 +522,7 @@ void FuncNode::add_to_val_loc_map(uint64_t val, void * loc)
 
        update_loc_may_equal_map(loc, locations);
        locations->add(loc);
-       values_may_read_from->add(val);
+       // values_may_read_from->add(val);
 }
 
 void FuncNode::add_to_val_loc_map(value_set_t * values, void * loc)
@@ -558,6 +559,21 @@ void FuncNode::update_loc_may_equal_map(void * new_loc, loc_set_t * old_location
        }
 }
 
+void FuncNode::init_predicate_tree_position(thread_id_t tid)
+{
+       uint thread_id = id_to_int(tid);
+       if (predicate_tree_position.size() <= thread_id)
+               predicate_tree_position.resize(thread_id + 1);
+
+       predicate_tree_position[thread_id] = predicate_tree_entry;
+}
+
+void FuncNode::unset_predicate_tree_position(thread_id_t tid)
+{
+       uint thread_id = id_to_int(tid);
+       predicate_tree_position[thread_id] = NULL;
+}
+
 void FuncNode::print_predicate_tree()
 {
        model_print("digraph function_%s {\n", func_name);
@@ -567,6 +583,7 @@ void FuncNode::print_predicate_tree()
 
 void FuncNode::print_val_loc_map()
 {
+/*
        value_set_iter * val_it = values_may_read_from->iterator();
        while (val_it->hasNext()) {
                uint64_t value = val_it->next();
@@ -580,13 +597,14 @@ void FuncNode::print_val_loc_map()
                }
                model_print("\n");
        }
+*/
 }
 
 /* @param tid thread id
  * Print the values read by the last read actions for each memory location
  */
 /*
-void FuncNode::print_last_read(uint32_t tid)
+void FuncNode::print_last_read(thread_id_t tid)
 {
        ASSERT(thrd_read_map.size() > tid);
        read_map_t * read_map = thrd_read_map[tid];

diff --git a/funcnode.h b/funcnode.h
index e757b650df5770c41fc627551d300c9bab839546..e414b4b9b7c74582aa4028fe5c6b9e41d0a9e148 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -33,9 +33,9 @@ public:
        void update_tree(action_list_t * act_list);
        void update_inst_tree(func_inst_list_t * inst_list);
 
-       void store_read(ModelAction * act, uint32_t tid);
-       uint64_t query_last_read(void * location, uint32_t tid);
-       void clear_read_map(uint32_t tid);
+       void store_read(ModelAction * act, thread_id_t tid);
+       uint64_t query_last_read(void * location, thread_id_t tid);
+       void clear_read_map(thread_id_t tid);
 
        void update_predicate_tree(action_list_t * act_list);
        bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, HashTable<FuncInst *, ModelAction *, uintptr_t, 0>* inst_act_map, SnapVector<Predicate *> * unset_predicates);
@@ -51,9 +51,13 @@ public:
        void add_to_val_loc_map(value_set_t * values, void * loc);
        void update_loc_may_equal_map(void * new_loc, loc_set_t * old_locations);
 
+       void init_predicate_tree_position(thread_id_t tid);
+       void unset_predicate_tree_position(thread_id_t tid);
+       Predicate * get_predicate_tree_position(thread_id_t tid);
+
        void print_predicate_tree();
        void print_val_loc_map();
-       void print_last_read(uint32_t tid);
+       void print_last_read(thread_id_t tid);
 
        MEMALLOC
 private:
@@ -89,7 +93,10 @@ private:
        loc_set_t * read_locations;
        HashTable<uint64_t, loc_set_t *, uint64_t, 0> * val_loc_map;
        HashTable<void *, loc_set_t *, uintptr_t, 0> * loc_may_equal_map;
-       value_set_t * values_may_read_from;
+       // value_set_t * values_may_read_from;
+
+       /* run-time position in the predicate tree for each thread */
+       ModelVector<Predicate *> predicate_tree_position;
 };
 
 #endif /* __FUNCNODE_H__ */

diff --git a/history.cc b/history.cc
index 9b0780e9f09d8ed2243143bdd3e63ee9b10f1612..b546cd0abd1bc65e48ec631b6cd47eb3eb832951 100644 (file)
--- a/history.cc
+++ b/history.cc
@@ -48,6 +48,9 @@ void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
 
        if ( func_nodes.size() <= func_id )
                resize_func_nodes( func_id + 1 );
+
+       FuncNode * func_node = func_nodes[func_id];
+       func_node->init_predicate_tree_position(tid);
 }
 
 /* @param func_id a non-zero value */
@@ -63,12 +66,13 @@ void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid)
 
        if (last_func_id == func_id) {
                FuncNode * func_node = func_nodes[func_id];
+               func_node->unset_predicate_tree_position(tid);
                //func_node->clear_read_map(tid);
 
                action_list_t * curr_act_list = func_act_lists->back();
 
                /* defer the processing of curr_act_list until the function has exits a few times 
-                * (currently 2 times) so that more information can be gathered to infer nullity predicates.
+                * (currently twice) so that more information can be gathered to infer nullity predicates.
                 */
                func_node->incr_exit_count();
                if (func_node->get_exit_count() >= 2) {
@@ -99,7 +103,7 @@ void ModelHistory::resize_func_nodes(uint32_t new_size)
        if ( old_size < new_size )
                func_nodes.resize(new_size);
 
-       for (uint32_t id = old_size;id < new_size;id++) {
+       for (uint32_t id = old_size; id < new_size; id++) {
                const char * func_name = func_map_rev[id];
                FuncNode * func_node = new FuncNode(this);
                func_node->set_func_id(id);