From fa84bee017477630eea9a93890e0e2abf3855bf9 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sun, 14 Mar 2021 01:25:09 +0100 Subject: [PATCH] The checker now have a reference to the session --- src/mc/api.cpp | 8 ++++---- src/mc/checker/Checker.hpp | 14 +++++++++----- src/mc/checker/CommunicationDeterminismChecker.cpp | 6 +++--- src/mc/checker/CommunicationDeterminismChecker.hpp | 2 +- src/mc/checker/LivenessChecker.cpp | 8 +++----- src/mc/checker/LivenessChecker.hpp | 2 +- src/mc/checker/SafetyChecker.cpp | 6 +++--- src/mc/checker/SafetyChecker.hpp | 2 +- src/mc/checker/UdporChecker.cpp | 6 +++--- src/mc/checker/UdporChecker.hpp | 2 +- src/mc/sosp/Snapshot.hpp | 8 ++++---- 11 files changed, 33 insertions(+), 31 deletions(-) diff --git a/src/mc/api.cpp b/src/mc/api.cpp index ecab76bb40..ce7b065d37 100644 --- a/src/mc/api.cpp +++ b/src/mc/api.cpp @@ -399,19 +399,19 @@ simgrid::mc::Checker* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm simgrid::mc::Checker* checker; switch (algo) { case CheckerAlgorithm::CommDeterminism: - checker = simgrid::mc::createCommunicationDeterminismChecker(); + checker = simgrid::mc::createCommunicationDeterminismChecker(session); break; case CheckerAlgorithm::UDPOR: - checker = simgrid::mc::createUdporChecker(); + checker = simgrid::mc::createUdporChecker(session); break; case CheckerAlgorithm::Safety: - checker = simgrid::mc::createSafetyChecker(); + checker = simgrid::mc::createSafetyChecker(session); break; case CheckerAlgorithm::Liveness: - checker = simgrid::mc::createLivenessChecker(); + checker = simgrid::mc::createLivenessChecker(session); break; default: diff --git a/src/mc/checker/Checker.hpp b/src/mc/checker/Checker.hpp index 1fe6c64571..ebc0448538 100644 --- a/src/mc/checker/Checker.hpp +++ b/src/mc/checker/Checker.hpp @@ -26,8 +26,10 @@ namespace mc { * have all the necessary features). */ // abstract class Checker { + Session* session_; + public: - explicit Checker() = default; + explicit Checker(Session* session) : session_(session) {} // No copy: Checker(Checker const&) = delete; @@ -52,13 +54,15 @@ public: /** Log additional information about the state of the model-checker */ virtual void log_state() = 0; + + Session* get_session() { return session_; } }; // External constructors so that the types (and the types of their content) remain hidden -XBT_PUBLIC Checker* createLivenessChecker(); -XBT_PUBLIC Checker* createSafetyChecker(); -XBT_PUBLIC Checker* createCommunicationDeterminismChecker(); -XBT_PUBLIC Checker* createUdporChecker(); +XBT_PUBLIC Checker* createLivenessChecker(Session* session); +XBT_PUBLIC Checker* createSafetyChecker(Session* session); +XBT_PUBLIC Checker* createCommunicationDeterminismChecker(Session* session); +XBT_PUBLIC Checker* createUdporChecker(Session* session); } // namespace mc } // namespace simgrid diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index 47b7ad591b..b0f373af77 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -255,7 +255,7 @@ void CommunicationDeterminismChecker::complete_comm_pattern(RemotePtrreal_run(); } -Checker* createCommunicationDeterminismChecker() +Checker* createCommunicationDeterminismChecker(Session* session) { - return new CommunicationDeterminismChecker(); + return new CommunicationDeterminismChecker(session); } } // namespace mc diff --git a/src/mc/checker/CommunicationDeterminismChecker.hpp b/src/mc/checker/CommunicationDeterminismChecker.hpp index ca9f6948fd..3c92f89ad7 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.hpp +++ b/src/mc/checker/CommunicationDeterminismChecker.hpp @@ -18,7 +18,7 @@ namespace mc { class XBT_PRIVATE CommunicationDeterminismChecker : public Checker { public: - explicit CommunicationDeterminismChecker(); + explicit CommunicationDeterminismChecker(Session* session); ~CommunicationDeterminismChecker() override; void run() override; RecordTrace get_record_trace() override; diff --git a/src/mc/checker/LivenessChecker.cpp b/src/mc/checker/LivenessChecker.cpp index a1b2ca6fd7..f5b56430e6 100644 --- a/src/mc/checker/LivenessChecker.cpp +++ b/src/mc/checker/LivenessChecker.cpp @@ -202,9 +202,7 @@ void LivenessChecker::purge_visited_pairs() } } -LivenessChecker::LivenessChecker() : Checker() -{ -} +LivenessChecker::LivenessChecker(Session* session) : Checker(session) {} RecordTrace LivenessChecker::get_record_trace() // override { @@ -408,9 +406,9 @@ void LivenessChecker::run() api::get().log_state(); } -Checker* createLivenessChecker() +Checker* createLivenessChecker(Session* session) { - return new LivenessChecker(); + return new LivenessChecker(session); } } // namespace mc diff --git a/src/mc/checker/LivenessChecker.hpp b/src/mc/checker/LivenessChecker.hpp index 39f899fdb0..cb972c5a5f 100644 --- a/src/mc/checker/LivenessChecker.hpp +++ b/src/mc/checker/LivenessChecker.hpp @@ -51,7 +51,7 @@ public: class XBT_PRIVATE LivenessChecker : public Checker { public: - explicit LivenessChecker(); + explicit LivenessChecker(Session* session); void run() override; RecordTrace get_record_trace() override; std::vector get_textual_trace() override; diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index 42e8bc6e85..cefde1f770 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -253,7 +253,7 @@ void SafetyChecker::restore_state() } } -SafetyChecker::SafetyChecker() : Checker() +SafetyChecker::SafetyChecker(Session* session) : Checker(session) { reductionMode_ = reduction_mode; if (_sg_mc_termination) @@ -290,9 +290,9 @@ SafetyChecker::SafetyChecker() : Checker() stack_.push_back(std::move(initial_state)); } -Checker* createSafetyChecker() +Checker* createSafetyChecker(Session* session) { - return new SafetyChecker(); + return new SafetyChecker(session); } } // namespace mc diff --git a/src/mc/checker/SafetyChecker.hpp b/src/mc/checker/SafetyChecker.hpp index a16070e0e2..4fc2d7eedc 100644 --- a/src/mc/checker/SafetyChecker.hpp +++ b/src/mc/checker/SafetyChecker.hpp @@ -23,7 +23,7 @@ class XBT_PRIVATE SafetyChecker : public Checker { ReductionMode reductionMode_ = ReductionMode::unset; public: - explicit SafetyChecker(); + explicit SafetyChecker(Session* session); void run() override; RecordTrace get_record_trace() override; std::vector get_textual_trace() override; diff --git a/src/mc/checker/UdporChecker.cpp b/src/mc/checker/UdporChecker.cpp index 8d3e8f714d..a3e4265f88 100644 --- a/src/mc/checker/UdporChecker.cpp +++ b/src/mc/checker/UdporChecker.cpp @@ -11,7 +11,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to MC safety ver namespace simgrid { namespace mc { -UdporChecker::UdporChecker() : Checker() {} +UdporChecker::UdporChecker(Session* session) : Checker(session) {} void UdporChecker::run() {} @@ -29,9 +29,9 @@ std::vector UdporChecker::get_textual_trace() void UdporChecker::log_state() {} -Checker* createUdporChecker() +Checker* createUdporChecker(Session* session) { - return new UdporChecker(); + return new UdporChecker(session); } } // namespace mc diff --git a/src/mc/checker/UdporChecker.hpp b/src/mc/checker/UdporChecker.hpp index 57dbe95c59..e20e7e291d 100644 --- a/src/mc/checker/UdporChecker.hpp +++ b/src/mc/checker/UdporChecker.hpp @@ -15,7 +15,7 @@ namespace mc { class XBT_PRIVATE UdporChecker : public Checker { public: - explicit UdporChecker(); + explicit UdporChecker(Session* session); void run() override; RecordTrace get_record_trace() override; std::vector get_textual_trace() override; diff --git a/src/mc/sosp/Snapshot.hpp b/src/mc/sosp/Snapshot.hpp index a39b0d0e1f..bc658e5026 100644 --- a/src/mc/sosp/Snapshot.hpp +++ b/src/mc/sosp/Snapshot.hpp @@ -60,7 +60,7 @@ namespace mc { class XBT_PRIVATE Snapshot final : public AddressSpace { public: /* Initialization */ - Snapshot(int num_state, RemoteProcess* get_remote_simulation = &mc_model_checker->get_remote_process()); + Snapshot(int num_state, RemoteProcess* process = &mc_model_checker->get_remote_process()); /* Regular use */ bool on_heap(const void* address) const @@ -73,7 +73,7 @@ public: ReadOptions options = ReadOptions::none()) const override; Region* get_region(const void* addr) const; Region* get_region(const void* addr, Region* hinted_region) const; - void restore(RemoteProcess* get_remote_simulation) const; + void restore(RemoteProcess* process) const; // To be private int num_state_; @@ -88,8 +88,8 @@ public: private: void add_region(RegionType type, ObjectInformation* object_info, void* start_addr, std::size_t size); - void snapshot_regions(RemoteProcess* get_remote_simulation); - void snapshot_stacks(RemoteProcess* get_remote_simulation); + void snapshot_regions(RemoteProcess* process); + void snapshot_stacks(RemoteProcess* process); }; } // namespace mc } // namespace simgrid -- 2.20.1