Handle predicate weight updates

diff --git a/funcnode.cc b/funcnode.cc
index 896c60ebb4b8049f6d366fa20e615d55863a6354..c01173ae747334bff1a913e897da88d5e7243a4b 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -20,10 +20,10 @@ FuncNode::FuncNode(ModelHistory * history) :
        thrd_inst_pred_map(),
        thrd_inst_id_map(),
        thrd_loc_inst_map(),
        thrd_inst_pred_map(),
        thrd_inst_id_map(),
        thrd_loc_inst_map(),

-       predicate_tree_position(),
+       thrd_predicate_tree_position(),
+       thrd_predicate_trace(),

        predicate_leaves(),
        leaves_tmp_storage(),
        predicate_leaves(),
        leaves_tmp_storage(),

-       weight_debug_vec(),

        failed_predicates(),
        edge_table(32),
        out_edges()
        failed_predicates(),
        edge_table(32),
        out_edges()


@@ -169,9 +169,9 @@ void FuncNode::add_entry_inst(FuncInst * inst)
 void FuncNode::function_entry_handler(thread_id_t tid)
 {
        set_marker(tid);
 void FuncNode::function_entry_handler(thread_id_t tid)
 {
        set_marker(tid);

-       init_predicate_tree_position(tid);

        init_inst_act_map(tid);
        init_inst_act_map(tid);

-       init_maps(tid);
+       init_local_maps(tid);
+       init_predicate_tree_data_structure(tid);

 }
 
 void FuncNode::function_exit_handler(thread_id_t tid)
 }
 
 void FuncNode::function_exit_handler(thread_id_t tid)


@@ -179,7 +179,7 @@ void FuncNode::function_exit_handler(thread_id_t tid)
        exit_count++;
 
        reset_inst_act_map(tid);
        exit_count++;
 
        reset_inst_act_map(tid);

-       reset_maps(tid);
+       reset_local_maps(tid);

 
        Predicate * exit_pred = get_predicate_tree_position(tid);
        if (exit_pred->get_exit() == NULL) {
 
        Predicate * exit_pred = get_predicate_tree_position(tid);
        if (exit_pred->get_exit() == NULL) {


@@ -187,8 +187,8 @@ void FuncNode::function_exit_handler(thread_id_t tid)
                exit_pred->set_exit(predicate_tree_exit);
        }
 
                exit_pred->set_exit(predicate_tree_exit);
        }
 

