X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/90319766c67d84542aace23dac42b74a63b1c707..90b0fa923c841996f89a17c252a443a65493fbfc:/src/mc/checker/SafetyChecker.cpp diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index 2d766e2f70..3713b9378b 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -1,9 +1,21 @@ -/* Copyright (c) 2016. The SimGrid Team. - * All rights reserved. */ +/* Copyright (c) 2016-2022. The SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ +#include "src/mc/checker/SafetyChecker.hpp" +#include "src/mc/Session.hpp" +#include "src/mc/VisitedState.hpp" +#include "src/mc/mc_config.hpp" +#include "src/mc/mc_exit.hpp" +#include "src/mc/mc_private.hpp" +#include "src/mc/mc_record.hpp" +#include "src/mc/transition/Transition.hpp" + +#include "src/xbt/mmalloc/mmprivate.h" +#include "xbt/log.h" +#include "xbt/sysdep.h" + #include #include @@ -11,331 +23,296 @@ #include #include -#include -#include - -#include "src/mc/mc_state.h" -#include "src/mc/mc_request.h" -#include "src/mc/mc_safety.h" -#include "src/mc/mc_private.h" -#include "src/mc/mc_record.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" +using api = simgrid::mc::Api; -#include "src/xbt/mmalloc/mmprivate.h" +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc, "Logging specific to MC safety verification "); -XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc, - "Logging specific to MC safety verification "); namespace simgrid { namespace mc { -static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2) -{ - simgrid::mc::Snapshot* s1 = state1->system_state.get(); - simgrid::mc::Snapshot* s2 = state2->system_state.get(); - int num1 = state1->num; - int num2 = state2->num; - return snapshot_compare(num1, s1, num2, s2); -} +xbt::signal SafetyChecker::on_exploration_start_signal; +xbt::signal SafetyChecker::on_backtracking_signal; + +xbt::signal SafetyChecker::on_state_creation_signal; + +xbt::signal SafetyChecker::on_restore_system_state_signal; +xbt::signal SafetyChecker::on_restore_initial_state_signal; +xbt::signal SafetyChecker::on_transition_replay_signal; +xbt::signal SafetyChecker::on_transition_execute_signal; -void SafetyChecker::checkNonTermination(simgrid::mc::State* current_state) +xbt::signal SafetyChecker::on_log_state_signal; + +void SafetyChecker::check_non_termination(const State* current_state) { for (auto state = stack_.rbegin(); state != stack_.rend(); ++state) - if (snapshot_compare(state->get(), current_state) == 0) { - XBT_INFO("Non-progressive cycle: state %d -> state %d", (*state)->num, current_state->num); + if (api::get().snapshot_equal((*state)->system_state_.get(), current_state->system_state_.get())) { + XBT_INFO("Non-progressive cycle: state %ld -> state %ld", (*state)->num_, current_state->num_); XBT_INFO("******************************************"); XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***"); XBT_INFO("******************************************"); XBT_INFO("Counter-example execution trace:"); - for (auto& s : mc_model_checker->getChecker()->getTextualTrace()) - XBT_INFO("%s", s.c_str()); - simgrid::mc::session->logState(); + for (auto const& s : get_textual_trace()) + XBT_INFO(" %s", s.c_str()); + XBT_INFO("Path = %s", get_record_trace().to_string().c_str()); + api::get().log_state(); - throw simgrid::mc::TerminationError(); + throw TerminationError(); } } -RecordTrace SafetyChecker::getRecordTrace() // override +RecordTrace SafetyChecker::get_record_trace() // override { RecordTrace res; for (auto const& state : stack_) - res.push_back(state->getTransition()); + res.push_back(state->get_transition()); return res; } -std::vector SafetyChecker::getTextualTrace() // override +std::vector SafetyChecker::get_textual_trace() // override { std::vector trace; - for (auto const& state : stack_) { - int value = state->transition.argument; - smx_simcall_t req = &state->executed_req; - if (req) - trace.push_back(simgrid::mc::request_to_string( - req, value, simgrid::mc::RequestType::executed)); - } + for (auto const& state : stack_) + trace.push_back(state->get_transition()->to_string()); return trace; } -void SafetyChecker::logState() // override +void SafetyChecker::log_state() // override { - Checker::logState(); - XBT_INFO("Expanded states = %lu", expandedStatesCount_); - XBT_INFO("Visited states = %lu", mc_model_checker->visited_states); - XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions); + on_log_state_signal(); + XBT_INFO("DFS exploration ended. %ld unique states visited; %ld backtracks (%lu transition replays, %lu states " + "visited overall)", + State::get_expanded_states(), backtrack_count_, api::get().mc_get_visited_states(), + Transition::get_replayed_transitions()); } void SafetyChecker::run() { + on_exploration_start_signal(); /* 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. */ - - while (!stack_.empty()) { + * This allows one to explore the call stack at will. */ + while (not stack_.empty()) { /* Get current state */ - simgrid::mc::State* state = stack_.back().get(); + State* state = stack_.back().get(); XBT_DEBUG("**************************************************"); - XBT_DEBUG("Exploration depth=%zi (state=%p, num %d)(%zu interleave)", - stack_.size(), state, state->num, state->interleaveSize()); + XBT_VERB("Exploration depth=%zu (state=%p, num %ld)(%zu interleave)", stack_.size(), state, state->num_, + state->count_todo()); - mc_model_checker->visited_states++; + api::get().mc_inc_visited_states(); // Backtrack if we reached the maximum depth if (stack_.size() > (std::size_t)_sg_mc_max_depth) { - XBT_WARN("/!\\ Max depth reached ! /!\\ "); + if (reductionMode_ == ReductionMode::dpor) { + XBT_ERROR("/!\\ Max depth of %d reached! THIS WILL PROBABLY BREAK the dpor reduction /!\\", + _sg_mc_max_depth.get()); + XBT_ERROR("/!\\ If bad things happen, disable dpor with --cfg=model-check/reduction:none /!\\"); + } else + XBT_WARN("/!\\ Max depth reached ! /!\\ "); this->backtrack(); continue; } // 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); + if (visited_state_ != nullptr) { + XBT_DEBUG("State already visited (equal to state %ld), exploration stopped on this path.", + visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num); - visitedState_ = nullptr; + visited_state_ = nullptr; this->backtrack(); continue; } - // Search an enabled transition in the current state; backtrack if the interleave set is empty - smx_simcall_t req = MC_state_get_request(state); - if (req == nullptr) { - XBT_DEBUG("There are no more processes to interleave. (depth %zi)", stack_.size() + 1); + // Search for the next transition + int next = state->next_transition(); + + if (next < 0) { // If there is no more transition in the current state, backtrack. + XBT_DEBUG("There remains %zu actors, but none to interleave (depth %zu).", + mc_model_checker->get_remote_process().actors().size(), stack_.size() + 1); + if (mc_model_checker->get_remote_process().actors().empty()) + mc_model_checker->finalize_app(); this->backtrack(); continue; } + /* Actually answer the request: let's execute the selected request (MCed does one step) */ + state->execute_next(next); + on_transition_execute_signal(state->get_transition()); + // 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", - simgrid::mc::request_to_string( - req, state->transition.argument, simgrid::mc::RequestType::simix).c_str()); + XBT_DEBUG("Execute: %s", state->get_transition()->to_string().c_str()); std::string req_str; if (dot_output != nullptr) - req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument); - - mc_model_checker->executed_transitions++; + req_str = api::get().request_get_dot_output(state->get_transition()); - /* Answer the request */ - this->getSession().execute(state->transition); - - /* Create the new expanded state */ - std::unique_ptr next_state = - std::unique_ptr(new simgrid::mc::State(++expandedStatesCount_)); + /* Create the new expanded state (copy the state of MCed into our MCer data) */ + auto next_state = std::make_unique(); + on_state_creation_signal(next_state.get()); if (_sg_mc_termination) - this->checkNonTermination(next_state.get()); + this->check_non_termination(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) - visitedState_ = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), true); + if (_sg_mc_max_visited_states > 0) + visited_state_ = visited_states_.addVisitedState(next_state->num_, next_state.get(), true); /* If this is a new state (or if we don't care about state-equality reduction) */ - if (visitedState_ == nullptr) { - + if (visited_state_ == nullptr) { /* Get an enabled process and insert it in the interleave set of the next state */ - for (auto& actor : mc_model_checker->process().actors()) - if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) { - next_state->interleave(actor.copy.getBuffer()); - if (reductionMode_ == simgrid::mc::ReductionMode::dpor) - break; + auto actors = api::get().get_actors(); + for (auto& remoteActor : actors) { + auto actor = remoteActor.copy.get_buffer(); + if (get_session().actor_is_enabled(actor->get_pid())) { + next_state->mark_todo(actor->get_pid()); + if (reductionMode_ == ReductionMode::dpor) + break; // With DPOR, we take the first enabled transition } + } if (dot_output != nullptr) - std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - state->num, next_state->num, req_str.c_str()); + std::fprintf(dot_output, "\"%ld\" -> \"%ld\" [%s];\n", 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, "\"%ld\" -> \"%ld\" [%s];\n", state->num_, + visited_state_->original_num == -1 ? visited_state_->num : visited_state_->original_num, + req_str.c_str()); stack_.push_back(std::move(next_state)); } - XBT_INFO("No property violation found."); - simgrid::mc::session->logState(); + api::get().log_state(); } void SafetyChecker::backtrack() { + backtrack_count_++; + XBT_VERB("Backtracking from %s", get_record_trace().to_string().c_str()); + on_backtracking_signal(); stack_.pop_back(); - /* Check for deadlocks */ - if (mc_model_checker->checkDeadlock()) { - MC_show_deadlock(); - throw simgrid::mc::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 it's predecessor state), depends on any other previous request - executed before it. If it does then add it to the interleave set of the - state that executed that previous request. */ + /* 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 + * predecessor state), depends on any other previous request executed before it. If it does then add it to the + * interleave set of the state that executed that previous request. */ - while (!stack_.empty()) { - std::unique_ptr state = std::move(stack_.back()); + while (not stack_.empty()) { + std::unique_ptr state = std::move(stack_.back()); stack_.pop_back(); - 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"); - const smx_actor_t issuer = MC_smx_simcall_get_issuer(req); + if (reductionMode_ == ReductionMode::dpor) { + aid_t issuer_id = state->get_transition()->aid_; for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) { - simgrid::mc::State* prev_state = i->get(); - 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; - smx_simcall_t prev_req = &prev_state->executed_req; - XBT_DEBUG("%s (state=%d)", - simgrid::mc::request_to_string( - prev_req, value, simgrid::mc::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, simgrid::mc::RequestType::executed).c_str(), - state->num); - } - - if (!prev_state->processStates[issuer->pid].isDone()) - prev_state->interleave(issuer); - else - XBT_DEBUG("Process %p is in done set", req->issuer); - + State* prev_state = i->get(); + if (state->get_transition()->aid_ == prev_state->get_transition()->aid_) { + XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_string().c_str(), + prev_state->get_transition()->to_string().c_str(), issuer_id); break; + } else if (prev_state->get_transition()->depends(state->get_transition())) { + XBT_VERB("Dependent Transitions:"); + XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->num_); + XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->num_); - } else if (req->issuer == prev_state->internal_req.issuer) { - - XBT_DEBUG("Simcall %d and %d with same issuer", req->call, prev_state->internal_req.call); + if (not prev_state->actor_states_[issuer_id].is_done()) + prev_state->mark_todo(issuer_id); + else + XBT_DEBUG("Actor %ld is in done set", issuer_id); break; - } 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", - req->call, issuer->pid, state->num, - prev_state->internal_req.call, - previous_issuer->pid, - prev_state->num); - + XBT_VERB("INDEPENDENT Transitions:"); + XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->num_); + XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->num_); } } } - if (state->interleaveSize() - && stack_.size() < (std::size_t) _sg_mc_max_depth) { + if (state->count_todo() && 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 %ld at depth %zu", state->num_, stack_.size() + 1); stack_.push_back(std::move(state)); - this->restoreState(); - XBT_DEBUG("Back-tracking to state %d at depth %zi done", - stack_.back()->num, stack_.size()); + this->restore_state(); + XBT_DEBUG("Back-tracking to state %ld at depth %zu done", stack_.back()->num_, stack_.size()); break; } else { - XBT_DEBUG("Delete state %d at depth %zi", - state->num, stack_.size() + 1); + XBT_DEBUG("Delete state %ld at depth %zu", state->num_, stack_.size() + 1); } } } -void SafetyChecker::restoreState() +void SafetyChecker::restore_state() { - /* Intermediate backtracking */ - simgrid::mc::State* state = stack_.back().get(); - if (state->system_state) { - simgrid::mc::restore_snapshot(state->system_state); + /* If asked to rollback on a state that has a snapshot, restore it */ + State* last_state = stack_.back().get(); + if (last_state->system_state_) { + api::get().restore_state(last_state->system_state_); + on_restore_system_state_signal(last_state); return; } - /* Restore the initial state */ - simgrid::mc::session->restoreInitialState(); + /* if no snapshot, we need to restore the initial state and replay the transitions */ + get_session().restore_initial_state(); + on_restore_initial_state_signal(); /* 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()) + for (std::unique_ptr const& state : stack_) { + if (state == stack_.back()) // If we are arrived on the target state, don't replay the outgoing transition *. break; - session->execute(state->transition); + state->get_transition()->replay(); + on_transition_replay_signal(state->get_transition()); /* Update statistics */ - mc_model_checker->visited_states++; - mc_model_checker->executed_transitions++; + api::get().mc_inc_visited_states(); } } -SafetyChecker::SafetyChecker(Session& session) : Checker(session) +SafetyChecker::SafetyChecker(Session* session) : Checker(session) { - reductionMode_ = simgrid::mc::reduction_mode; + reductionMode_ = reduction_mode; if (_sg_mc_termination) - reductionMode_ = simgrid::mc::ReductionMode::none; - else if (reductionMode_ == simgrid::mc::ReductionMode::unset) - reductionMode_ = simgrid::mc::ReductionMode::dpor; + reductionMode_ = ReductionMode::none; + else if (reductionMode_ == ReductionMode::unset) + reductionMode_ = ReductionMode::dpor; if (_sg_mc_termination) XBT_INFO("Check non progressive cycles"); else - XBT_INFO("Check a safety property"); - simgrid::mc::session->initialize(); + XBT_INFO("Start a DFS exploration. Reduction is: %s.", + (reductionMode_ == ReductionMode::none ? "none" + : (reductionMode_ == ReductionMode::dpor ? "dpor" : "unknown"))); + + get_session().take_initial_snapshot(); XBT_DEBUG("Starting the safety algorithm"); - std::unique_ptr initial_state = - std::unique_ptr(new simgrid::mc::State(++expandedStatesCount_)); + auto initial_state = std::make_unique(); XBT_DEBUG("**************************************************"); - 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->process().actors()) - if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer())) { - initial_state->interleave(actor.copy.getBuffer()); - if (reductionMode_ != simgrid::mc::ReductionMode::none) + auto actors = api::get().get_actors(); + XBT_DEBUG("Initial state. %zu actors to consider", actors.size()); + for (auto& actor : actors) { + aid_t aid = actor.copy.get_buffer()->get_pid(); + if (get_session().actor_is_enabled(aid)) { + initial_state->mark_todo(aid); + if (reductionMode_ == ReductionMode::dpor) { + XBT_DEBUG("Actor %ld is TODO, DPOR is ON so let's go for this one.", aid); break; + } + XBT_DEBUG("Actor %ld is TODO", aid); } + } stack_.push_back(std::move(initial_state)); } -SafetyChecker::~SafetyChecker() -{ -} - -Checker* createSafetyChecker(Session& session) +Checker* create_safety_checker(Session* session) { return new SafetyChecker(session); } - -} -} + +} // namespace mc +} // namespace simgrid