From: Martin Quinson Date: Fri, 18 Feb 2022 22:13:26 +0000 (+0100) Subject: Make CommDet a plugin on top of Safety X-Git-Tag: v3.31~374 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/97e5210852e84ebe84d8344987fa1b92b1d369fa Make CommDet a plugin on top of Safety --- diff --git a/ChangeLog b/ChangeLog index 687a3c5086..e2a31854bb 100644 --- a/ChangeLog +++ b/ChangeLog @@ -2,6 +2,8 @@ SimGrid (3.30.1) NOT RELEASED YET (v3.31 expected March 20. 2022, 15:33 UTC) MC: - Rework the internals, for simpler and modern code. This shall unlock many future improvements. + - You can now define plugins onto SafetyChecker (a simple DFS explorer), using the declared signals. + See CommunicationDeterminism for an example. SMPI: - fix for FG#100 by ensuring small asynchronous messages never overtake larger diff --git a/MANIFEST.in b/MANIFEST.in index 69f054611a..08f5b112ee 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -2347,7 +2347,6 @@ include src/mc/api/TransitionComm.cpp include src/mc/api/TransitionComm.hpp include src/mc/checker/Checker.hpp include src/mc/checker/CommunicationDeterminismChecker.cpp -include src/mc/checker/CommunicationDeterminismChecker.hpp include src/mc/checker/LivenessChecker.cpp include src/mc/checker/LivenessChecker.hpp include src/mc/checker/SafetyChecker.cpp diff --git a/examples/smpi/mc/only_send_deterministic.c b/examples/smpi/mc/only_send_deterministic.c index f828daf54c..fcb11e1b79 100644 --- a/examples/smpi/mc/only_send_deterministic.c +++ b/examples/smpi/mc/only_send_deterministic.c @@ -1,14 +1,12 @@ /* ../../../smpi_script/bin/smpirun -hostfile hostfile_send_deterministic -platform ../../platforms/cluster_backbone.xml -np 3 --cfg=smpi/send-is-detached-thresh:0 gdb\ --args\ ./send_deterministic */ -/* Copyright (c) 2009-2022. The SimGrid Team. - * All rights reserved. */ +/* Copyright (c) 2009-2022. The SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ #include #include -#include int main(int argc, char **argv) { diff --git a/examples/smpi/mc/only_send_deterministic.tesh b/examples/smpi/mc/only_send_deterministic.tesh index a32552cba7..03b63b6971 100644 --- a/examples/smpi/mc/only_send_deterministic.tesh +++ b/examples/smpi/mc/only_send_deterministic.tesh @@ -2,13 +2,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_backbone.xml --cfg=model-check/communications-determinism:1 --cfg=smpi/buffering:zero --cfg=smpi/host-speed:1Gf ./smpi_only_send_deterministic +> [0.000000] [mc_safety/INFO] Start a DFS exploration. Reduction is: dpor. > [0.000000] [mc_comm_determinism/INFO] Check communication determinism > [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 = 519 +> [0.000000] [mc_comm_determinism/INFO] The recv communications pattern of the actor 0 is different! Different source for communication #1 > [0.000000] [mc_comm_determinism/INFO] Send-deterministic : Yes > [0.000000] [mc_comm_determinism/INFO] Recv-deterministic : No +> [0.000000] [mc_safety/INFO] DFS exploration successful. 36 unique states visited; 13 backtracks (97 transition replays, 49 states visited overall) \ No newline at end of file diff --git a/include/simgrid/forward.h b/include/simgrid/forward.h index e9f6f61676..88f7a95201 100644 --- a/include/simgrid/forward.h +++ b/include/simgrid/forward.h @@ -195,7 +195,6 @@ class Profile; } // namespace profile } // namespace kernel namespace mc { -class CommunicationDeterminismChecker; class State; } } // namespace simgrid diff --git a/src/kernel/activity/MailboxImpl.hpp b/src/kernel/activity/MailboxImpl.hpp index 33fd74bd1d..3247b0573e 100644 --- a/src/kernel/activity/MailboxImpl.hpp +++ b/src/kernel/activity/MailboxImpl.hpp @@ -34,7 +34,6 @@ class MailboxImpl { friend s4u::Mailbox; friend s4u::Mailbox* s4u::Engine::mailbox_by_name_or_create(const std::string& name) const; friend s4u::Mailbox* s4u::Mailbox::by_name(const std::string& name); - friend mc::CommunicationDeterminismChecker; static unsigned next_id_; // Next ID to be given const unsigned id_ = next_id_++; diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index 68117addc8..042bd34dfe 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -3,10 +3,10 @@ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ -#include "src/mc/checker/CommunicationDeterminismChecker.hpp" #include "src/kernel/activity/MailboxImpl.hpp" #include "src/mc/Session.hpp" #include "src/mc/api/TransitionComm.hpp" +#include "src/mc/checker/SafetyChecker.hpp" #include "src/mc/mc_config.hpp" #include "src/mc/mc_exit.hpp" #include "src/mc/mc_private.hpp" @@ -65,14 +65,6 @@ struct PatternCommunicationList { struct CommDetExtension { static simgrid::xbt::Extension EXTENSION_ID; - CommDetExtension() - { - const unsigned long maxpid = api::get().get_maxpid(); - - initial_communications_pattern.resize(maxpid); - incomplete_communications_pattern.resize(maxpid); - } - std::vector initial_communications_pattern; std::vector> incomplete_communications_pattern; @@ -82,6 +74,13 @@ struct CommDetExtension { std::string send_diff; std::string recv_diff; + void exploration_start() + { + const unsigned long maxpid = api::get().get_maxpid(); + + initial_communications_pattern.resize(maxpid); + incomplete_communications_pattern.resize(maxpid); + } void restore_communications_pattern(const simgrid::mc::State* state); void enforce_deterministic_pattern(aid_t process, const PatternCommunication* comm); void get_comm_pattern(const Transition* transition); @@ -149,16 +148,16 @@ void CommDetExtension::restore_communications_pattern(const simgrid::mc::State* } } -static std::string print_determinism_result(simgrid::mc::CommPatternDifference diff, aid_t process, +static std::string print_determinism_result(simgrid::mc::CommPatternDifference diff, aid_t actor, const simgrid::mc::PatternCommunication* comm, unsigned int cursor) { std::string type; std::string res; if (comm->type == simgrid::mc::PatternCommunicationType::send) - type = xbt::string_printf("The send communications pattern of the process %ld is different!", process - 1); + type = xbt::string_printf("The send communications pattern of the actor %ld is different!", actor - 1); else - type = xbt::string_printf("The recv communications pattern of the process %ld is different!", process - 1); + type = xbt::string_printf("The recv communications pattern of the actor %ld is different!", actor - 1); using simgrid::mc::CommPatternDifference; switch (diff) { @@ -199,7 +198,8 @@ void CommDetExtension::enforce_deterministic_pattern(aid_t actor, const PatternC send_diff = print_determinism_result(diff, actor, comm, list.index_comm + 1); } else { recv_deterministic = false; - recv_diff = print_determinism_result(diff, actor, comm, list.index_comm + 1); + if (recv_diff.empty()) + recv_diff = print_determinism_result(diff, actor, comm, list.index_comm + 1); } if (_sg_mc_send_determinism && not send_deterministic) { XBT_INFO("*********************************************************"); @@ -283,108 +283,6 @@ void CommDetExtension::complete_comm_pattern(const CommWaitTransition* transitio } } -CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session* session) : Checker(session) -{ - CommDetExtension::EXTENSION_ID = simgrid::mc::Checker::extension_create(); - StateCommDet::EXTENSION_ID = simgrid::mc::State::extension_create(); -} - -CommunicationDeterminismChecker::~CommunicationDeterminismChecker() = default; - -RecordTrace CommunicationDeterminismChecker::get_record_trace() // override -{ - RecordTrace res; - for (auto const& state : stack_) - res.push_back(state->get_transition()); - return res; -} - -std::vector CommunicationDeterminismChecker::get_textual_trace() // override -{ - std::vector trace; - for (auto const& state : stack_) - trace.push_back(state->get_transition()->to_string()); - return trace; -} - -void CommunicationDeterminismChecker::log_state() // override -{ - if (_sg_mc_comms_determinism) { - if (extension()->send_deterministic && not extension()->recv_deterministic) { - XBT_INFO("*******************************************************"); - XBT_INFO("**** Only-send-deterministic communication pattern ****"); - XBT_INFO("*******************************************************"); - XBT_INFO("%s", extension()->recv_diff.c_str()); - } - if (not extension()->send_deterministic && extension()->recv_deterministic) { - XBT_INFO("*******************************************************"); - XBT_INFO("**** Only-recv-deterministic communication pattern ****"); - XBT_INFO("*******************************************************"); - XBT_INFO("%s", extension()->send_diff.c_str()); - } - } - XBT_INFO("Expanded states = %ld", State::get_expanded_states()); - XBT_INFO("Visited states = %lu", api::get().mc_get_visited_states()); - XBT_INFO("Executed transitions = %lu", Transition::get_executed_transitions()); - XBT_INFO("Send-deterministic : %s", extension()->send_deterministic ? "Yes" : "No"); - if (_sg_mc_comms_determinism) - XBT_INFO("Recv-deterministic : %s", extension()->recv_deterministic ? "Yes" : "No"); -} - -void CommunicationDeterminismChecker::prepare() -{ - auto initial_state = std::make_unique(); - extension_set(new CommDetExtension()); - initial_state->extension_set(new StateCommDet(extension())); - - XBT_DEBUG("********* Start communication determinism verification *********"); - - /* Add all enabled actors to the interleave set of the initial state */ - for (auto& act : api::get().get_actors()) { - auto actor = act.copy.get_buffer(); - if (get_session().actor_is_enabled(actor->get_pid())) - initial_state->mark_todo(actor->get_pid()); - } - - stack_.push_back(std::move(initial_state)); -} - -void CommunicationDeterminismChecker::restoreState() -{ - auto extension = this->extension(); - - /* If asked to rollback on a state that has a snapshot, restore it */ - State* last_state = stack_.back().get(); - if (last_state->system_state_) { - api::get().restore_state(last_state->system_state_); - extension->restore_communications_pattern(last_state); - return; - } - - /* if no snapshot, we need to restore the initial state and replay the transitions */ - get_session().restore_initial_state(); - - const unsigned long maxpid = api::get().get_maxpid(); - assert(maxpid == extension->incomplete_communications_pattern.size()); - assert(maxpid == extension->initial_communications_pattern.size()); - for (unsigned long j = 0; j < maxpid; j++) { - extension->incomplete_communications_pattern[j].clear(); - extension->initial_communications_pattern[j].index_comm = 0; - } - - /* Traverse the stack from the state at position start and re-execute the transitions */ - for (std::unique_ptr const& state : stack_) { - if (state == stack_.back()) - break; - - auto* transition = state->get_transition(); - transition->replay(); - extension->handle_comm_pattern(transition); - - /* Update statistics */ - api::get().mc_inc_visited_states(); - } -} void CommDetExtension::handle_comm_pattern(const Transition* transition) { @@ -412,44 +310,7 @@ void CommDetExtension::handle_comm_pattern(const Transition* transition) } } -void CommunicationDeterminismChecker::real_run() -{ - auto extension = this->extension(); - - std::unique_ptr visited_state = nullptr; - const unsigned long maxpid = api::get().get_maxpid(); - - while (not stack_.empty()) { - /* Get current state */ - State* cur_state = stack_.back().get(); - - XBT_DEBUG("**************************************************"); - XBT_DEBUG("Exploration depth = %zu (state = %ld, interleaved processes = %zu)", stack_.size(), cur_state->num_, - cur_state->count_todo()); - - /* Update statistics */ - api::get().mc_inc_visited_states(); - - int next_transition = -1; - if (stack_.size() <= (std::size_t)_sg_mc_max_depth) - next_transition = cur_state->next_transition(); - - if (next_transition >= 0 && visited_state == nullptr) { - cur_state->execute_next(next_transition); - - auto* transition = cur_state->get_transition(); - XBT_DEBUG("Execute: %s", transition->to_string().c_str()); - - std::string req_str; - if (dot_output != nullptr) - req_str = api::get().request_get_dot_output(transition); - - extension->handle_comm_pattern(transition); - - /* Create the new expanded state */ - auto next_state = std::make_unique(); - next_state->extension_set(new StateCommDet(extension)); - +/* FIXME: CommDet probably don't play nicely with stateful exploration bool all_communications_are_finished = true; for (size_t current_actor = 1; all_communications_are_finished && current_actor < maxpid; current_actor++) { if (not extension->incomplete_communications_pattern[current_actor].empty()) { @@ -457,87 +318,61 @@ void CommunicationDeterminismChecker::real_run() all_communications_are_finished = false; } } + */ - /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at - * least, data are transferred). These communications are incomplete and they cannot be analyzed and compared - * with the initial pattern. */ - bool compare_snapshots = extension->initial_communications_pattern_done && all_communications_are_finished; - - if (_sg_mc_max_visited_states != 0) - visited_state = visited_states_.addVisitedState(next_state->num_, next_state.get(), compare_snapshots); - else - visited_state = nullptr; - - if (visited_state == nullptr) { - /* Add all enabled actors to the interleave set of the next state */ - for (auto& act : api::get().get_actors()) { - auto actor = act.copy.get_buffer(); - if (get_session().actor_is_enabled(actor->get_pid())) - next_state->mark_todo(actor->get_pid()); - } - - if (dot_output != nullptr) - fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", cur_state->num_, next_state->num_, req_str.c_str()); - - } else if (dot_output != nullptr) - fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", cur_state->num_, - visited_state->original_num == -1 ? visited_state->num : visited_state->original_num, req_str.c_str()); - - stack_.push_back(std::move(next_state)); - } else { - if (stack_.size() > (std::size_t)_sg_mc_max_depth) - XBT_WARN("/!\\ Max depth reached! /!\\ "); - else if (visited_state != nullptr) - XBT_DEBUG("State already visited (equal to state %ld), exploration stopped on this path.", - visited_state->original_num == -1 ? visited_state->num : visited_state->original_num); - else - XBT_DEBUG("There are no more processes to interleave. (depth %zu)", stack_.size()); - - extension->initial_communications_pattern_done = true; - - /* Trash the current state, no longer needed */ - XBT_DEBUG("Delete state %ld at depth %zu", cur_state->num_, stack_.size()); - stack_.pop_back(); - - visited_state = nullptr; +Checker* create_communication_determinism_checker(Session* session) +{ + CommDetExtension::EXTENSION_ID = simgrid::mc::Checker::extension_create(); + StateCommDet::EXTENSION_ID = simgrid::mc::State::extension_create(); - api::get().mc_check_deadlock(); + XBT_DEBUG("********* Start communication determinism verification *********"); - while (not stack_.empty()) { - std::unique_ptr state(std::move(stack_.back())); - stack_.pop_back(); - if (state->count_todo() && stack_.size() < (std::size_t)_sg_mc_max_depth) { - /* We found a back-tracking point, let's loop */ - XBT_DEBUG("Back-tracking to state %ld at depth %zu", state->num_, stack_.size() + 1); - stack_.push_back(std::move(state)); + auto extension = new CommDetExtension(); - this->restoreState(); + SafetyChecker::on_exploration_start([&extension]() { + XBT_INFO("Check communication determinism"); + extension->exploration_start(); + }); + SafetyChecker::on_backtracking([&extension]() { extension->initial_communications_pattern_done = true; }); + SafetyChecker::on_state_creation([&extension](State* state) { state->extension_set(new StateCommDet(extension)); }); - XBT_DEBUG("Back-tracking to state %ld at depth %zu done", stack_.back()->num_, stack_.size()); + SafetyChecker::on_restore_system_state( + [&extension](State* state) { extension->restore_communications_pattern(state); }); - break; - } else { - XBT_DEBUG("Delete state %ld at depth %zu", state->num_, stack_.size() + 1); - } + SafetyChecker::on_restore_initial_state([&extension]() { + const unsigned long maxpid = api::get().get_maxpid(); + assert(maxpid == extension->incomplete_communications_pattern.size()); + assert(maxpid == extension->initial_communications_pattern.size()); + for (unsigned long j = 0; j < maxpid; j++) { + extension->incomplete_communications_pattern[j].clear(); + extension->initial_communications_pattern[j].index_comm = 0; + } + }); + + SafetyChecker::on_transition_replay([&extension](Transition* t) { extension->handle_comm_pattern(t); }); + SafetyChecker::on_transition_execute([&extension](Transition* t) { extension->handle_comm_pattern(t); }); + + SafetyChecker::on_log_state([&extension]() { + if (_sg_mc_comms_determinism) { + if (extension->send_deterministic && not extension->recv_deterministic) { + XBT_INFO("*******************************************************"); + XBT_INFO("**** Only-send-deterministic communication pattern ****"); + XBT_INFO("*******************************************************"); + XBT_INFO("%s", extension->recv_diff.c_str()); + } + if (not extension->send_deterministic && extension->recv_deterministic) { + XBT_INFO("*******************************************************"); + XBT_INFO("**** Only-recv-deterministic communication pattern ****"); + XBT_INFO("*******************************************************"); + XBT_INFO("%s", extension->send_diff.c_str()); } } - } + XBT_INFO("Send-deterministic : %s", extension->send_deterministic ? "Yes" : "No"); + if (_sg_mc_comms_determinism) + XBT_INFO("Recv-deterministic : %s", extension->recv_deterministic ? "Yes" : "No"); + }); - api::get().log_state(); -} - -void CommunicationDeterminismChecker::run() -{ - XBT_INFO("Check communication determinism"); - get_session().take_initial_snapshot(); - - this->prepare(); - this->real_run(); -} - -Checker* create_communication_determinism_checker(Session* session) -{ - return new CommunicationDeterminismChecker(session); + return new SafetyChecker(session); } } // namespace mc diff --git a/src/mc/checker/CommunicationDeterminismChecker.hpp b/src/mc/checker/CommunicationDeterminismChecker.hpp deleted file mode 100644 index 3ac6c2a66f..0000000000 --- a/src/mc/checker/CommunicationDeterminismChecker.hpp +++ /dev/null @@ -1,40 +0,0 @@ -/* Copyright (c) 2016-2022. The SimGrid Team. All rights reserved. */ - -/* This program is free software; you can redistribute it and/or modify it - * under the terms of the license (GNU LGPL) which comes with this package. */ - -#include "src/mc/VisitedState.hpp" -#include "src/mc/checker/Checker.hpp" - -#include -#include - -#ifndef SIMGRID_MC_COMMUNICATION_DETERMINISM_CHECKER_HPP -#define SIMGRID_MC_COMMUNICATION_DETERMINISM_CHECKER_HPP - -namespace simgrid { -namespace mc { - -class XBT_PRIVATE CommunicationDeterminismChecker : public Checker { -public: - explicit CommunicationDeterminismChecker(Session* session); - ~CommunicationDeterminismChecker() override; - void run() override; - RecordTrace get_record_trace() override; - std::vector get_textual_trace() override; - -private: - void prepare(); - void real_run(); - void log_state() override; - void restoreState(); - - /** Stack representing the position in the exploration graph */ - std::list> stack_; - VisitedStates visited_states_; -}; -} // namespace mc -} // namespace simgrid - -#endif - diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index 8806934f6d..cb65299f6b 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -30,6 +30,18 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc, "Logging specific to MC safety ve namespace simgrid { namespace mc { +xbt::signal SafetyChecker::on_exploration_start_signal; +xbt::signal SafetyChecker::on_backtracking_signal; + +xbt::signal SafetyChecker::on_state_creation_signal; + +xbt::signal SafetyChecker::on_restore_system_state_signal; +xbt::signal SafetyChecker::on_restore_initial_state_signal; +xbt::signal SafetyChecker::on_transition_replay_signal; +xbt::signal SafetyChecker::on_transition_execute_signal; + +xbt::signal SafetyChecker::on_log_state_signal; + void SafetyChecker::check_non_termination(const State* current_state) { for (auto state = stack_.rbegin(); state != stack_.rend(); ++state) @@ -66,13 +78,16 @@ std::vector SafetyChecker::get_textual_trace() // override void SafetyChecker::log_state() // override { - XBT_INFO("%ld unique states visited; %ld backtracks (%lu transition replays, %lu states visited overall)", + on_log_state_signal(); + XBT_INFO("DFS exploration successful. %ld unique states visited; %ld backtracks (%lu transition replays, %lu states " + "visited overall)", State::get_expanded_states(), backtrack_count_, api::get().mc_get_visited_states(), Transition::get_replayed_transitions()); } void SafetyChecker::run() { + on_exploration_start_signal(); /* This function runs the DFS algorithm the state space. * We do so iteratively instead of recursively, dealing with the call stack manually. * This allows one to explore the call stack at will. */ @@ -124,6 +139,7 @@ void SafetyChecker::run() /* Actually answer the request: let's execute the selected request (MCed does one step) */ state->execute_next(next); + on_transition_execute_signal(state->get_transition()); // If there are processes to interleave and the maximum depth has not been // reached then perform one step of the exploration algorithm. @@ -135,6 +151,7 @@ void SafetyChecker::run() /* Create the new expanded state (copy the state of MCed into our MCer data) */ auto next_state = std::make_unique(); + on_state_creation_signal(next_state.get()); if (_sg_mc_termination) this->check_non_termination(next_state.get()); @@ -167,7 +184,6 @@ void SafetyChecker::run() stack_.push_back(std::move(next_state)); } - XBT_INFO("No property violation found."); api::get().log_state(); } @@ -175,6 +191,7 @@ void SafetyChecker::backtrack() { backtrack_count_++; XBT_VERB("Backtracking from %s", get_record_trace().to_string().c_str()); + on_backtracking_signal(); stack_.pop_back(); api::get().mc_check_deadlock(); @@ -228,20 +245,24 @@ void SafetyChecker::backtrack() void SafetyChecker::restore_state() { - /* Intermediate backtracking */ - const State* last_state = stack_.back().get(); + /* If asked to rollback on a state that has a snapshot, restore it */ + State* last_state = stack_.back().get(); if (last_state->system_state_) { api::get().restore_state(last_state->system_state_); + on_restore_system_state_signal(last_state); return; } + /* if no snapshot, we need to restore the initial state and replay the transitions */ get_session().restore_initial_state(); + on_restore_initial_state_signal(); /* Traverse the stack from the state at position start and re-execute the transitions */ for (std::unique_ptr const& state : stack_) { - if (state == stack_.back()) + if (state == stack_.back()) // If we are arrived on the target state, don't replay the outgoing transition *. break; state->get_transition()->replay(); + on_transition_replay_signal(state->get_transition()); /* Update statistics */ api::get().mc_inc_visited_states(); } @@ -258,7 +279,7 @@ SafetyChecker::SafetyChecker(Session* session) : Checker(session) if (_sg_mc_termination) XBT_INFO("Check non progressive cycles"); else - XBT_INFO("Check a safety property. Reduction is: %s.", + XBT_INFO("Start a DFS exploration. Reduction is: %s.", (reductionMode_ == ReductionMode::none ? "none" : (reductionMode_ == ReductionMode::dpor ? "dpor" : "unknown"))); diff --git a/src/mc/checker/SafetyChecker.hpp b/src/mc/checker/SafetyChecker.hpp index 4cf5f252ba..3851d39a7f 100644 --- a/src/mc/checker/SafetyChecker.hpp +++ b/src/mc/checker/SafetyChecker.hpp @@ -23,6 +23,18 @@ class XBT_PRIVATE SafetyChecker : public Checker { ReductionMode reductionMode_ = ReductionMode::unset; long backtrack_count_ = 0; + static xbt::signal on_exploration_start_signal; + static xbt::signal on_backtracking_signal; + + static xbt::signal on_state_creation_signal; + + static xbt::signal on_restore_system_state_signal; + static xbt::signal on_restore_initial_state_signal; + static xbt::signal on_transition_replay_signal; + static xbt::signal on_transition_execute_signal; + + static xbt::signal on_log_state_signal; + public: explicit SafetyChecker(Session* session); void run() override; @@ -30,6 +42,24 @@ public: std::vector get_textual_trace() override; void log_state() override; + /** Called once when the exploration starts */ + static void on_exploration_start(std::function f) { on_exploration_start_signal.connect(f); } + /** Called each time that the exploration backtracks from a exploration end */ + static void on_backtracking(std::function f) { on_backtracking_signal.connect(f); } + /** Called each time that a new state is create */ + static void on_state_creation(std::function f) { on_state_creation_signal.connect(f); } + /** Called when rollbacking directly onto a previously checkpointed state */ + static void on_restore_system_state(std::function f) { on_restore_system_state_signal.connect(f); } + /** Called when the state to which we backtrack was not checkpointed state, forcing us to restore the initial state + * before replaying some transitions */ + static void on_restore_initial_state(std::function f) { on_restore_initial_state_signal.connect(f); } + /** Called when replaying a transition that was previously executed, to reach a backtracked state */ + static void on_transition_replay(std::function f) { on_transition_replay_signal.connect(f); } + /** Called when executing a new transition */ + static void on_transition_execute(std::function f) { on_transition_execute_signal.connect(f); } + /** Called when displaying the statistics at the end of the exploration */ + static void on_log_state(std::function f) { on_log_state_signal.connect(f); } + private: void check_non_termination(const State* current_state); void backtrack(); diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 04762e37e5..3976d7403e 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -558,7 +558,6 @@ set(MC_SRC_BASE set(MC_SRC src/mc/checker/Checker.hpp src/mc/checker/CommunicationDeterminismChecker.cpp - src/mc/checker/CommunicationDeterminismChecker.hpp src/mc/checker/SafetyChecker.cpp src/mc/checker/SafetyChecker.hpp src/mc/checker/LivenessChecker.cpp