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))
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);
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);
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:
typedef enum {
MC_MESSAGE_NONE,
- MC_MESSAGE_HELLO,
MC_MESSAGE_CONTINUE,
MC_MESSAGE_IGNORE_HEAP,
MC_MESSAGE_UNIGNORE_HEAP,
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);
#include <sys/wait.h>
#include <sys/socket.h>
#include <sys/signalfd.h>
+#include <sys/ptrace.h>
#include <xbt/log.h>
#include <xbt/automaton.h>
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);
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()
#include <sys/types.h>
#include <sys/socket.h>
#include <sys/wait.h>
+#include <sys/ptrace.h>
#ifdef __linux__
#include <sys/prctl.h>
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;
}
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')
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);
* 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"
// 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();
}
}