From: Martin Quinson Date: Mon, 20 Mar 2023 16:09:17 +0000 (+0100) Subject: Put everything in position to re-fork the verified App X-Git-Tag: v3.34~290 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/10c3d34b00fc9a569ef0e281b0d955610476a0be Put everything in position to re-fork the verified App If you pass "need_memory_introspection = false" to the Exploration constructor, then the application is re-forked systematically instead of taking snapshot that are then restored. But it's still in progress, in the sense that the memory is still introspected even if we don't need it. The network protocol still needs to be changed so that the memory info are asked only if "need_memory_introspection = true" and not otherwise. For the time being, using reforks is very memory intensive for some reason, and my computers gets to its knees when running the tests. Until after the OOM killer saves me by cleaning stuff. --- diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp index 2ddd5c0876..e57e931a01 100644 --- a/src/mc/api/RemoteApp.cpp +++ b/src/mc/api/RemoteApp.cpp @@ -29,11 +29,15 @@ XBT_LOG_EXTERNAL_CATEGORY(mc_global); namespace simgrid::mc { -RemoteApp::RemoteApp(const std::vector& args) +RemoteApp::RemoteApp(const std::vector& args, bool need_memory_introspection) { - checker_side_ = std::make_unique(args); + for (auto* arg : args) + app_args_.push_back(arg); - initial_snapshot_ = std::make_shared(0, page_store_, checker_side_->get_remote_memory()); + checker_side_ = std::make_unique(app_args_); + + if (need_memory_introspection) + initial_snapshot_ = std::make_shared(0, page_store_, checker_side_->get_remote_memory()); } RemoteApp::~RemoteApp() @@ -42,9 +46,15 @@ RemoteApp::~RemoteApp() shutdown(); } -void RemoteApp::restore_initial_state() const +void RemoteApp::restore_initial_state() { - this->initial_snapshot_->restore(checker_side_->get_remote_memory()); + if (initial_snapshot_ == nullptr) { // No memory introspection + shutdown(); + checker_side_.reset( + nullptr); // We need to destroy the existing CheckerSide before creating the new one, or libevent gets crazy + checker_side_.reset(new simgrid::mc::CheckerSide(app_args_)); + } else + initial_snapshot_->restore(checker_side_->get_remote_memory()); } unsigned long RemoteApp::get_maxpid() const diff --git a/src/mc/api/RemoteApp.hpp b/src/mc/api/RemoteApp.hpp index d6e5eee825..5ad3559f9f 100644 --- a/src/mc/api/RemoteApp.hpp +++ b/src/mc/api/RemoteApp.hpp @@ -30,6 +30,8 @@ private: PageStore page_store_{500}; std::shared_ptr initial_snapshot_; + std::vector app_args_; + // No copy: RemoteApp(RemoteApp const&) = delete; RemoteApp& operator=(RemoteApp const&) = delete; @@ -42,11 +44,11 @@ public: * * The code is expected to `exec` the model-checked application. */ - explicit RemoteApp(const std::vector& args); + explicit RemoteApp(const std::vector& args, bool need_memory_introspection); ~RemoteApp(); - void restore_initial_state() const; + void restore_initial_state(); void wait_for_requests(); /** Ask to the application to check for a deadlock. If so, do an error message and throw a DeadlockError. */ diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 98396111b1..99379b8e06 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -297,7 +297,7 @@ void DFSExplorer::backtrack() } // If no backtracing point, then the stack is empty and the exploration is over } -DFSExplorer::DFSExplorer(const std::vector& args, bool with_dpor) : Exploration(args) +DFSExplorer::DFSExplorer(const std::vector& args, bool with_dpor) : Exploration(args, true) { if (with_dpor) reduction_mode_ = ReductionMode::dpor; diff --git a/src/mc/explo/Exploration.cpp b/src/mc/explo/Exploration.cpp index 1dbe4c41e3..463a5e36c7 100644 --- a/src/mc/explo/Exploration.cpp +++ b/src/mc/explo/Exploration.cpp @@ -20,7 +20,8 @@ static simgrid::config::Flag cfg_dot_output_file{ Exploration* Exploration::instance_ = nullptr; // singleton instance -Exploration::Exploration(const std::vector& args) : remote_app_(std::make_unique(args)) +Exploration::Exploration(const std::vector& args, bool need_memory_introspection) + : remote_app_(std::make_unique(args, need_memory_introspection)) { xbt_assert(instance_ == nullptr, "Cannot have more than one exploration instance"); instance_ = this; diff --git a/src/mc/explo/Exploration.hpp b/src/mc/explo/Exploration.hpp index c027256ade..7a30470f2c 100644 --- a/src/mc/explo/Exploration.hpp +++ b/src/mc/explo/Exploration.hpp @@ -34,7 +34,7 @@ class Exploration : public xbt::Extendable { FILE* dot_output_ = nullptr; public: - explicit Exploration(const std::vector& args); + explicit Exploration(const std::vector& args, bool need_memory_introspection); virtual ~Exploration(); static Exploration* get_instance() { return instance_; } diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp index 72909308dc..ea293ae825 100644 --- a/src/mc/explo/LivenessChecker.cpp +++ b/src/mc/explo/LivenessChecker.cpp @@ -180,7 +180,7 @@ void LivenessChecker::purge_visited_pairs() } } -LivenessChecker::LivenessChecker(const std::vector& args) : Exploration(args) {} +LivenessChecker::LivenessChecker(const std::vector& args) : Exploration(args, true) {} LivenessChecker::~LivenessChecker() { xbt_automaton_free(property_automaton_); diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp index 1506a16cdd..17cca8dae3 100644 --- a/src/mc/explo/UdporChecker.cpp +++ b/src/mc/explo/UdporChecker.cpp @@ -13,7 +13,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to verification namespace simgrid::mc::udpor { -UdporChecker::UdporChecker(const std::vector& args) : Exploration(args) +UdporChecker::UdporChecker(const std::vector& args) : Exploration(args, true) { // Initialize the map } diff --git a/src/mc/remote/CheckerSide.cpp b/src/mc/remote/CheckerSide.cpp index bd7b16b367..54c8563ccb 100644 --- a/src/mc/remote/CheckerSide.cpp +++ b/src/mc/remote/CheckerSide.cpp @@ -126,6 +126,8 @@ static void wait_application_process(pid_t pid) void CheckerSide::setup_events() { + if (base_ != nullptr) + event_base_free(base_.get()); auto* base = event_base_new(); base_.reset(base); diff --git a/src/mc/remote/CheckerSide.hpp b/src/mc/remote/CheckerSide.hpp index 2461d335c3..40e74c5121 100644 --- a/src/mc/remote/CheckerSide.hpp +++ b/src/mc/remote/CheckerSide.hpp @@ -18,12 +18,16 @@ namespace simgrid::mc { /* CheckerSide: All what the checker needs to interact with a given application process */ class CheckerSide { + void (*const free_event_fun)(event*) = [](event* evt) { + event_del(evt); + event_free(evt); + }; + std::unique_ptr socket_event_{nullptr, free_event_fun}; + std::unique_ptr signal_event_{nullptr, free_event_fun}; std::unique_ptr base_{nullptr, &event_base_free}; - std::unique_ptr socket_event_{nullptr, &event_free}; - std::unique_ptr signal_event_{nullptr, &event_free}; std::unique_ptr remote_memory_; - Channel channel_; + Channel channel_; bool running_ = false; pid_t pid_;