Remove the uses of inst_act_maps

diff --git a/classlist.h b/classlist.h
index bebbf39fa0cd7e1770e2033377fa55f500f63be3..ccbbbb1418a9ca785394e41df2480f24f22a923d 100644 (file)
--- a/classlist.h
+++ b/classlist.h
@@ -29,7 +29,6 @@ struct bug_message;
 typedef SnapList<ModelAction *> action_list_t;
 typedef SnapList<uint32_t> func_id_list_t;
 typedef SnapList<FuncInst *> func_inst_list_t;
 typedef SnapList<ModelAction *> action_list_t;
 typedef SnapList<uint32_t> func_id_list_t;
 typedef SnapList<FuncInst *> func_inst_list_t;

-typedef HashTable<FuncInst *, ModelAction *, uintptr_t, 0> inst_act_map_t;

 
 typedef HashSet<Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> PredSet;
 typedef HSIterator<Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> PredSetIter;
 
 typedef HashSet<Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> PredSet;
 typedef HSIterator<Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> PredSetIter;

diff --git a/funcnode.cc b/funcnode.cc
index 5d372f300d8ac31e8db0021f382578dfbf1d8038..92e37955dd97f673fc2bf1abc714cba2731c8f5e 100644 (file)
--- a/funcnode.cc
+++ b/funcnode.cc
@@ -17,9 +17,9 @@ FuncNode::FuncNode(ModelHistory * history) :
        func_inst_map(),
        inst_list(),
        entry_insts(),
        func_inst_map(),
        inst_list(),
        entry_insts(),

-       thrd_inst_pred_map(),
-       thrd_inst_id_map(),
-       thrd_loc_inst_map(),
+       thrd_inst_pred_maps(),
+       thrd_inst_id_maps(),
+       thrd_loc_inst_maps(),

        thrd_predicate_tree_position(),
        thrd_predicate_trace(),
        edge_table(32),
        thrd_predicate_tree_position(),
        thrd_predicate_trace(),
        edge_table(32),


@@ -166,7 +166,6 @@ void FuncNode::add_entry_inst(FuncInst * inst)
 void FuncNode::function_entry_handler(thread_id_t tid)
 {
        init_marker(tid);
 void FuncNode::function_entry_handler(thread_id_t tid)
 {
        init_marker(tid);

-       init_inst_act_map(tid);

        init_local_maps(tid);
        init_predicate_tree_data_structure(tid);
 }
        init_local_maps(tid);
        init_predicate_tree_data_structure(tid);
 }


