From: weiyu Date: Thu, 30 Jan 2020 19:35:18 +0000 (-0800) Subject: Separate the marking algorithm and action removal algorithm X-Git-Url: http://demsky.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=fbed9b2aaf6ac4f928a59dd0dd885348dcb0eb4c Separate the marking algorithm and action removal algorithm --- diff --git a/action.cc b/action.cc index df73d209..89a61b74 100644 --- a/action.cc +++ b/action.cc @@ -623,7 +623,7 @@ uint64_t ModelAction::get_reads_from_value() const */ uint64_t ModelAction::get_write_value() const { - ASSERT(is_write() || is_free()); + ASSERT(is_write()); return value; } diff --git a/execution.cc b/execution.cc index 796e9b74..999a58f0 100644 --- a/execution.cc +++ b/execution.cc @@ -1755,27 +1755,6 @@ 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 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; if (act->is_write()) { write = act; @@ -1820,25 +1799,6 @@ void ModelExecution::collectActions() { } if (act->is_read()) { - // 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()) { // Save the original action type diff --git a/funcnode.cc b/funcnode.cc index 63dd382b..4172f417 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -185,20 +185,20 @@ void FuncNode::update_tree(action_list_t * act_list) for (sllnode * it = act_list->begin();it != NULL;it = it->getNext()) { ModelAction * act = it->getVal(); - // 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. + // For every read or rmw actions in this list, the reads_from was marked, and not deleted. // So it is safe to call get_reads_from ModelAction * rf = act->get_reads_from(); + if (rf->get_original_type() != ATOMIC_NOP && rf->get_swap_flag() == false) + rf->use_original_type(); + rf->setFuncActRef(NULL); } + act->setFuncActRef(NULL); FuncInst * func_inst = get_inst(act); void * loc = act->get_location(); @@ -242,33 +242,34 @@ void FuncNode::update_tree(action_list_t * act_list) update_predicate_tree(&rw_act_list); // Revert back action types and free - for (sllnode * it = act_list->begin(); it != NULL; it = it->getNext()) { + for (sllnode * it = act_list->begin(); it != NULL;) { ModelAction * act = it->getVal(); + // Do iteration early in case we delete act + it = it->getNext(); // Revert back action types for actions whose types have been changed. + if (act->is_read()) { + ModelAction * rf = act->get_reads_from(); + if (rf->get_swap_flag() == true) + rf->use_original_type(); + } + 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; + // TODO } 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; + if (act->is_rmw()) { + // reads_from can not be READY_FREE + } else { + ModelAction *rf = act->get_reads_from(); + if (rf->is_free()) { + model_print("delete read %d; %p\n", act->get_seq_number(), act); + delete act; + } } - }*/ + } } // print_predicate_tree(); diff --git a/history.cc b/history.cc index 32aacf70..d5179332 100644 --- a/history.cc +++ b/history.cc @@ -182,6 +182,15 @@ void ModelHistory::process_action(ModelAction *act, thread_id_t tid) /* Add to curr_inst_list */ act->setFuncActRef(curr_act_list->add_back(act)); + if (act->is_read()) { + ModelAction * rf = act->get_reads_from(); + void * func_act_ref = rf->getFuncActRef(); + if (func_act_ref == WRITE_REFERENCED) { + // do nothing + } else if (func_act_ref == NULL) { + rf->setFuncActRef(WRITE_REFERENCED); + } + } FuncNode * func_node = func_nodes[func_id]; func_node->add_inst(act);