From b1d63a0675cd3977c8da862007ba8461ca10db88 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Mon, 21 Mar 2016 17:10:03 +0100 Subject: [PATCH 1/1] [mc] Move MC_replay_liveness() as a static function of mc_liveness.c --- src/mc/mc_global.cpp | 67 ------------------------------------------ src/mc/mc_liveness.cpp | 67 ++++++++++++++++++++++++++++++++++++++++++ src/mc/mc_private.h | 1 - 3 files changed, 67 insertions(+), 68 deletions(-) diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index e92fcaf53b..dbd46774bf 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -223,73 +223,6 @@ void MC_replay(xbt_fifo_t stack) XBT_DEBUG("**** End Replay ****"); } -void MC_replay_liveness(xbt_fifo_t stack) -{ - xbt_fifo_item_t item; - simgrid::mc::Pair* pair = nullptr; - mc_state_t state = nullptr; - smx_simcall_t req = nullptr, saved_req = NULL; - int value, depth = 1; - char *req_str; - - XBT_DEBUG("**** Begin Replay ****"); - - /* Intermediate backtracking */ - if(_sg_mc_checkpoint > 0) { - item = xbt_fifo_get_first_item(stack); - pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item); - if(pair->graph_state->system_state){ - simgrid::mc::restore_snapshot(pair->graph_state->system_state); - return; - } - } - - /* Restore the initial state */ - simgrid::mc::restore_snapshot(initial_global_state->snapshot); - - /* Traverse the stack from the initial state and re-execute the transitions */ - for (item = xbt_fifo_get_last_item(stack); - item != xbt_fifo_get_first_item(stack); - item = xbt_fifo_get_prev_item(item)) { - - pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item); - - state = (mc_state_t) pair->graph_state; - - if (pair->exploration_started) { - - saved_req = MC_state_get_executed_request(state, &value); - - if (saved_req != nullptr) { - /* because we got a copy of the executed request, we have to fetch the - real one, pointed by the request field of the issuer process */ - const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); - req = &issuer->simcall; - - /* Debug information */ - if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) { - req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix); - XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state); - xbt_free(req_str); - } - - } - - simgrid::mc::handle_simcall(req, value); - mc_model_checker->wait_for_requests(); - } - - /* Update statistics */ - mc_stats->visited_pairs++; - mc_stats->executed_transitions++; - - depth++; - - } - - XBT_DEBUG("**** End Replay ****"); -} - /** * \brief Dumps the contents of a model-checker's stack and shows the actual * execution trace diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp index edf700d15d..2266c832f5 100644 --- a/src/mc/mc_liveness.cpp +++ b/src/mc/mc_liveness.cpp @@ -207,6 +207,73 @@ static void MC_pre_modelcheck_liveness(void) } } +static void MC_replay_liveness(xbt_fifo_t stack) +{ + xbt_fifo_item_t item; + simgrid::mc::Pair* pair = nullptr; + mc_state_t state = nullptr; + smx_simcall_t req = nullptr, saved_req = NULL; + int value, depth = 1; + char *req_str; + + XBT_DEBUG("**** Begin Replay ****"); + + /* Intermediate backtracking */ + if(_sg_mc_checkpoint > 0) { + item = xbt_fifo_get_first_item(stack); + pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item); + if(pair->graph_state->system_state){ + simgrid::mc::restore_snapshot(pair->graph_state->system_state); + return; + } + } + + /* Restore the initial state */ + simgrid::mc::restore_snapshot(initial_global_state->snapshot); + + /* Traverse the stack from the initial state and re-execute the transitions */ + for (item = xbt_fifo_get_last_item(stack); + item != xbt_fifo_get_first_item(stack); + item = xbt_fifo_get_prev_item(item)) { + + pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item); + + state = (mc_state_t) pair->graph_state; + + if (pair->exploration_started) { + + saved_req = MC_state_get_executed_request(state, &value); + + if (saved_req != nullptr) { + /* because we got a copy of the executed request, we have to fetch the + real one, pointed by the request field of the issuer process */ + const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); + req = &issuer->simcall; + + /* Debug information */ + if (XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)) { + req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix); + XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state); + xbt_free(req_str); + } + + } + + simgrid::mc::handle_simcall(req, value); + mc_model_checker->wait_for_requests(); + } + + /* Update statistics */ + mc_stats->visited_pairs++; + mc_stats->executed_transitions++; + + depth++; + + } + + XBT_DEBUG("**** End Replay ****"); +} + static int MC_modelcheck_liveness_main(void) { simgrid::mc::Pair* current_pair = nullptr; diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 869042cdf6..28f1178c21 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -48,7 +48,6 @@ XBT_PRIVATE extern FILE *dot_output; XBT_PRIVATE extern int user_max_depth_reached; XBT_PRIVATE void MC_replay(xbt_fifo_t stack); -XBT_PRIVATE void MC_replay_liveness(xbt_fifo_t stack); XBT_PRIVATE void MC_show_deadlock(smx_simcall_t req); XBT_PRIVATE void MC_show_stack_safety(xbt_fifo_t stack); XBT_PRIVATE void MC_dump_stack_safety(xbt_fifo_t stack); -- 2.20.1