X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/11ce6b59ec29ed55d422a0c97a7d734ac1eb7a39..0eead244337fde8f0508629f8f8473f946c19f88:/src/mc/SafetyChecker.cpp diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index 0f20188764..0c8d7aff95 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -7,7 +7,9 @@ #include #include -#include +#include +#include +#include #include #include @@ -23,6 +25,8 @@ #include "src/mc/Checker.hpp" #include "src/mc/SafetyChecker.hpp" #include "src/mc/VisitedState.hpp" +#include "src/mc/Transition.hpp" +#include "src/mc/Session.hpp" #include "src/xbt/mmalloc/mmprivate.h" @@ -39,7 +43,7 @@ static void MC_show_non_termination(void) XBT_INFO("Counter-example execution trace:"); for (auto& s : mc_model_checker->getChecker()->getTextualTrace()) XBT_INFO("%s", s.c_str()); - MC_print_statistics(mc_stats); + simgrid::mc::session->logState(); } static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* state2) @@ -65,13 +69,8 @@ bool SafetyChecker::checkNonTermination(simgrid::mc::State* current_state) RecordTrace SafetyChecker::getRecordTrace() // override { RecordTrace res; - for (auto const& state : stack_) { - int value = 0; - smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value); - const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); - const int pid = issuer->pid; - res.push_back(RecordTraceElement(pid, value)); - } + for (auto const& state : stack_) + res.push_back(state->getTransition()); return res; } @@ -79,24 +78,27 @@ std::vector SafetyChecker::getTextualTrace() // override { std::vector trace; for (auto const& state : stack_) { - int value; - smx_simcall_t req = MC_state_get_executed_request(state.get(), &value); - if (req) { - char* req_str = simgrid::mc::request_to_string( - req, value, simgrid::mc::RequestType::executed); - trace.push_back(req_str); - xbt_free(req_str); - } + 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)); } return trace; } +void SafetyChecker::logState() // 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); +} + int SafetyChecker::run() { this->init(); - int value; - while (!stack_.empty()) { /* Get current state */ @@ -108,13 +110,13 @@ int SafetyChecker::run() stack_.size(), state, state->num, state->interleaveSize()); - mc_stats->visited_states++; + mc_model_checker->visited_states++; // The interleave set is empty or the maximum depth is reached, // let's back-track. smx_simcall_t req = nullptr; if (stack_.size() > (std::size_t) _sg_mc_max_depth - || (req = MC_state_get_request(state, &value)) == nullptr + || (req = MC_state_get_request(state)) == nullptr || visitedState_ != nullptr) { int res = this->backtrack(); if (res) @@ -125,30 +127,22 @@ int 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", + simgrid::mc::request_to_string( + req, state->transition.argument, simgrid::mc::RequestType::simix).c_str()); - if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { - char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix); - XBT_DEBUG("Execute: %s", req_str); - xbt_free(req_str); - } - - char* req_str = nullptr; + std::string req_str; if (dot_output != nullptr) - req_str = simgrid::mc::request_get_dot_output(req, value); + req_str = simgrid::mc::request_get_dot_output(req, state->transition.argument); - MC_state_set_executed_request(state, req, value); - mc_stats->executed_transitions++; - - // TODO, bundle both operations in a single message - // MC_execute_transition(req, value) + mc_model_checker->executed_transitions++; /* Answer the request */ - simgrid::mc::handle_simcall(req, value); - mc_model_checker->wait_for_requests(); + this->getSession().execute(state->transition); /* Create the new expanded state */ std::unique_ptr next_state = - std::unique_ptr(MC_state_new()); + std::unique_ptr(MC_state_new(++expandedStatesCount_)); if (_sg_mc_termination && this->checkNonTermination(next_state.get())) { MC_show_non_termination(); @@ -156,31 +150,30 @@ int SafetyChecker::run() } if (_sg_mc_visited == 0 - || (visitedState_ = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) { + || (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)) { - MC_state_interleave_process(next_state.get(), &p.copy); + if (simgrid::mc::process_is_enabled(p.copy.getBuffer())) { + next_state->interleave(p.copy.getBuffer()); if (reductionMode_ != simgrid::mc::ReductionMode::none) break; } if (dot_output != nullptr) - std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str); + std::fprintf(dot_output, "\"%d\" -> \"%d\" [%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); + std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", + state->num, + visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str()); stack_.push_back(std::move(next_state)); - - if (dot_output != nullptr) - xbt_free(req_str); } XBT_INFO("No property violation found."); - MC_print_statistics(mc_stats); - initial_global_state = nullptr; + simgrid::mc::session->logState(); return SIMGRID_MC_EXIT_SUCCESS; } @@ -219,46 +212,49 @@ int SafetyChecker::backtrack() std::unique_ptr state = std::move(stack_.back()); stack_.pop_back(); if (reductionMode_ == simgrid::mc::ReductionMode::dpor) { - smx_simcall_t req = MC_state_get_internal_request(state.get()); + 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_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, MC_state_get_internal_request(prev_state))) { + && 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; - smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value); - char* req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal); - XBT_DEBUG("%s (state=%d)", req_str, prev_state->num); - xbt_free(req_str); - prev_req = MC_state_get_executed_request(state.get(), &value); - req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed); - XBT_DEBUG("%s (state=%d)", req_str, state->num); - xbt_free(req_str); + 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].done()) - MC_state_interleave_process(prev_state, issuer); + if (!prev_state->processStates[issuer->pid].isDone()) + prev_state->interleave(issuer); else XBT_DEBUG("Process %p is in done set", req->issuer); break; - } else if (req->issuer == MC_state_get_internal_request(prev_state)->issuer) { + } else if (req->issuer == prev_state->internal_req.issuer) { - XBT_DEBUG("Simcall %d and %d with same issuer", req->call, MC_state_get_internal_request(prev_state)->call); + XBT_DEBUG("Simcall %d and %d with same issuer", req->call, prev_state->internal_req.call); break; } else { - const smx_process_t previous_issuer = MC_smx_simcall_get_issuer(MC_state_get_internal_request(prev_state)); + 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, - MC_state_get_internal_request(prev_state)->call, + prev_state->internal_req.call, previous_issuer->pid, prev_state->num); @@ -272,7 +268,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; @@ -284,6 +280,31 @@ int SafetyChecker::backtrack() return SIMGRID_MC_EXIT_SUCCESS; } +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++; + } +} + void SafetyChecker::init() { reductionMode_ = simgrid::mc::reduction_mode; @@ -296,32 +317,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()); + std::unique_ptr(MC_state_new(++expandedStatesCount_)); XBT_DEBUG("**************************************************"); XBT_DEBUG("Initial state"); - /* Wait for requests (schedules processes) */ - mc_model_checker->wait_for_requests(); - /* 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)) { - MC_state_interleave_process(initial_state.get(), &p.copy); + if (simgrid::mc::process_is_enabled(p.copy.getBuffer())) { + initial_state->interleave(p.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)