From 37628abb1a6de84ea9ddee484632b6a9d6245c96 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Wed, 13 Apr 2016 12:26:49 +0200 Subject: [PATCH] [mc] Move MC_print_statistics() as Session::logState() --- examples/smpi/mc/only_send_deterministic.tesh | 18 +++---- src/mc/CommunicationDeterminismChecker.cpp | 6 +-- src/mc/LivenessChecker.cpp | 4 +- src/mc/SafetyChecker.cpp | 4 +- src/mc/Session.cpp | 48 ++++++++++++++++++ src/mc/Session.hpp | 1 + src/mc/mc_global.cpp | 50 ++----------------- src/mc/mc_private.h | 2 - 8 files changed, 68 insertions(+), 65 deletions(-) diff --git a/examples/smpi/mc/only_send_deterministic.tesh b/examples/smpi/mc/only_send_deterministic.tesh index c7993f4453..97b804e550 100644 --- a/examples/smpi/mc/only_send_deterministic.tesh +++ b/examples/smpi/mc/only_send_deterministic.tesh @@ -3,12 +3,12 @@ ! timeout 60 $ ../../../smpi_script/bin/smpirun -wrapper "${bindir:=.}/../../../bin/simgrid-mc" --log=xbt_cfg.thresh:warning -hostfile ${srcdir:=.}/hostfile_only_send_deterministic -platform ${srcdir:=.}/../../platforms/cluster.xml --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thresh:0 --cfg=smpi/running_power:1e9 ./smpi_only_send_deterministic > [0.000000] [mc_comm_determinism/INFO] Check communication determinism -> [0.000000] [mc_global/INFO] ****************************************************** -> [0.000000] [mc_global/INFO] **** Only-send-deterministic communication pattern **** -> [0.000000] [mc_global/INFO] ****************************************************** -> [0.000000] [mc_global/INFO] The recv communications pattern of the process 0 is different! Different source for communication #2 -> [0.000000] [mc_global/INFO] Expanded states = 520 -> [0.000000] [mc_global/INFO] Visited states = 1476 -> [0.000000] [mc_global/INFO] Executed transitions = 1312 -> [0.000000] [mc_global/INFO] Send-deterministic : Yes -> [0.000000] [mc_global/INFO] Recv-deterministic : No +> [0.000000] [mc_Session/INFO] ****************************************************** +> [0.000000] [mc_Session/INFO] **** Only-send-deterministic communication pattern **** +> [0.000000] [mc_Session/INFO] ****************************************************** +> [0.000000] [mc_Session/INFO] The recv communications pattern of the process 0 is different! Different source for communication #2 +> [0.000000] [mc_Session/INFO] Expanded states = 520 +> [0.000000] [mc_Session/INFO] Visited states = 1476 +> [0.000000] [mc_Session/INFO] Executed transitions = 1312 +> [0.000000] [mc_Session/INFO] Send-deterministic : Yes +> [0.000000] [mc_Session/INFO] Recv-deterministic : No diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index 2b20a33cf5..57a8ee8d34 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -144,7 +144,7 @@ static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunic XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff); xbt_free(simgrid::mc::initial_global_state->send_diff); simgrid::mc::initial_global_state->send_diff = nullptr; - MC_print_statistics(mc_stats); + simgrid::mc::session->logState(); mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM); }else if(_sg_mc_comms_determinism && (!simgrid::mc::initial_global_state->send_deterministic @@ -158,7 +158,7 @@ static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunic simgrid::mc::initial_global_state->send_diff = nullptr; xbt_free(simgrid::mc::initial_global_state->recv_diff); simgrid::mc::initial_global_state->recv_diff = nullptr; - MC_print_statistics(mc_stats); + simgrid::mc::session->logState(); mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM); } } @@ -503,7 +503,7 @@ int CommunicationDeterminismChecker::main(void) } } - MC_print_statistics(mc_stats); + simgrid::mc::session->logState(); return SIMGRID_MC_EXIT_SUCCESS; } diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index 537dd9bf74..39f6bdb719 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -310,7 +310,7 @@ void LivenessChecker::showAcceptanceCycle(std::size_t depth) simgrid::mc::dumpRecordPath(); for (auto& s : this->getTextualTrace()) XBT_INFO("%s", s.c_str()); - MC_print_statistics(mc_stats); + simgrid::mc::session->logState(); XBT_INFO("Counter-example depth : %zd", depth); } @@ -422,7 +422,7 @@ int LivenessChecker::main(void) } XBT_INFO("No property violation found."); - MC_print_statistics(mc_stats); + simgrid::mc::session->logState(); return SIMGRID_MC_EXIT_SUCCESS; } diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index d565169835..28cfb9bf54 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -43,7 +43,7 @@ static void MC_show_non_termination(void) XBT_INFO("Counter-example execution trace:"); for (auto& s : mc_model_checker->getChecker()->getTextualTrace()) XBT_INFO("%s", s.c_str()); - MC_print_statistics(mc_stats); + simgrid::mc::session->logState(); } static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2) @@ -165,7 +165,7 @@ int SafetyChecker::run() } XBT_INFO("No property violation found."); - MC_print_statistics(mc_stats); + simgrid::mc::session->logState(); initial_global_state = nullptr; return SIMGRID_MC_EXIT_SUCCESS; } diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp index 842fa3c86a..e600b30222 100644 --- a/src/mc/Session.cpp +++ b/src/mc/Session.cpp @@ -9,11 +9,15 @@ #include +#include #include #include #include +#include #include "src/mc/Session.hpp" +#include "src/mc/mc_state.h" +#include "src/mc/mc_private.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session"); @@ -100,6 +104,50 @@ void Session::execute(Transition const& transition) modelChecker_->wait_for_requests(); } +void Session::logState() +{ + if(_sg_mc_comms_determinism) { + if (!simgrid::mc::initial_global_state->recv_deterministic && + simgrid::mc::initial_global_state->send_deterministic){ + XBT_INFO("******************************************************"); + XBT_INFO("**** Only-send-deterministic communication pattern ****"); + XBT_INFO("******************************************************"); + XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff); + }else if(!simgrid::mc::initial_global_state->send_deterministic && + simgrid::mc::initial_global_state->recv_deterministic) { + XBT_INFO("******************************************************"); + XBT_INFO("**** Only-recv-deterministic communication pattern ****"); + XBT_INFO("******************************************************"); + XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff); + } + } + + if (mc_stats->expanded_pairs == 0) { + XBT_INFO("Expanded states = %lu", mc_stats->expanded_states); + XBT_INFO("Visited states = %lu", mc_stats->visited_states); + } else { + XBT_INFO("Expanded pairs = %lu", mc_stats->expanded_pairs); + XBT_INFO("Visited pairs = %lu", mc_stats->visited_pairs); + } + XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions); + if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0')) { + fprintf(dot_output, "}\n"); + fclose(dot_output); + } + if (simgrid::mc::initial_global_state != nullptr + && (_sg_mc_comms_determinism || _sg_mc_send_determinism)) { + XBT_INFO("Send-deterministic : %s", + !simgrid::mc::initial_global_state->send_deterministic ? "No" : "Yes"); + if (_sg_mc_comms_determinism) + XBT_INFO("Recv-deterministic : %s", + !simgrid::mc::initial_global_state->recv_deterministic ? "No" : "Yes"); + } + if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")){ + int ret=system("free"); + if(ret!=0)XBT_WARN("system call did not return 0, but %d",ret); + } +} + // static Session* Session::fork(std::function code) { diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp index 23e3eaa6f2..dd2e031b99 100644 --- a/src/mc/Session.hpp +++ b/src/mc/Session.hpp @@ -51,6 +51,7 @@ public: public: void execute(Transition const& transition); + void logState(); public: // static constructors diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index 5ad3660d61..630adb9fe8 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -208,51 +208,7 @@ void MC_show_deadlock(void) XBT_INFO("Counter-example execution trace:"); for (auto& s : mc_model_checker->getChecker()->getTextualTrace()) XBT_INFO("%s", s.c_str()); - MC_print_statistics(mc_stats); -} - -void MC_print_statistics(mc_stats_t stats) -{ - if(_sg_mc_comms_determinism) { - if (!simgrid::mc::initial_global_state->recv_deterministic && - simgrid::mc::initial_global_state->send_deterministic){ - XBT_INFO("******************************************************"); - XBT_INFO("**** Only-send-deterministic communication pattern ****"); - XBT_INFO("******************************************************"); - XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff); - }else if(!simgrid::mc::initial_global_state->send_deterministic && - simgrid::mc::initial_global_state->recv_deterministic) { - XBT_INFO("******************************************************"); - XBT_INFO("**** Only-recv-deterministic communication pattern ****"); - XBT_INFO("******************************************************"); - XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff); - } - } - - if (stats->expanded_pairs == 0) { - XBT_INFO("Expanded states = %lu", stats->expanded_states); - XBT_INFO("Visited states = %lu", stats->visited_states); - } else { - XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs); - XBT_INFO("Visited pairs = %lu", stats->visited_pairs); - } - XBT_INFO("Executed transitions = %lu", stats->executed_transitions); - if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0')) { - fprintf(dot_output, "}\n"); - fclose(dot_output); - } - if (simgrid::mc::initial_global_state != nullptr - && (_sg_mc_comms_determinism || _sg_mc_send_determinism)) { - XBT_INFO("Send-deterministic : %s", - !simgrid::mc::initial_global_state->send_deterministic ? "No" : "Yes"); - if (_sg_mc_comms_determinism) - XBT_INFO("Recv-deterministic : %s", - !simgrid::mc::initial_global_state->recv_deterministic ? "No" : "Yes"); - } - if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")){ - int ret=system("free"); - if(ret!=0)XBT_WARN("system call did not return 0, but %d",ret); - } + simgrid::mc::session->logState(); } void MC_automaton_load(const char *file) @@ -341,7 +297,7 @@ void MC_report_assertion_error(void) simgrid::mc::dumpRecordPath(); for (auto& s : mc_model_checker->getChecker()->getTextualTrace()) XBT_INFO("%s", s.c_str()); - MC_print_statistics(mc_stats); + simgrid::mc::session->logState(); } void MC_report_crash(int status) @@ -361,7 +317,7 @@ void MC_report_crash(int status) simgrid::mc::dumpRecordPath(); for (auto& s : mc_model_checker->getChecker()->getTextualTrace()) XBT_INFO("%s", s.c_str()); - MC_print_statistics(mc_stats); + simgrid::mc::session->logState(); XBT_INFO("Stack trace:"); mc_model_checker->process().dumpStack(); } diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index ceaf9c1bfc..143aac7dbf 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -77,8 +77,6 @@ typedef struct mc_stats { XBT_PRIVATE extern mc_stats_t mc_stats; -XBT_PRIVATE void MC_print_statistics(mc_stats_t stats); - /********************************** Snapshot comparison **********************************/ //#define MC_DEBUG 1 -- 2.20.1