Eager update predicate trees rather than lazy update; under construction
authorweiyu <weiyuluo1232@gmail.com>
Tue, 11 Feb 2020 02:04:16 +0000 (18:04 -0800)
committerweiyu <weiyuluo1232@gmail.com>
Tue, 11 Feb 2020 02:04:16 +0000 (18:04 -0800)
action.cc
action.h
execution.cc
funcnode.cc
funcnode.h
history.cc

index ee980b8..d656954 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -41,11 +41,8 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
        trace_ref(NULL),
        thrdmap_ref(NULL),
        action_ref(NULL),
-       func_ref_count(0),
        value(value),
        type(type),
-       original_type(ATOMIC_NOP),
-       swap_flag(false),
        order(order),
        original_order(order),
        seq_number(ACTION_INITIAL_CLOCK)
@@ -78,11 +75,8 @@ ModelAction::ModelAction(action_type_t type, memory_order order, uint64_t value,
        trace_ref(NULL),
        thrdmap_ref(NULL),
        action_ref(NULL),
-       func_ref_count(0),
        value(value),
        type(type),
-       original_type(ATOMIC_NOP),
-       swap_flag(false),
        order(order),
        original_order(order),
        seq_number(ACTION_INITIAL_CLOCK)
@@ -114,11 +108,8 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
        trace_ref(NULL),
        thrdmap_ref(NULL),
        action_ref(NULL),
-       func_ref_count(0),
        value(value),
        type(type),
-       original_type(ATOMIC_NOP),
-       swap_flag(false),
        order(order),
        original_order(order),
        seq_number(ACTION_INITIAL_CLOCK)
@@ -154,11 +145,8 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order
        trace_ref(NULL),
        thrdmap_ref(NULL),
        action_ref(NULL),
-       func_ref_count(0),
        value(value),
        type(type),
-       original_type(ATOMIC_NOP),
-       swap_flag(false),
        order(order),
        original_order(order),
        seq_number(ACTION_INITIAL_CLOCK)
@@ -195,11 +183,8 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order
        trace_ref(NULL),
        thrdmap_ref(NULL),
        action_ref(NULL),
-       func_ref_count(0),
        value(value),
        type(type),
-       original_type(ATOMIC_NOP),
-       swap_flag(false),
        order(order),
        original_order(order),
        seq_number(ACTION_INITIAL_CLOCK)
@@ -787,16 +772,3 @@ cdsc::mutex * ModelAction::get_mutex() const
        else
                return NULL;
 }
-
-/** @brief Swap type with original type */
-void ModelAction::use_original_type()
-{
-       action_type_t tmp = type;
-       type = original_type;
-       original_type = tmp;
-
-       if (swap_flag)
-               swap_flag = false;
-       else
-               swap_flag = true;
-}
index f792de2..35368ef 100644 (file)
--- a/action.h
+++ b/action.h
@@ -104,8 +104,6 @@ public:
        thread_id_t get_tid() const { return tid; }
        action_type get_type() const { return type; }
        void set_type(action_type _type) { type = _type; }
-       action_type get_original_type() const { return original_type; }
-       void set_original_type(action_type _type) { original_type = _type; }
        void set_free() { type = READY_FREE; }
        memory_order get_mo() const { return order; }
        memory_order get_original_mo() const { return original_order; }
@@ -120,7 +118,6 @@ public:
        ModelAction * get_reads_from() const { return reads_from; }
        uint64_t get_time() const {return time;}
        cdsc::mutex * get_mutex() const;
-       bool get_swap_flag() const { return swap_flag; }
 
        void set_read_from(ModelAction *act);
 
@@ -192,8 +189,6 @@ public:
        bool equals(const ModelAction *x) const { return this == x; }
        void set_value(uint64_t val) { value = val; }
 
-       void use_original_type();
-
        /* to accomodate pthread create and join */
        Thread * thread_operand;
        void set_thread_operand(Thread *th) { thread_operand = th; }
@@ -204,10 +199,6 @@ public:
        sllnode<ModelAction *> * getThrdMapRef() { return thrdmap_ref; }
        sllnode<ModelAction *> * getActionRef() { return action_ref; }
 
-       void incr_func_ref_count() { func_ref_count++; }
-       void decr_func_ref_count() { if (func_ref_count > 0) func_ref_count--; }
-       uint32_t get_func_ref_count() { return func_ref_count; }
-
        SNAPSHOTALLOC
 private:
        const char * get_type_str() const;