-       int thread_id = id_to_int(tid);
-       predicate_tree_position[thread_id]->pop_back();
+       update_predicate_tree_weight(tid);
+       reset_predicate_tree_data_structure(tid);

 }
 
 /**
 }
 
 /**


@@ -290,9 +290,6 @@ void FuncNode::update_predicate_tree(ModelAction * next_act)
        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];
 
        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();
-

        Predicate * curr_pred = get_predicate_tree_position(tid);
        while (true) {
                FuncInst * next_inst = get_inst(next_act);
        Predicate * curr_pred = get_predicate_tree_position(tid);
        while (true) {
                FuncInst * next_inst = get_inst(next_act);


@@ -322,9 +319,6 @@ void FuncNode::update_predicate_tree(ModelAction * next_act)
                                Predicate * old_pred = inst_pred_map->get(next_inst);
                                Predicate * back_pred = old_pred->get_parent();
 
                                Predicate * old_pred = inst_pred_map->get(next_inst);
                                Predicate * back_pred = old_pred->get_parent();
 

-                               // For updating weights
-                               leaves_tmp_storage.push_back(curr_pred);
-

                                // Add to the set of backedges
                                curr_pred->add_backedge(back_pred);
                                curr_pred = back_pred;
                                // Add to the set of backedges
                                curr_pred->add_backedge(back_pred);
                                curr_pred = back_pred;


@@ -356,11 +350,11 @@ void FuncNode::update_predicate_tree(ModelAction * next_act)
                        inst_id_map->put(next_inst, inst_counter++);
 
                curr_pred->incr_expl_count();
                        inst_id_map->put(next_inst, inst_counter++);
 
                curr_pred->incr_expl_count();

+               add_predicate_to_trace(tid, curr_pred);

                break;
        }
 
 //     leaves_tmp_storage.push_back(curr_pred);
                break;
        }
 
 //     leaves_tmp_storage.push_back(curr_pred);

-//     update_predicate_tree_weight();

 }
 
 /* Given curr_pred and next_inst, find the branch following curr_pred that
 }
 
 /* Given curr_pred and next_inst, find the branch following curr_pred that


@@ -652,25 +646,10 @@ void FuncNode::update_loc_may_equal_map(void * new_loc, loc_set_t * old_location
        delete loc_it;
 }
 
        delete loc_it;
 }
 

-void FuncNode::init_predicate_tree_position(thread_id_t tid)
-{
-       int thread_id = id_to_int(tid);
-       int old_size = predicate_tree_position.size();
-
-       if (old_size <= thread_id + 1) {
-               predicate_tree_position.resize(thread_id + 1);
-
-               for (int i = old_size; i < thread_id + 1; i++)
-                       predicate_tree_position[i] = new ModelVector<Predicate *>();
-       }
-
-       predicate_tree_position[thread_id]->push_back(predicate_tree_entry);
-}
-

 void FuncNode::set_predicate_tree_position(thread_id_t tid, Predicate * pred)
 {
        int thread_id = id_to_int(tid);
 void FuncNode::set_predicate_tree_position(thread_id_t tid, Predicate * pred)
 {
        int thread_id = id_to_int(tid);

-       ModelVector<Predicate *> * stack = predicate_tree_position[thread_id];
+       ModelVector<Predicate *> * stack = thrd_predicate_tree_position[thread_id];

        (*stack)[stack->size() - 1] = pred;
 }
 
        (*stack)[stack->size() - 1] = pred;
 }
 


@@ -678,7 +657,13 @@ void FuncNode::set_predicate_tree_position(thread_id_t tid, Predicate * pred)
 Predicate * FuncNode::get_predicate_tree_position(thread_id_t tid)
 {
        int thread_id = id_to_int(tid);
 Predicate * FuncNode::get_predicate_tree_position(thread_id_t tid)
 {
        int thread_id = id_to_int(tid);

-       return predicate_tree_position[thread_id]->back();
+       return thrd_predicate_tree_position[thread_id]->back();
+}
+
+void FuncNode::add_predicate_to_trace(thread_id_t tid, Predicate * pred)
+{
+       int thread_id = id_to_int(tid);
+       thrd_predicate_trace[thread_id]->back()->push_back(pred);

 }
 
 /* Make sure elements of thrd_inst_act_map are initialized properly when threads enter functions */
 }
 
 /* Make sure elements of thrd_inst_act_map are initialized properly when threads enter functions */


@@ -737,13 +722,14 @@ void FuncNode::set_marker(thread_id_t tid)
 }
 
 /* Make sure elements of maps are initialized properly when threads enter functions */
 }
 
 /* Make sure elements of maps are initialized properly when threads enter functions */

