From 80636e60075039dfb7de739cd9dc7094db092962 Mon Sep 17 00:00:00 2001 From: Ehsan Azimi Date: Mon, 26 Oct 2020 15:45:18 +0100 Subject: [PATCH] mc_api class introduced, SafetyChecher's constructor and main() in simgrid_mc.cpp call mc_api's functions --- src/mc/checker/SafetyChecker.cpp | 11 ++- src/mc/checker/simgrid_mc.cpp | 15 +-- src/mc/mc_api.cpp | 151 +++++++++++++++++++++++++++++++ src/mc/mc_api.hpp | 71 +++++++++++++++ src/mc/mc_base.cpp | 2 + tools/cmake/DefinePackages.cmake | 4 +- 6 files changed, 240 insertions(+), 14 deletions(-) create mode 100644 src/mc/mc_api.cpp create mode 100644 src/mc/mc_api.hpp diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index 9f9716fe6f..4ef3b7dd28 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -23,9 +23,12 @@ #include "src/mc/mc_record.hpp" #include "src/mc/mc_request.hpp" #include "src/mc/mc_smx.hpp" +#include "src/mc/mc_api.hpp" #include "src/xbt/mmalloc/mmprivate.h" +using mcapi = simgrid::mc::mc_api; + XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc, "Logging specific to MC safety verification "); namespace simgrid { @@ -279,7 +282,8 @@ SafetyChecker::SafetyChecker(Session& s) : Checker(s) XBT_INFO("Check a safety property. Reduction is: %s.", (reductionMode_ == ReductionMode::none ? "none" : (reductionMode_ == ReductionMode::dpor ? "dpor" : "unknown"))); - session->initialize(); + + mcapi::get().s_initialize(); XBT_DEBUG("Starting the safety algorithm"); @@ -290,8 +294,9 @@ SafetyChecker::SafetyChecker(Session& s) : Checker(s) XBT_DEBUG("Initial state"); /* Get an enabled actor and insert it in the interleave set of the initial state */ - for (auto& actor : mc_model_checker->get_remote_simulation().actors()) - if (actor_is_enabled(actor.copy.get_buffer())) { + auto actors = mcapi::get().get_actors(); + for (auto& actor : actors) + if (mcapi::get().actor_is_enabled(actor.copy.get_buffer()->get_pid())) { initial_state->add_interleaving_set(actor.copy.get_buffer()); if (reductionMode_ != ReductionMode::none) break; diff --git a/src/mc/checker/simgrid_mc.cpp b/src/mc/checker/simgrid_mc.cpp index 9168cc9b5b..e382e9ff9f 100644 --- a/src/mc/checker/simgrid_mc.cpp +++ b/src/mc/checker/simgrid_mc.cpp @@ -10,6 +10,7 @@ #include "src/mc/mc_config.hpp" #include "src/mc/mc_exit.hpp" #include "src/internal_config.h" +#include "src/mc/mc_api.hpp" #if HAVE_SMPI #include "smpi/smpi.h" @@ -19,6 +20,8 @@ #include #include +using mcapi = simgrid::mc::mc_api; + static inline char** argvdup(int argc, char** argv) { @@ -54,15 +57,7 @@ int main(int argc, char** argv) smpi_init_options(); // only performed once #endif sg_config_init(&argc, argv); - simgrid::mc::session = new simgrid::mc::Session([argv_copy] { - int i = 1; - while (argv_copy[i] != nullptr && argv_copy[i][0] == '-') - i++; - xbt_assert(argv_copy[i] != nullptr, - "Unable to find a binary to exec on the command line. Did you only pass config flags?"); - execvp(argv_copy[i], argv_copy + i); - xbt_die("The model-checked process failed to exec(): %s", strerror(errno)); - }); + mcapi::get().initialize(argv_copy); delete[] argv_copy; auto checker = create_checker(*simgrid::mc::session); @@ -77,6 +72,6 @@ int main(int argc, char** argv) res = SIMGRID_MC_EXIT_LIVENESS; } checker = nullptr; - simgrid::mc::session->close(); + mcapi::get().s_close(); return res; } diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp new file mode 100644 index 0000000000..28fc643151 --- /dev/null +++ b/src/mc/mc_api.cpp @@ -0,0 +1,151 @@ +#include "mc_api.hpp" + +#include "src/mc/Session.hpp" +#include "src/mc/mc_private.hpp" +#include "src/mc/remote/RemoteSimulation.hpp" +#include +#include + +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_api, mc, "Logging specific to MC Fasade APIs "); + +namespace simgrid { +namespace mc { + +void mc_api::initialize(char** argv) +{ + simgrid::mc::session = new simgrid::mc::Session([argv] { + int i = 1; + while (argv[i] != nullptr && argv[i][0] == '-') + i++; + xbt_assert(argv[i] != nullptr, + "Unable to find a binary to exec on the command line. Did you only pass config flags?"); + execvp(argv[i], argv + i); + xbt_die("The model-checked process failed to exec(): %s", strerror(errno)); + }); +} + +void mc_api::s_initialize() const +{ + session->initialize(); +} + +void mc_api::create_model_checker(std::unique_ptr remote_simulation, int sockfd) +{ + +} + +ModelChecker* mc_api::get_model_checker() const +{ + return mc_model_checker; +} + +void mc_api::mc_inc_visited_states() const +{ + mc_model_checker->visited_states++; +} + +void mc_api::mc_inc_executed_trans() const +{ + mc_model_checker->executed_transitions++; +} + +unsigned long mc_api::mc_get_visited_states() const +{ + return mc_model_checker->visited_states; +} + +unsigned long mc_api::mc_get_executed_trans() const +{ + return mc_model_checker->executed_transitions; +} + +bool mc_api::mc_check_deadlock() const +{ + return mc_model_checker->checkDeadlock(); +} + +std::vector& mc_api::get_actors() const +{ + return mc_model_checker->get_remote_simulation().actors(); +} + +bool mc_api::actor_is_enabled(aid_t pid) const +{ + return session->actor_is_enabled(pid); +} + +void mc_api::mc_assert(bool notNull, const char* message) const +{ + if (notNull) + xbt_assert(mc_model_checker == nullptr, message); + else + xbt_assert(mc_model_checker != nullptr, message); +} + +bool mc_api::mc_is_null() const +{ + auto is_null = (mc_model_checker == nullptr) ? true : false; + return is_null; +} + +Checker* mc_api::mc_get_checker() const +{ + return mc_model_checker->getChecker(); +} + +RemoteSimulation& mc_api::mc_get_remote_simulation() const +{ + return mc_model_checker->get_remote_simulation(); +} + +void mc_api::handle_simcall(Transition const& transition) const +{ + mc_model_checker->handle_simcall(transition); +} + +void mc_api::mc_wait_for_requests() const +{ + mc_model_checker->wait_for_requests(); +} + +void mc_api::mc_exit(int status) const +{ + mc_model_checker->exit(status); +} + +std::string const& mc_api::mc_get_host_name(std::string const& hostname) const +{ + return mc_model_checker->get_host_name(hostname); +} + +PageStore& mc_api::mc_page_store() const +{ + return mc_model_checker->page_store(); +} + +void mc_api::mc_cleanup() +{ +} + +void mc_api::s_close() const +{ + session->close(); +} + +void mc_api::s_restore_initial_state() const +{ + session->restore_initial_state(); +} + +void mc_api::execute(Transition const& transition) +{ + session->execute(transition); +} + +void mc_api::s_log_state() const +{ + session->log_state(); +} + +} // namespace mc +} // namespace simgrid diff --git a/src/mc/mc_api.hpp b/src/mc/mc_api.hpp new file mode 100644 index 0000000000..bafc17894a --- /dev/null +++ b/src/mc/mc_api.hpp @@ -0,0 +1,71 @@ +#ifndef SIMGRID_MC_API_HPP +#define SIMGRID_MC_API_HPP + +#include +#include + +#include "simgrid/forward.h" +#include "src/mc/mc_forward.hpp" +#include "xbt/base.h" + +namespace simgrid { +namespace mc { + +/* +** This class aimes to implement FACADE APIs for simgrid. The FACADE layer sits between the CheckerSide +** (Unfolding_Checker, DPOR, ...) layer and the +** AppSide layer. The goal is to drill down into the entagled details in the CheckerSide layer and break down the +** detailes in a way that the CheckerSide eventually +** be capable to acquire the required information through the FACADE layer rather than the direct access to the AppSide. +*/ + +class mc_api { +private: + mc_api() = default; + +public: + // No copy: + mc_api(mc_api const&) = delete; + void operator=(mc_api const&) = delete; + + static mc_api& get() + { + static mc_api mcapi; + return mcapi; + } + + void initialize(char** argv); + + // MODEL_CHECKER FUNCTIONS + void create_model_checker(std::unique_ptr remote_simulation, int sockfd); + ModelChecker* get_model_checker() const; + void mc_inc_visited_states() const; + void mc_inc_executed_trans() const; + unsigned long mc_get_visited_states() const; + unsigned long mc_get_executed_trans() const; + bool mc_check_deadlock() const; + std::vector& get_actors() const; + bool actor_is_enabled(aid_t pid) const; + void mc_assert(bool notNull, const char* message = "") const; + bool mc_is_null() const; + Checker* mc_get_checker() const; + RemoteSimulation& mc_get_remote_simulation() const; + void handle_simcall(Transition const& transition) const; + void mc_wait_for_requests() const; + void mc_exit(int status) const; + std::string const& mc_get_host_name(std::string const& hostname) const; + PageStore& mc_page_store() const; + void mc_cleanup(); + + // SESSION FUNCTIONS + void s_initialize() const; + void s_close() const; + void s_restore_initial_state() const; + void execute(Transition const& transition); + void s_log_state() const; +}; + +} // namespace mc +} // namespace simgrid + +#endif \ No newline at end of file diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index 2a59567386..c0811633bd 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -70,12 +70,14 @@ void wait_for_requests() // Called from both MCer and MCed: bool actor_is_enabled(smx_actor_t actor) { +// #del #if SIMGRID_HAVE_MC // If in the MCer, ask the client app since it has all the data if (mc_model_checker != nullptr) { return simgrid::mc::session->actor_is_enabled(actor->get_pid()); } #endif +// # // Now, we are in the client app, no need for remote memory reading. smx_simcall_t req = &actor->simcall_; diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index 1062af7dbe..25525840c2 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -611,7 +611,7 @@ set(MC_SRC src/mc/checker/SimcallInspector.hpp src/mc/checker/LivenessChecker.cpp src/mc/checker/LivenessChecker.hpp - + src/mc/inspect/DwarfExpression.hpp src/mc/inspect/DwarfExpression.cpp src/mc/inspect/Frame.hpp @@ -661,6 +661,8 @@ set(MC_SRC src/mc/mc_comm_pattern.cpp src/mc/mc_comm_pattern.hpp src/mc/compare.cpp + src/mc/mc_api.cpp + src/mc/mc_api.hpp src/mc/mc_hash.hpp src/mc/mc_hash.cpp src/mc/mc_ignore.hpp -- 2.20.1