X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/e8b892d82b85cf919ae6afe05617ea74e4e0cfbf..4493661dc7abfbb53a26fab6bacba9d15adb861d:/src/mc/ModelChecker.cpp diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index a753c9d3fa..8fca2ee299 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -1,17 +1,16 @@ -/* Copyright (c) 2008-2022. The SimGrid Team. All rights reserved. */ +/* Copyright (c) 2008-2023. 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/ModelChecker.hpp" -#include "src/mc/Session.hpp" -#include "src/mc/Transition.hpp" -#include "src/mc/TransitionComm.hpp" -#include "src/mc/checker/Checker.hpp" +#include "src/mc/explo/Exploration.hpp" +#include "src/mc/explo/LivenessChecker.hpp" #include "src/mc/mc_config.hpp" #include "src/mc/mc_exit.hpp" #include "src/mc/mc_private.hpp" #include "src/mc/remote/RemoteProcess.hpp" +#include "src/mc/transition/TransitionComm.hpp" #include "xbt/automaton.hpp" #include "xbt/system_error.hpp" @@ -24,16 +23,13 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker"); ::simgrid::mc::ModelChecker* mc_model_checker = nullptr; -using simgrid::mc::remote; - #ifdef __linux__ # define WAITPID_CHECKED_FLAGS __WALL #else # define WAITPID_CHECKED_FLAGS 0 #endif -namespace simgrid { -namespace mc { +namespace simgrid::mc { ModelChecker::ModelChecker(std::unique_ptr remote_simulation, int sockfd) : checker_side_(sockfd), remote_process_(std::move(remote_simulation)) @@ -56,6 +52,8 @@ void ModelChecker::start() } else if (events == EV_SIGNAL) { if (sig == SIGCHLD) mc->handle_waitpid(); + else + xbt_die("Unexpected signal: %d", sig); } else { xbt_die("Unexpected event"); } @@ -71,11 +69,9 @@ void ModelChecker::start() xbt_assert(waitpid(pid, &status, WAITPID_CHECKED_FLAGS) == pid && WIFSTOPPED(status) && WSTOPSIG(status) == SIGSTOP, "Could not wait model-checked process"); - if (not _sg_mc_dot_output_file.get().empty()) - MC_init_dot_output(); - setup_ignore(); + errno = 0; #ifdef __linux__ ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT); ptrace(PTRACE_CONT, pid, 0, 0); @@ -84,6 +80,11 @@ void ModelChecker::start() #else # error "no ptrace equivalent coded for this platform" #endif + xbt_assert(errno == 0, + "Ptrace does not seem to be usable in your setup (errno: %d). " + "If you run from within a docker, adding `--cap-add SYS_PTRACE` to the docker line may help. " + "If it does not help, please report this bug.", + errno); } static constexpr auto ignored_local_variables = { @@ -97,8 +98,8 @@ static constexpr auto ignored_local_variables = { void ModelChecker::setup_ignore() { const RemoteProcess& process = this->get_remote_process(); - for (auto const& var : ignored_local_variables) - process.ignore_local_variable(var.first, var.second); + for (auto const& [var, frame] : ignored_local_variables) + process.ignore_local_variable(var, frame); /* Static variable used for tracing */ process.ignore_global_variable("counter"); @@ -119,13 +120,12 @@ void ModelChecker::shutdown() void ModelChecker::resume() { - int res = checker_side_.get_channel().send(MessageType::CONTINUE); - if (res) + if (checker_side_.get_channel().send(MessageType::CONTINUE) != 0) throw xbt::errno_error(); remote_process_->clear_cache(); } -static void MC_report_crash(int status) +static void MC_report_crash(Exploration* explorer, int status) { XBT_INFO("**************************"); XBT_INFO("** CRASH IN THE PROGRAM **"); @@ -136,16 +136,20 @@ static void MC_report_crash(int status) XBT_INFO("From exit: %i", WEXITSTATUS(status)); if (not xbt_log_no_loc) XBT_INFO("%s core dump was generated by the system.", WCOREDUMP(status) ? "A" : "No"); - XBT_INFO("Counter-example execution trace:"); - for (auto const& s : mc_model_checker->getChecker()->get_textual_trace()) - XBT_INFO(" %s", s.c_str()); - dumpRecordPath(); - session_singleton->log_state(); - if (xbt_log_no_loc) { - XBT_INFO("Stack trace not displayed because you passed --log=no_loc"); - } else { - XBT_INFO("Stack trace:"); - mc_model_checker->get_remote_process().dump_stack(); + if (explorer) { + XBT_INFO("Counter-example execution trace:"); + for (auto const& s : explorer->get_textual_trace()) + XBT_INFO(" %s", s.c_str()); + XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with " + "--cfg=model-check/replay:'%s'", + explorer->get_record_trace().to_string().c_str()); + explorer->log_state(); + if (xbt_log_no_loc) { + XBT_INFO("Stack trace not displayed because you passed --log=no_loc"); + } else { + XBT_INFO("Stack trace:"); + explorer->get_remote_app().get_remote_process().dump_stack(); + } } } @@ -161,7 +165,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) xbt_assert(size == sizeof(message), "Broken message. Got %d bytes instead of %d.", (int)size, (int)sizeof(message)); memcpy(&message, buffer, sizeof(message)); - get_remote_process().init(message.mmalloc_default_mdp, message.maxpid, message.actors, message.dead_actors); + get_remote_process().init(message.mmalloc_default_mdp); break; } @@ -209,14 +213,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) xbt_assert(not message.callback, "Support for client-side function proposition is not implemented."); XBT_DEBUG("Received symbol: %s", message.name.data()); - if (property_automaton == nullptr) - property_automaton = xbt_automaton_new(); - - const RemoteProcess* process = &this->get_remote_process(); - RemotePtr address = remote((int*)message.data); - xbt::add_proposition(property_automaton, message.name.data(), - [process, address]() { return process->read(address); }); - + LivenessChecker::automaton_register_symbol(get_remote_process(), message.name.data(), remote((int*)message.data)); break; } @@ -228,10 +225,12 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) XBT_INFO("*** PROPERTY NOT VALID ***"); XBT_INFO("**************************"); XBT_INFO("Counter-example execution trace:"); - for (auto const& s : getChecker()->get_textual_trace()) + for (auto const& s : get_exploration()->get_textual_trace()) XBT_INFO(" %s", s.c_str()); - dumpRecordPath(); - session_singleton->log_state(); + XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with " + "--cfg=model-check/replay:'%s'", + get_exploration()->get_record_trace().to_string().c_str()); + exploration_->log_state(); this->exit(SIMGRID_MC_EXIT_SAFETY); @@ -269,9 +268,11 @@ void ModelChecker::handle_waitpid() // From PTRACE_O_TRACEEXIT: #ifdef __linux__ if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) { - xbt_assert(ptrace(PTRACE_GETEVENTMSG, remote_process_->pid(), 0, &status) != -1, "Could not get exit status"); + unsigned long eventmsg; + xbt_assert(ptrace(PTRACE_GETEVENTMSG, remote_process_->pid(), 0, &eventmsg) != -1, "Could not get exit status"); + status = static_cast(eventmsg); if (WIFSIGNALED(status)) { - MC_report_crash(status); + MC_report_crash(exploration_, status); this->get_remote_process().terminate(); this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); } @@ -291,7 +292,7 @@ void ModelChecker::handle_waitpid() } else if (WIFSIGNALED(status)) { - MC_report_crash(status); + MC_report_crash(exploration_, status); this->get_remote_process().terminate(); this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); } else if (WIFEXITED(status)) { @@ -309,107 +310,47 @@ void ModelChecker::wait_for_requests() checker_side_.dispatch(); } -Transition* ModelChecker::handle_simcall(Transition const& transition, bool new_transition) +Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool new_transition) { - s_mc_message_simcall_execute_t m; - memset(&m, 0, sizeof(m)); + s_mc_message_simcall_execute_t m = {}; m.type = MessageType::SIMCALL_EXECUTE; - m.aid_ = transition.aid_; - m.times_considered_ = transition.times_considered_; + m.aid_ = aid; + m.times_considered_ = times_considered; checker_side_.get_channel().send(m); - s_mc_message_simcall_execute_answer_t answer; - ssize_t s = checker_side_.get_channel().receive(answer); - xbt_assert(s != -1, "Could not receive message"); - xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALL_EXECUTE_ANSWER, - "Received unexpected message %s (%i, size=%i) " - "expected MessageType::SIMCALL_EXECUTE_ANSWER (%i, size=%i)", - to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_EXECUTE_ANSWER, - (int)sizeof(answer)); - this->remote_process_->clear_cache(); if (this->remote_process_->running()) checker_side_.dispatch(); // The app may send messages while processing the transition - if (new_transition) - return recv_transition(transition.aid_, transition.times_considered_, answer.simcall, answer.buffer); - else - return nullptr; -} -bool ModelChecker::simcall_is_visible(aid_t aid) -{ - xbt_assert(mc_model_checker != nullptr, "This should be called from the checker side"); - - s_mc_message_simcall_is_visible_t m; - memset(&m, 0, sizeof(m)); - m.type = MessageType::SIMCALL_IS_VISIBLE; - m.aid = aid; - checker_side_.get_channel().send(m); - - s_mc_message_simcall_is_visible_answer_t answer; - ssize_t s = checker_side_.get_channel().receive(answer); - xbt_assert(s != -1, "Could not receive message"); - xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALL_IS_VISIBLE_ANSWER, - "Received unexpected message %s (%i, size=%i) " - "expected MessageType::SIMCALL_IS_VISIBLE_ANSWER (%i, size=%i)", - to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_IS_VISIBLE_ANSWER, - (int)sizeof(answer)); - - XBT_DEBUG("is_visible(%ld) is returning %s", aid, answer.value ? "true" : "false"); - - this->remote_process_->clear_cache(); - return answer.value; -} - -std::string ModelChecker::simcall_dot_label(aid_t aid, int times_considered) -{ - xbt_assert(mc_model_checker != nullptr, "This should be called from the checker side"); - - s_mc_message_simcall_to_string_t m; - memset(&m, 0, sizeof(m)); - m.type = MessageType::SIMCALL_DOT_LABEL; - m.aid = aid; - m.time_considered = times_considered; - checker_side_.get_channel().send(m); - - s_mc_message_simcall_to_string_answer_t answer; + s_mc_message_simcall_execute_answer_t answer; ssize_t s = checker_side_.get_channel().receive(answer); xbt_assert(s != -1, "Could not receive message"); - xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALL_DOT_LABEL_ANSWER, - "Received unexpected message %s (%i, size=%i) " - "expected MessageType::SIMCALL_TO_STRING_ANSWER (%i, size=%i)", - to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_DOT_LABEL_ANSWER, - (int)sizeof(answer)); - - XBT_DEBUG("dot_label(%ld) is returning %s", aid, answer.value); - return answer.value; + xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer); + xbt_assert(answer.type == MessageType::SIMCALL_EXECUTE_ANSWER, + "Received unexpected message %s (%i); expected MessageType::SIMCALL_EXECUTE_ANSWER (%i)", + to_c_str(answer.type), (int)answer.type, (int)MessageType::SIMCALL_EXECUTE_ANSWER); + + if (new_transition) { + std::stringstream stream(answer.buffer.data()); + return deserialize_transition(aid, times_considered, stream); + } else + return nullptr; } void ModelChecker::finalize_app(bool terminate_asap) { - s_mc_message_int_t m; - memset(&m, 0, sizeof m); + s_mc_message_int_t m = {}; m.type = MessageType::FINALIZE; m.value = terminate_asap; xbt_assert(checker_side_.get_channel().send(m) == 0, "Could not ask the app to finalize on need"); s_mc_message_t answer; - xbt_assert(checker_side_.get_channel().receive(answer) != -1, "Could not receive answer to FINALIZE"); -} - -bool ModelChecker::checkDeadlock() -{ - xbt_assert(checker_side_.get_channel().send(MessageType::DEADLOCK_CHECK) == 0, "Could not check deadlock state"); - s_mc_message_int_t message; - ssize_t s = checker_side_.get_channel().receive(message); - xbt_assert(s != -1, "Could not receive message"); - xbt_assert(s == sizeof(message) && message.type == MessageType::DEADLOCK_CHECK_REPLY, - "Received unexpected message %s (%i, size=%i) " - "expected MessageType::DEADLOCK_CHECK_REPLY (%i, size=%i)", - to_c_str(message.type), (int)message.type, (int)s, (int)MessageType::DEADLOCK_CHECK_REPLY, - (int)sizeof(message)); - return message.value != 0; + ssize_t s = checker_side_.get_channel().receive(answer); + xbt_assert(s != -1, "Could not receive answer to FINALIZE"); + xbt_assert(s == sizeof answer, "Broken message (size=%zd; expected %zu)", s, sizeof answer); + xbt_assert(answer.type == MessageType::FINALIZE_REPLY, + "Received unexpected message %s (%i); expected MessageType::FINALIZE_REPLY (%i)", to_c_str(answer.type), + (int)answer.type, (int)MessageType::FINALIZE_REPLY); } -} // namespace mc -} // namespace simgrid +} // namespace simgrid::mc