-void FuncNode::init_maps(thread_id_t tid)
+void FuncNode::init_local_maps(thread_id_t tid)

 {
        int thread_id = id_to_int(tid);
        uint old_size = thrd_loc_inst_map.size();
 
        if (old_size <= (uint) thread_id) {
                uint new_size = thread_id + 1;
 {
        int thread_id = id_to_int(tid);
        uint old_size = thrd_loc_inst_map.size();
 
        if (old_size <= (uint) thread_id) {
                uint new_size = thread_id + 1;

+

                thrd_loc_inst_map.resize(new_size);
                thrd_inst_id_map.resize(new_size);
                thrd_inst_pred_map.resize(new_size);
                thrd_loc_inst_map.resize(new_size);
                thrd_inst_id_map.resize(new_size);
                thrd_inst_pred_map.resize(new_size);


@@ -757,7 +743,7 @@ void FuncNode::init_maps(thread_id_t tid)
 }
 
 /* Reset elements of maps when threads exit functions */
 }
 
 /* Reset elements of maps when threads exit functions */

-void FuncNode::reset_maps(thread_id_t tid)
+void FuncNode::reset_local_maps(thread_id_t tid)

 {
        int thread_id = id_to_int(tid);
        thrd_loc_inst_map[thread_id]->reset();
 {
        int thread_id = id_to_int(tid);
        thrd_loc_inst_map[thread_id]->reset();


@@ -765,6 +751,35 @@ void FuncNode::reset_maps(thread_id_t tid)
        thrd_inst_pred_map[thread_id]->reset();
 }
 
        thrd_inst_pred_map[thread_id]->reset();
 }
 

+void FuncNode::init_predicate_tree_data_structure(thread_id_t tid)
+{
+       int thread_id = id_to_int(tid);
+       int old_size = thrd_predicate_tree_position.size();
+
+       if (old_size <= thread_id + 1) {
+               thrd_predicate_tree_position.resize(thread_id + 1);
+               thrd_predicate_trace.resize(thread_id + 1);
+
+               for (int i = old_size; i < thread_id + 1; i++) {
+                       thrd_predicate_tree_position[i] = new ModelVector<Predicate *>();
+                       thrd_predicate_trace[i] = new ModelVector<predicate_trace_t *>();
+               }
+       }
+
+       thrd_predicate_tree_position[thread_id]->push_back(predicate_tree_entry);
+       thrd_predicate_trace[thread_id]->push_back(new predicate_trace_t());
+}
+
+void FuncNode::reset_predicate_tree_data_structure(thread_id_t tid)
+{
+       int thread_id = id_to_int(tid);
+       thrd_predicate_tree_position[thread_id]->pop_back();
+
+       predicate_trace_t * trace = thrd_predicate_trace[thread_id]->back();
+       delete trace;
+       thrd_predicate_trace[thread_id]->pop_back();
+}
+

 /* Add FuncNodes that this node may follow */
 void FuncNode::add_out_edge(FuncNode * other)
 {
 /* Add FuncNodes that this node may follow */
 void FuncNode::add_out_edge(FuncNode * other)
 {


@@ -866,130 +881,33 @@ static void quickSort(ModelVector<_Tp *> * arr, int low, int high)
        }
 }
 
        }
 }
 

