From 4f0921c868b916da79370ef6ba03d368be06a6e3 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Fri, 6 Nov 2015 14:49:16 +0100 Subject: [PATCH] [mc] ptrace the model-checker application The first goal is to be able to detect crashes of the model-checked application in the model-checker. This first patch only implement the ptrace but does not detect the crashed properly yet. As we are using ptrace, we do not need to using messages to stop/resume the model-checked application. The HELLO message is removed whose only purpose was to synchronise the execution of the two processes (wait for the model-checked application to be ready before trying to read its memory map). --- src/mc/mc_client.cpp | 6 ------ src/mc/mc_client.h | 1 - src/mc/mc_protocol.cpp | 30 ------------------------------ src/mc/mc_protocol.h | 2 -- src/mc/mc_server.cpp | 28 ++++++++++++++++------------ src/mc/simgrid_mc.cpp | 8 +++++--- src/simix/smx_global.c | 8 +++++++- 7 files changed, 28 insertions(+), 55 deletions(-) diff --git a/src/mc/mc_client.cpp b/src/mc/mc_client.cpp index 5ed0cf3cd9..6865abda95 100644 --- a/src/mc/mc_client.cpp +++ b/src/mc/mc_client.cpp @@ -56,12 +56,6 @@ void MC_client_init(void) mc_client->active = 1; } -void MC_client_hello(void) -{ - if (MC_protocol_hello(mc_client->fd) != 0) - xbt_die("Could not say hello the MC server"); -} - void MC_client_send_message(void* message, size_t size) { if (MC_protocol_send(mc_client->fd, message, size)) diff --git a/src/mc/mc_client.h b/src/mc/mc_client.h index 515abb7ec9..079c441714 100644 --- a/src/mc/mc_client.h +++ b/src/mc/mc_client.h @@ -20,7 +20,6 @@ typedef struct s_mc_client { extern XBT_PRIVATE mc_client_t mc_client; XBT_PRIVATE void MC_client_init(void); -XBT_PRIVATE void MC_client_hello(void); XBT_PRIVATE void MC_client_handle_messages(void); XBT_PRIVATE void MC_client_send_message(void* message, size_t size); XBT_PRIVATE void MC_client_send_simple_message(e_mc_message_type type); diff --git a/src/mc/mc_protocol.cpp b/src/mc/mc_protocol.cpp index 325b43320b..e56e12108b 100644 --- a/src/mc/mc_protocol.cpp +++ b/src/mc/mc_protocol.cpp @@ -41,34 +41,6 @@ int MC_protocol_send_simple_message(int socket, e_mc_message_type type) return MC_protocol_send(socket, &message, sizeof(message)); } -int MC_protocol_hello(int socket) -{ - int e; - if ((e = MC_protocol_send_simple_message(socket, MC_MESSAGE_HELLO)) != 0) { - XBT_ERROR("Could not send HELLO message"); - return 1; - } - - s_mc_message_t message; - message.type = MC_MESSAGE_NONE; - - ssize_t s; - while ((s = MC_receive_message(socket, &message, sizeof(message), 0)) == -1) { - if (errno == EINTR) - continue; - else { - XBT_ERROR("Could not receive HELLO message"); - return 2; - } - } - if ((size_t) s < sizeof(message) || message.type != MC_MESSAGE_HELLO) { - XBT_ERROR("Did not receive suitable HELLO message. Who are you?"); - return 3; - } - - return 0; -} - ssize_t MC_receive_message(int socket, void* message, size_t size, int options) { int res = recv(socket, message, size, options); @@ -85,8 +57,6 @@ const char* MC_message_type_name(e_mc_message_type type) switch(type) { case MC_MESSAGE_NONE: return "NONE"; - case MC_MESSAGE_HELLO: - return "HELLO"; case MC_MESSAGE_CONTINUE: return "CONTINUE"; case MC_MESSAGE_IGNORE_HEAP: diff --git a/src/mc/mc_protocol.h b/src/mc/mc_protocol.h index 1c39fa7252..80b144e456 100644 --- a/src/mc/mc_protocol.h +++ b/src/mc/mc_protocol.h @@ -37,7 +37,6 @@ extern e_mc_mode_t mc_mode; typedef enum { MC_MESSAGE_NONE, - MC_MESSAGE_HELLO, MC_MESSAGE_CONTINUE, MC_MESSAGE_IGNORE_HEAP, MC_MESSAGE_UNIGNORE_HEAP, @@ -105,7 +104,6 @@ typedef struct s_mc_register_symbol_message { XBT_PRIVATE int MC_protocol_send(int socket, const void* message, size_t size); XBT_PRIVATE int MC_protocol_send_simple_message(int socket, e_mc_message_type type); -XBT_PRIVATE int MC_protocol_hello(int socket); XBT_PRIVATE ssize_t MC_receive_message(int socket, void* message, size_t size, int options); XBT_PRIVATE const char* MC_message_type_name(e_mc_message_type type); diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp index 8368238ba9..e618b32f60 100644 --- a/src/mc/mc_server.cpp +++ b/src/mc/mc_server.cpp @@ -12,6 +12,7 @@ #include #include #include +#include #include #include @@ -38,21 +39,11 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic"); mc_server_t mc_server; -s_mc_server::s_mc_server(pid_t pid, int socket) -{ - this->pid = pid; - this->socket = socket; -} +s_mc_server::s_mc_server(pid_t pid_, int socket_) + : pid(pid_), socket(socket_) {} void s_mc_server::start() { - /* Wait for the target process to initialize and exchange a HELLO messages - * before trying to look at its memory map. - */ - int res = MC_protocol_hello(socket); - if (res != 0) - throw std::system_error(res, std::system_category()); - // Block SIGCHLD (this will be handled with accept/signalfd): sigset_t set; sigemptyset(&set); @@ -78,6 +69,19 @@ void s_mc_server::start() signalfd_pollfd->fd = signal_fd; signalfd_pollfd->events = POLLIN; signalfd_pollfd->revents = 0; + + XBT_DEBUG("Waiting for the model-checked process"); + int status; + + // The model-checked process SIGSTOP itself to signal it's ready: + pid_t res = waitpid(pid, &status, __WALL); + if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP) + xbt_die("Could not wait model-checked process"); + + // The model-checked process is ready, we can read its memory layout: + MC_init_model_checker(pid, socket); + + ptrace(PTRACE_CONT, pid, 0, 0); } void s_mc_server::shutdown() diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp index cd2e84bf38..93cf397e2b 100644 --- a/src/mc/simgrid_mc.cpp +++ b/src/mc/simgrid_mc.cpp @@ -18,6 +18,7 @@ #include #include #include +#include #ifdef __linux__ #include @@ -80,7 +81,7 @@ static int do_child(int socket, char** argv) setenv(MC_ENV_SOCKET_FD, buffer, 1); execvp(argv[1], argv+1); - std::perror("simgrid-mc"); + XBT_ERROR("Could not execute the child process"); return MC_SERVER_ERROR; } @@ -93,7 +94,6 @@ static int do_parent(int socket, pid_t child) mc_mode = MC_MODE_SERVER; mc_server = new s_mc_server(child, socket); mc_server->start(); - MC_init_model_checker(child, socket); if (_sg_mc_comms_determinism || _sg_mc_send_determinism) MC_modelcheck_comm_determinism(); else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') @@ -149,7 +149,9 @@ int main(int argc, char** argv) return MC_SERVER_ERROR; } else if (pid == 0) { close(sockets[1]); - return do_child(sockets[0], argv); + int res = do_child(sockets[0], argv); + XBT_DEBUG("Error in the child process creation"); + return res; } else { close(sockets[0]); return do_parent(sockets[1], pid); diff --git a/src/simix/smx_global.c b/src/simix/smx_global.c index 25882af65f..3b92c94667 100644 --- a/src/simix/smx_global.c +++ b/src/simix/smx_global.c @@ -5,6 +5,7 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include +#include #include "smx_private.h" #include "xbt/heap.h" @@ -226,9 +227,14 @@ void SIMIX_global_init(int *argc, char **argv) // We need to communicate initialization of the different layers to the model-checker. if (mc_mode == MC_MODE_NONE) { if (getenv(MC_ENV_SOCKET_FD)) { + mc_mode = MC_MODE_CLIENT; MC_client_init(); - MC_client_hello(); + + // Waiting for the model-checker: + if (ptrace(PTRACE_TRACEME, 0, NULL, NULL) == -1 || raise(SIGSTOP) != 0) + xbt_die("Could not wait for the model-checker"); + MC_client_handle_messages(); } } -- 2.20.1