From 533aa98d0e7df1435defd4b0698aedf5300a1ad3 Mon Sep 17 00:00:00 2001 From: weiyu Date: Wed, 21 Aug 2019 13:52:25 -0700 Subject: [PATCH] add helper functions; prepare for computing which memory locations may store the same values --- classlist.h | 10 ++++--- funcnode.cc | 78 +++++++++++++++++++++++++++++++++++++++++++++-------- funcnode.h | 9 ++++++- history.cc | 49 +++++++++++++++++++-------------- history.h | 11 ++++---- model.cc | 2 +- 6 files changed, 118 insertions(+), 41 deletions(-) diff --git a/classlist.h b/classlist.h index 664301e9..5a17449c 100644 --- a/classlist.h +++ b/classlist.h @@ -24,10 +24,14 @@ struct bug_message; typedef SnapList action_list_t; typedef SnapList func_id_list_t; typedef SnapList func_inst_list_t; -typedef HSIterator PredSetIter; + typedef HashSet PredSet; -typedef HSIterator write_set_iter; -typedef HashSet write_set_t; +typedef HSIterator PredSetIter; + +typedef HashSet value_set_t; +typedef HSIterator value_set_iter; +typedef HashSet loc_set_t; +typedef HSIterator loc_set_iter; extern volatile int modellock; #endif diff --git a/funcnode.cc b/funcnode.cc index dc013965..ccb930fa 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -3,26 +3,33 @@ FuncNode::FuncNode(ModelHistory * history) : history(history), predicate_tree_initialized(false), - predicate_tree_entry(new Predicate(NULL, true)), exit_count(0), func_inst_map(), inst_list(), entry_insts(), - thrd_read_map(), +// thrd_read_map(), action_list_buffer() { + predicate_tree_entry = new Predicate(NULL, true); predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true); + + // memory will be reclaimed after each execution + read_locations = new loc_set_t(); + val_loc_map = new HashTable(); } void FuncNode::set_new_exec_flag() { - for (uint i = 0; i < thrd_read_map.size(); i++) - thrd_read_map[i] = new read_map_t(); +// for (uint i = 0; i < thrd_read_map.size(); i++) +// thrd_read_map[i] = new read_map_t(); for (mllnode * it = inst_list.begin(); it != NULL; it = it->getNext()) { FuncInst * inst = it->getVal(); inst->reset_location(); } + + read_locations = new loc_set_t(); + val_loc_map = new HashTable(); } /* Check whether FuncInst with the same type, position, and location @@ -119,6 +126,8 @@ void FuncNode::update_tree(action_list_t * act_list) if (act_list == NULL || act_list->size() == 0) return; + HashTable * write_history = history->getWriteHistory(); + /* build inst_list from act_list for later processing */ func_inst_list_t inst_list; action_list_t read_act_list; @@ -132,8 +141,21 @@ void FuncNode::update_tree(action_list_t * act_list) inst_list.push_back(func_inst); - if (func_inst->is_read()) + if (func_inst->is_read()) { read_act_list.push_back(act); + + /* 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. + */ + void * loc = act->get_location(); + if (!read_locations->contains(loc)) { + read_locations->add(loc); + value_set_t * write_values = write_history->get(loc); + add_to_val_loc_map(write_values, loc); + history->add_to_loc_func_nodes_map(loc, this); + } + } } // model_print("function %s\n", func_name); @@ -181,13 +203,13 @@ void FuncNode::update_inst_tree(func_inst_list_t * inst_list) * Store the values read by atomic read actions into thrd_read_map */ void FuncNode::store_read(ModelAction * act, uint32_t tid) { +/* ASSERT(act); void * location = act->get_location(); uint64_t read_from_val = act->get_reads_from_value(); - /* resize and initialize */ - + // resize and initialize uint32_t old_size = thrd_read_map.size(); if (old_size <= tid) { thrd_read_map.resize(tid + 1); @@ -197,24 +219,24 @@ void FuncNode::store_read(ModelAction * act, uint32_t tid) read_map_t * read_map = thrd_read_map[tid]; read_map->put(location, read_from_val); - - /* Store the memory locations where atomic reads happen */ - // read_locations.add(location); +*/ } uint64_t FuncNode::query_last_read(void * location, uint32_t tid) { +/* if (thrd_read_map.size() <= tid) return VALUE_NONE; read_map_t * read_map = thrd_read_map[tid]; - /* last read value not found */ + // last read value not found if ( !read_map->contains(location) ) return VALUE_NONE; uint64_t read_val = read_map->get(location); return read_val; +*/ } /* @param tid thread id @@ -223,10 +245,12 @@ uint64_t FuncNode::query_last_read(void * location, uint32_t tid) */ void FuncNode::clear_read_map(uint32_t tid) { +/* if (thrd_read_map.size() <= tid) return; thrd_read_map[tid]->reset(); +*/ } void FuncNode::update_predicate_tree(action_list_t * act_list) @@ -454,6 +478,38 @@ bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, Model return branch_found; } +void FuncNode::add_to_val_loc_map(uint64_t val, void * loc) +{ + loc_set_t * locations = val_loc_map->get(val); + + if (locations == NULL) { + locations = new loc_set_t(); + val_loc_map->put(val, locations); + } + + locations->add(loc); + +/* + model_print("val %llx: ", val); + loc_set_iter * it = locations->iterator(); + while (it->hasNext()) { + void * location = it->next(); + model_print("%p ", location); + } + model_print("\n"); +*/ +} + +void FuncNode::add_to_val_loc_map(value_set_t * values, void * loc) +{ + value_set_iter * it = values->iterator(); + while (it->hasNext()) { + uint64_t val = it->next(); + add_to_val_loc_map(val, loc); + } +} + + void FuncNode::print_predicate_tree() { model_print("digraph function_%s {\n", func_name); diff --git a/funcnode.h b/funcnode.h index c84815cf..6e08fc26 100644 --- a/funcnode.h +++ b/funcnode.h @@ -47,6 +47,9 @@ public: ModelList * 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 print_predicate_tree(); void print_last_read(uint32_t tid); @@ -72,9 +75,13 @@ private: func_inst_list_mt entry_insts; /* Store the values read by atomic read actions per memory location for each thread */ - ModelVector thrd_read_map; + //ModelVector thrd_read_map; + /* store action_lists when calls to update_tree are deferred */ ModelList action_list_buffer; + + loc_set_t * read_locations; + HashTable * val_loc_map; }; #endif /* __FUNCNODE_H__ */ diff --git a/history.cc b/history.cc index 2dbc556e..68e8575f 100644 --- a/history.cc +++ b/history.cc @@ -14,8 +14,8 @@ ModelHistory::ModelHistory() : func_map(), func_map_rev(), func_nodes(), - write_history(), - write_locations() + write_history(), // snapshot data structure + loc_func_nodes_map() // shapshot data structure {} void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid) @@ -63,15 +63,14 @@ 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->clear_read_map(tid); + //func_node->clear_read_map(tid); action_list_t * curr_act_list = func_act_lists->back(); - func_node->incr_exit_count(); - /* 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. */ + func_node->incr_exit_count(); if (func_node->get_exit_count() >= 2) { ModelList * action_list_buffer = func_node->get_action_list_buffer(); while (action_list_buffer->size() > 0) { @@ -125,32 +124,30 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid) uint32_t func_id = (*thrd_func_list)[id].back(); SnapList * func_act_lists = (*thrd_func_act_lists)[id]; - if (act->is_write()) + if (act->is_write()) { add_to_write_history(act->get_location(), act->get_write_value()); + + } - if (func_id == 0) + /* the following does not care about actions without a position */ + if (func_id == 0 || act->get_position() == NULL) return; - else if ( func_nodes.size() <= func_id ) + + if ( func_nodes.size() <= func_id ) resize_func_nodes( func_id + 1 ); FuncNode * func_node = func_nodes[func_id]; - /* do not care about actions without a position */ - - if (act->get_position() == NULL) - return; - - if (act->is_read()) - func_node->store_read(act, tid); +// if (act->is_read()) +// func_node->store_read(act, tid); /* add to curr_inst_list */ - bool second_part_of_rmw = act->is_rmwc() || act->is_rmw(); if (!second_part_of_rmw) { action_list_t * curr_act_list = func_act_lists->back(); ASSERT(curr_act_list != NULL); - ModelAction * last_act; + ModelAction * last_act = NULL; if (curr_act_list->size() != 0) last_act = curr_act_list->back(); @@ -172,6 +169,7 @@ FuncNode * ModelHistory::get_func_node(uint32_t func_id) return func_nodes[func_id]; } +/* uint64_t ModelHistory::query_last_read(void * location, thread_id_t tid) { SnapVector * thrd_func_list = model->get_execution()->get_thrd_func_list(); @@ -188,18 +186,29 @@ uint64_t ModelHistory::query_last_read(void * location, thread_id_t tid) return last_read_val; } +*/ void ModelHistory::add_to_write_history(void * location, uint64_t write_val) { - write_set_t * write_set = write_history.get(location); + value_set_t * write_set = write_history.get(location); if (write_set == NULL) { - write_set = new write_set_t(); + write_set = new value_set_t(); write_history.put(location, write_set); } write_set->add(write_val); - write_locations.add(location); +} + +void ModelHistory::add_to_loc_func_nodes_map(void * location, FuncNode * node) +{ + SnapList * func_node_list = loc_func_nodes_map.get(location); + if (func_node_list == NULL) { + func_node_list = new SnapList(); + loc_func_nodes_map.put(location, func_node_list); + } + + func_node_list->push_back(node); } void ModelHistory::set_new_exec_flag() diff --git a/history.h b/history.h index 36b58483..3bb61564 100644 --- a/history.h +++ b/history.h @@ -7,7 +7,6 @@ #include "hashset.h" #include "threads-model.h" - class ModelHistory { public: ModelHistory(); @@ -27,10 +26,11 @@ public: ModelVector * getFuncNodes() { return &func_nodes; } FuncNode * get_func_node(uint32_t func_id); - uint64_t query_last_read(void * location, thread_id_t tid); +// uint64_t query_last_read(void * location, thread_id_t tid); void add_to_write_history(void * location, uint64_t write_val); - HashTable * getWriteHistory() { return &write_history; } + HashTable * getWriteHistory() { return &write_history; } + void add_to_loc_func_nodes_map(void * location, FuncNode * node); void set_new_exec_flag(); void print_write(); @@ -42,13 +42,14 @@ private: /* map function names to integer ids */ HashTable func_map; + /* map integer ids to function names */ ModelVector func_map_rev; ModelVector func_nodes; - HashTable write_history; - HashSet write_locations; + HashTable write_history; + HashTable *, uintptr_t, 4> loc_func_nodes_map; }; #endif /* __HISTORY_H__ */ diff --git a/model.cc b/model.cc index 5802b5d0..58a78592 100644 --- a/model.cc +++ b/model.cc @@ -40,7 +40,7 @@ ModelChecker::ModelChecker() : inspect_plugin(NULL) { memset(&stats,0,sizeof(struct execution_stats)); - init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program + init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL); #ifdef TLS init_thread->setTLS((char *)get_tls_addr()); #endif -- 2.34.1