-void FuncNode::assign_initial_weight()
-{
-       PredSetIter * it = predicate_leaves.iterator();
-       leaves_tmp_storage.clear();
-
-       while (it->hasNext()) {
-               Predicate * pred = it->next();
-               double weight = 100.0 / sqrt(pred->get_expl_count() + pred->get_fail_count() + 1);
-               pred->set_weight(weight);
-               leaves_tmp_storage.push_back(pred);
-       }
-       delete it;
-
-       quickSort(&leaves_tmp_storage, 0, leaves_tmp_storage.size() - 1);
-
-       // assign scores for internal nodes;
-       while ( !leaves_tmp_storage.empty() ) {
-               Predicate * leaf = leaves_tmp_storage.back();
-               leaves_tmp_storage.pop_back();
-
-               Predicate * curr = leaf->get_parent();
-               while (curr != NULL) {
-                       if (curr->get_weight() != 0) {
-                               // Has been exlpored
-                               break;
-                       }
-
-                       ModelVector<Predicate *> * children = curr->get_children();
-                       double weight_sum = 0;
-                       bool has_unassigned_node = false;
-
-                       for (uint i = 0;i < children->size();i++) {
-                               Predicate * child = (*children)[i];
-
-                               // If a child has unassigned weight
-                               double weight = child->get_weight();
-                               if (weight == 0) {
-                                       has_unassigned_node = true;
-                                       break;
-                               } else
-                                       weight_sum += weight;
-                       }
-
-                       if (!has_unassigned_node) {
-                               double average_weight = (double) weight_sum / (double) children->size();
-                               double weight = average_weight * pow(0.9, curr->get_depth());
-                               curr->set_weight(weight);
-                       } else
-                               break;
-
-                       curr = curr->get_parent();
-               }
-       }
-}
-
-void FuncNode::update_predicate_tree_weight()
+void FuncNode::update_predicate_tree_weight(thread_id_t tid)

 {
 {

-       if (marker == 2) {
-               // Predicate tree is initially built
-               assign_initial_weight();
-               return;
-       }
-
-       weight_debug_vec.clear();
-
-       PredSetIter * it = failed_predicates.iterator();
-       while (it->hasNext()) {
-               Predicate * pred = it->next();
-               leaves_tmp_storage.push_back(pred);
-       }
-       delete it;

        failed_predicates.reset();
 
        failed_predicates.reset();
 

-       quickSort(&leaves_tmp_storage, 0, leaves_tmp_storage.size() - 1);
-       for (uint i = 0;i < leaves_tmp_storage.size();i++) {
-               Predicate * pred = leaves_tmp_storage[i];
-               double weight = 100.0 / sqrt(pred->get_expl_count() + pred->get_fail_count() + 1);
-               pred->set_weight(weight);
-       }
-
-       // Update weights in internal nodes
-       while ( !leaves_tmp_storage.empty() ) {
-               Predicate * leaf = leaves_tmp_storage.back();
-               leaves_tmp_storage.pop_back();
+       predicate_trace_t * trace = thrd_predicate_trace[id_to_int(tid)]->back();

 
 

-               Predicate * curr = leaf->get_parent();
-               while (curr != NULL) {
-                       ModelVector<Predicate *> * children = curr->get_children();
-                       double weight_sum = 0;
-                       bool has_unassigned_node = false;
+       // Update predicate weights based on prediate trace
+       for (mllnode<Predicate *> * rit = trace->end(); rit != NULL; rit = rit->getPrev()) {
+               Predicate * node = rit->getVal();

 
 

+               if (predicate_leaves.contains(node)) {
+                       double weight = 100.0 / sqrt(node->get_expl_count() + node->get_fail_count() + 1);
+                       node->set_weight(weight);
+               } else {
+                       double weight_sum = 0.0;
+                       ModelVector<Predicate *> * children = node->get_children();

                        for (uint i = 0;i < children->size();i++) {
                                Predicate * child = (*children)[i];
                        for (uint i = 0;i < children->size();i++) {
                                Predicate * child = (*children)[i];

-

                                double weight = child->get_weight();
                                double weight = child->get_weight();

-                               if (weight != 0)
-                                       weight_sum += weight;
-                               else if ( predicate_leaves.contains(child) ) {
-                                       // If this child is a leaf
-                                       double weight = 100.0 / sqrt(child->get_expl_count() + 1);
-                                       child->set_weight(weight);
-                                       weight_sum += weight;
-                               } else {
-                                       has_unassigned_node = true;
-                                       weight_debug_vec.push_back(child);      // For debugging purpose
-                                       break;
-                               }
+                               weight_sum += weight;

                        }
 
                        }
 

-                       if (!has_unassigned_node) {
-                               double average_weight = (double) weight_sum / (double) children->size();
-                               double weight = average_weight * pow(0.9, curr->get_depth());
-                               curr->set_weight(weight);
-                       } else
-                               break;
-
-                       curr = curr->get_parent();
+                       double average_weight = (double) weight_sum / (double) children->size();
+                       double weight = average_weight * pow(0.9, node->get_depth());
+                       node->set_weight(weight);

                }
        }
                }
        }

-
-       for (uint i = 0;i < weight_debug_vec.size();i++) {
-               Predicate * tmp = weight_debug_vec[i];
-               ASSERT( tmp->get_weight() != 0 );
-       }

 }
 
 void FuncNode::print_predicate_tree()
 }
 
 void FuncNode::print_predicate_tree()

