From 5ca7bf3bd5afb9ca961fe8daaa1fae2d88c39211 Mon Sep 17 00:00:00 2001 From: weiyu Date: Tue, 28 Jan 2020 16:56:59 -0800 Subject: [PATCH] Improve the algorithm that marks which actions are needed by FuncNode --- action.cc | 16 ++++++++++++- action.h | 9 +++++-- execution.cc | 68 +++++++++++++++++++++++++++++++++------------------- funcnode.cc | 50 ++++++++++++++++++++++++++++++++++---- predicate.cc | 3 ++- 5 files changed, 114 insertions(+), 32 deletions(-) diff --git a/action.cc b/action.cc index 85a2a766..df73d209 100644 --- a/action.cc +++ b/action.cc @@ -45,6 +45,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, value(value), type(type), original_type(ATOMIC_NOP), + swap_flag(false), order(order), original_order(order), seq_number(ACTION_INITIAL_CLOCK) @@ -77,9 +78,11 @@ ModelAction::ModelAction(action_type_t type, memory_order order, uint64_t value, trace_ref(NULL), thrdmap_ref(NULL), action_ref(NULL), + func_act_ref(NULL), value(value), type(type), original_type(ATOMIC_NOP), + swap_flag(false), order(order), original_order(order), seq_number(ACTION_INITIAL_CLOCK) @@ -111,9 +114,11 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, trace_ref(NULL), thrdmap_ref(NULL), action_ref(NULL), + func_act_ref(NULL), value(value), type(type), original_type(ATOMIC_NOP), + swap_flag(false), order(order), original_order(order), seq_number(ACTION_INITIAL_CLOCK) @@ -149,9 +154,11 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order trace_ref(NULL), thrdmap_ref(NULL), action_ref(NULL), + func_act_ref(NULL), value(value), type(type), original_type(ATOMIC_NOP), + swap_flag(false), order(order), original_order(order), seq_number(ACTION_INITIAL_CLOCK) @@ -188,9 +195,11 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order trace_ref(NULL), thrdmap_ref(NULL), action_ref(NULL), + func_act_ref(NULL), value(value), type(type), original_type(ATOMIC_NOP), + swap_flag(false), order(order), original_order(order), seq_number(ACTION_INITIAL_CLOCK) @@ -614,7 +623,7 @@ uint64_t ModelAction::get_reads_from_value() const */ uint64_t ModelAction::get_write_value() const { - ASSERT(is_write()); + ASSERT(is_write() || is_free()); return value; } @@ -785,4 +794,9 @@ void ModelAction::use_original_type() action_type_t tmp = type; type = original_type; original_type = tmp; + + if (swap_flag) + swap_flag = false; + else + swap_flag = true; } diff --git a/action.h b/action.h index e830a74e..67c1ae81 100644 --- a/action.h +++ b/action.h @@ -34,7 +34,7 @@ using std::memory_order_seq_cst; * iteself does not indicate no value. */ #define VALUE_NONE 0xdeadbeef -#define HAS_REFERENCE ((void *)0x1) +#define WRITE_REFERENCED ((void *)0x1) /** * @brief The "location" at which a fence occurs @@ -104,7 +104,7 @@ public: thread_id_t get_tid() const { return tid; } action_type get_type() const { return type; } void set_type(action_type _type) { type = _type; } - action_type get_original_type() const { return type; } + action_type get_original_type() const { return original_type; } void set_original_type(action_type _type) { original_type = _type; } void set_free() { type = READY_FREE; } memory_order get_mo() const { return order; } @@ -120,6 +120,7 @@ public: ModelAction * get_reads_from() const { return reads_from; } uint64_t get_time() const {return time;} cdsc::mutex * get_mutex() const; + bool get_swap_flag() const { return swap_flag; } void set_read_from(ModelAction *act); @@ -254,6 +255,10 @@ private: * set as READY_FREE or weaken from a RMW to a write */ action_type original_type; + /** @brief Indicate whether the action type and the original action type + * has been swapped. */ + bool swap_flag; + /** @brief The memory order for this operation. */ memory_order order; diff --git a/execution.cc b/execution.cc index 47edb31a..796e9b74 100644 --- a/execution.cc +++ b/execution.cc @@ -1755,11 +1755,25 @@ void ModelExecution::collectActions() { //Free if it is invisible or we have set a flag to remove visible actions. if (actseq <= tid_clock || params->removevisible) { - // For read actions being used by ModelHistory, mark the reads_from as being used. - if (act->is_read() && act->getFuncActRef() != NULL) { - ModelAction * reads_from = act->get_reads_from(); - if (reads_from->getFuncActRef() == NULL) - reads_from->setFuncActRef(HAS_REFERENCE); + // For read or rmw actions being used by ModelHistory, mark the reads_from as being used. + if (act->is_read()) { + if (act->is_rmw()) { + void * func_act_ref = act->getFuncActRef(); + if (func_act_ref == WRITE_REFERENCED) { + // Only the write part of this rmw is referenced, do nothing + } else if (func_act_ref != NULL) { + // The read part of rmw is potentially referenced + ModelAction * reads_from = act->get_reads_from(); + if (reads_from->getFuncActRef() == NULL) + reads_from->setFuncActRef(WRITE_REFERENCED); + } + } else { + if (act->getFuncActRef() != NULL) { + ModelAction * reads_from = act->get_reads_from(); + if (reads_from->getFuncActRef() == NULL) + reads_from->setFuncActRef(WRITE_REFERENCED); + } + } } ModelAction * write; @@ -1781,10 +1795,8 @@ void ModelExecution::collectActions() { CycleNode * prevnode = node->getInEdge(i); ModelAction * prevact = prevnode->getAction(); if (prevact->get_type() != READY_FREE) { - if (prevact->getFuncActRef() != NULL) { - // Copy the original type if being used by ModelHistory - prevact->set_original_type(prevact->get_type()); - } + // Save the original action type + prevact->set_original_type(prevact->get_type()); prevact->set_free(); queue->push_back(prevnode); } @@ -1808,19 +1820,29 @@ void ModelExecution::collectActions() { } if (act->is_read()) { - // For read actions being used by ModelHistory, mark the reads_from as being used. - if (act->getFuncActRef() != NULL) { - ModelAction * reads_from = act->get_reads_from(); - if (reads_from->getFuncActRef() == NULL) - reads_from->setFuncActRef(HAS_REFERENCE); + // For read or rmw actions being used by ModelHistory, mark the reads_from as being used. + if (act->is_rmw()) { + void * func_act_ref = act->getFuncActRef(); + if (func_act_ref == WRITE_REFERENCED) { + // Only the write part of this rmw is referenced, do nothing + } else if (func_act_ref != NULL) { + // The read part of rmw is potentially referenced + ModelAction * reads_from = act->get_reads_from(); + if (reads_from->getFuncActRef() == NULL) + reads_from->setFuncActRef(WRITE_REFERENCED); + } + } else { + if (act->getFuncActRef() != NULL) { + ModelAction * reads_from = act->get_reads_from(); + if (reads_from->getFuncActRef() == NULL) + reads_from->setFuncActRef(WRITE_REFERENCED); + } } if (act->get_reads_from()->is_free()) { if (act->is_rmw()) { - if (act->getFuncActRef() != NULL) { - // Copy the original type if being used by ModelHistory - act->set_original_type(act->get_type()); - } + // Save the original action type + act->set_original_type(act->get_type()); //Weaken a RMW from a freed store to a write act->set_type(ATOMIC_WRITE); } else { @@ -1829,8 +1851,8 @@ void ModelExecution::collectActions() { fixupLastAct(act); } - //Only delete this action if not being using by ModelHistory. - //Otherwise, the deletion of action is deferred. + // Only delete this action if not being using by ModelHistory. + // Otherwise, the deletion of action is deferred. if (act->getFuncActRef() == NULL) { delete act; continue; @@ -1865,10 +1887,8 @@ void ModelExecution::collectActions() { if (act->is_read()) { if (act->get_reads_from()->is_free()) { if (act->is_rmw()) { - if (act->getFuncActRef() != NULL) { - // Copy the original type if being used by ModelHistory - act->set_original_type(act->get_type()); - } + // Save the original action type + act->set_original_type(act->get_type()); act->set_type(ATOMIC_WRITE); } else { removeAction(act); diff --git a/funcnode.cc b/funcnode.cc index 69d8b80e..63dd382b 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -184,7 +184,22 @@ void FuncNode::update_tree(action_list_t * act_list) for (sllnode * it = act_list->begin();it != NULL;it = it->getNext()) { ModelAction * act = it->getVal(); - act->setFuncActRef(NULL); // Remove func_act_ref so that this action can be removed + + // Only ATOMIC_RMW or ATOMIC_WRITE may be swapped with their original types, + // which are later added to rw_act_list. Therefore, it is safe to only revert + // back action types for actions in rw_act_list whose types have been swapped. + if (act->get_original_type() != ATOMIC_NOP && act->get_swap_flag() == false) + act->use_original_type(); + + // Remove func_act_ref so that actions can be deleted by Execution::collectActions + act->setFuncActRef(NULL); + if (act->is_read()) { + // For every read or rmw actions in this list, the reads_from is not deleted. + // So it is safe to call get_reads_from + ModelAction * rf = act->get_reads_from(); + rf->setFuncActRef(NULL); + } + FuncInst * func_inst = get_inst(act); void * loc = act->get_location(); @@ -223,12 +238,39 @@ void FuncNode::update_tree(action_list_t * act_list) } } -// model_print("function %s\n", func_name); -// print_val_loc_map(); - update_inst_tree(&inst_list); update_predicate_tree(&rw_act_list); + // Revert back action types and free + for (sllnode * it = act_list->begin(); it != NULL; it = it->getNext()) { + ModelAction * act = it->getVal(); + + // Revert back action types for actions whose types have been changed. + if (act->get_swap_flag() == true) + act->use_original_type(); + + /** Free actions + * case 1. READY_FREE -> delete + * case 2. Read action whose read from is READY_FREE -> delete both actions + * In both cases, the actions have already been removed from core model + * action lists. + */ + + /* Problematic: could double free actions + if (act->is_free()) { + model_print("delete free act %d\n", act->get_seq_number()); + delete act; + } else if (act->is_read()) { + ModelAction * rf = act->get_reads_from(); + if (rf->is_free()) { + model_print("delete act %d\n", act->get_seq_number()); + model_print("delete act %d\n", rf->get_seq_number()); + delete rf; + delete act; + } + }*/ + } + // print_predicate_tree(); } diff --git a/predicate.cc b/predicate.cc index f6454dbc..22fb0c7e 100644 --- a/predicate.cc +++ b/predicate.cc @@ -87,7 +87,8 @@ void Predicate::copy_predicate_expr(Predicate * other) */ Predicate * Predicate::follow_write_child(FuncInst * inst) { - ASSERT(inst->get_type() == ATOMIC_WRITE); + action_type type = inst->get_type(); + ASSERT(type == ATOMIC_WRITE || type == ATOMIC_INIT); for (uint i = 0;i < children.size();i++) { Predicate * child = children[i]; -- 2.34.1