@@ -174,12 +173,12 @@ void FuncNode::function_entry_handler(thread_id_t tid)
 void FuncNode::function_exit_handler(thread_id_t tid)
 {
        int thread_id = id_to_int(tid);
 void FuncNode::function_exit_handler(thread_id_t tid)
 {
        int thread_id = id_to_int(tid);

-       thrd_recursion_depth[thread_id]--;
-       thrd_markers[thread_id]->pop_back();

 
 

-       reset_inst_act_map(tid);

        reset_local_maps(tid);
 
        reset_local_maps(tid);
 

+       thrd_recursion_depth[thread_id]--;
+       thrd_markers[thread_id]->pop_back();
+

        Predicate * exit_pred = get_predicate_tree_position(tid);
        if (exit_pred->get_exit() == NULL) {
                // Exit predicate is unset yet
        Predicate * exit_pred = get_predicate_tree_position(tid);
        if (exit_pred->get_exit() == NULL) {
                // Exit predicate is unset yet


@@ -286,9 +285,9 @@ void FuncNode::update_predicate_tree(ModelAction * next_act)
        uint32_t this_marker = thrd_markers[thread_id]->back();
        int recursion_depth = thrd_recursion_depth[thread_id];
 
        uint32_t this_marker = thrd_markers[thread_id]->back();
        int recursion_depth = thrd_recursion_depth[thread_id];
 

-       loc_inst_map_t * loc_inst_map = thrd_loc_inst_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];
+       loc_inst_map_t * loc_inst_map = thrd_loc_inst_maps[thread_id]->back();
+       inst_pred_map_t * inst_pred_map = thrd_inst_pred_maps[thread_id]->back();
+       inst_id_map_t * inst_id_map = thrd_inst_id_maps[thread_id]->back();

 
        Predicate * curr_pred = get_predicate_tree_position(tid);
        while (true) {
 
        Predicate * curr_pred = get_predicate_tree_position(tid);
        while (true) {


@@ -404,6 +403,7 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst,
                        case EQUALITY:
                                FuncInst * to_be_compared;
                                to_be_compared = pred_expression->func_inst;
                        case EQUALITY:
                                FuncInst * to_be_compared;
                                to_be_compared = pred_expression->func_inst;

+                               ASSERT(to_be_compared != next_inst);

 
                                last_read = to_be_compared->get_associated_read(tid, recursion_depth, this_marker);
                                ASSERT(last_read != VALUE_NONE);
 
                                last_read = to_be_compared->get_associated_read(tid, recursion_depth, this_marker);
                                ASSERT(last_read != VALUE_NONE);


@@ -446,7 +446,7 @@ void FuncNode::infer_predicates(FuncInst * next_inst, ModelAction * next_act,
 {
        void * loc = next_act->get_location();
        int thread_id = id_to_int(next_act->get_tid());
 {
        void * loc = next_act->get_location();
        int thread_id = id_to_int(next_act->get_tid());

-       loc_inst_map_t * loc_inst_map = thrd_loc_inst_map[thread_id];
+       loc_inst_map_t * loc_inst_map = thrd_loc_inst_maps[thread_id]->back();

 
        if (next_inst->is_read()) {
                /* read + rmw */
 
        if (next_inst->is_read()) {
                /* read + rmw */


@@ -656,50 +656,6 @@ void FuncNode::add_predicate_to_trace(thread_id_t tid, Predicate * pred)
        thrd_predicate_trace[thread_id]->back()->push_back(pred);
 }
 
        thrd_predicate_trace[thread_id]->back()->push_back(pred);
 }
 

-/* Make sure elements of thrd_inst_act_map are initialized properly when threads enter functions */
-void FuncNode::init_inst_act_map(thread_id_t tid)
-{
-       int thread_id = id_to_int(tid);
-       SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
-       uint old_size = thrd_inst_act_map->size();
-
-       if (old_size <= (uint) thread_id) {
-               uint new_size = thread_id + 1;
-               thrd_inst_act_map->resize(new_size);
-
-               for (uint i = old_size;i < new_size;i++)
-                       (*thrd_inst_act_map)[i] = new inst_act_map_t(128);
-       }
-}
-
-/* Reset elements of thrd_inst_act_map when threads exit functions */
-void FuncNode::reset_inst_act_map(thread_id_t tid)
-{
-       int thread_id = id_to_int(tid);
-       SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
-
-       inst_act_map_t * map = (*thrd_inst_act_map)[thread_id];
-       map->reset();
-}
-
-void FuncNode::update_inst_act_map(thread_id_t tid, ModelAction * read_act)
-{
-       int thread_id = id_to_int(tid);
-       SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
-
-       inst_act_map_t * map = (*thrd_inst_act_map)[thread_id];
-       FuncInst * read_inst = get_inst(read_act);
-       map->put(read_inst, read_act);
-}
-
-inst_act_map_t * FuncNode::get_inst_act_map(thread_id_t tid)
-{
-       int thread_id = id_to_int(tid);
-       SnapVector<inst_act_map_t *> * thrd_inst_act_map = history->getThrdInstActMap(func_id);
-
-       return (*thrd_inst_act_map)[thread_id];
-}
-

 void FuncNode::init_marker(thread_id_t tid)
 {
        marker++;
 void FuncNode::init_marker(thread_id_t tid)
 {
        marker++;


@@ -720,34 +676,70 @@ void FuncNode::init_marker(thread_id_t tid)
        thrd_recursion_depth[thread_id]++;
 }
 
        thrd_recursion_depth[thread_id]++;
 }
 

+uint32_t FuncNode::get_marker(thread_id_t tid)
+{
+       int thread_id = id_to_int(tid);
+       return thrd_markers[thread_id]->back();
+}
+
+int FuncNode::get_recursion_depth(thread_id_t tid)
+{
+       return thrd_recursion_depth[id_to_int(tid)];
+}
+

 /* Make sure elements of maps are initialized properly when threads enter functions */
 void FuncNode::init_local_maps(thread_id_t tid)
 {
        int thread_id = id_to_int(tid);
 /* Make sure elements of maps are initialized properly when threads enter functions */
 void FuncNode::init_local_maps(thread_id_t tid)
 {
        int thread_id = id_to_int(tid);

-       int old_size = thrd_loc_inst_map.size();
+       int old_size = thrd_loc_inst_maps.size();

 
        if (old_size < thread_id + 1) {
                int new_size = thread_id + 1;
 
 
        if (old_size < thread_id + 1) {
                int 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_maps.resize(new_size);
+               thrd_inst_id_maps.resize(new_size);
+               thrd_inst_pred_maps.resize(new_size);

 
                for (int i = old_size; i < new_size; i++) {
 
                for (int i = old_size; i < new_size; i++) {

-                       thrd_loc_inst_map[i] = new loc_inst_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);
+                       thrd_loc_inst_maps[i] = new ModelVector<loc_inst_map_t *>;
+                       thrd_inst_id_maps[i] = new ModelVector<inst_id_map_t *>;
+                       thrd_inst_pred_maps[i] = new ModelVector<inst_pred_map_t *>;

                }
        }
                }
        }

+
+       ModelVector<loc_inst_map_t *> * map = thrd_loc_inst_maps[thread_id];
+       int index = thrd_recursion_depth[thread_id];
+
+       // If there are recursive calls, push more hashtables into the vector.
+       if (map->size() < (uint) index + 1) {
+               thrd_loc_inst_maps[thread_id]->push_back(new loc_inst_map_t(64));
+               thrd_inst_id_maps[thread_id]->push_back(new inst_id_map_t(64));
+               thrd_inst_pred_maps[thread_id]->push_back(new inst_pred_map_t(64));
+       }
+
+       ASSERT(map->size() == (uint) index + 1);

 }
 
 /* Reset elements of maps when threads exit functions */
 void FuncNode::reset_local_maps(thread_id_t tid)
 {
        int thread_id = id_to_int(tid);
 }
 
 /* Reset elements of maps when threads exit functions */
 void FuncNode::reset_local_maps(thread_id_t tid)
 {
        int thread_id = id_to_int(tid);

-       thrd_loc_inst_map[thread_id]->reset();
-       thrd_inst_id_map[thread_id]->reset();
-       thrd_inst_pred_map[thread_id]->reset();
+       int index = thrd_recursion_depth[thread_id];
+
+       // When recursive call ends, keep only one hashtable in the vector
+       if (index > 0) {
+               delete thrd_loc_inst_maps[thread_id]->back();
+               delete thrd_inst_id_maps[thread_id]->back();
+               delete thrd_inst_pred_maps[thread_id]->back();
+
+               thrd_loc_inst_maps[thread_id]->pop_back();
+               thrd_inst_id_maps[thread_id]->pop_back();
+               thrd_inst_pred_maps[thread_id]->pop_back();
+       } else {
+               thrd_loc_inst_maps[thread_id]->back()->reset();
+               thrd_inst_id_maps[thread_id]->back()->reset();
+               thrd_inst_pred_maps[thread_id]->back()->reset();
+       }

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

diff --git a/funcnode.h b/funcnode.h
index 133d5522df64810c138d49c2257f373cfe01ff89..8afc04ed037121faba7b64b277ae07c3cb31a453 100644 (file)
--- a/funcnode.h
+++ b/funcnode.h
@@ -56,10 +56,8 @@ public:
 
        void add_predicate_to_trace(thread_id_t tid, Predicate *pred);
 
 
        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);
-       inst_act_map_t * get_inst_act_map(thread_id_t tid);
+       uint32_t get_marker(thread_id_t tid);
+       int get_recursion_depth(thread_id_t tid);

 
        void add_out_edge(FuncNode * other);
        ModelList<FuncNode *> * get_out_edges() { return &out_edges; }
 
        void add_out_edge(FuncNode * other);
        ModelList<FuncNode *> * get_out_edges() { return &out_edges; }


@@ -78,7 +76,7 @@ private:
        uint32_t inst_counter;
        uint32_t marker;
        ModelVector< ModelVector<uint32_t> *> thrd_markers;
        uint32_t inst_counter;
        uint32_t marker;
        ModelVector< ModelVector<uint32_t> *> thrd_markers;

-       ModelVector<int> thrd_recursion_depth;
+       ModelVector<int> thrd_recursion_depth;  // Recursion depth starts from 0 to match with vector indexes.

 
        void init_marker(thread_id_t tid);
 
 
        void init_marker(thread_id_t tid);
 


@@ -94,13 +92,13 @@ private:
        func_inst_list_mt entry_insts;
 
        /* Map a FuncInst to the its predicate when updating predicate trees */
        func_inst_list_mt entry_insts;
 
        /* Map a FuncInst to the its predicate when updating predicate trees */

-       ModelVector<inst_pred_map_t *> thrd_inst_pred_map;
+       ModelVector< ModelVector<inst_pred_map_t *> * > thrd_inst_pred_maps;

 
        /* Number FuncInsts to detect loops when updating predicate trees */
 
        /* Number FuncInsts to detect loops when updating predicate trees */

-       ModelVector<inst_id_map_t *> thrd_inst_id_map;
+       ModelVector< ModelVector<inst_id_map_t *> *> thrd_inst_id_maps;

 
        /* Detect read actions at the same locations when updating predicate trees */
 
        /* Detect read actions at the same locations when updating predicate trees */

-       ModelVector<loc_inst_map_t *> thrd_loc_inst_map;
+       ModelVector< ModelVector<loc_inst_map_t *> *> thrd_loc_inst_maps;

 
        void init_local_maps(thread_id_t tid);
        void reset_local_maps(thread_id_t tid);
 
        void init_local_maps(thread_id_t tid);
        void reset_local_maps(thread_id_t tid);

diff --git a/history.cc b/history.cc
index cb30a7deeb9e047cf27034d5bcdb2d5964aa8ab5..081f85d1e8fd23e724cedae4040a95432d61e7c6 100644 (file)
--- a/history.cc
+++ b/history.cc
@@ -28,7 +28,6 @@ ModelHistory::ModelHistory() :
        thrd_last_entered_func = new SnapVector<uint32_t>();
        thrd_waiting_write = new SnapVector<ConcretePredicate *>();
        thrd_wait_obj = new SnapVector<WaitObj *>();
        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);

 }
 
 ModelHistory::~ModelHistory()
 }
 
 ModelHistory::~ModelHistory()


@@ -149,8 +148,6 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid)
        func_node->add_inst(act);
 
        if (act->is_read()) {
        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);


@@ -402,19 +399,6 @@ void ModelHistory::stop_waiting_for_node(thread_id_t self_id,
        }
 }
 
        }
 }
 

-SnapVector<inst_act_map_t *> * ModelHistory::getThrdInstActMap(uint32_t func_id)
-{
-       ASSERT(func_id != 0);
-
-       SnapVector<inst_act_map_t *> * maps = func_inst_act_maps->get(func_id);
-       if (maps == NULL) {
-               maps = new SnapVector<inst_act_map_t *>();
-               func_inst_act_maps->put(func_id, maps);
-       }
-
-       return maps;
-}
-

 bool ModelHistory::skip_action(ModelAction * act)
 {
        bool second_part_of_rmw = act->is_rmwc() || act->is_rmw();
 bool ModelHistory::skip_action(ModelAction * act)
 {
        bool second_part_of_rmw = act->is_rmwc() || act->is_rmw();

diff --git a/history.h b/history.h
index dbc9f1d19f9a8230285a3cca3caf22580c35ae9a..4670a65fcb5cc4d0995725f5271a7c3367c0506a 100644 (file)
--- a/history.h
+++ b/history.h
@@ -44,8 +44,6 @@ public:
        void remove_waiting_thread(thread_id_t tid);
        void stop_waiting_for_node(thread_id_t self_id, thread_id_t waiting_for_id, FuncNode * target_node);
 
        void remove_waiting_thread(thread_id_t tid);
        void stop_waiting_for_node(thread_id_t self_id, thread_id_t waiting_for_id, FuncNode * target_node);
 

-       SnapVector<inst_act_map_t *> * getThrdInstActMap(uint32_t func_id);
-

        void set_new_exec_flag();
        void dump_func_node_graph();
        void print_func_node();
        void set_new_exec_flag();
        void dump_func_node_graph();
        void print_func_node();


@@ -88,10 +86,6 @@ private:
        SnapVector<ConcretePredicate *> * thrd_waiting_write;
        SnapVector<WaitObj *> * thrd_wait_obj;
 
        SnapVector<ConcretePredicate *> * thrd_waiting_write;
        SnapVector<WaitObj *> * thrd_wait_obj;
 

-       /* A run-time map from FuncInst to ModelAction per thread, per FuncNode.
-        * Manipulated by FuncNode, and needed by NewFuzzer */
-       HashTable<uint32_t, SnapVector<inst_act_map_t *> *, int, 0> * func_inst_act_maps;
-

        bool skip_action(ModelAction * act);
        void monitor_waiting_thread(uint32_t func_id, thread_id_t tid);
        void monitor_waiting_thread_counter(thread_id_t tid);
        bool skip_action(ModelAction * act);
        void monitor_waiting_thread(uint32_t func_id, thread_id_t tid);
        void monitor_waiting_thread_counter(thread_id_t tid);

diff --git a/newfuzzer.cc b/newfuzzer.cc
index 35e16d2ee10b70c839e97ce9b1cea67901793092..ff19354ca3cacb06dfe37f0c0442315933017539 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);


@@ -49,7 +49,9 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
                FuncNode * func_node = history->get_curr_func_node(tid);
                Predicate * curr_pred = func_node->get_predicate_tree_position(tid);
                FuncInst * read_inst = func_node->get_inst(read);
                FuncNode * func_node = history->get_curr_func_node(tid);
                Predicate * curr_pred = func_node->get_predicate_tree_position(tid);
                FuncInst * read_inst = func_node->get_inst(read);

-               inst_act_map_t * inst_act_map = func_node->get_inst_act_map(tid);
+
+               int index = func_node->get_recursion_depth(tid);
+               uint32_t marker = func_node->get_marker(tid);

 
                if (curr_pred != NULL)  {
                        Predicate * selected_branch = NULL;
 
                if (curr_pred != NULL)  {
                        Predicate * selected_branch = NULL;


@@ -72,7 +74,7 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
                                delete it;
                        }
 
                                delete it;
                        }
 

-                       prune_writes(tid, selected_branch, rf_set, inst_act_map);
+                       prune_writes(tid, index, marker, selected_branch, rf_set);

                }
 
                if (!failed_predicates.isEmpty())
                }
 
                if (!failed_predicates.isEmpty())


