From 082cedd275c8f6dc3478097595380d3e496c74f6 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Wed, 23 Mar 2016 12:29:49 +0100 Subject: [PATCH] [mc] Remove some globals from is_visted_state() --- src/include/mc/mc.h | 1 - src/mc/SafetyChecker.cpp | 4 +--- src/mc/mc_comm_determinism.cpp | 23 ++++++++++++++++++++++- src/mc/mc_config.cpp | 1 - src/mc/mc_safety.h | 2 +- src/mc/mc_visited.cpp | 32 ++------------------------------ 6 files changed, 26 insertions(+), 37 deletions(-) diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index d6352f567c..74c6ed8fa2 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -44,7 +44,6 @@ extern XBT_PUBLIC(int) _sg_mc_visited; extern XBT_PRIVATE char* _sg_mc_dot_output_file; extern XBT_PUBLIC(int) _sg_mc_comms_determinism; extern XBT_PUBLIC(int) _sg_mc_send_determinism; -extern XBT_PRIVATE int _sg_mc_safety; extern XBT_PRIVATE int _sg_mc_liveness; extern XBT_PRIVATE int _sg_mc_snapshot_fds; extern XBT_PRIVATE int _sg_mc_termination; diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index ea0b775153..442b871eed 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -128,7 +128,7 @@ int SafetyChecker::run() return SIMGRID_MC_EXIT_NON_TERMINATION; } - if ((visited_state = simgrid::mc::is_visited_state(next_state)) == nullptr) { + if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, true)) == nullptr) { /* Get an enabled process and insert it in the interleave set of the next state */ for (auto& p : mc_model_checker->process().simix_processes()) @@ -262,8 +262,6 @@ void SafetyChecker::init() else if (reductionMode_ == simgrid::mc::ReductionMode::unset) reductionMode_ = simgrid::mc::ReductionMode::dpor; - _sg_mc_safety = 1; - if (_sg_mc_termination) XBT_INFO("Check non progressive cycles"); else diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp index 7e7d2b1814..54fe76e0f8 100644 --- a/src/mc/mc_comm_determinism.cpp +++ b/src/mc/mc_comm_determinism.cpp @@ -337,6 +337,20 @@ static void MC_pre_modelcheck_comm_determinism(void) xbt_fifo_unshift(mc_stack, initial_state); } +static inline +bool all_communications_are_finished() +{ + for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) { + xbt_dynar_t pattern = xbt_dynar_get_as( + incomplete_communications_pattern, current_process, xbt_dynar_t); + if (!xbt_dynar_is_empty(pattern)) { + XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited."); + return false; + } + } + return true; +} + static int MC_modelcheck_comm_determinism_main(void) { @@ -392,7 +406,14 @@ static int MC_modelcheck_comm_determinism_main(void) /* Create the new expanded state */ next_state = MC_state_new(); - if ((visited_state = simgrid::mc::is_visited_state(next_state)) == nullptr) { + /* If comm determinism verification, we cannot stop the exploration if + some communications are not finished (at least, data are transfered). + These communications are incomplete and they cannot be analyzed and + compared with the initial pattern. */ + bool compare_snapshots = all_communications_are_finished() + && initial_global_state->initial_communications_pattern_done; + + if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, compare_snapshots)) == nullptr) { /* Get enabled processes and insert them in the interleave set of the next state */ for (auto& p : mc_model_checker->process().simix_processes()) diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index 58a6b3146a..eadc3704cc 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -61,7 +61,6 @@ int _sg_mc_visited = 0; char *_sg_mc_dot_output_file = nullptr; int _sg_mc_comms_determinism = 0; int _sg_mc_send_determinism = 0; -int _sg_mc_safety = 0; int _sg_mc_liveness = 0; int _sg_mc_snapshot_fds = 0; int _sg_mc_termination = 0; diff --git a/src/mc/mc_safety.h b/src/mc/mc_safety.h index 0bbe379011..4ee245f647 100644 --- a/src/mc/mc_safety.h +++ b/src/mc/mc_safety.h @@ -43,7 +43,7 @@ struct XBT_PRIVATE VisitedState { }; extern XBT_PRIVATE std::vector> visited_states; -XBT_PRIVATE std::unique_ptr is_visited_state(mc_state_t graph_state); +XBT_PRIVATE std::unique_ptr is_visited_state(mc_state_t graph_state, bool compare_snpashots); XBT_PRIVATE int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::VisitedState* state2); } diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp index 11687b19d7..6f136ec18d 100644 --- a/src/mc/mc_visited.cpp +++ b/src/mc/mc_visited.cpp @@ -116,26 +116,6 @@ VisitedPair::~VisitedPair() MC_state_delete(this->graph_state, 1); } -} -} - -static -bool some_communications_are_not_finished() -{ - for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) { - xbt_dynar_t pattern = xbt_dynar_get_as( - incomplete_communications_pattern, current_process, xbt_dynar_t); - if (!xbt_dynar_is_empty(pattern)) { - XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited."); - return true; - } - } - return false; -} - -namespace simgrid { -namespace mc { - static void prune_visited_states() { while (visited_states.size() > (std::size_t) _sg_mc_visited) { @@ -154,16 +134,9 @@ static void prune_visited_states() /** * \brief Checks whether a given state has already been visited by the algorithm. */ -std::unique_ptr is_visited_state(mc_state_t graph_state) +std::unique_ptr is_visited_state(mc_state_t graph_state, bool compare_snpashots) { - if (_sg_mc_visited == 0) - return nullptr; - /* If comm determinism verification, we cannot stop the exploration if some - communications are not finished (at least, data are transfered). These communications - are incomplete and they cannot be analyzed and compared with the initial pattern. */ - int partial_comm = (_sg_mc_comms_determinism || _sg_mc_send_determinism) && - some_communications_are_not_finished(); std::unique_ptr new_state = std::unique_ptr(new VisitedState()); @@ -174,8 +147,7 @@ std::unique_ptr is_visited_state(mc_state_t graph_sta auto range = std::equal_range(visited_states.begin(), visited_states.end(), new_state.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap()); - if (_sg_mc_safety || (!partial_comm - && initial_global_state->initial_communications_pattern_done)) { + if (compare_snpashots) { for (auto i = range.first; i != range.second; ++i) { auto& visited_state = *i; -- 2.20.1