From 385bb0a582f5987febe5d5c4e3bd8b50cbc1638f Mon Sep 17 00:00:00 2001 From: weiyu Date: Fri, 2 Aug 2019 18:12:10 -0700 Subject: [PATCH] toward building a naive predicate tree --- funcinst.cc | 13 ++++--- funcinst.h | 4 +++ funcnode.cc | 102 ++++++++++++++++++++++++++++++++++++++++------------ funcnode.h | 9 ++--- history.cc | 3 +- 5 files changed, 99 insertions(+), 32 deletions(-) diff --git a/funcinst.cc b/funcinst.cc index 8d9c23ba..3216baee 100644 --- a/funcinst.cc +++ b/funcinst.cc @@ -8,6 +8,7 @@ FuncInst::FuncInst(ModelAction *act, FuncNode *func_node) : this->position = act->get_position(); this->location = act->get_location(); this->type = act->get_type(); + this->order = act->get_mo(); this->func_node = func_node; } @@ -47,10 +48,10 @@ FuncInst * FuncInst::search_in_collision(ModelAction *act) { action_type type = act->get_type(); - mllnode* it; - for (it = collisions.begin();it != NULL;it=it->getNext()) { + mllnode * it; + for (it = collisions.begin(); it != NULL; it = it->getNext()) { FuncInst * inst = it->getVal(); - if ( inst->get_type() == type ) + if (inst->get_type() == type) return inst; } return NULL; @@ -58,7 +59,7 @@ FuncInst * FuncInst::search_in_collision(ModelAction *act) bool FuncInst::is_read() const { - return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMWRCAS; /* type == ATOMIC_RMW ? */ + return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMWRCAS || type == ATOMIC_RMW; } bool FuncInst::is_write() const @@ -66,3 +67,7 @@ bool FuncInst::is_write() const return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == ATOMIC_UNINIT || type == NONATOMIC_WRITE; } +void FuncInst::print() +{ + model_print("func inst - position: %s, location: %p, type: %d, order: %d\n", position, location, type, order); +} diff --git a/funcinst.h b/funcinst.h index bc56e277..654ba653 100644 --- a/funcinst.h +++ b/funcinst.h @@ -17,6 +17,7 @@ public: const char * get_position() const { return position; } void * get_location() const { return location; } action_type get_type() const { return type; } + memory_order get_mo() const { return order; } FuncNode * get_func_node() const { return func_node; } bool add_pred(FuncInst * other); @@ -31,12 +32,15 @@ public: bool is_read() const; bool is_write() const; + void print(); + MEMALLOC private: //ModelAction * const action; const char * position; void * location; action_type type; + memory_order order; FuncNode * func_node; /* collisions store a list of FuncInsts with the same position diff --git a/funcnode.cc b/funcnode.cc index 6233d3f3..190dce8e 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -5,7 +5,8 @@ FuncNode::FuncNode() : func_inst_map(), inst_list(), entry_insts(), - thrd_read_map() + thrd_read_map(), + predicate_tree_entry() {} /* Check whether FuncInst with the same type, position, and location @@ -18,10 +19,8 @@ FuncInst * FuncNode::get_or_add_inst(ModelAction *act) ASSERT(act); const char * position = act->get_position(); - /* Actions THREAD_CREATE, THREAD_START, THREAD_YIELD, THREAD_JOIN, - * THREAD_FINISH, PTHREAD_CREATE, PTHREAD_JOIN, - * ATOMIC_LOCK, ATOMIC_TRYLOCK, and ATOMIC_UNLOCK are not tagged with their - * source line numbers + /* THREAD* actions, ATOMIC_LOCK, ATOMIC_TRYLOCK, and ATOMIC_UNLOCK + * actions are not tagged with their source line numbers */ if (position == NULL) return NULL; @@ -61,7 +60,7 @@ void FuncNode::add_entry_inst(FuncInst * inst) if (inst == NULL) return; - mllnode* it; + mllnode * it; for (it = entry_insts.begin(); it != NULL; it = it->getNext()) { if (inst == it->getVal()) return; @@ -70,10 +69,11 @@ void FuncNode::add_entry_inst(FuncInst * inst) entry_insts.push_back(inst); } -/* @param act_list a list of ModelActions; this argument comes from ModelExecution - * convert act_inst to inst_list do linking - add one FuncInst to another's predecessors and successors +/** + * @brief Convert ModelAdtion list to FuncInst list + * @param act_list A list of ModelActions */ -void FuncNode::update_inst_tree(action_list_t * act_list) +void FuncNode::update_tree(action_list_t * act_list) { if (act_list == NULL) return; @@ -82,16 +82,47 @@ void FuncNode::update_inst_tree(action_list_t * act_list) /* build inst_list from act_list for later processing */ func_inst_list_t inst_list; + func_inst_list_t read_inst_list; + HashTable read_val_map; + for (sllnode * it = act_list->begin(); it != NULL; it = it->getNext()) { ModelAction * act = it->getVal(); FuncInst * func_inst = get_or_add_inst(act); - if (func_inst != NULL) - inst_list.push_back(func_inst); + if (func_inst == NULL) + continue; + + inst_list.push_back(func_inst); + + if (!predicate_tree_initialized) { + model_print("position: %s ", act->get_position()); + act->print(); + } + + if (func_inst->is_read()) { + read_inst_list.push_back(func_inst); + read_val_map.put(func_inst, act->get_reads_from_value()); + } } + update_inst_tree(&inst_list); + model_print("line break\n"); + init_predicate_tree(&read_inst_list, &read_val_map); +} + +/** + * @brief Link FuncInsts in inst_list - add one FuncInst to another's predecessors and successors + * @param inst_list A list of FuncInsts + */ +void FuncNode::update_inst_tree(func_inst_list_t * inst_list) +{ + if (inst_list == NULL) + return; + else if (inst_list->size() == 0) + return; + /* start linking */ - sllnode* it = inst_list.begin(); + sllnode* it = inst_list->begin(); sllnode* prev; /* add the first instruction to the list of entry insts */ @@ -163,13 +194,16 @@ void FuncNode::clear_read_map(uint32_t tid) thrd_read_map[tid]->reset(); } -void FuncNode::init_predicate_tree(func_inst_list_t * inst_list) +void FuncNode::init_predicate_tree(func_inst_list_t * inst_list, HashTable * read_val_map) { if (inst_list == NULL || inst_list->size() == 0) return; - if (predicate_tree_initialized) + if (predicate_tree_initialized) { + model_print("function %s\n", func_name); + print_predicate_tree(); return; + } predicate_tree_initialized = true; @@ -182,7 +216,8 @@ void FuncNode::init_predicate_tree(func_inst_list_t * inst_list) FuncInst * entry_inst = it->getVal(); /* entry instruction has no predicate expression */ - Predicate * pred_entry = new Predicate(entry_inst); + Predicate * curr_pred = new Predicate(entry_inst); + predicate_tree_entry.add(curr_pred); loc_inst_map.put(entry_inst->get_location(), entry_inst); it = it->getNext(); @@ -193,11 +228,25 @@ void FuncNode::init_predicate_tree(func_inst_list_t * inst_list) FuncInst * prev_inst = prev->getVal(); if ( loc_inst_map.contains(curr_inst->get_location()) ) { - Predicate * pred1 = new Predicate(curr_inst); - pred1->add_predicate(EQUALITY, curr_inst->get_location(), 0); - - Predicate * pred2 = new Predicate(curr_inst); - pred2->add_predicate(EQUALITY, curr_inst->get_location(), 1); +// model_print("new predicate created at location: %p\n", curr_inst->get_location()); + Predicate * new_pred1 = new Predicate(curr_inst); + new_pred1->add_predicate(EQUALITY, curr_inst->get_location(), true); + + Predicate * new_pred2 = new Predicate(curr_inst); + new_pred2->add_predicate(EQUALITY, curr_inst->get_location(), false); + + curr_pred->add_child(new_pred1); + curr_pred->add_child(new_pred2); + + uint64_t last_read = read_val_map->get(prev_inst); + if ( last_read == read_val_map->get(curr_inst) ) + curr_pred = new_pred1; + else + curr_pred = new_pred2; + } else { + Predicate * new_pred = new Predicate(curr_inst); + curr_pred->add_child(new_pred); + curr_pred = new_pred; } loc_inst_map.put(curr_inst->get_location(), curr_inst); @@ -207,19 +256,26 @@ void FuncNode::init_predicate_tree(func_inst_list_t * inst_list) } -void FuncNode::generate_predicate(FuncInst *func_inst) +void FuncNode::print_predicate_tree() { + HSIterator * it; + it = predicate_tree_entry.iterator(); + while (it->hasNext()) { + Predicate * p = it->next(); + p->print_pred_subtree(); + } } /* @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) { ASSERT(thrd_read_map.size() > tid); read_map_t * read_map = thrd_read_map[tid]; -/* + mllnode * it; for (it = read_locations.begin();it != NULL;it=it->getNext()) { if ( !read_map->contains(it->getVal()) ) @@ -228,5 +284,5 @@ void FuncNode::print_last_read(uint32_t tid) uint64_t read_val = read_map->get(it->getVal()); model_print("last read of thread %d at %p: 0x%x\n", tid, it->getVal(), read_val); } -*/ } +*/ diff --git a/funcnode.h b/funcnode.h index 36729746..61ab0593 100644 --- a/funcnode.h +++ b/funcnode.h @@ -26,15 +26,17 @@ public: func_inst_list_mt * get_inst_list() { return &inst_list; } func_inst_list_mt * get_entry_insts() { return &entry_insts; } void add_entry_inst(FuncInst * inst); - void update_inst_tree(action_list_t * act_list); + + 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); /* TODO: generate EQUALITY or NULLITY predicate based on write_history in history.cc */ - void init_predicate_tree(func_inst_list_t * inst_list); - void generate_predicate(FuncInst * func_inst); + void init_predicate_tree(func_inst_list_t * inst_list, HashTable * read_val_map); + void print_predicate_tree(); void print_last_read(uint32_t tid); @@ -58,7 +60,6 @@ private: /* Store the values read by atomic read actions per memory location for each thread */ ModelVector thrd_read_map; - /* TODO: how to guarantee unique predicate? Or add an equal function */ HashSet predicate_tree_entry; }; diff --git a/history.cc b/history.cc index a6d0c96f..283c248f 100644 --- a/history.cc +++ b/history.cc @@ -67,8 +67,9 @@ void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid) FuncNode * func_node = func_nodes[func_id]; func_node->clear_read_map(tid); + // model_print("hello function %s and thread %d\n", func_node->get_func_name(), tid); action_list_t * curr_act_list = func_act_lists->back(); - func_node->update_inst_tree(curr_act_list); + func_node->update_tree(curr_act_list); (*thrd_func_list)[id].pop_back(); func_act_lists->pop_back(); -- 2.34.1