From 101fb4b351d4463209d346b758708eaeb025c99e Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Tue, 9 May 2023 10:36:13 +0200 Subject: [PATCH] Integrate SDPOR into `model-check/reduction` flag SDPOR and ODPOR can be used as part of the DFSExplorer (ODPOR should integrate with some minor details in the DFS implementation, but that's for a later PR). This commit replaces the simple `with_dpor` boolean flag used to control the reduction with the more precise `ReductionMode` that is newly extracted from within `DFSExplorer` and is instead made "public" --- .../explo/CommunicationDeterminismChecker.cpp | 4 +-- src/mc/explo/DFSExplorer.cpp | 16 ++++------ src/mc/explo/DFSExplorer.hpp | 6 ++-- src/mc/explo/Exploration.hpp | 7 ++-- src/mc/explo/simgrid_mc.cpp | 5 +-- src/mc/mc_config.cpp | 32 +++++++++++++++---- src/mc/mc_config.hpp | 5 +-- 7 files changed, 47 insertions(+), 28 deletions(-) diff --git a/src/mc/explo/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp index c36dfffe4a..a340c2cf94 100644 --- a/src/mc/explo/CommunicationDeterminismChecker.cpp +++ b/src/mc/explo/CommunicationDeterminismChecker.cpp @@ -320,14 +320,14 @@ void CommDetExtension::handle_comm_pattern(const Transition* transition) } */ -Exploration* create_communication_determinism_checker(const std::vector& args, bool with_dpor) +Exploration* create_communication_determinism_checker(const std::vector& args, ReductionMode mode) { CommDetExtension::EXTENSION_ID = simgrid::mc::Exploration::extension_create(); StateCommDet::EXTENSION_ID = simgrid::mc::State::extension_create(); XBT_DEBUG("********* Start communication determinism verification *********"); - auto base = new DFSExplorer(args, with_dpor, true); + auto base = new DFSExplorer(args, mode, true); auto extension = new CommDetExtension(*base); DFSExplorer::on_exploration_start([extension](RemoteApp const&) { diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 38e73f0ba6..3e9e5199fe 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -439,20 +439,16 @@ void DFSExplorer::backtrack() this->restore_stack(backtracking_point); } -DFSExplorer::DFSExplorer(const std::vector& args, bool with_dpor, bool need_memory_info) +DFSExplorer::DFSExplorer(const std::vector& args, ReductionMode mode, bool need_memory_info) : Exploration(args, need_memory_info || _sg_mc_termination #if SIMGRID_HAVE_STATEFUL_MC || _sg_mc_checkpoint > 0 #endif - ) + ) + , reduction_mode_(mode) { - if (with_dpor) - reduction_mode_ = ReductionMode::dpor; - else - reduction_mode_ = ReductionMode::none; - if (_sg_mc_termination) { - if (with_dpor) { + if (mode != ReductionMode::none) { XBT_INFO("Check non progressive cycles (turning DPOR off)"); reduction_mode_ = ReductionMode::none; } else { @@ -478,9 +474,9 @@ DFSExplorer::DFSExplorer(const std::vector& args, bool with_dpor, bool ne opened_states_.emplace_back(stack_.back()); } -Exploration* create_dfs_exploration(const std::vector& args, bool with_dpor) +Exploration* create_dfs_exploration(const std::vector& args, ReductionMode mode) { - return new DFSExplorer(args, with_dpor); + return new DFSExplorer(args, mode); } } // namespace simgrid::mc diff --git a/src/mc/explo/DFSExplorer.hpp b/src/mc/explo/DFSExplorer.hpp index 320754dc35..0c33d84b16 100644 --- a/src/mc/explo/DFSExplorer.hpp +++ b/src/mc/explo/DFSExplorer.hpp @@ -10,6 +10,7 @@ #include "src/mc/api/State.hpp" #include "src/mc/explo/Exploration.hpp" #include "src/mc/explo/odpor/Execution.hpp" +#include "src/mc/mc_config.hpp" #if SIMGRID_HAVE_STATEFUL_MC #include "src/mc/VisitedState.hpp" @@ -28,8 +29,7 @@ namespace simgrid::mc { using stack_t = std::deque>; class XBT_PRIVATE DFSExplorer : public Exploration { - XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor, sdpor); - +private: ReductionMode reduction_mode_; unsigned long backtrack_count_ = 0; // for statistics unsigned long visited_states_count_ = 0; // for statistics @@ -47,7 +47,7 @@ class XBT_PRIVATE DFSExplorer : public Exploration { static xbt::signal on_log_state_signal; public: - explicit DFSExplorer(const std::vector& args, bool with_dpor, bool need_memory_info = false); + explicit DFSExplorer(const std::vector& args, ReductionMode mode, bool need_memory_info = false); void run() override; RecordTrace get_record_trace() override; void log_state() override; diff --git a/src/mc/explo/Exploration.hpp b/src/mc/explo/Exploration.hpp index 824adcd3f7..64114d4bf2 100644 --- a/src/mc/explo/Exploration.hpp +++ b/src/mc/explo/Exploration.hpp @@ -8,6 +8,7 @@ #include "simgrid/forward.h" #include "src/mc/api/RemoteApp.hpp" +#include "src/mc/mc_config.hpp" #include "src/mc/mc_exit.hpp" #include "src/mc/mc_record.hpp" #include @@ -40,7 +41,7 @@ public: static Exploration* get_instance() { return instance_; } // No copy: - Exploration(Exploration const&) = delete; + Exploration(Exploration const&) = delete; Exploration& operator=(Exploration const&) = delete; /** Main function of this algorithm */ @@ -72,8 +73,8 @@ public: // External constructors so that the types (and the types of their content) remain hidden XBT_PUBLIC Exploration* create_liveness_checker(const std::vector& args); -XBT_PUBLIC Exploration* create_dfs_exploration(const std::vector& args, bool with_dpor); -XBT_PUBLIC Exploration* create_communication_determinism_checker(const std::vector& args, bool with_dpor); +XBT_PUBLIC Exploration* create_dfs_exploration(const std::vector& args, ReductionMode mode); +XBT_PUBLIC Exploration* create_communication_determinism_checker(const std::vector& args, ReductionMode mode); XBT_PUBLIC Exploration* create_udpor_checker(const std::vector& args); } // namespace simgrid::mc diff --git a/src/mc/explo/simgrid_mc.cpp b/src/mc/explo/simgrid_mc.cpp index 4e51cdd027..513c99727e 100644 --- a/src/mc/explo/simgrid_mc.cpp +++ b/src/mc/explo/simgrid_mc.cpp @@ -37,14 +37,15 @@ int main(int argc, char** argv) #if SIMGRID_HAVE_STATEFUL_MC if (_sg_mc_comms_determinism || _sg_mc_send_determinism) - explo = std::unique_ptr(create_communication_determinism_checker(argv_copy, cfg_use_DPOR())); + explo = std::unique_ptr( + create_communication_determinism_checker(argv_copy, get_model_checking_reduction())); else if (_sg_mc_unfolding_checker) explo = std::unique_ptr(create_udpor_checker(argv_copy)); else if (not _sg_mc_property_file.get().empty()) explo = std::unique_ptr(create_liveness_checker(argv_copy)); else #endif - explo = std::unique_ptr(create_dfs_exploration(argv_copy, cfg_use_DPOR())); + explo = std::unique_ptr(create_dfs_exploration(argv_copy, get_model_checking_reduction())); ExitStatus status; try { diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index 069d1cee7d..d451db1729 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -57,8 +57,9 @@ int _sg_mc_max_visited_states = 0; static simgrid::config::Flag cfg_mc_reduction{ "model-check/reduction", "Specify the kind of exploration reduction (either none or DPOR)", "dpor", [](std::string_view value) { - if (value != "none" && value != "dpor") - xbt_die("configuration option 'model-check/reduction' can only take 'none' or 'dpor' as a value"); + if (value != "none" && value != "dpor" && value != "sdpor" && value != "odpor") + xbt_die("configuration option 'model-check/reduction' must be one of the following: " + " 'none', 'dpor', 'sdpor', or 'odpor'"); }}; simgrid::config::Flag _sg_mc_sleep_set{ @@ -135,11 +136,30 @@ simgrid::config::Flag _sg_mc_termination{ "model-check/termination", "Whether to enable non progressive cycle detection", false, [](bool) { _mc_cfg_cb_check("value to enable/disable the detection of non progressive cycles"); }}; -bool simgrid::mc::cfg_use_DPOR() +simgrid::mc::ReductionMode simgrid::mc::get_model_checking_reduction() { - if (cfg_mc_reduction.get() == "dpor" && _sg_mc_max_visited_states__ > 0) { + if ((cfg_mc_reduction.get() == "dpor" || cfg_mc_reduction.get() == "sdpor" || cfg_mc_reduction.get() == "odpor") && + _sg_mc_max_visited_states__ > 0) { XBT_INFO("Disabling DPOR since state-equality reduction is activated with 'model-check/visited'"); - return false; + return simgrid::mc::ReductionMode::none; + } + + if (cfg_mc_reduction.get() == "none") { + return ReductionMode::none; + } else if (cfg_mc_reduction.get() == "dpor") { + return ReductionMode::dpor; + } else if (cfg_mc_reduction.get() == "sdpor") { + return ReductionMode::sdpor; + } else if (cfg_mc_reduction.get() == "odpor") { + XBT_INFO("No reduction will be used: ODPOR is not yet supported in SimGrid"); + return simgrid::mc::ReductionMode::none; + } else if (cfg_mc_reduction.get() == "udpor") { + XBT_INFO("No reduction will be used: " + "UDPOR is has a dedicated invocation 'model-check/unfolding-checker' " + "but is not yet supported in SimGrid"); + return ReductionMode::none; + } else { + XBT_INFO("Unknown reduction mode: defaulting to no reduction"); + return ReductionMode::none; } - return cfg_mc_reduction.get() == "dpor"; } diff --git a/src/mc/mc_config.hpp b/src/mc/mc_config.hpp index 64acccc142..b544580d3c 100644 --- a/src/mc/mc_config.hpp +++ b/src/mc/mc_config.hpp @@ -10,11 +10,12 @@ /********************************** Configuration of MC **************************************/ namespace simgrid::mc { -bool cfg_use_DPOR(); // "model-check/reduction" == "DPOR" +XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor, sdpor, odpor); XBT_DECLARE_ENUM_CLASS(ModelCheckingMode, NONE, APP_SIDE, CHECKER_SIDE, REPLAY); +ReductionMode get_model_checking_reduction(); // "model-check/reduction" == "DPOR" XBT_PUBLIC ModelCheckingMode get_model_checking_mode(); XBT_PUBLIC void set_model_checking_mode(ModelCheckingMode mode); -}; +}; // namespace simgrid::mc extern XBT_PUBLIC simgrid::config::Flag _sg_mc_buffering; extern XBT_PRIVATE simgrid::config::Flag _sg_mc_checkpoint; -- 2.20.1