[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).

diff --git a/src/mc/mc_client.cpp b/src/mc/mc_client.cpp
index 5ed0cf3..6865abd 100644 (file)
--- 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 515abb7..079c441 100644 (file)
--- 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 325b433..e56e121 100644 (file)
--- 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 1c39fa7..80b144e 100644 (file)
--- 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 8368238..e618b32 100644 (file)
--- a/src/mc/mc_server.cpp
+++ b/src/mc/mc_server.cpp
@@ -12,6 +12,7 @@
 #include <sys/wait.h>
 #include <sys/socket.h>
 #include <sys/signalfd.h>
+#include <sys/ptrace.h>
 
 #include <xbt/log.h>
 #include <xbt/automaton.h>
@@ -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 cd2e84b..93cf397 100644 (file)
--- a/src/mc/simgrid_mc.cpp
+++ b/src/mc/simgrid_mc.cpp
@@ -18,6 +18,7 @@
 #include <sys/types.h>
 #include <sys/socket.h>
 #include <sys/wait.h>
+#include <sys/ptrace.h>
 
 #ifdef __linux__
 #include <sys/prctl.h>
@@ -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 25882af..3b92c94 100644 (file)
--- 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 <stdlib.h>
+#include <sys/ptrace.h>
 
 #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();
     }
   }