@@ -246,23 +237,12 @@ private:
        sllnode<ModelAction *> * thrdmap_ref;
        sllnode<ModelAction *> * action_ref;
 
-       /** @brief Number of read actions that are reading from this store */
-       uint32_t func_ref_count;
-
        /** @brief The value written (for write or RMW; undefined for read) */
        uint64_t value;
 
        /** @brief Type of action (read, write, RMW, fence, thread create, etc.) */
        action_type type;
 
-       /** @brief The original type of action (read, write, RMW) before it was 
-        * set as READY_FREE or weaken from a RMW to a write */
-       action_type original_type;
-
-       /** @brief Indicate whether the action type and the original action type 
-        *  has been swapped. */
-       bool swap_flag;
-
        /** @brief The memory order for this operation. */
        memory_order order;
 
index bfb9327..a98567e 100644 (file)
@@ -1774,8 +1774,6 @@ void ModelExecution::collectActions() {
                                                CycleNode * prevnode = node->getInEdge(i);
                                                ModelAction * prevact = prevnode->getAction();
                                                if (prevact->get_type() != READY_FREE) {
-                                                       // Save the original action type
-                                                       prevact->set_original_type(prevact->get_type());
                                                        prevact->set_free();
                                                        queue->push_back(prevnode);
                                                }
@@ -1801,8 +1799,6 @@ void ModelExecution::collectActions() {
                if (act->is_read()) {
                        if (act->get_reads_from()->is_free()) {
                                if (act->is_rmw()) {
-                                       // Save the original action type
-                                       act->set_original_type(act->get_type());
                                        //Weaken a RMW from a freed store to a write
                                        act->set_type(ATOMIC_WRITE);
                                } else {
@@ -1811,12 +1807,8 @@ void ModelExecution::collectActions() {
                                                fixupLastAct(act);
                                        }
 
-                                       // Only delete this action if not being using by ModelHistory.
-                                       // Otherwise, the deletion of action is deferred.
-                                       if (act->get_func_ref_count() == 0) {
-                                               delete act;
-                                               continue;
-                                       }
+                                       delete act;
+                                       continue;
                                }
                        }
                }
@@ -1847,18 +1839,14 @@ void ModelExecution::collectActions() {
                if (act->is_read()) {
                        if (act->get_reads_from()->is_free()) {
                                if (act->is_rmw()) {
-                                       // Save the original action type
-                                       act->set_original_type(act->get_type());
                                        act->set_type(ATOMIC_WRITE);
                                } else {
                                        removeAction(act);
                                        if (islastact) {
                                                fixupLastAct(act);
                                        }
-                                       if (act->get_func_ref_count() == 0) {
-                                               delete act;
-                                               continue;
-                                       }
+                                       delete act;
+                                       continue;
                                }
                        }
                } else if (act->is_free()) {
@@ -1866,10 +1854,8 @@ void ModelExecution::collectActions() {
                        if (islastact) {
                                fixupLastAct(act);
                        }
-                       if (act->get_func_ref_count() == 0) {
-                               delete act;
-                               continue;
-                       }
+                       delete act;
+                       continue;
                } else if (act->is_write()) {
                        //Do nothing with write that hasn't been marked to be freed
                } else if (islastact) {
index 9f972f0..a0850c7 100644 (file)
@@ -12,12 +12,13 @@ FuncNode::FuncNode(ModelHistory * history) :
        history(history),
        exit_count(0),
        marker(1),
+       inst_counter(1),
        func_inst_map(),
        inst_list(),
        entry_insts(),
-       inst_pred_map(128),
-       inst_id_map(128),
-       loc_act_map(128),
+       thrd_inst_pred_map(),
+       thrd_inst_id_map(),
+       thrd_loc_act_map(),
        predicate_tree_position(),
        predicate_leaves(),
        leaves_tmp_storage(),
@@ -33,7 +34,6 @@ FuncNode::FuncNode(ModelHistory * history) :
        predicate_tree_exit->set_depth(MAX_DEPTH);
 
        /* Snapshot data structures below */
-       action_list_buffer = new SnapList<action_list_t *>();
        read_locations = new loc_set_t();
        write_locations = new loc_set_t();
        val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free, int64_hash>();
@@ -45,7 +45,6 @@ FuncNode::FuncNode(ModelHistory * history) :
 /* Reallocate snapshotted memories when new executions start */
 void FuncNode::set_new_exec_flag()
 {
-       action_list_buffer = new SnapList<action_list_t *>();
        read_locations = new loc_set_t();
        write_locations = new loc_set_t();
        val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free, int64_hash>();
@@ -152,7 +151,6 @@ FuncInst * FuncNode::get_inst(ModelAction *act)
        }
 }
 
-
 void FuncNode::add_entry_inst(FuncInst * inst)
 {
        if (inst == NULL)
@@ -167,134 +165,80 @@ void FuncNode::add_entry_inst(FuncInst * inst)
        entry_insts.push_back(inst);
 }
 
+void FuncNode::function_entry_handler(thread_id_t tid)
+{
+       marker++;
+
+       init_predicate_tree_position(tid);
+       init_inst_act_map(tid);
+       init_maps(tid);
+}
+
+void FuncNode::function_exit_handler(thread_id_t tid)
+{
+       exit_count++;
+
+       reset_inst_act_map(tid);
+       reset_maps(tid);
+
+       Predicate * exit_pred = get_predicate_tree_position(tid);
+       if (exit_pred->get_exit() == NULL) {
+               // Exit predicate is unset yet
+               exit_pred->set_exit(predicate_tree_exit);
+       }
+
+       set_predicate_tree_position(tid, NULL);
+}
+
 /**
  * @brief Convert ModelAdtion list to FuncInst list
  * @param act_list A list of ModelActions
  */
-void FuncNode::update_tree(action_list_t * act_list)
+void FuncNode::update_tree(ModelAction * act)
 {
-       if (act_list == NULL || act_list->size() == 0)
-               return;
-
        HashTable<void *, value_set_t *, uintptr_t, 0> * write_history = history->getWriteHistory();
        HashSet<ModelAction *, uintptr_t, 2> write_actions;
 
        /* build inst_list from act_list for later processing */
-       func_inst_list_t inst_list;
-       action_list_t rw_act_list;
-
-       for (sllnode<ModelAction *> * it = act_list->begin();it != NULL;it = it->getNext()) {
-               ModelAction * act = it->getVal();
-
-               // Use the original action type and decrement ref count
-               // so that actions may be deleted by Execution::collectActions
-               if (act->get_original_type() != ATOMIC_NOP && act->get_swap_flag() == false)
-                       act->use_original_type();
+//     func_inst_list_t inst_list;
 
-               act->decr_func_ref_count();
+       FuncInst * func_inst = get_inst(act);
+       void * loc = act->get_location();
 
-               if (act->is_read()) {
-                       // For every read or rmw actions in this list, the reads_from was marked, and not deleted.
-                       // So it is safe to call get_reads_from
-                       ModelAction * rf = act->get_reads_from();
-                       if (rf->get_original_type() != ATOMIC_NOP && rf->get_swap_flag() == false)
-                               rf->use_original_type();
-
-                       rf->decr_func_ref_count();
-               }
-
-               FuncInst * func_inst = get_inst(act);
-               void * loc = act->get_location();
-
-               if (func_inst == NULL)
-                       continue;
+       if (func_inst == NULL)
+               return;
 
-               inst_list.push_back(func_inst);
-               bool act_added = false;
+//     inst_list.push_back(func_inst);
 
-               if (act->is_write()) {
-                       rw_act_list.push_back(act);
-                       act_added = true;
-                       if (!write_locations->contains(loc)) {
-                               write_locations->add(loc);
-                               history->update_loc_wr_func_nodes_map(loc, this);
-                       }
+       if (act->is_write()) {
+               if (!write_locations->contains(loc)) {
+                       write_locations->add(loc);
+                       history->update_loc_wr_func_nodes_map(loc, this);
                }
 
-               if (act->is_read()) {
-                       if (!act_added)
-                               rw_act_list.push_back(act);
-
-                       /* If func_inst may only read_from a single location, then:
-                        *
-                        * The first time an action reads from some location,
-                        * import all the values that have been written to this
-                        * location from ModelHistory and notify ModelHistory
-                        * that this FuncNode may read from this location.
-                        */
-                       if (!read_locations->contains(loc) && func_inst->is_single_location()) {
-                               read_locations->add(loc);
-                               value_set_t * write_values = write_history->get(loc);
-                               add_to_val_loc_map(write_values, loc);
-                               history->update_loc_rd_func_nodes_map(loc, this);
-                       }
-               }
+               // Do not process writes for now
+               return;
        }
 
-       update_inst_tree(&inst_list);
-       update_predicate_tree(&rw_act_list);
-
-       // Revert back action types and free
-       for (sllnode<ModelAction *> * it = act_list->begin(); it != NULL;) {
-               ModelAction * act = it->getVal();
-               // Do iteration early in case we delete read actions
-               it = it->getNext();
-
-               // Collect write actions and reads_froms
-               if (act->is_read()) {
-                       if (act->is_rmw()) {
-                               write_actions.add(act);
-                       }
-
-                       ModelAction * rf = act->get_reads_from();
-                       write_actions.add(rf);
-               } else if (act->is_write()) {
-                       write_actions.add(act);
-               }
-
-               // Revert back action types
-               if (act->is_read()) {
-                       ModelAction * rf = act->get_reads_from();
-                       if (rf->get_swap_flag() == true)
-                               rf->use_original_type();
-               }
-
-               if (act->get_swap_flag() == true)
-                       act->use_original_type();
-
-               //  Free read actions
-               if (act->is_read()) {
-                       if (act->is_rmw()) {
-                               // Do nothing. Its reads_from can not be READY_FREE
-                       } else {
-                               ModelAction *rf = act->get_reads_from();
-                               if (rf->is_free()) {
-                                       model_print("delete read %d; %p\n", act->get_seq_number(), act);
-                                       delete act;
-                               }
-                       }
+       if (act->is_read()) {
+
+               /* If func_inst may only read_from a single location, then:
+                *
+                * The first time an action reads from some location,
+                * import all the values that have been written to this
+                * location from ModelHistory and notify ModelHistory
+                * that this FuncNode may read from this location.
+                */
+               if (!read_locations->contains(loc) && func_inst->is_single_location()) {
+                       read_locations->add(loc);
+                       value_set_t * write_values = write_history->get(loc);
+                       add_to_val_loc_map(write_values, loc);
+                       history->update_loc_rd_func_nodes_map(loc, this);
                }
        }
 
-       // Free write actions if possible
-       HSIterator<ModelAction *, uintptr_t, 2> * it = write_actions.iterator();
-       while (it->hasNext()) {
-               ModelAction * act = it->next();
-
-               if (act->is_free() && act->get_func_ref_count() == 0)
-                       delete act;
-       }
-       delete it;
+//     update_inst_tree(&inst_list); TODO
+       update_predicate_tree(act);
 
 //     print_predicate_tree();
 }
@@ -332,26 +276,21 @@ void FuncNode::update_inst_tree(func_inst_list_t * inst_list)
        }
 }
 
-void FuncNode::update_predicate_tree(action_list_t * act_list)
+void FuncNode::update_predicate_tree(ModelAction * next_act)
 {
-       if (act_list == NULL || act_list->size() == 0)
-               return;
-
-       incr_marker();
-       uint32_t inst_counter = 0;
+       thread_id_t tid = next_act->get_tid();
+       int thread_id = id_to_int(tid);
 
        // Clear hashtables
-       loc_act_map.reset();
-       inst_pred_map.reset();
-       inst_id_map.reset();
+       loc_act_map_t * loc_act_map = thrd_loc_act_map[thread_id];
+       inst_pred_map_t * inst_pred_map = thrd_inst_pred_map[thread_id];
+       inst_id_map_t * inst_id_map = thrd_inst_id_map[thread_id];
 
        // Clear the set of leaves encountered in this path
-       leaves_tmp_storage.clear();
+       // leaves_tmp_storage.clear();
 
-       sllnode<ModelAction *> *it = act_list->begin();
-       Predicate * curr_pred = predicate_tree_entry;
-       while (it != NULL) {
-               ModelAction * next_act = it->getVal();
+       Predicate * curr_pred = get_predicate_tree_position(tid);
+       while (true) {
                FuncInst * next_inst = get_inst(next_act);
                next_inst->set_associated_act(next_act, marker);
 
@@ -370,13 +309,13 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
                }
 
                // Detect loops
-               if (!branch_found && inst_id_map.contains(next_inst)) {
+               if (!branch_found && inst_id_map->contains(next_inst)) {
                        FuncInst * curr_inst = curr_pred->get_func_inst();
-                       uint32_t curr_id = inst_id_map.get(curr_inst);
-                       uint32_t next_id = inst_id_map.get(next_inst);
+                       uint32_t curr_id = inst_id_map->get(curr_inst);
+                       uint32_t next_id = inst_id_map->get(next_inst);
 
                        if (curr_id >= next_id) {
-                               Predicate * old_pred = inst_pred_map.get(next_inst);
+                               Predicate * old_pred = inst_pred_map->get(next_inst);
                                Predicate * back_pred = old_pred->get_parent();
 
                                // For updating weights
@@ -402,24 +341,21 @@ void FuncNode::update_predicate_tree(action_list_t * act_list)
 
                if (next_act->is_read()) {
                        /* Only need to store the locations of read actions */
-                       loc_act_map.put(next_act->get_location(), next_act);
+                       loc_act_map->put(next_act->get_location(), next_act);
                }
 
-               inst_pred_map.put(next_inst, curr_pred);
-               if (!inst_id_map.contains(next_inst))
-                       inst_id_map.put(next_inst, inst_counter++);
+               inst_pred_map->put(next_inst, curr_pred);
+               set_predicate_tree_position(tid, curr_pred);
 
-               it = it->getNext();
-               curr_pred->incr_expl_count();
-       }
+               if (!inst_id_map->contains(next_inst))
+                       inst_id_map->put(next_inst, inst_counter++);
 
-       if (curr_pred->get_exit() == NULL) {
-               // Exit predicate is unset yet
-               curr_pred->set_exit(predicate_tree_exit);
+               curr_pred->incr_expl_count();
+               break;
        }
 
-       leaves_tmp_storage.push_back(curr_pred);
-       update_predicate_tree_weight();
+//     leaves_tmp_storage.push_back(curr_pred);
+//     update_predicate_tree_weight();
 }
 
 /* Given curr_pred and next_inst, find the branch following curr_pred that
@@ -444,6 +380,7 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst,
                /* Only read and rmw actions my have unset predicate expressions */
                if (pred_expressions->getSize() == 0) {
                        predicate_correct = false;
+
                        if (*unset_predicate == NULL)
                                *unset_predicate = branch;
                        else
@@ -507,11 +444,13 @@ void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act,
                                                                                                                                SnapVector<struct half_pred_expr *> * half_pred_expressions)
 {
        void * loc = next_act->get_location();
+       int thread_id = id_to_int(next_act->get_tid());
+       loc_act_map_t * loc_act_map = thrd_loc_act_map[thread_id];
 
        if (next_inst->is_read()) {
                /* read + rmw */
-               if ( loc_act_map.contains(loc) ) {
-                       ModelAction * last_act = loc_act_map.get(loc);
+               if ( loc_act_map->contains(loc) ) {
+                       ModelAction * last_act = loc_act_map->get(loc);
                        FuncInst * last_inst = get_inst(last_act);
                        struct half_pred_expr * expression = new half_pred_expr(EQUALITY, last_inst);
                        half_pred_expressions->push_back(expression);
@@ -522,8 +461,8 @@ void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act,
                                loc_set_iter * loc_it = loc_may_equal->iterator();
                                while (loc_it->hasNext()) {
                                        void * neighbor = loc_it->next();
-                                       if (loc_act_map.contains(neighbor)) {
-                                               ModelAction * last_act = loc_act_map.get(neighbor);
+                                       if (loc_act_map->contains(neighbor)) {
+                                               ModelAction * last_act = loc_act_map->get(neighbor);
                                                FuncInst * last_inst = get_inst(last_act);
 
                                                struct half_pred_expr * expression = new half_pred_expr(EQUALITY, last_inst);
@@ -738,7 +677,7 @@ void FuncNode::init_inst_act_map(thread_id_t tid)
        SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
        uint old_size = thrd_inst_act_map->size();
 
-       if (thrd_inst_act_map->size() <= (uint) thread_id) {
+       if (old_size <= (uint) thread_id) {
                uint new_size = thread_id + 1;
                thrd_inst_act_map->resize(new_size);
 
@@ -775,6 +714,35 @@ inst_act_map_t * FuncNode::get_inst_act_map(thread_id_t tid)
        return (*thrd_inst_act_map)[thread_id];
 }
 
+/* Make sure elements of thrd_loc_act_map are initialized properly when threads enter functions */
+void FuncNode::init_maps(thread_id_t tid)
+{
+       int thread_id = id_to_int(tid);
+       uint old_size = thrd_loc_act_map.size();
+
+       if (old_size <= (uint) thread_id) {
+               uint new_size = thread_id + 1;
+               thrd_loc_act_map.resize(new_size);
+               thrd_inst_id_map.resize(new_size);
+               thrd_inst_pred_map.resize(new_size);
+
+               for (uint i = old_size; i < new_size;i++) {
+                       thrd_loc_act_map[i] = new loc_act_map_t(128);
+                       thrd_inst_id_map[i] = new inst_id_map_t(128);
+                       thrd_inst_pred_map[i] = new inst_pred_map_t(128);
+               }
+       }
+}
+
+/* Reset elements of thrd_loc_act_map when threads exit functions */
+void FuncNode::reset_maps(thread_id_t tid)
+{
+       int thread_id = id_to_int(tid);
+       thrd_loc_act_map[thread_id]->reset();
+       thrd_inst_id_map[thread_id]->reset();
+       thrd_inst_pred_map[thread_id]->reset();
+}
+
 /* Add FuncNodes that this node may follow */
 void FuncNode::add_out_edge(FuncNode * other)
 {
index a0eb623..be0fdd8 100644 (file)
@@ -9,6 +9,10 @@
 #define MAX_DIST 10
 
 typedef ModelList<FuncInst *> func_inst_list_mt;
+typedef HashTable<void *, ModelAction *, uintptr_t, 0, model_malloc, model_calloc, model_free> loc_act_map_t;
+typedef HashTable<FuncInst *, uint32_t, uintptr_t, 0, model_malloc, model_calloc, model_free> inst_id_map_t;
+typedef HashTable<FuncInst *, Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> inst_pred_map_t;
+
 typedef enum edge_type {
        IN_EDGE, OUT_EDGE, BI_EDGE
 } edge_type_t;
@@ -33,16 +37,16 @@ public:
        func_inst_list_mt * get_entry_insts() { return &entry_insts; }
        void add_entry_inst(FuncInst * inst);
 
-       void update_tree(action_list_t * act_list);
+       void function_entry_handler(thread_id_t tid);
+       void function_exit_handler(thread_id_t tid);
+
+       void update_tree(ModelAction * act);
        void update_inst_tree(func_inst_list_t * inst_list);
-       void update_predicate_tree(action_list_t * act_list);
+       void update_predicate_tree(ModelAction * act);
        bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, Predicate ** unset_predicate);
 
-       void incr_exit_count() { exit_count++; }
        uint32_t get_exit_count() { return exit_count; }
 
-       SnapList<action_list_t *> * get_action_list_buffer() { return action_list_buffer; }
-
        void add_to_val_loc_map(uint64_t val, void * loc);
        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);
@@ -74,8 +78,7 @@ private:
 
        uint32_t exit_count;
        uint32_t marker;
-
-       void incr_marker() { marker++; }
+       uint32_t inst_counter;
 
        /* Use source line number as the key of hashtable, to check if
         * atomic operation with this line number has been added or not
@@ -89,21 +92,21 @@ private:
        func_inst_list_mt entry_insts;
 
        /* Map a FuncInst to the its predicate when updating predicate trees */
-       HashTable<FuncInst *, Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> inst_pred_map;
+       SnapVector<inst_pred_map_t *> thrd_inst_pred_map;
 
        /* Number FuncInsts to detect loops when updating predicate trees */
-       HashTable<FuncInst *, uint32_t, uintptr_t, 0, model_malloc, model_calloc, model_free> inst_id_map;
+       SnapVector<inst_id_map_t *> thrd_inst_id_map;
 
        /* Delect read actions at the same locations when updating predicate trees */
-       HashTable<void *, ModelAction *, uintptr_t, 0, model_malloc, model_calloc, model_free> loc_act_map;
+       SnapVector<loc_act_map_t *> thrd_loc_act_map;
+
+       void init_maps(thread_id_t tid);
+       void reset_maps(thread_id_t tid);
 
        void infer_predicates(FuncInst * next_inst, ModelAction * next_act, SnapVector<struct half_pred_expr *> * half_pred_expressions);
        void generate_predicates(Predicate * curr_pred, FuncInst * next_inst, SnapVector<struct half_pred_expr *> * half_pred_expressions);
        bool amend_predicate_expr(Predicate * curr_pred, FuncInst * next_inst, ModelAction * next_act);
 
-       /* Store action_lists when calls to update_tree are deferred */
-       SnapList<action_list_t *> * action_list_buffer;
-
        /* Set of locations read by this FuncNode */
        loc_set_t * read_locations;
 
index 90951ab..b11614b 100644 (file)
@@ -69,8 +69,7 @@ void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
                resize_func_nodes( func_id + 1 );
 
        FuncNode * func_node = func_nodes[func_id];
-       func_node->init_predicate_tree_position(tid);
-       func_node->init_inst_act_map(tid);
+       func_node->function_entry_handler(tid);
 
        /* Add edges between FuncNodes */
        if (last_entered_func_id != 0) {
@@ -92,26 +91,7 @@ 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->set_predicate_tree_position(tid, NULL);
-               func_node->reset_inst_act_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 twice) so that more information can be gathered to infer nullity predicates.
-                */
-               func_node->incr_exit_count();
-               if (func_node->get_exit_count() >= 2) {
-                       SnapList<action_list_t *> * action_list_buffer = func_node->get_action_list_buffer();
-                       while (action_list_buffer->size() > 0) {
-                               action_list_t * act_list = action_list_buffer->back();
-                               action_list_buffer->pop_back();
-                               func_node->update_tree(act_list);
-                       }
-
-                       func_node->update_tree(curr_act_list);
-               } else
-                       func_node->get_action_list_buffer()->push_front(curr_act_list);
+               func_node->function_exit_handler(tid);
 
                (*thrd_func_list)[id].pop_back();
                func_act_lists->pop_back();
@@ -183,24 +163,17 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid)
        /* Add to curr_inst_list */
        curr_act_list->push_back(act);
 
-       // Increment ref count for every action and reads_froms
-       act->incr_func_ref_count();
-       if (act->is_read()) {
-               ModelAction * rf = act->get_reads_from();
-               rf->incr_func_ref_count();
-       }
-
        FuncNode * func_node = func_nodes[func_id];
        func_node->add_inst(act);
 
        if (act->is_read()) {
                func_node->update_inst_act_map(tid, act);
 
-               Fuzzer * fuzzer = model->get_execution()->getFuzzer();
-               Predicate * selected_branch = ((NewFuzzer *)fuzzer)->get_selected_child_branch(tid);
-               func_node->set_predicate_tree_position(tid, selected_branch);
+//             Fuzzer * fuzzer = model->get_execution()->getFuzzer();
+//             Predicate * selected_branch = ((NewFuzzer *)fuzzer)->get_selected_child_branch(tid);
+//             func_node->set_predicate_tree_position(tid, selected_branch);
        }
-
+/*
        if (act->is_write()) {
                Predicate * curr_pred = func_node->get_predicate_tree_position(tid);
                FuncInst * curr_inst = func_node->get_inst(act);
@@ -211,6 +184,9 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid)
                }
                func_node->set_predicate_tree_position(tid, curr_pred);
        }
+*/
+
+       func_node->update_tree(act);
 }
 
 /* Return the FuncNode given its func_id  */
@@ -582,15 +558,15 @@ void ModelHistory::print_func_node()
                func_node->print_predicate_tree();
 
 /*
-                func_inst_list_mt * entry_insts = func_node->get_entry_insts();
-                model_print("function %s has entry actions\n", func_node->get_func_name());
-
-                mllnode<FuncInst*>* it;
-                for (it = entry_insts->begin();it != NULL;it=it->getNext()) {
-                        FuncInst *inst = it->getVal();
-                        model_print("type: %d, at: %s\n", inst->get_type(), inst->get_position());
-                }
- */
+               func_inst_list_mt * entry_insts = func_node->get_entry_insts();
+               model_print("function %s has entry actions\n", func_node->get_func_name());
+
+               mllnode<FuncInst*>* it;
+               for (it = entry_insts->begin();it != NULL;it=it->getNext()) {
+                       FuncInst *inst = it->getVal();
+                       model_print("type: %d, at: %s\n", inst->get_type(), inst->get_position());
+               }
+*/
        }
 }