From 9151772f7b6bba10099b552d18cde911aeb39c76 Mon Sep 17 00:00:00 2001 From: root Date: Wed, 25 Dec 2019 16:52:47 -0800 Subject: [PATCH] Fix bug --- execution.cc | 20 +++++++++----------- execution.h | 2 +- model.cc | 2 +- 3 files changed, 11 insertions(+), 13 deletions(-) diff --git a/execution.cc b/execution.cc index cd277c55..9b179880 100644 --- a/execution.cc +++ b/execution.cc @@ -283,7 +283,7 @@ ModelAction * ModelExecution::convertNonAtomicStore(void * location) { * Processes a read model action. * @param curr is the read model action to process. * @param rf_set is the set of model actions we can possibly read from - * @return True if processing this read updates the mo_graph. + * @return True if the read can be pruned from the thread map list. */ bool ModelExecution::process_read(ModelAction *curr, SnapVector * rf_set) { @@ -320,12 +320,7 @@ bool ModelExecution::process_read(ModelAction *curr, SnapVector * read_from(curr, rf); get_thread(curr)->set_return_value(curr->get_return_value()); delete priorset; - if (canprune && curr->get_type() == ATOMIC_READ) { - int tid = id_to_int(curr->get_tid()); - (*obj_thrd_map.get(curr->get_location()))[tid].pop_back(); - curr->setThrdMapRef(NULL); - } - return true; + return canprune && curr->get_type() == ATOMIC_READ; } priorset->clear(); (*rf_set)[index] = rf_set->back(); @@ -728,15 +723,17 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (newly_explored && curr->is_read()) rf_set = build_may_read_from(curr); + bool canprune = false; + if (curr->is_read() && !second_part_of_rmw) { - process_read(curr, rf_set); + canprune = process_read(curr, rf_set); delete rf_set; } else ASSERT(rf_set == NULL); /* Add the action to lists */ if (!second_part_of_rmw) - add_action_to_lists(curr); + add_action_to_lists(curr, canprune); if (curr->is_write()) add_write_to_lists(curr); @@ -1118,7 +1115,7 @@ ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const { * * @param act is the ModelAction to add. */ -void ModelExecution::add_action_to_lists(ModelAction *act) +void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune) { int tid = id_to_int(act->get_tid()); if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) { @@ -1138,7 +1135,8 @@ void ModelExecution::add_action_to_lists(ModelAction *act) for(uint i = oldsize;i < priv->next_thread_id;i++) new (&(*vec)[i]) action_list_t(); } - act->setThrdMapRef((*vec)[tid].add_back(act)); + if (!canprune) + act->setThrdMapRef((*vec)[tid].add_back(act)); // Update thrd_last_action, the last action taken by each thread if ((int)thrd_last_action.size() <= tid) diff --git a/execution.h b/execution.h index 2d227d21..72efcd67 100644 --- a/execution.h +++ b/execution.h @@ -109,7 +109,7 @@ private: void process_thread_action(ModelAction *curr); void read_from(ModelAction *act, ModelAction *rf); bool synchronize(const ModelAction *first, ModelAction *second); - void add_action_to_lists(ModelAction *act); + void add_action_to_lists(ModelAction *act, bool canprune); void add_normal_write_to_lists(ModelAction *act); void add_write_to_lists(ModelAction *act); ModelAction * get_last_fence_release(thread_id_t tid) const; diff --git a/model.cc b/model.cc index 4f8a0324..d1e94e5e 100644 --- a/model.cc +++ b/model.cc @@ -261,7 +261,7 @@ void ModelChecker::finish_execution(bool more_executions) // test code execution_number ++; if (more_executions) - reset_to_initial_state(); + reset_to_initial_state(); history->set_new_exec_flag(); } -- 2.34.1