@@ -87,6 +89,9 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
                Predicate * selected_branch = get_selected_child_branch(tid);
                FuncNode * func_node = history->get_curr_func_node(tid);
 
                Predicate * selected_branch = get_selected_child_branch(tid);
                FuncNode * func_node = history->get_curr_func_node(tid);
 

+               int index = func_node->get_recursion_depth(tid);
+               uint32_t marker = func_node->get_marker(tid);
+

                // Add failed predicate to NewFuzzer and FuncNode
                failed_predicates.put(selected_branch, true);
                selected_branch->incr_fail_count();
                // Add failed predicate to NewFuzzer and FuncNode
                failed_predicates.put(selected_branch, true);
                selected_branch->incr_fail_count();


@@ -103,8 +108,7 @@ int NewFuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set
                FuncInst * read_inst = thrd_last_func_inst[thread_id];
                selected_branch = selectBranch(tid, curr_pred, read_inst);
 
                FuncInst * read_inst = thrd_last_func_inst[thread_id];
                selected_branch = selectBranch(tid, curr_pred, read_inst);
 

-               inst_act_map_t * inst_act_map = func_node->get_inst_act_map(tid);
-               prune_writes(tid, selected_branch, rf_set, inst_act_map);
+               prune_writes(tid, index, marker, selected_branch, rf_set);

 
                ASSERT(selected_branch);
        }
 
                ASSERT(selected_branch);
        }


