X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/90319766c67d84542aace23dac42b74a63b1c707..35b406733ae5c5b8463d3712a09b430d8585ce6d:/src/mc/checker/SafetyChecker.cpp diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index 2d766e2f70..643c734c5b 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -14,18 +14,18 @@ #include #include -#include "src/mc/mc_state.h" -#include "src/mc/mc_request.h" -#include "src/mc/mc_safety.h" +#include "src/mc/Session.hpp" +#include "src/mc/Transition.hpp" +#include "src/mc/VisitedState.hpp" +#include "src/mc/checker/SafetyChecker.hpp" +#include "src/mc/mc_exit.h" #include "src/mc/mc_private.h" #include "src/mc/mc_record.h" +#include "src/mc/mc_request.h" +#include "src/mc/mc_safety.h" #include "src/mc/mc_smx.h" -#include "src/mc/Client.hpp" -#include "src/mc/mc_exit.h" -#include "src/mc/checker/SafetyChecker.hpp" -#include "src/mc/VisitedState.hpp" -#include "src/mc/Transition.hpp" -#include "src/mc/Session.hpp" +#include "src/mc/mc_state.h" +#include "src/mc/remote/Client.hpp" #include "src/xbt/mmalloc/mmprivate.h" @@ -93,7 +93,7 @@ void SafetyChecker::run() { /* This function runs the DFS algorithm the state space. * We do so iteratively instead of recursively, dealing with the call stack manually. - * This allows to explore the call stack when we want to. */ + * This allows to explore the call stack at wish. */ while (!stack_.empty()) { @@ -116,7 +116,7 @@ void SafetyChecker::run() // Backtrack if we are revisiting a state we saw previously if (visitedState_ != nullptr) { XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", - visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num); + visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num); visitedState_ = nullptr; this->backtrack(); @@ -124,7 +124,10 @@ void SafetyChecker::run() } // Search an enabled transition in the current state; backtrack if the interleave set is empty + // get_request also sets state.transition to be the one corresponding to the returned req smx_simcall_t req = MC_state_get_request(state); + // req is now the transition of the process that was selected to be executed + if (req == nullptr) { XBT_DEBUG("There are no more processes to interleave. (depth %zi)", stack_.size() + 1); @@ -144,10 +147,10 @@ void SafetyChecker::run() mc_model_checker->executed_transitions++; - /* Answer the request */ + /* Actually answer the request: let execute the selected request (MCed does one step) */ this->getSession().execute(state->transition); - /* Create the new expanded state */ + /* Create the new expanded state (copy the state of MCed into our MCer data) */ std::unique_ptr next_state = std::unique_ptr(new simgrid::mc::State(++expandedStatesCount_)); @@ -155,7 +158,7 @@ void SafetyChecker::run() this->checkNonTermination(next_state.get()); /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */ - if (_sg_mc_visited == true) + if (_sg_mc_max_visited_states > 0) visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true); /* If this is a new state (or if we don't care about state-equality reduction) */ @@ -174,9 +177,9 @@ void SafetyChecker::run() state->num, next_state->num, req_str.c_str()); } else if (dot_output != nullptr) - std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - state->num, - visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str()); + std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, + visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num, + req_str.c_str()); stack_.push_back(std::move(next_state)); } @@ -208,8 +211,8 @@ void SafetyChecker::backtrack() if (reductionMode_ == simgrid::mc::ReductionMode::dpor) { smx_simcall_t req = &state->internal_req; 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"); + xbt_die("Mutex is currently not supported with DPOR, use --cfg=model-check/reduction:none"); + const smx_actor_t issuer = MC_smx_simcall_get_issuer(req); for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) { simgrid::mc::State* prev_state = i->get(); @@ -230,7 +233,7 @@ void SafetyChecker::backtrack() state->num); } - if (!prev_state->processStates[issuer->pid].isDone()) + if (!prev_state->actorStates[issuer->pid].isDone()) prev_state->interleave(issuer); else XBT_DEBUG("Process %p is in done set", req->issuer); @@ -245,7 +248,7 @@ void SafetyChecker::backtrack() } else { const smx_actor_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req); - XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independant", + XBT_DEBUG("Simcall %d, process %lu (state %d) and simcall %d, process %lu (state %d) are independent", req->call, issuer->pid, state->num, prev_state->internal_req.call, previous_issuer->pid, @@ -258,8 +261,7 @@ void SafetyChecker::backtrack() if (state->interleaveSize() && stack_.size() < (std::size_t) _sg_mc_max_depth) { /* We found a back-tracking point, let's loop */ - XBT_DEBUG("Back-tracking to state %d at depth %zi", - state->num, stack_.size() + 1); + XBT_DEBUG("Back-tracking to state %d at depth %zi", state->num, stack_.size() + 1); stack_.push_back(std::move(state)); this->restoreState(); XBT_DEBUG("Back-tracking to state %d at depth %zi done", @@ -306,7 +308,9 @@ SafetyChecker::SafetyChecker(Session& session) : Checker(session) if (_sg_mc_termination) XBT_INFO("Check non progressive cycles"); else - XBT_INFO("Check a safety property"); + XBT_INFO("Check a safety property. Reduction is: %s.", + (reductionMode_ == simgrid::mc::ReductionMode::none ? "none": + (reductionMode_ == simgrid::mc::ReductionMode::dpor ? "dpor": "unknown"))); simgrid::mc::session->initialize(); XBT_DEBUG("Starting the safety algorithm");