From 39657d7de68ca06c1c3064d52c025aacdd8a9add Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Wed, 13 Apr 2016 12:45:26 +0200 Subject: [PATCH] [mc] Delegate some part of Session::logState() to Checker::logState() This separates the Checker-specific code from the generic/shared code. The session should not need to know about every existing Checker. --- examples/smpi/mc/only_send_deterministic.tesh | 18 +++++----- src/mc/Checker.cpp | 5 +++ src/mc/Checker.hpp | 1 + src/mc/CommunicationDeterminismChecker.cpp | 29 ++++++++++++++++ src/mc/CommunicationDeterminismChecker.hpp | 1 + src/mc/LivenessChecker.cpp | 8 +++++ src/mc/LivenessChecker.hpp | 1 + src/mc/SafetyChecker.cpp | 8 +++++ src/mc/SafetyChecker.hpp | 1 + src/mc/Session.cpp | 33 ++----------------- 10 files changed, 65 insertions(+), 40 deletions(-) diff --git a/examples/smpi/mc/only_send_deterministic.tesh b/examples/smpi/mc/only_send_deterministic.tesh index 97b804e550..10cdd9a736 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_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 +> [0.000000] [mc_comm_determinism/INFO] ****************************************************** +> [0.000000] [mc_comm_determinism/INFO] **** Only-send-deterministic communication pattern **** +> [0.000000] [mc_comm_determinism/INFO] ****************************************************** +> [0.000000] [mc_comm_determinism/INFO] The recv communications pattern of the process 0 is different! Different source for communication #2 +> [0.000000] [mc_comm_determinism/INFO] Expanded states = 520 +> [0.000000] [mc_comm_determinism/INFO] Visited states = 1476 +> [0.000000] [mc_comm_determinism/INFO] Executed transitions = 1312 +> [0.000000] [mc_comm_determinism/INFO] Send-deterministic : Yes +> [0.000000] [mc_comm_determinism/INFO] Recv-deterministic : No diff --git a/src/mc/Checker.cpp b/src/mc/Checker.cpp index 1fefd9d3df..6ae0aae946 100644 --- a/src/mc/Checker.cpp +++ b/src/mc/Checker.cpp @@ -37,5 +37,10 @@ std::vector Checker::getTextualTrace() return {}; } +// virtual +void Checker::logState() +{ +} + } } diff --git a/src/mc/Checker.hpp b/src/mc/Checker.hpp index 8f7e0cc2e6..58fa3d63ea 100644 --- a/src/mc/Checker.hpp +++ b/src/mc/Checker.hpp @@ -48,6 +48,7 @@ public: */ virtual RecordTrace getRecordTrace(); virtual std::vector getTextualTrace(); + virtual void logState(); protected: Session& getSession() { return *session_; } diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index 57a8ee8d34..e5b383d922 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -326,6 +326,35 @@ std::vector CommunicationDeterminismChecker::getTextualTrace() // o return trace; } +void CommunicationDeterminismChecker::logState() // override +{ + Checker::logState(); + if (_sg_mc_comms_determinism && + !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(_sg_mc_comms_determinism && + !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); + } + XBT_INFO("Expanded states = %lu", mc_stats->expanded_states); + XBT_INFO("Visited states = %lu", mc_stats->visited_states); + XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions); + if (simgrid::mc::initial_global_state != nullptr) + XBT_INFO("Send-deterministic : %s", + !simgrid::mc::initial_global_state->send_deterministic ? "No" : "Yes"); + if (simgrid::mc::initial_global_state != nullptr && _sg_mc_comms_determinism) + XBT_INFO("Recv-deterministic : %s", + !simgrid::mc::initial_global_state->recv_deterministic ? "No" : "Yes"); +} + void CommunicationDeterminismChecker::prepare() { diff --git a/src/mc/CommunicationDeterminismChecker.hpp b/src/mc/CommunicationDeterminismChecker.hpp index bd30d0435e..291d98ec4f 100644 --- a/src/mc/CommunicationDeterminismChecker.hpp +++ b/src/mc/CommunicationDeterminismChecker.hpp @@ -29,6 +29,7 @@ public: private: void prepare(); int main(); + void logState() override; private: /** Stack representing the position in the exploration graph */ std::list> stack_; diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index 39f6bdb719..15a0a731e3 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -301,6 +301,14 @@ RecordTrace LivenessChecker::getRecordTrace() // override return res; } +void LivenessChecker::logState() // override +{ + Checker::logState(); + 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); +} + void LivenessChecker::showAcceptanceCycle(std::size_t depth) { XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*"); diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp index 7ce79cea7f..2c482ade18 100644 --- a/src/mc/LivenessChecker.hpp +++ b/src/mc/LivenessChecker.hpp @@ -68,6 +68,7 @@ public: int run() override; RecordTrace getRecordTrace() override; std::vector getTextualTrace() override; + void logState() override; private: int main(); void prepare(); diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index 28cfb9bf54..b51d39adae 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -87,6 +87,14 @@ std::vector SafetyChecker::getTextualTrace() // override return trace; } +void SafetyChecker::logState() // override +{ + Checker::logState(); + XBT_INFO("Expanded states = %lu", mc_stats->expanded_states); + XBT_INFO("Visited states = %lu", mc_stats->visited_states); + XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions); +} + int SafetyChecker::run() { this->init(); diff --git a/src/mc/SafetyChecker.hpp b/src/mc/SafetyChecker.hpp index 8d237cea3e..a9662be45b 100644 --- a/src/mc/SafetyChecker.hpp +++ b/src/mc/SafetyChecker.hpp @@ -27,6 +27,7 @@ public: int run() override; RecordTrace getRecordTrace() override; std::vector getTextualTrace() override; + void logState() override; private: // Temp void init(); diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp index e600b30222..1bb2878b62 100644 --- a/src/mc/Session.cpp +++ b/src/mc/Session.cpp @@ -18,6 +18,7 @@ #include "src/mc/Session.hpp" #include "src/mc/mc_state.h" #include "src/mc/mc_private.h" +#include "src/mc/Checker.hpp" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session"); @@ -106,42 +107,12 @@ void Session::execute(Transition const& transition) 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); - } - } + mc_model_checker->getChecker()->logState(); - 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); -- 2.20.1