diff --git a/funcnode.h b/funcnode.h
index ed2213a73382e40d0e799aea9c976da3863613a2..d8b0bc1a0a6342421dce0c17f1859175495dc158 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -13,6 +13,8 @@ typedef HashTable<void *, FuncInst *, uintptr_t, 0, model_malloc, model_calloc,
 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 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 ModelList<Predicate *> predicate_trace_t;
+

 typedef enum edge_type {
        IN_EDGE, OUT_EDGE, BI_EDGE
 } edge_type_t;
 typedef enum edge_type {
        IN_EDGE, OUT_EDGE, BI_EDGE
 } edge_type_t;


@@ -51,10 +53,11 @@ 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 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 set_predicate_tree_position(thread_id_t tid, Predicate * pred);
        Predicate * get_predicate_tree_position(thread_id_t tid);
 
        void set_predicate_tree_position(thread_id_t tid, Predicate * pred);
        Predicate * get_predicate_tree_position(thread_id_t tid);
 

+       void add_predicate_to_trace(thread_id_t tid, Predicate *pred);
+

        void init_inst_act_map(thread_id_t tid);
        void reset_inst_act_map(thread_id_t tid);
        void update_inst_act_map(thread_id_t tid, ModelAction * read_act);
        void init_inst_act_map(thread_id_t tid);
        void reset_inst_act_map(thread_id_t tid);
        void update_inst_act_map(thread_id_t tid, ModelAction * read_act);


@@ -103,8 +106,8 @@ private:
        /* Delect read actions at the same locations when updating predicate trees */
        ModelVector<loc_inst_map_t *> thrd_loc_inst_map;
 
        /* Delect read actions at the same locations when updating predicate trees */
        ModelVector<loc_inst_map_t *> thrd_loc_inst_map;
 

-       void init_maps(thread_id_t tid);
-       void reset_maps(thread_id_t tid);
+       void init_local_maps(thread_id_t tid);
+       void reset_local_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);
 
        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);


@@ -126,11 +129,15 @@ private:
 
        /* Run-time position in the predicate tree for each thread
         * The inner vector is used to deal with recursive functions. */
 
        /* Run-time position in the predicate tree for each thread
         * The inner vector is used to deal with recursive functions. */

-       ModelVector< ModelVector<Predicate *> * > predicate_tree_position;
+       ModelVector< ModelVector<Predicate *> * > thrd_predicate_tree_position;
+
+       ModelVector< ModelVector<predicate_trace_t *> * > thrd_predicate_trace;
+
+       void init_predicate_tree_data_structure(thread_id_t tid);
+       void reset_predicate_tree_data_structure(thread_id_t tid);

 
        PredSet predicate_leaves;
        ModelVector<Predicate *> leaves_tmp_storage;
 
        PredSet predicate_leaves;
        ModelVector<Predicate *> leaves_tmp_storage;

-       ModelVector<Predicate *> weight_debug_vec;

        PredSet failed_predicates;
 
        /* Store the relation between this FuncNode and other FuncNodes */
        PredSet failed_predicates;
 
        /* Store the relation between this FuncNode and other FuncNodes */


@@ -139,8 +146,7 @@ private:
        /* FuncNodes that follow this node */
        ModelList<FuncNode *> out_edges;
 
        /* FuncNodes that follow this node */
        ModelList<FuncNode *> out_edges;
 

-       void assign_initial_weight();
-       void update_predicate_tree_weight();
+       void update_predicate_tree_weight(thread_id_t tid);

 };
 
 #endif /* __FUNCNODE_H__ */
 };
 
 #endif /* __FUNCNODE_H__ */