@@ -165,15 +169,15 @@ Predicate * NewFuzzer::selectBranch(thread_id_t tid, Predicate * curr_pred, Func
        }
 
        int index = choose_branch_index(&available_branches_tmp_storage);
        }
 
        int index = choose_branch_index(&available_branches_tmp_storage);

-       Predicate * random_branch = available_branches_tmp_storage[ index ];
-       thrd_selected_child_branch[thread_id] = random_branch;
+       Predicate * selected_branch = available_branches_tmp_storage[ index ];
+       thrd_selected_child_branch[thread_id] = selected_branch;

 
        /* Remove the chosen branch from vec in case that this
         * branch fails and need to choose another one */
        available_branches_tmp_storage[index] = available_branches_tmp_storage.back();
        available_branches_tmp_storage.pop_back();
 
 
        /* Remove the chosen branch from vec in case that this
         * branch fails and need to choose another one */
        available_branches_tmp_storage[index] = available_branches_tmp_storage.back();
        available_branches_tmp_storage.pop_back();
 

-       return random_branch;
+       return selected_branch;

 }
 
 /**
 }
 
 /**


@@ -223,8 +227,8 @@ Predicate * NewFuzzer::get_selected_child_branch(thread_id_t tid)
  *
  * @return true if rf_set is pruned
  */
  *
  * @return true if rf_set is pruned
  */

