From: Ehsan Azimi Date: Mon, 26 Oct 2020 15:45:19 +0000 (+0100) Subject: SafetyChecker::backtrack() calls mc_api functions X-Git-Tag: v3.26~72^2^2~66 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/1a321ac4a2db98b98089b977f9964a068b552be7?ds=sidebyside SafetyChecker::backtrack() calls mc_api functions --- diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index a77bb189b1..95f1f6be5a 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -180,8 +180,8 @@ void SafetyChecker::backtrack() stack_.pop_back(); /* Check for deadlocks */ - if (mc_model_checker->checkDeadlock()) { - MC_show_deadlock(); + if (mcapi::get().mc_check_deadlock()) { + mcapi::get().mc_show_deadlock(); throw DeadlockError(); } @@ -198,19 +198,19 @@ void SafetyChecker::backtrack() if (req->call_ == SIMCALL_MUTEX_LOCK || req->call_ == SIMCALL_MUTEX_TRYLOCK) xbt_die("Mutex is currently not supported with DPOR, use --cfg=model-check/reduction:none"); - const kernel::actor::ActorImpl* issuer = MC_smx_simcall_get_issuer(req); + const kernel::actor::ActorImpl* issuer = mcapi::get().mc_smx_simcall_get_issuer(req); for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) { State* prev_state = i->get(); - if (request_depend(req, &prev_state->internal_req_)) { + if (mcapi::get().request_depend(req, &prev_state->internal_req_)) { if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { XBT_DEBUG("Dependent Transitions:"); int value = prev_state->transition_.argument_; smx_simcall_t prev_req = &prev_state->executed_req_; - XBT_DEBUG("%s (state=%d)", simgrid::mc::request_to_string(prev_req, value, RequestType::internal).c_str(), + XBT_DEBUG("%s (state=%d)", mcapi::get().request_to_string(prev_req, value, RequestType::internal).c_str(), prev_state->num_); value = state->transition_.argument_; prev_req = &state->executed_req_; - XBT_DEBUG("%s (state=%d)", simgrid::mc::request_to_string(prev_req, value, RequestType::executed).c_str(), + XBT_DEBUG("%s (state=%d)", mcapi::get().request_to_string(prev_req, value, RequestType::executed).c_str(), state->num_); } @@ -220,14 +220,14 @@ void SafetyChecker::backtrack() XBT_DEBUG("Process %p is in done set", req->issuer_); break; } else if (req->issuer_ == prev_state->internal_req_.issuer_) { - XBT_DEBUG("Simcall %s and %s with same issuer", SIMIX_simcall_name(req->call_), - SIMIX_simcall_name(prev_state->internal_req_.call_)); + XBT_DEBUG("Simcall %s and %s with same issuer", mcapi::get().simix_simcall_name(req->call_), + mcapi::get().simix_simcall_name(prev_state->internal_req_.call_)); break; } else { - const kernel::actor::ActorImpl* previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req_); + const kernel::actor::ActorImpl* previous_issuer = mcapi::get().mc_smx_simcall_get_issuer(&prev_state->internal_req_); XBT_DEBUG("Simcall %s, process %ld (state %d) and simcall %s, process %ld (state %d) are independent", - SIMIX_simcall_name(req->call_), issuer->get_pid(), state->num_, - SIMIX_simcall_name(prev_state->internal_req_.call_), previous_issuer->get_pid(), prev_state->num_); + mcapi::get().simix_simcall_name(req->call_), issuer->get_pid(), state->num_, + mcapi::get().simix_simcall_name(prev_state->internal_req_.call_), previous_issuer->get_pid(), prev_state->num_); } } } diff --git a/src/mc/mc_api.cpp b/src/mc/mc_api.cpp index 28fc643151..c6012a47a8 100644 --- a/src/mc/mc_api.cpp +++ b/src/mc/mc_api.cpp @@ -3,6 +3,8 @@ #include "src/mc/Session.hpp" #include "src/mc/mc_private.hpp" #include "src/mc/remote/RemoteSimulation.hpp" +#include "src/mc/mc_smx.hpp" + #include #include @@ -64,6 +66,16 @@ bool mc_api::mc_check_deadlock() const return mc_model_checker->checkDeadlock(); } +void mc_api::mc_show_deadlock() const +{ + MC_show_deadlock(); +} + +smx_actor_t mc_api::mc_smx_simcall_get_issuer(s_smx_simcall const* req) const +{ + return MC_smx_simcall_get_issuer(req); +} + std::vector& mc_api::get_actors() const { return mc_model_checker->get_remote_simulation().actors(); @@ -127,6 +139,21 @@ void mc_api::mc_cleanup() { } +bool mc_api::request_depend(smx_simcall_t req1, smx_simcall_t req2) const +{ + return simgrid::mc::request_depend(req1, req2); +} + +std::string mc_api::request_to_string(smx_simcall_t req, int value, RequestType request_type) const +{ + return simgrid::mc::request_to_string(req, value, request_type).c_str(); +} + +const char * mc_api::simix_simcall_name(e_smx_simcall_t kind) const +{ + return SIMIX_simcall_name(kind); +} + void mc_api::s_close() const { session->close(); diff --git a/src/mc/mc_api.hpp b/src/mc/mc_api.hpp index bafc17894a..c85f87f1b7 100644 --- a/src/mc/mc_api.hpp +++ b/src/mc/mc_api.hpp @@ -6,6 +6,7 @@ #include "simgrid/forward.h" #include "src/mc/mc_forward.hpp" +#include "src/mc/mc_request.hpp" #include "xbt/base.h" namespace simgrid { @@ -44,6 +45,8 @@ public: unsigned long mc_get_visited_states() const; unsigned long mc_get_executed_trans() const; bool mc_check_deadlock() const; + void mc_show_deadlock() const; + smx_actor_t mc_smx_simcall_get_issuer(s_smx_simcall const* req) const; std::vector& get_actors() const; bool actor_is_enabled(aid_t pid) const; void mc_assert(bool notNull, const char* message = "") const; @@ -57,6 +60,11 @@ public: PageStore& mc_page_store() const; void mc_cleanup(); + // SIMCALL FUNCTIONS + bool request_depend(smx_simcall_t req1, smx_simcall_t req2) const; + std::string request_to_string(smx_simcall_t req, int value, RequestType request_type) const; + const char *simix_simcall_name(e_smx_simcall_t kind) const; + // SESSION FUNCTIONS void s_initialize() const; void s_close() const;