From 18b7aceed37f1a27c766bc85abab2ac60c4bfed5 Mon Sep 17 00:00:00 2001 From: weiyu Date: Mon, 26 Aug 2019 15:27:48 -0700 Subject: [PATCH] add a data structrue to keep track of the run-time position in the predicate tree for each thread --- funcinst.h | 2 +- funcnode.cc | 44 +++++++++++++++++++++++++++++++------------- funcnode.h | 17 ++++++++++++----- history.cc | 8 ++++++-- 4 files changed, 50 insertions(+), 21 deletions(-) diff --git a/funcinst.h b/funcinst.h index 9aec00f6..95d92ff3 100644 --- a/funcinst.h +++ b/funcinst.h @@ -17,7 +17,7 @@ public: void * get_location() const { return location; } void set_location(void * loc) { location = loc; } - void reset_location() { location = NULL; } + void unset_location() { location = NULL; } action_type get_type() const { return type; } memory_order get_mo() const { return order; } diff --git a/funcnode.cc b/funcnode.cc index 6402a9ae..f4c6c986 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -8,19 +8,20 @@ FuncNode::FuncNode(ModelHistory * history) : inst_list(), entry_insts(), // thrd_read_map(), - action_list_buffer() + action_list_buffer(), + predicate_tree_position() { predicate_tree_entry = new Predicate(NULL, true); predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true); - // memory will be reclaimed after each execution + // memories that are reclaimed after each execution read_locations = new loc_set_t(); val_loc_map = new HashTable(); loc_may_equal_map = new HashTable(); - values_may_read_from = new value_set_t(); + //values_may_read_from = new value_set_t(); } -/* Reallocate some snapshotted memories when new executions start */ +/* Reallocate snapshotted memories when new executions start */ void FuncNode::set_new_exec_flag() { // for (uint i = 0; i < thrd_read_map.size(); i++) @@ -28,13 +29,13 @@ void FuncNode::set_new_exec_flag() for (mllnode * it = inst_list.begin(); it != NULL; it = it->getNext()) { FuncInst * inst = it->getVal(); - inst->reset_location(); + inst->unset_location(); } read_locations = new loc_set_t(); val_loc_map = new HashTable(); loc_may_equal_map = new HashTable(); - values_may_read_from = new value_set_t(); + //values_may_read_from = new value_set_t(); } /* Check whether FuncInst with the same type, position, and location @@ -163,13 +164,13 @@ void FuncNode::update_tree(action_list_t * act_list) } } - model_print("function %s\n", func_name); +// model_print("function %s\n", func_name); // print_val_loc_map(); update_inst_tree(&inst_list); update_predicate_tree(&read_act_list); - print_predicate_tree(); +// print_predicate_tree(); } /** @@ -207,7 +208,7 @@ void FuncNode::update_inst_tree(func_inst_list_t * inst_list) /* @param tid thread id * Store the values read by atomic read actions into thrd_read_map */ -void FuncNode::store_read(ModelAction * act, uint32_t tid) +void FuncNode::store_read(ModelAction * act, thread_id_t tid) { /* ASSERT(act); @@ -228,7 +229,7 @@ void FuncNode::store_read(ModelAction * act, uint32_t tid) */ } -uint64_t FuncNode::query_last_read(void * location, uint32_t tid) +uint64_t FuncNode::query_last_read(void * location, thread_id_t tid) { /* if (thrd_read_map.size() <= tid) @@ -249,7 +250,7 @@ uint64_t FuncNode::query_last_read(void * location, uint32_t tid) * Reset read map for a thread. This function shall only be called * when a thread exits a function */ -void FuncNode::clear_read_map(uint32_t tid) +void FuncNode::clear_read_map(thread_id_t tid) { /* if (thrd_read_map.size() <= tid) @@ -521,7 +522,7 @@ void FuncNode::add_to_val_loc_map(uint64_t val, void * loc) update_loc_may_equal_map(loc, locations); locations->add(loc); - values_may_read_from->add(val); + // values_may_read_from->add(val); } void FuncNode::add_to_val_loc_map(value_set_t * values, void * loc) @@ -558,6 +559,21 @@ void FuncNode::update_loc_may_equal_map(void * new_loc, loc_set_t * old_location } } +void FuncNode::init_predicate_tree_position(thread_id_t tid) +{ + uint thread_id = id_to_int(tid); + if (predicate_tree_position.size() <= thread_id) + predicate_tree_position.resize(thread_id + 1); + + predicate_tree_position[thread_id] = predicate_tree_entry; +} + +void FuncNode::unset_predicate_tree_position(thread_id_t tid) +{ + uint thread_id = id_to_int(tid); + predicate_tree_position[thread_id] = NULL; +} + void FuncNode::print_predicate_tree() { model_print("digraph function_%s {\n", func_name); @@ -567,6 +583,7 @@ void FuncNode::print_predicate_tree() void FuncNode::print_val_loc_map() { +/* value_set_iter * val_it = values_may_read_from->iterator(); while (val_it->hasNext()) { uint64_t value = val_it->next(); @@ -580,13 +597,14 @@ void FuncNode::print_val_loc_map() } model_print("\n"); } +*/ } /* @param tid thread id * Print the values read by the last read actions for each memory location */ /* -void FuncNode::print_last_read(uint32_t tid) +void FuncNode::print_last_read(thread_id_t tid) { ASSERT(thrd_read_map.size() > tid); read_map_t * read_map = thrd_read_map[tid]; diff --git a/funcnode.h b/funcnode.h index e757b650..e414b4b9 100644 --- a/funcnode.h +++ b/funcnode.h @@ -33,9 +33,9 @@ public: void update_tree(action_list_t * act_list); void update_inst_tree(func_inst_list_t * inst_list); - void store_read(ModelAction * act, uint32_t tid); - uint64_t query_last_read(void * location, uint32_t tid); - void clear_read_map(uint32_t tid); + void store_read(ModelAction * act, thread_id_t tid); + uint64_t query_last_read(void * location, thread_id_t tid); + void clear_read_map(thread_id_t tid); void update_predicate_tree(action_list_t * act_list); bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, HashTable* inst_act_map, SnapVector * unset_predicates); @@ -51,9 +51,13 @@ public: void add_to_val_loc_map(value_set_t * values, void * loc); void update_loc_may_equal_map(void * new_loc, loc_set_t * old_locations); + void init_predicate_tree_position(thread_id_t tid); + void unset_predicate_tree_position(thread_id_t tid); + Predicate * get_predicate_tree_position(thread_id_t tid); + void print_predicate_tree(); void print_val_loc_map(); - void print_last_read(uint32_t tid); + void print_last_read(thread_id_t tid); MEMALLOC private: @@ -89,7 +93,10 @@ private: loc_set_t * read_locations; HashTable * val_loc_map; HashTable * loc_may_equal_map; - value_set_t * values_may_read_from; + // value_set_t * values_may_read_from; + + /* run-time position in the predicate tree for each thread */ + ModelVector predicate_tree_position; }; #endif /* __FUNCNODE_H__ */ diff --git a/history.cc b/history.cc index 9b0780e9..b546cd0a 100644 --- a/history.cc +++ b/history.cc @@ -48,6 +48,9 @@ void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid) if ( func_nodes.size() <= func_id ) resize_func_nodes( func_id + 1 ); + + FuncNode * func_node = func_nodes[func_id]; + func_node->init_predicate_tree_position(tid); } /* @param func_id a non-zero value */ @@ -63,12 +66,13 @@ void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid) if (last_func_id == func_id) { FuncNode * func_node = func_nodes[func_id]; + func_node->unset_predicate_tree_position(tid); //func_node->clear_read_map(tid); action_list_t * curr_act_list = func_act_lists->back(); /* defer the processing of curr_act_list until the function has exits a few times - * (currently 2 times) so that more information can be gathered to infer nullity predicates. + * (currently twice) so that more information can be gathered to infer nullity predicates. */ func_node->incr_exit_count(); if (func_node->get_exit_count() >= 2) { @@ -99,7 +103,7 @@ void ModelHistory::resize_func_nodes(uint32_t new_size) if ( old_size < new_size ) func_nodes.resize(new_size); - for (uint32_t id = old_size;id < new_size;id++) { + for (uint32_t id = old_size; id < new_size; id++) { const char * func_name = func_map_rev[id]; FuncNode * func_node = new FuncNode(this); func_node->set_func_id(id); -- 2.34.1