X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/cf64c8ceb2027a65be8789e5fb36902e9274be4c..07483e97b12350d1d293f19689575f0fbdcf0246:/src/mc/SafetyChecker.cpp diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index 5e106adb04..47e2e70e4c 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -59,8 +59,7 @@ bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state) { for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) if (snapshot_compare(i->get(), current_state) == 0){ - XBT_INFO("Non-progressive cycle : state %d -> state %d", - (*i)->num, current_state->num); + XBT_INFO("Non-progressive cycle: state %d -> state %d", (*i)->num, current_state->num); return true; } return false; @@ -97,8 +96,6 @@ void SafetyChecker::logState() // override int SafetyChecker::run() { - this->init(); - while (!stack_.empty()) { /* Get current state */ @@ -142,7 +139,7 @@ int SafetyChecker::run() /* Create the new expanded state */ std::unique_ptr next_state = - std::unique_ptr(MC_state_new(++expandedStatesCount_)); + std::unique_ptr(new simgrid::mc::State(++expandedStatesCount_)); if (_sg_mc_termination && this->checkNonTermination(next_state.get())) { MC_show_non_termination(); @@ -153,9 +150,9 @@ int SafetyChecker::run() || (visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true)) == nullptr) { /* Get an enabled process and insert it in the interleave set of the next state */ - for (auto& p : mc_model_checker->process().simix_processes()) - if (simgrid::mc::process_is_enabled(&p.copy)) { - next_state->interleave(&p.copy); + for (auto& p : mc_model_checker->process().actors()) + if (simgrid::mc::actor_is_enabled(p.copy.getBuffer())) { + next_state->interleave(p.copy.getBuffer()); if (reductionMode_ != simgrid::mc::ReductionMode::none) break; } @@ -174,7 +171,6 @@ int SafetyChecker::run() XBT_INFO("No property violation found."); simgrid::mc::session->logState(); - initial_global_state = nullptr; return SIMGRID_MC_EXIT_SUCCESS; } @@ -217,11 +213,10 @@ int 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 smx_process_t issuer = MC_smx_simcall_get_issuer(req); + 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(); - if (reductionMode_ != simgrid::mc::ReductionMode::none - && simgrid::mc::request_depend(req, &prev_state->internal_req)) { + if (simgrid::mc::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; @@ -252,7 +247,7 @@ int SafetyChecker::backtrack() } else { - const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(&prev_state->internal_req); + 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", req->call, issuer->pid, state->num, prev_state->internal_req.call, @@ -269,7 +264,7 @@ int SafetyChecker::backtrack() XBT_DEBUG("Back-tracking to state %d at depth %zi", state->num, stack_.size() + 1); stack_.push_back(std::move(state)); - simgrid::mc::replay(stack_); + this->restoreState(); XBT_DEBUG("Back-tracking to state %d at depth %zi done", stack_.back()->num, stack_.size()); break; @@ -281,10 +276,35 @@ int SafetyChecker::backtrack() return SIMGRID_MC_EXIT_SUCCESS; } -void SafetyChecker::init() +void SafetyChecker::restoreState() +{ + /* Intermediate backtracking */ + { + simgrid::mc::State* state = stack_.back().get(); + if (state->system_state) { + simgrid::mc::restore_snapshot(state->system_state); + return; + } + } + + /* Restore the initial state */ + simgrid::mc::session->restoreInitialState(); + + /* Traverse the stack from the state at position start and re-execute the transitions */ + for (std::unique_ptr const& state : stack_) { + if (state == stack_.back()) + break; + session->execute(state->transition); + /* Update statistics */ + mc_model_checker->visited_states++; + mc_model_checker->executed_transitions++; + } +} + +SafetyChecker::SafetyChecker(Session& session) : Checker(session) { reductionMode_ = simgrid::mc::reduction_mode; - if( _sg_mc_termination) + if (_sg_mc_termination) reductionMode_ = simgrid::mc::ReductionMode::none; else if (reductionMode_ == simgrid::mc::ReductionMode::unset) reductionMode_ = simgrid::mc::ReductionMode::dpor; @@ -293,33 +313,25 @@ void SafetyChecker::init() XBT_INFO("Check non progressive cycles"); else XBT_INFO("Check a safety property"); - mc_model_checker->wait_for_requests(); + simgrid::mc::session->initialize(); XBT_DEBUG("Starting the safety algorithm"); std::unique_ptr initial_state = - std::unique_ptr(MC_state_new(++expandedStatesCount_)); + std::unique_ptr(new simgrid::mc::State(++expandedStatesCount_)); XBT_DEBUG("**************************************************"); XBT_DEBUG("Initial state"); - /* Get an enabled process and insert it in the interleave set of the initial state */ - for (auto& p : mc_model_checker->process().simix_processes()) - if (simgrid::mc::process_is_enabled(&p.copy)) { - initial_state->interleave(&p.copy); + /* Get an enabled actor and insert it in the interleave set of the initial state */ + for (auto& actor : mc_model_checker->process().actors()) + if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) { + initial_state->interleave(actor.copy.getBuffer()); if (reductionMode_ != simgrid::mc::ReductionMode::none) break; } stack_.push_back(std::move(initial_state)); - - /* Save the initial state */ - initial_global_state = std::unique_ptr(new s_mc_global_t()); - initial_global_state->snapshot = simgrid::mc::take_snapshot(0); -} - -SafetyChecker::SafetyChecker(Session& session) : Checker(session) -{ } SafetyChecker::~SafetyChecker()