From a7b4dab68db8b1fc466a7ca4098d5a6fb006e353 Mon Sep 17 00:00:00 2001 From: weiyu Date: Wed, 23 Oct 2019 12:26:48 -0700 Subject: [PATCH] Add a collision list for FuncInsts with the same source line number --- execution.cc | 5 ++-- funcinst.cc | 10 +++++--- funcinst.h | 17 +++++++------- funcnode.cc | 66 +++++++++++++++++++++++++++++++++++----------------- funcnode.h | 1 + 5 files changed, 65 insertions(+), 34 deletions(-) diff --git a/execution.cc b/execution.cc index e285156f..e6203cb5 100644 --- a/execution.cc +++ b/execution.cc @@ -821,8 +821,9 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) { * * @param curr The current action. Must be a read. * @param rf The ModelAction or Promise that curr reads from. Must be a write. - * @param check_only Only check if the current action satisfies read - * modification order or not, without modifiying priorsetand canprune + * @param check_only If true, then only check whether the current action satisfies + * read modification order or not, without modifiying priorset and canprune. + * False by default. * @return True if modification order edges were added; false otherwise */ diff --git a/funcinst.cc b/funcinst.cc index 44bb167e..df91edc8 100644 --- a/funcinst.cc +++ b/funcinst.cc @@ -3,7 +3,7 @@ FuncInst::FuncInst(ModelAction *act, FuncNode *func_node) : single_location(true), - execution_number(model->get_execution_number()), + execution_number(0), action_marker(0) /* The marker for FuncNode starts from 1 */ { ASSERT(act); @@ -61,7 +61,7 @@ ModelAction * FuncInst::get_associated_act(uint32_t marker) return NULL; } -/* +/* Search the FuncInst that has the same type as act in the collision list */ FuncInst * FuncInst::search_in_collision(ModelAction *act) { action_type type = act->get_type(); @@ -74,7 +74,11 @@ FuncInst * FuncInst::search_in_collision(ModelAction *act) } return NULL; } -*/ + +void FuncInst::add_to_collision(FuncInst * inst) +{ + collisions.push_back(inst); +} /* Note: is_read() is equivalent to ModelAction::is_read() */ bool FuncInst::is_read() const diff --git a/funcinst.h b/funcinst.h index 98af6bcb..e96eb190 100644 --- a/funcinst.h +++ b/funcinst.h @@ -25,8 +25,8 @@ public: bool add_pred(FuncInst * other); bool add_succ(FuncInst * other); - //FuncInst * search_in_collision(ModelAction *act); - //func_inst_list_mt * get_collisions() { return &collisions; } + FuncInst * search_in_collision(ModelAction *act); + void add_to_collision(FuncInst * inst); func_inst_list_mt * get_preds() { return &predecessors; } func_inst_list_mt * get_succs() { return &successors; } @@ -67,12 +67,13 @@ private: ModelAction * associated_act; uint32_t action_marker; - /* Currently not in use. May remove this field later - * - * collisions store a list of FuncInsts with the same position - * but different action types. For example, CAS is broken down - * as three different atomic operations in cmodelint.cc */ - // func_inst_list_mt collisions; + /** + * Collisions store a list of FuncInsts with the same position + * but different action types. For example, + * volatile int x; x++; produces read and write + * actions with the same position. + */ + func_inst_list_mt collisions; func_inst_list_mt predecessors; func_inst_list_mt successors; diff --git a/funcnode.cc b/funcnode.cc index 2972b86e..909d4a8d 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -46,9 +46,6 @@ void FuncNode::set_new_exec_flag() /* Check whether FuncInst with the same type, position, and location * as act has been added to func_inst_map or not. If not, add it. - * - * Note: currently, actions with the same position are filtered out by process_action, - * so the collision list of FuncInst is not used. May remove it later. */ void FuncNode::add_inst(ModelAction *act) { @@ -61,31 +58,54 @@ void FuncNode::add_inst(ModelAction *act) if (position == NULL) return; - if ( func_inst_map.contains(position) ) { - FuncInst * inst = func_inst_map.get(position); + FuncInst * func_inst = func_inst_map.get(position); - /* TODO: The assertion fails when encountering volatile variables that use ++ or -- syntax, i.e. read and write have the same position */ - ASSERT(inst->get_type() == act->get_type()); - int curr_execution_number = model->get_execution_number(); + /* This position has not been inserted into hashtable before */ + if (func_inst == NULL) { + func_inst = create_new_inst(act); + func_inst_map.put(position, func_inst); + return; + } - /* Reset locations when new executions start */ - if (inst->get_execution_number() != curr_execution_number) { - inst->set_location(act->get_location()); - inst->set_execution_number(curr_execution_number); + /* Volatile variables that use ++ or -- syntax may result in read and write actions with the same position */ + if (func_inst->get_type() != act->get_type()) { + FuncInst * collision_inst = func_inst->search_in_collision(act); + + if (collision_inst == NULL) { + collision_inst = create_new_inst(act); + func_inst->add_to_collision(collision_inst); + return; + } else { + func_inst = collision_inst; } + } - if (inst->get_location() != act->get_location()) - inst->not_single_location(); + ASSERT(func_inst->get_type() == act->get_type()); + int curr_execution_number = model->get_execution_number(); - return; + /* Reset locations when new executions start */ + if (func_inst->get_execution_number() != curr_execution_number) { + func_inst->set_location(act->get_location()); + func_inst->set_execution_number(curr_execution_number); } + /* Mark the memory location of such inst as not unique */ + if (func_inst->get_location() != act->get_location()) + func_inst->not_single_location(); +} + +FuncInst * FuncNode::create_new_inst(ModelAction * act) +{ FuncInst * func_inst = new FuncInst(act, this); + int exec_num = model->get_execution_number(); + func_inst->set_execution_number(exec_num); - func_inst_map.put(position, func_inst); inst_list.push_back(func_inst); + + return func_inst; } + /* Get the FuncInst with the same type, position, and location * as act * @@ -108,14 +128,18 @@ FuncInst * FuncNode::get_inst(ModelAction *act) action_type inst_type = inst->get_type(); action_type act_type = act->get_type(); - // else if branch: an RMWRCAS action is converted to a RMW or READ action - if (inst_type == act_type) + if (inst_type == act_type) { return inst; + } + /* RMWRCAS actions are converted to RMW or READ actions */ else if (inst_type == ATOMIC_RMWRCAS && - (act_type == ATOMIC_RMW || act_type == ATOMIC_READ)) + (act_type == ATOMIC_RMW || act_type == ATOMIC_READ)) { return inst; - - return NULL; + } + /* Return the FuncInst in the collision list */ + else { + return inst->search_in_collision(act); + } } diff --git a/funcnode.h b/funcnode.h index fab4db50..ea591a2e 100644 --- a/funcnode.h +++ b/funcnode.h @@ -25,6 +25,7 @@ public: void set_new_exec_flag(); void add_inst(ModelAction *act); + FuncInst * create_new_inst(ModelAction *act); FuncInst * get_inst(ModelAction *act); HashTable * getFuncInstMap() { return &func_inst_map; } -- 2.34.1