X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/975faee3cab10e7dadee66a29bbdb7bfaef6e05f..fa84bee017477630eea9a93890e0e2abf3855bf9:/src/mc/checker/SafetyChecker.cpp diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index 6d06ac4601..cefde1f770 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -21,7 +21,6 @@ #include "src/mc/mc_private.hpp" #include "src/mc/mc_record.hpp" #include "src/mc/mc_request.hpp" -#include "src/mc/mc_smx.hpp" #include "src/xbt/mmalloc/mmprivate.h" @@ -41,8 +40,7 @@ void SafetyChecker::check_non_termination(const State* current_state) XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***"); XBT_INFO("******************************************"); XBT_INFO("Counter-example execution trace:"); - auto checker = api::get().mc_get_checker(); - for (auto const& s : checker->get_textual_trace()) + for (auto const& s : get_textual_trace()) XBT_INFO(" %s", s.c_str()); api::get().dump_record_path(); api::get().log_state(); @@ -121,8 +119,7 @@ void SafetyChecker::run() // If there are processes to interleave and the maximum depth has not been // reached then perform one step of the exploration algorithm. - XBT_DEBUG("Execute: %s", - api::get().request_to_string(req, state->transition_.times_considered_, RequestType::simix).c_str()); + XBT_DEBUG("Execute: %s", api::get().request_to_string(req, state->transition_.times_considered_).c_str()); std::string req_str; if (dot_output != nullptr) @@ -176,11 +173,7 @@ void SafetyChecker::backtrack() { stack_.pop_back(); - /* Check for deadlocks */ - if (api::get().mc_check_deadlock()) { - api::get().mc_show_deadlock(); - throw DeadlockError(); - } + api::get().mc_check_deadlock(); /* Traverse the stack backwards until a state with a non empty interleave set is found, deleting all the states that * have it empty in the way. For each deleted state, check if the request that has generated it (from its @@ -191,40 +184,35 @@ void SafetyChecker::backtrack() std::unique_ptr state = std::move(stack_.back()); stack_.pop_back(); if (reductionMode_ == ReductionMode::dpor) { - smx_simcall_t req = &state->internal_req_; - if (req->call_ == simix::Simcall::MUTEX_LOCK || req->call_ == simix::Simcall::MUTEX_TRYLOCK) - xbt_die("Mutex is currently not supported with DPOR, use --cfg=model-check/reduction:none"); - - const kernel::actor::ActorImpl* issuer = api::get().simcall_get_issuer(req); + auto call = state->executed_req_.call_; + const kernel::actor::ActorImpl* issuer = api::get().simcall_get_issuer(&state->executed_req_); for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) { State* prev_state = i->get(); - if (api::get().simcall_check_dependency(req, &prev_state->internal_req_)) { + if (state->executed_req_.issuer_ == prev_state->executed_req_.issuer_) { + XBT_DEBUG("Simcall %s and %s with same issuer", SIMIX_simcall_name(call), + SIMIX_simcall_name(prev_state->executed_req_.call_)); + break; + } else if (api::get().simcall_check_dependency(&state->internal_req_, &prev_state->internal_req_)) { if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { XBT_DEBUG("Dependent Transitions:"); int value = prev_state->transition_.times_considered_; smx_simcall_t prev_req = &prev_state->executed_req_; - XBT_DEBUG("%s (state=%d)", api::get().request_to_string(prev_req, value, RequestType::internal).c_str(), - prev_state->num_); + XBT_DEBUG("%s (state=%d)", api::get().request_to_string(prev_req, value).c_str(), prev_state->num_); value = state->transition_.times_considered_; prev_req = &state->executed_req_; - XBT_DEBUG("%s (state=%d)", api::get().request_to_string(prev_req, value, RequestType::executed).c_str(), - state->num_); + XBT_DEBUG("%s (state=%d)", api::get().request_to_string(prev_req, value).c_str(), state->num_); } if (not prev_state->actor_states_[issuer->get_pid()].is_done()) prev_state->mark_todo(issuer); else - 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", api::get().simcall_get_name(req->call_), - api::get().simcall_get_name(prev_state->internal_req_.call_)); + XBT_DEBUG("Actor %s %ld is in done set", issuer->get_cname(), issuer->get_pid()); break; } else { - const kernel::actor::ActorImpl* previous_issuer = api::get().simcall_get_issuer(&prev_state->internal_req_); + const kernel::actor::ActorImpl* previous_issuer = api::get().simcall_get_issuer(&prev_state->executed_req_); XBT_DEBUG("Simcall %s, process %ld (state %d) and simcall %s, process %ld (state %d) are independent", - api::get().simcall_get_name(req->call_), issuer->get_pid(), state->num_, - api::get().simcall_get_name(prev_state->internal_req_.call_), previous_issuer->get_pid(), prev_state->num_); + SIMIX_simcall_name(call), issuer->get_pid(), state->num_, + SIMIX_simcall_name(prev_state->executed_req_.call_), previous_issuer->get_pid(), prev_state->num_); } } } @@ -247,7 +235,7 @@ void SafetyChecker::restore_state() /* Intermediate backtracking */ const State* last_state = stack_.back().get(); if (last_state->system_state_) { - Api::get().restore_state(last_state->system_state_); + api::get().restore_state(last_state->system_state_); return; } @@ -265,7 +253,7 @@ void SafetyChecker::restore_state() } } -SafetyChecker::SafetyChecker() : Checker() +SafetyChecker::SafetyChecker(Session* session) : Checker(session) { reductionMode_ = reduction_mode; if (_sg_mc_termination) @@ -302,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