-bool NewFuzzer::prune_writes(thread_id_t tid, Predicate * pred,
-                                                                                                                SnapVector<ModelAction *> * rf_set, inst_act_map_t * inst_act_map)
+bool NewFuzzer::prune_writes(thread_id_t tid, int index, uint32_t marker, 
+                       Predicate * pred, SnapVector<ModelAction *> * rf_set)

 {
        if (pred == NULL)
                return false;
 {
        if (pred == NULL)
                return false;


@@ -245,25 +249,25 @@ bool NewFuzzer::prune_writes(thread_id_t tid, Predicate * pred,
        pruned_writes->clear(); // clear the old pruned_writes set
 
        bool pruned = false;
        pruned_writes->clear(); // clear the old pruned_writes set
 
        bool pruned = false;

-       uint index = 0;
+       uint rf_index = 0;

 
 

-       while ( index < rf_set->size() ) {
-               ModelAction * write_act = (*rf_set)[index];
+       while ( rf_index < rf_set->size() ) {
+               ModelAction * write_act = (*rf_set)[rf_index];

                uint64_t write_val = write_act->get_write_value();
                bool no_predicate = false;
                uint64_t write_val = write_act->get_write_value();
                bool no_predicate = false;

-               bool satisfy_predicate = check_predicate_expressions(pred_expressions, inst_act_map, write_val, &no_predicate);
+               bool satisfy_predicate = check_predicate_expressions(tid, index, marker, pred_expressions, write_val, &no_predicate);

 
                if (no_predicate)
                        return false;
 
                if (!satisfy_predicate) {
                        ASSERT(rf_set != NULL);
 
                if (no_predicate)
                        return false;
 
                if (!satisfy_predicate) {
                        ASSERT(rf_set != NULL);

-                       (*rf_set)[index] = rf_set->back();
+                       (*rf_set)[rf_index] = rf_set->back();

                        rf_set->pop_back();
                        pruned_writes->push_back(write_act);
                        pruned = true;
                } else
                        rf_set->pop_back();
                        pruned_writes->push_back(write_act);
                        pruned = true;
                } else

-                       index++;
+                       rf_index++;

        }
 
        return pruned;
        }
 
        return pruned;


@@ -275,24 +279,28 @@ bool NewFuzzer::prune_writes(thread_id_t tid, Predicate * pred,
  */
 void NewFuzzer::conditional_sleep(Thread * thread)
 {
  */
 void NewFuzzer::conditional_sleep(Thread * thread)
 {

+/*

        int index = paused_thread_list.size();
 
        model->getScheduler()->add_sleep(thread);
        paused_thread_list.push_back(thread);
        paused_thread_table.put(thread, index); // Update table
 
        int index = paused_thread_list.size();
 
        model->getScheduler()->add_sleep(thread);
        paused_thread_list.push_back(thread);
        paused_thread_table.put(thread, index); // Update table
 

-       /* Add the waiting condition to ModelHistory */
+       // Add the waiting condition to ModelHistory

        ModelAction * read = thread->get_pending();
        thread_id_t tid = thread->get_id();
        FuncNode * func_node = history->get_curr_func_node(tid);
        ModelAction * read = thread->get_pending();
        thread_id_t tid = thread->get_id();
        FuncNode * func_node = history->get_curr_func_node(tid);

-       inst_act_map_t * inst_act_map = func_node->get_inst_act_map(tid);
+//     inst_act_map_t * inst_act_map = func_node->get_inst_act_map(tid);

 
        Predicate * selected_branch = get_selected_child_branch(tid);
 
        Predicate * selected_branch = get_selected_child_branch(tid);

-       ConcretePredicate * concrete = selected_branch->evaluate(inst_act_map, tid);
+//     ConcretePredicate * concrete = selected_branch->evaluate(inst_act_map, tid);

        concrete->set_location(read->get_location());
 
        concrete->set_location(read->get_location());
 

-       history->add_waiting_write(concrete);
-       /* history->add_waiting_thread is already called in find_threads */
+       ASSERT(false);
+
+//     history->add_waiting_write(concrete);
+       // history->add_waiting_thread is already called in find_threads
+*/

 }
 
 bool NewFuzzer::has_paused_threads()
 }
 
 bool NewFuzzer::has_paused_threads()


@@ -408,8 +416,8 @@ bool NewFuzzer::find_threads(ModelAction * pending_read)
        return finds_waiting_for;
 }
 
        return finds_waiting_for;
 }
 

-bool NewFuzzer::check_predicate_expressions(PredExprSet * pred_expressions,
-                                                                                                                                                                               inst_act_map_t * inst_act_map, uint64_t write_val, bool * no_predicate)
+bool NewFuzzer::check_predicate_expressions(thread_id_t tid, int index, uint32_t marker, 
+                       PredExprSet * pred_expressions, uint64_t write_val, bool * no_predicate)

 {
        bool satisfy_predicate = true;
 
 {
        bool satisfy_predicate = true;
 


@@ -424,12 +432,11 @@ bool NewFuzzer::check_predicate_expressions(PredExprSet * pred_expressions,
                        break;
                case EQUALITY:
                        FuncInst * to_be_compared;
                        break;
                case EQUALITY:
                        FuncInst * to_be_compared;

-                       ModelAction * last_act;

                        uint64_t last_read;
 
                        to_be_compared = expression->func_inst;
                        uint64_t last_read;
 
                        to_be_compared = expression->func_inst;

-                       last_act = inst_act_map->get(to_be_compared);
-                       last_read = last_act->get_reads_from_value();
+                       last_read = to_be_compared->get_associated_read(tid, index, marker);
+                       ASSERT(last_read != VALUE_NONE);

 
                        equality = (write_val == last_read);
                        if (equality != expression->value)
 
                        equality = (write_val == last_read);
                        if (equality != expression->value)

diff --git a/newfuzzer.h b/newfuzzer.h
index 129364c10126df36d1cafb06de4e616b3790868f..c8a3f036fc12d3f978ce5ffe7f2cd58f92f4379e 100644 (file)
--- a/newfuzzer.h
+++ b/newfuzzer.h
@@ -51,7 +51,7 @@ private:
 
        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 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);
+       bool prune_writes(thread_id_t tid, int index, uint32_t marker, Predicate * pred, SnapVector<ModelAction *> * rf_set);

        int choose_branch_index(SnapVector<Predicate *> * branches);
 
        /* The set of Threads put to sleep by NewFuzzer because no writes in rf_set satisfies the selected predicate. Only used by selectWrite.
        int choose_branch_index(SnapVector<Predicate *> * branches);
 
        /* The set of Threads put to sleep by NewFuzzer because no writes in rf_set satisfies the selected predicate. Only used by selectWrite.


@@ -67,7 +67,7 @@ private:
 
        bool find_threads(ModelAction * pending_read);  //--
 
 
        bool find_threads(ModelAction * pending_read);  //--
 

-       bool check_predicate_expressions(PredExprSet * pred_expressions, inst_act_map_t * inst_act_map, uint64_t write_val, bool * no_predicate);
+       bool check_predicate_expressions(thread_id_t tid, int index, uint32_t marker, PredExprSet * pred_expressions, uint64_t write_val, bool * no_predicate);

 };
 
 #endif /* end of __NEWFUZZER_H__ */
 };
 
 #endif /* end of __NEWFUZZER_H__ */

diff --git a/predicate.cc b/predicate.cc
index 44f5e8d1844f55ec8e860a5118a6c780b5914d07..86bc30edf76651a813e09672f815f5c03d3946c2 100644 (file)
--- a/predicate.cc
+++ b/predicate.cc
@@ -100,8 +100,9 @@ Predicate * Predicate::follow_write_child(FuncInst * inst)
 }
 
 /* Evaluate predicate expressions against the given inst_act_map */
 }
 
 /* Evaluate predicate expressions against the given inst_act_map */

-ConcretePredicate * Predicate::evaluate(inst_act_map_t * inst_act_map, thread_id_t tid)
+ConcretePredicate * Predicate::evaluate(thread_id_t tid)

 {
 {

+       /*

        ConcretePredicate * concrete = new ConcretePredicate(tid);
        PredExprSetIter * it = pred_expressions.iterator();
 
        ConcretePredicate * concrete = new ConcretePredicate(tid);
        PredExprSetIter * it = pred_expressions.iterator();
 


@@ -130,6 +131,7 @@ ConcretePredicate * Predicate::evaluate(inst_act_map_t * inst_act_map, thread_id
        }
 
        delete it;
        }
 
        delete it;

+       */

        return concrete;
 }
 
        return concrete;
 }
 

diff --git a/predicate.h b/predicate.h
index df46ca1052551dc04b0423e5d3a394261c669f1c..cc9f714d567208a743876a894fe276bff1aa1b60 100644 (file)
--- a/predicate.h
+++ b/predicate.h
@@ -42,7 +42,7 @@ public:
        bool is_write() { return does_write; }
        void set_write(bool is_write) { does_write = is_write; }
 
        bool is_write() { return does_write; }
        void set_write(bool is_write) { does_write = is_write; }
 

-       ConcretePredicate * evaluate(inst_act_map_t * inst_act_map, thread_id_t tid);
+       ConcretePredicate * evaluate(thread_id_t tid);

 
        uint32_t get_expl_count() { return exploration_count; }
        uint32_t get_fail_count() { return failure_count; }
 
        uint32_t get_expl_count() { return exploration_count; }
        uint32_t get_fail_count() { return failure_count; }