diff --git a/newfuzzer.cc b/newfuzzer.cc
index 027b7d4fec9c13858ada1dcc96882396eb62e98e..299156b8fa8cbeb77ccc1dfecaf608d031fdf660 100644 (file)
--- a/newfuzzer.cc
+++ b/newfuzzer.cc
@@ -34,7 +34,7 @@ void NewFuzzer::register_engine(ModelChecker *_model, ModelExecution *execution)
 
 int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set)
 {
 
 int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set)
 {

-//     return random() % rf_set->size();
+       return random() % rf_set->size();

 
        thread_id_t tid = read->get_tid();
        int thread_id = id_to_int(tid);
 
        thread_id_t tid = read->get_tid();
        int thread_id = id_to_int(tid);


@@ -54,7 +54,7 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
                if (curr_pred != NULL)  {
                        Predicate * selected_branch = NULL;
 
                if (curr_pred != NULL)  {
                        Predicate * selected_branch = NULL;
 

-                       if (check_branch_inst(curr_pred, read_inst, inst_act_map, rf_set))
+                       if (check_branch_inst(curr_pred, read_inst, rf_set))

                                selected_branch = selectBranch(tid, curr_pred, read_inst);
                        else {
                                // no child of curr_pred matches read_inst, check back edges
                                selected_branch = selectBranch(tid, curr_pred, read_inst);
                        else {
                                // no child of curr_pred matches read_inst, check back edges


@@ -63,7 +63,7 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
 
                                while (it->hasNext()) {
                                        curr_pred = it->next();
 
                                while (it->hasNext()) {
                                        curr_pred = it->next();

-                                       if (check_branch_inst(curr_pred, read_inst, inst_act_map, rf_set)) {
+                                       if (check_branch_inst(curr_pred, read_inst, rf_set)) {

                                                selected_branch = selectBranch(tid, curr_pred, read_inst);
                                                break;
                                        }
                                                selected_branch = selectBranch(tid, curr_pred, read_inst);
                                                break;
                                        }


@@ -119,7 +119,7 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
  * @return False if no child matches read_inst
  */
 bool NewFuzzer::check_branch_inst(Predicate * curr_pred, FuncInst * read_inst,
  * @return False if no child matches read_inst
  */
 bool NewFuzzer::check_branch_inst(Predicate * curr_pred, FuncInst * read_inst,

-                                                                                                                                       inst_act_map_t * inst_act_map, SnapVector<ModelAction *> * rf_set)
+                                                                                                                                       SnapVector<ModelAction *> * rf_set)

 {
        available_branches_tmp_storage.clear();
 
 {
        available_branches_tmp_storage.clear();
 

diff --git a/newfuzzer.h b/newfuzzer.h
index 02c3fc0102d5e4b359fa43acb4b3737f85010078..129364c10126df36d1cafb06de4e616b3790868f 100644 (file)
--- a/newfuzzer.h
+++ b/newfuzzer.h
@@ -49,7 +49,7 @@ private:
        SnapVector<Predicate *> thrd_selected_child_branch;
        SnapVector< SnapVector<ModelAction *> *> thrd_pruned_writes;
 
        SnapVector<Predicate *> thrd_selected_child_branch;
        SnapVector< SnapVector<ModelAction *> *> thrd_pruned_writes;
 

-       bool check_branch_inst(Predicate * curr_pred, FuncInst * read_inst, inst_act_map_t * inst_act_map, SnapVector<ModelAction *> * rf_set);
+       bool check_branch_inst(Predicate * curr_pred, FuncInst * read_inst, SnapVector<ModelAction *> * rf_set);

        Predicate * selectBranch(thread_id_t tid, Predicate * curr_pred, FuncInst * read_inst);
        bool prune_writes(thread_id_t tid, Predicate * pred, SnapVector<ModelAction *> * rf_set, inst_act_map_t * inst_act_map);
        int choose_branch_index(SnapVector<Predicate *> * branches);
        Predicate * selectBranch(thread_id_t tid, Predicate * curr_pred, FuncInst * read_inst);
        bool prune_writes(thread_id_t tid, Predicate * pred, SnapVector<ModelAction *> * rf_set, inst_act_map_t * inst_act_map);
        int choose_branch_index(SnapVector<Predicate *> * branches);