From: weiyu Date: Thu, 1 Aug 2019 00:57:46 +0000 (-0700) Subject: change the data structure of thrd_func_inst_list because more information about the... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=04a39b7be7672034249091a7df9a4c8407a8b787 change the data structure of thrd_func_inst_list because more information about the action trace is needed --- diff --git a/execution.cc b/execution.cc index 94be82ac..cf4c9028 100644 --- a/execution.cc +++ b/execution.cc @@ -66,7 +66,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : mo_graph(new CycleGraph()), fuzzer(new Fuzzer()), thrd_func_list(), - thrd_func_inst_lists(), + thrd_func_act_lists(), isfinished(false) { /* Initialize a model-checker thread, for special ModelActions */ @@ -1654,7 +1654,7 @@ Thread * ModelExecution::take_step(ModelAction *curr) ASSERT(curr); /* Process this action in ModelHistory for records*/ - // model->get_history()->process_action( curr, curr->get_tid() ); + model->get_history()->process_action( curr, curr->get_tid() ); if (curr_thrd->is_blocked() || curr_thrd->is_complete()) scheduler->remove_thread(curr_thrd); diff --git a/execution.h b/execution.h index 22f694c9..343a5074 100644 --- a/execution.h +++ b/execution.h @@ -90,7 +90,7 @@ public: ModelAction * check_current_action(ModelAction *curr); SnapVector * get_thrd_func_list() { return &thrd_func_list; } - SnapVector< SnapList *> * get_thrd_func_inst_lists() { return &thrd_func_inst_lists; } + SnapVector< SnapList *> * get_thrd_func_act_lists() { return &thrd_func_act_lists; } bool isFinished() {return isfinished;} void setFinished() {isfinished = true;} @@ -213,7 +213,7 @@ private: * * This data structure is handled by ModelHistory */ - SnapVector< SnapList< func_inst_list_t *> *> thrd_func_inst_lists; + SnapVector< SnapList *> thrd_func_act_lists; bool isfinished; }; diff --git a/funcnode.cc b/funcnode.cc index 2b252546..6233d3f3 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -1,7 +1,7 @@ #include "funcnode.h" -#include "predicate.h" FuncNode::FuncNode() : + predicate_tree_initialized(false), func_inst_map(), inst_list(), entry_insts(), @@ -13,7 +13,7 @@ FuncNode::FuncNode() : * if not, add it and return it. * * @return FuncInst with the same type, position, and location as act */ -FuncInst * FuncNode::get_or_add_action(ModelAction *act) +FuncInst * FuncNode::get_or_add_inst(ModelAction *act) { ASSERT(act); const char * position = act->get_position(); @@ -62,7 +62,7 @@ void FuncNode::add_entry_inst(FuncInst * inst) return; mllnode* it; - for (it = entry_insts.begin();it != NULL;it=it->getNext()) { + for (it = entry_insts.begin(); it != NULL; it = it->getNext()) { if (inst == it->getVal()) return; } @@ -70,27 +70,36 @@ void FuncNode::add_entry_inst(FuncInst * inst) entry_insts.push_back(inst); } -/* @param inst_list a list of FuncInsts; this argument comes from ModelExecution - * Link FuncInsts in a list - add one FuncInst to another's predecessors and successors +/* @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 */ -void FuncNode::link_insts(func_inst_list_t * inst_list) +void FuncNode::update_inst_tree(action_list_t * act_list) { - if (inst_list == NULL) + if (act_list == NULL) + return; + else if (act_list->size() == 0) return; - sllnode* it = inst_list->begin(); - sllnode* prev; + /* build inst_list from act_list for later processing */ + func_inst_list_t inst_list; + for (sllnode * it = act_list->begin(); it != NULL; it = it->getNext()) { + ModelAction * act = it->getVal(); + FuncInst * func_inst = get_or_add_inst(act); - if (inst_list->size() == 0) - return; + if (func_inst != NULL) + inst_list.push_back(func_inst); + } + + /* start linking */ + sllnode* it = inst_list.begin(); + sllnode* prev; /* add the first instruction to the list of entry insts */ FuncInst * entry_inst = it->getVal(); add_entry_inst(entry_inst); - it=it->getNext(); + it = it->getNext(); while (it != NULL) { - prev = it; prev = it->getPrev(); FuncInst * prev_inst = prev->getVal(); @@ -99,7 +108,7 @@ void FuncNode::link_insts(func_inst_list_t * inst_list) prev_inst->add_succ(curr_inst); curr_inst->add_pred(prev_inst); - it=it->getNext(); + it = it->getNext(); } } @@ -116,7 +125,7 @@ void FuncNode::store_read(ModelAction * act, uint32_t tid) uint32_t old_size = thrd_read_map.size(); if (old_size <= tid) { thrd_read_map.resize(tid + 1); - for (uint32_t i = old_size;i < tid + 1;i++) + for (uint32_t i = old_size; i < tid + 1;i++) thrd_read_map[i] = new read_map_t(); } @@ -154,6 +163,50 @@ void FuncNode::clear_read_map(uint32_t tid) thrd_read_map[tid]->reset(); } +void FuncNode::init_predicate_tree(func_inst_list_t * inst_list) +{ + if (inst_list == NULL || inst_list->size() == 0) + return; + + if (predicate_tree_initialized) + return; + + predicate_tree_initialized = true; + + // maybe restrict the size of hashtable to save calloc time + HashTable loc_inst_map; + + sllnode *it = inst_list->begin(); + sllnode *prev; + + FuncInst * entry_inst = it->getVal(); + + /* entry instruction has no predicate expression */ + Predicate * pred_entry = new Predicate(entry_inst); + loc_inst_map.put(entry_inst->get_location(), entry_inst); + + it = it->getNext(); + while (it != NULL) { + prev = it->getPrev(); + + FuncInst * curr_inst = it->getVal(); + 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); + } + + loc_inst_map.put(curr_inst->get_location(), curr_inst); + + it = it->getNext(); + } +} + + void FuncNode::generate_predicate(FuncInst *func_inst) { diff --git a/funcnode.h b/funcnode.h index f293f195..36729746 100644 --- a/funcnode.h +++ b/funcnode.h @@ -5,6 +5,7 @@ #include "funcinst.h" #include "hashtable.h" #include "hashset.h" +#include "predicate.h" typedef ModelList func_inst_list_mt; typedef HashTable read_map_t; @@ -19,19 +20,20 @@ public: void set_func_id(uint32_t id) { func_id = id; } void set_func_name(const char * name) { func_name = name; } - FuncInst * get_or_add_action(ModelAction *act); + FuncInst * get_or_add_inst(ModelAction *act); HashTable * getFuncInstMap() { return &func_inst_map; } 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 link_insts(func_inst_list_t * inst_list); + void update_inst_tree(action_list_t * act_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 print_last_read(uint32_t tid); @@ -40,6 +42,7 @@ public: private: uint32_t func_id; const char * func_name; + bool predicate_tree_initialized; /* Use source line number as the key of hashtable, to check if * atomic operation with this line number has been added or not @@ -55,6 +58,8 @@ 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; }; -#endif /* __FUNCNODE_H__ */ +#endif /* __FUNCNODE_H__ */ diff --git a/history.cc b/history.cc index c1c9edf5..a6d0c96f 100644 --- a/history.cc +++ b/history.cc @@ -23,8 +23,8 @@ void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid) //model_print("thread %d entering func %d\n", tid, func_id); uint32_t id = id_to_int(tid); SnapVector * thrd_func_list = model->get_execution()->get_thrd_func_list(); - SnapVector< SnapList *> * - thrd_func_inst_lists = model->get_execution()->get_thrd_func_inst_lists(); + SnapVector< SnapList *> * + thrd_func_act_lists = model->get_execution()->get_thrd_func_act_lists(); if ( thrd_func_list->size() <= id ) { uint oldsize = thrd_func_list->size(); @@ -35,18 +35,18 @@ void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid) (*thrd_func_list)[i].push_back(0); } - thrd_func_inst_lists->resize( id + 1 ); + thrd_func_act_lists->resize( id + 1 ); } - SnapList * func_inst_lists = thrd_func_inst_lists->at(id); + SnapList * func_act_lists = thrd_func_act_lists->at(id); - if (func_inst_lists == NULL) { - func_inst_lists = new SnapList< func_inst_list_t *>(); - thrd_func_inst_lists->at(id) = func_inst_lists; + if (func_act_lists == NULL) { + func_act_lists = new SnapList(); + thrd_func_act_lists->at(id) = func_act_lists; } (*thrd_func_list)[id].push_back(func_id); - func_inst_lists->push_back( new func_inst_list_t() ); + func_act_lists->push_back( new action_list_t() ); if ( func_nodes.size() <= func_id ) resize_func_nodes( func_id + 1 ); @@ -57,21 +57,21 @@ void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid) { uint32_t id = id_to_int(tid); SnapVector * thrd_func_list = model->get_execution()->get_thrd_func_list(); - SnapVector< SnapList *> * - thrd_func_inst_lists = model->get_execution()->get_thrd_func_inst_lists(); + SnapVector< SnapList *> * + thrd_func_act_lists = model->get_execution()->get_thrd_func_act_lists(); - SnapList * func_inst_lists = thrd_func_inst_lists->at(id); + SnapList * func_act_lists = thrd_func_act_lists->at(id); uint32_t last_func_id = (*thrd_func_list)[id].back(); if (last_func_id == func_id) { FuncNode * func_node = func_nodes[func_id]; func_node->clear_read_map(tid); - func_inst_list_t * curr_inst_list = func_inst_lists->back(); - func_node->link_insts(curr_inst_list); + action_list_t * curr_act_list = func_act_lists->back(); + func_node->update_inst_tree(curr_act_list); (*thrd_func_list)[id].pop_back(); - func_inst_lists->pop_back(); + func_act_lists->pop_back(); } else { model_print("trying to exit with a wrong function id\n"); model_print("--- last_func: %d, func_id: %d\n", last_func_id, func_id); @@ -100,8 +100,8 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid) /* return if thread i has not entered any function or has exited from all functions */ SnapVector * thrd_func_list = model->get_execution()->get_thrd_func_list(); - SnapVector< SnapList *> * - thrd_func_inst_lists = model->get_execution()->get_thrd_func_inst_lists(); + SnapVector< SnapList *> * + thrd_func_act_lists = model->get_execution()->get_thrd_func_act_lists(); uint32_t id = id_to_int(tid); if ( thrd_func_list->size() <= id ) @@ -109,7 +109,7 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid) /* get the function id that thread i is currently in */ uint32_t func_id = (*thrd_func_list)[id].back(); - SnapList * func_inst_lists = thrd_func_inst_lists->at(id); + SnapList * func_act_lists = thrd_func_act_lists->at(id); if (func_id == 0) return; @@ -119,22 +119,20 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid) FuncNode * func_node = func_nodes[func_id]; ASSERT (func_node != NULL); - /* add corresponding FuncInst to func_node */ - FuncInst * inst = func_node->get_or_add_action(act); - - if (inst == NULL) + /* do not care actions without a position */ + if (act->get_position() == NULL) return; - if (inst->is_read()) + if (act->is_read()) func_node->store_read(act, tid); - if (inst->is_write()) + if (act->is_write()) add_to_write_history(act->get_location(), act->get_write_value()); /* add to curr_inst_list */ - func_inst_list_t * curr_inst_list = func_inst_lists->back(); - ASSERT(curr_inst_list != NULL); - curr_inst_list->push_back(inst); + action_list_t * curr_act_list = func_act_lists->back(); + ASSERT(curr_act_list != NULL); + curr_act_list->push_back(act); } /* return the FuncNode given its func_id */ diff --git a/include/mypthread.h b/include/mypthread.h index 31c410aa..ff7458ed 100644 --- a/include/mypthread.h +++ b/include/mypthread.h @@ -20,5 +20,4 @@ extern "C" { int user_main(int, char**); } -void check(); #endif diff --git a/pthread.cc b/pthread.cc index 272626d5..81263cf0 100644 --- a/pthread.cc +++ b/pthread.cc @@ -8,7 +8,6 @@ #include "mutex.h" #include -#include /* global "model" object */ #include "model.h" @@ -33,7 +32,6 @@ int pthread_create(pthread_t *t, const pthread_attr_t * attr, } int pthread_join(pthread_t t, void **value_ptr) { -// Thread *th = model->get_pthread(t); ModelExecution *execution = model->get_execution(); Thread *th = execution->get_pthread(t); @@ -62,13 +60,12 @@ void pthread_exit(void *value_ptr) { } int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) { - cdsc::snapmutex *m = new cdsc::snapmutex(); - if (!model) { snapshot_system_init(10000, 1024, 1024, 40000); model = new ModelChecker(); model->startChecker(); } + cdsc::snapmutex *m = new cdsc::snapmutex(); ModelExecution *execution = model->get_execution(); execution->getMutexMap()->put(p_mutex, m); @@ -83,7 +80,6 @@ int pthread_mutex_lock(pthread_mutex_t *p_mutex) { model->startChecker(); } - ModelExecution *execution = model->get_execution(); /* to protect the case where PTHREAD_MUTEX_INITIALIZER is used