X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/63834b5431ab8aadc3373b34be3a4ea0491fad5d..a3bd84b0137a58fad3300f954dbc43328ff1410e:/src/mc/ModelChecker.cpp?ds=sidebyside diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index 84e6a8dedc..a7f0a6d057 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -1,20 +1,22 @@ -/* Copyright (c) 2008-2021. The SimGrid Team. All rights reserved. */ +/* Copyright (c) 2008-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/ModelChecker.hpp" #include "src/mc/Session.hpp" -#include "src/mc/Transition.hpp" +#include "src/mc/api/Transition.hpp" +#include "src/mc/api/TransitionComm.hpp" #include "src/mc/checker/Checker.hpp" #include "src/mc/mc_config.hpp" #include "src/mc/mc_exit.hpp" #include "src/mc/mc_private.hpp" -#include "src/mc/remote/RemoteSimulation.hpp" +#include "src/mc/remote/RemoteProcess.hpp" #include "xbt/automaton.hpp" #include "xbt/system_error.hpp" #include +#include #include #include @@ -33,42 +35,41 @@ using simgrid::mc::remote; namespace simgrid { namespace mc { -ModelChecker::ModelChecker(std::unique_ptr remote_simulation, int sockfd) - : checker_side_(sockfd), remote_simulation_(std::move(remote_simulation)) +ModelChecker::ModelChecker(std::unique_ptr remote_simulation, int sockfd) + : checker_side_(sockfd), remote_process_(std::move(remote_simulation)) { } void ModelChecker::start() { - checker_side_.start([](evutil_socket_t sig, short events, void* arg) { - auto mc = static_cast(arg); - if (events == EV_READ) { - std::array buffer; - ssize_t size = mc->checker_side_.get_channel().receive(buffer.data(), buffer.size(), false); - if (size == -1 && errno != EAGAIN) - throw simgrid::xbt::errno_error(); - - if (not mc->handle_message(buffer.data(), size)) - mc->checker_side_.break_loop(); - } else if (events == EV_SIGNAL) { - if (sig == SIGCHLD) - mc->handle_waitpid(); - } else { - xbt_die("Unexpected event"); - } - }); + checker_side_.start( + [](evutil_socket_t sig, short events, void* arg) { + auto mc = static_cast(arg); + if (events == EV_READ) { + std::array buffer; + ssize_t size = mc->checker_side_.get_channel().receive(buffer.data(), buffer.size(), false); + if (size == -1 && errno != EAGAIN) + throw simgrid::xbt::errno_error(); + + if (not mc->handle_message(buffer.data(), size)) + mc->checker_side_.break_loop(); + } else if (events == EV_SIGNAL) { + if (sig == SIGCHLD) + mc->handle_waitpid(); + } else { + xbt_die("Unexpected event"); + } + }, + this); XBT_DEBUG("Waiting for the model-checked process"); int status; // The model-checked process SIGSTOP itself to signal it's ready: - const pid_t pid = remote_simulation_->pid(); - - pid_t res = waitpid(pid, &status, WAITPID_CHECKED_FLAGS); - if (res < 0 || not WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP) - xbt_die("Could not wait model-checked process"); + const pid_t pid = remote_process_->pid(); - remote_simulation_->init(); + 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(); @@ -95,7 +96,7 @@ static constexpr auto ignored_local_variables = { void ModelChecker::setup_ignore() { - const RemoteSimulation& process = this->get_remote_simulation(); + const RemoteProcess& process = this->get_remote_process(); for (auto const& var : ignored_local_variables) process.ignore_local_variable(var.first, var.second); @@ -107,20 +108,21 @@ void ModelChecker::shutdown() { XBT_DEBUG("Shutting down model-checker"); - RemoteSimulation* process = &this->get_remote_simulation(); - if (process->running()) { + RemoteProcess& process = get_remote_process(); + if (process.running()) { XBT_DEBUG("Killing process"); - kill(process->pid(), SIGKILL); - process->terminate(); + finalize_app(true); + kill(process.pid(), SIGKILL); + process.terminate(); } } -void ModelChecker::resume(RemoteSimulation& process) +void ModelChecker::resume() { int res = checker_side_.get_channel().send(MessageType::CONTINUE); if (res) throw xbt::errno_error(); - process.clear_cache(); + remote_process_->clear_cache(); } static void MC_report_crash(int status) @@ -138,27 +140,15 @@ static void MC_report_crash(int status) for (auto const& s : mc_model_checker->getChecker()->get_textual_trace()) XBT_INFO(" %s", s.c_str()); dumpRecordPath(); - session->log_state(); + 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_simulation().dump_stack(); + mc_model_checker->get_remote_process().dump_stack(); } } -static void MC_report_assertion_error() -{ - XBT_INFO("**************************"); - XBT_INFO("*** PROPERTY NOT VALID ***"); - XBT_INFO("**************************"); - 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->log_state(); -} - bool ModelChecker::handle_message(const char* buffer, ssize_t size) { s_mc_message_t base_message; @@ -166,6 +156,15 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) memcpy(&base_message, buffer, sizeof(base_message)); switch(base_message.type) { + case MessageType::INITIAL_ADDRESSES: { + s_mc_message_initial_addresses_t message; + 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); + break; + } + case MessageType::IGNORE_HEAP: { s_mc_message_ignore_heap_t message; xbt_assert(size == sizeof(message), "Broken message"); @@ -176,7 +175,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) region.fragment = message.fragment; region.address = message.address; region.size = message.size; - get_remote_simulation().ignore_heap(region); + get_remote_process().ignore_heap(region); break; } @@ -184,7 +183,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) s_mc_message_ignore_memory_t message; xbt_assert(size == sizeof(message), "Broken message"); memcpy(&message, buffer, sizeof(message)); - get_remote_simulation().unignore_heap((void*)(std::uintptr_t)message.addr, message.size); + get_remote_process().unignore_heap((void*)(std::uintptr_t)message.addr, message.size); break; } @@ -192,7 +191,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) s_mc_message_ignore_memory_t message; xbt_assert(size == sizeof(message), "Broken message"); memcpy(&message, buffer, sizeof(message)); - this->get_remote_simulation().ignore_region(message.addr, message.size); + this->get_remote_process().ignore_region(message.addr, message.size); break; } @@ -200,7 +199,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) s_mc_message_stack_region_t message; xbt_assert(size == sizeof(message), "Broken message"); memcpy(&message, buffer, sizeof(message)); - this->get_remote_simulation().stack_areas().push_back(message.stack_region); + this->get_remote_process().stack_areas().push_back(message.stack_region); } break; case MessageType::REGISTER_SYMBOL: { @@ -213,7 +212,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) if (property_automaton == nullptr) property_automaton = xbt_automaton_new(); - const RemoteSimulation* process = &this->get_remote_simulation(); + 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); }); @@ -225,7 +224,15 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) return false; case MessageType::ASSERTION_FAILED: - MC_report_assertion_error(); + XBT_INFO("**************************"); + XBT_INFO("*** PROPERTY NOT VALID ***"); + XBT_INFO("**************************"); + XBT_INFO("Counter-example execution trace:"); + for (auto const& s : getChecker()->get_textual_trace()) + XBT_INFO(" %s", s.c_str()); + dumpRecordPath(); + session_singleton->log_state(); + this->exit(SIMGRID_MC_EXIT_SAFETY); default: @@ -237,9 +244,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size) /** Terminate the model-checker application */ void ModelChecker::exit(int status) { - // TODO, terminate the model checker politely instead of exiting rudely - if (get_remote_simulation().running()) - kill(get_remote_simulation().pid(), SIGKILL); + shutdown(); ::exit(status); } @@ -252,7 +257,7 @@ void ModelChecker::handle_waitpid() if (pid == -1) { if (errno == ECHILD) { // No more children: - xbt_assert(not this->get_remote_simulation().running(), "Inconsistent state"); + xbt_assert(not this->get_remote_process().running(), "Inconsistent state"); break; } else { XBT_ERROR("Could not wait for pid"); @@ -260,15 +265,15 @@ void ModelChecker::handle_waitpid() } } - if (pid == this->get_remote_simulation().pid()) { + if (pid == this->get_remote_process().pid()) { // From PTRACE_O_TRACEEXIT: #ifdef __linux__ if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) { - xbt_assert(ptrace(PTRACE_GETEVENTMSG, remote_simulation_->pid(), 0, &status) != -1, - "Could not get exit status"); + xbt_assert(ptrace(PTRACE_GETEVENTMSG, remote_process_->pid(), 0, &status) != -1, "Could not get exit status"); if (WIFSIGNALED(status)) { MC_report_crash(status); - mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); + this->get_remote_process().terminate(); + this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); } } #endif @@ -278,19 +283,20 @@ void ModelChecker::handle_waitpid() XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status)); errno = 0; #ifdef __linux__ - ptrace(PTRACE_CONT, remote_simulation_->pid(), 0, WSTOPSIG(status)); + ptrace(PTRACE_CONT, remote_process_->pid(), 0, WSTOPSIG(status)); #elif defined BSD - ptrace(PT_CONTINUE, remote_simulation_->pid(), (caddr_t)1, WSTOPSIG(status)); + ptrace(PT_CONTINUE, remote_process_->pid(), (caddr_t)1, WSTOPSIG(status)); #endif xbt_assert(errno == 0, "Could not PTRACE_CONT"); } else if (WIFSIGNALED(status)) { MC_report_crash(status); - mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); + this->get_remote_process().terminate(); + this->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH); } else if (WIFEXITED(status)) { XBT_DEBUG("Child process is over"); - this->get_remote_simulation().terminate(); + this->get_remote_process().terminate(); } } } @@ -298,47 +304,39 @@ void ModelChecker::handle_waitpid() void ModelChecker::wait_for_requests() { - this->resume(get_remote_simulation()); - if (this->get_remote_simulation().running()) + this->resume(); + if (this->get_remote_process().running()) checker_side_.dispatch(); } -void ModelChecker::handle_simcall(Transition const& transition) -{ - s_mc_message_simcall_handle_t m; - memset(&m, 0, sizeof(m)); - m.type = MessageType::SIMCALL_HANDLE; - m.pid = transition.pid_; - m.value = transition.times_considered_; - checker_side_.get_channel().send(m); - this->remote_simulation_->clear_cache(); - if (this->remote_simulation_->running()) - checker_side_.dispatch(); -} -bool ModelChecker::simcall_is_pending(int aid, int times_considered) +Transition* ModelChecker::handle_simcall(Transition const& transition, bool new_transition) { - s_mc_message_simcall_is_pending_t m; + s_mc_message_simcall_execute_t m; memset(&m, 0, sizeof(m)); - m.type = MessageType::SIMCALL_IS_PENDING; - m.aid = aid; - m.time_considered = times_considered; + m.type = MessageType::SIMCALL_EXECUTE; + m.aid_ = transition.aid_; + m.times_considered_ = transition.times_considered_; checker_side_.get_channel().send(m); - s_mc_message_simcall_is_pending_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_IS_PENDING_ANSWER, + xbt_assert(s == sizeof(answer) && answer.type == MessageType::SIMCALL_EXECUTE_ANSWER, "Received unexpected message %s (%i, size=%i) " - "expected MessageType::SIMCALL_IS_PENDING_ANSWER (%i, size=%i)", - to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_IS_PENDING_ANSWER, + "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)); - XBT_DEBUG("is_pending(%d, %d) is returning %s", aid, times_considered, answer.value ? "true" : "false"); + this->remote_process_->clear_cache(); + if (this->remote_process_->running()) + checker_side_.dispatch(); // The app may send messages while processing the transition - this->remote_simulation_->clear_cache(); - return answer.value; + if (new_transition) + return recv_transition(transition.aid_, transition.times_considered_, answer.simcall, answer.buffer); + else + return nullptr; } -bool ModelChecker::simcall_is_visible(int aid) +bool ModelChecker::simcall_is_visible(aid_t aid) { xbt_assert(mc_model_checker != nullptr, "This should be called from the checker side"); @@ -357,36 +355,13 @@ bool ModelChecker::simcall_is_visible(int aid) to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_IS_VISIBLE_ANSWER, (int)sizeof(answer)); - XBT_DEBUG("is_visible(%d) is returning %s", aid, answer.value ? "true" : "false"); + XBT_DEBUG("is_visible(%ld) is returning %s", aid, answer.value ? "true" : "false"); - this->remote_simulation_->clear_cache(); + this->remote_process_->clear_cache(); return answer.value; } -std::string ModelChecker::simcall_to_string(int 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_TO_STRING; - m.aid = aid; - m.time_considered = times_considered; - checker_side_.get_channel().send(m); - s_mc_message_simcall_to_string_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_TO_STRING_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_TO_STRING_ANSWER, - (int)sizeof(answer)); - - XBT_DEBUG("to_string(%d) is returning %s", aid, answer.value); - - return std::string(answer.value); -} -std::string ModelChecker::simcall_dot_label(int aid, int times_considered) +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"); @@ -400,21 +375,31 @@ std::string ModelChecker::simcall_dot_label(int aid, int times_considered) s_mc_message_simcall_to_string_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_TO_STRING_ANSWER, + 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_TO_STRING_ANSWER, + to_c_str(answer.type), (int)answer.type, (int)s, (int)MessageType::SIMCALL_DOT_LABEL_ANSWER, (int)sizeof(answer)); - XBT_DEBUG("dot_label(%d) is returning %s", aid, answer.value); + XBT_DEBUG("dot_label(%ld) is returning %s", aid, answer.value); + return answer.value; +} - return std::string(answer.value); +void ModelChecker::finalize_app(bool terminate_asap) +{ + s_mc_message_int_t m; + memset(&m, 0, sizeof 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() { - int res = checker_side_.get_channel().send(MessageType::DEADLOCK_CHECK); - xbt_assert(res == 0, "Could not check deadlock state"); + 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");