src/mc/mc_visited.c
src/mc/mc_memory_map.h
src/mc/memory_map.c
+ src/mc/mc_client.c
+ src/mc/mc_client.h
+ src/mc/mc_protocol.h
+ src/mc/mc_protocol.c
+ src/mc/mc_server.cpp
+ src/mc/mc_server.h
)
set(MC_SIMGRID_MC_SRC
- src/mc/simgrid_mc.c)
+ src/mc/simgrid_mc.cpp)
set(headers_to_install
include/instr/instr.h
add_dependencies(simgrid maintainer_files)
if(enable_model-checking)
- add_executable(simgrid-mc "${MC_SIMGRID_MC_SRC}")
+ add_executable(simgrid-mc ${MC_SIMGRID_MC_SRC})
target_link_libraries(simgrid-mc simgrid)
set_target_properties(simgrid-mc
PROPERTIES
! timeout 20
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack_size:256
> [ 0.000000] (0:@) Check a safety property
-> [ 0.000000] (0:@) Get debug information ...
-> [ 0.000000] (0:@) Get debug information done !
> [ 0.000000] (2:client@HostB) Sent!
> [ 0.000000] (3:client@HostC) Sent!
> [ 0.000000] (1:server@HostA) OK
! timeout 20
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256
> [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness
-> [ 0.000000] (0:@) Get debug information ...
-> [ 0.000000] (0:@) Get debug information done !
> [ 0.000000] (2:client@Boivin) Ask the request
> [ 0.000000] (3:client@Fafard) Ask the request
> [ 0.000000] (2:client@Boivin) Propositions changed : r=1, cs=0
! timeout 60
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes
> [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness
-> [ 0.000000] (0:@) Get debug information ...
-> [ 0.000000] (0:@) Get debug information done !
> [ 0.000000] (2:client@Boivin) Ask the request
> [ 0.000000] (3:client@Fafard) Ask the request
> [ 0.000000] (2:client@Boivin) Propositions changed : r=1, cs=0
! timeout 90
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256
> [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness
-> [ 0.000000] (0:@) Get debug information ...
-> [ 0.000000] (0:@) Get debug information done !
> [ 0.000000] (2:client@Boivin) Ask the request
> [ 0.000000] (3:client@Fafard) Ask the request
> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
! timeout 90
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.}/../../platforms/platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack_size:256 --cfg=model-check/sparse-checkpoint:yes
> [ 0.000000] (0:@) Check the liveness property promela_bugged1_liveness
-> [ 0.000000] (0:@) Get debug information ...
-> [ 0.000000] (0:@) Get debug information done !
> [ 0.000000] (2:client@Boivin) Ask the request
> [ 0.000000] (3:client@Fafard) Ask the request
> [ 0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
! timeout 20
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged2 --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=contexts/stack_size:256
> [ 0.000000] (0:@) Check a safety property
-> [ 0.000000] (0:@) Get debug information ...
-> [ 0.000000] (0:@) Get debug information done !
> [ 0.000000] (2:client@HostB) Send 1!
> [ 0.000000] (3:client@HostC) Send 2!
> [ 0.000000] (1:server@HostA) Received 1
#! ./tesh
! timeout 60
-$ ${bindir:=.}/../../../bin/simgrid-mc ../../../smpi_script/bin/smpirun -hostfile ${srcdir:=.}/hostfile_non_deterministic -platform ${srcdir:=.}/../../platforms/cluster.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_non_deterministic
+$ ../../../smpi_script/bin/smpirun -wrapper ${bindir:=.}/../../../bin/simgrid-mc -hostfile ${srcdir:=.}/hostfile_non_deterministic -platform ${srcdir:=.}/../../platforms/cluster.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 --cfg=model-check/communications_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_non_deterministic
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check communication determinism
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> [0.000000] [mc_comm_determinism/INFO] The communications pattern of the process 1 is different! (Different communication : 1)
> [0.000000] [mc_comm_determinism/INFO] ****************************************************
> [0.000000] [mc_comm_determinism/INFO] ***** Non-deterministic communications pattern *****
$ ../../../smpi_script/bin/smpirun -wrapper "${bindir:=.}/../../../bin/simgrid-mc" -hostfile ${srcdir:=.}/hostfile_send_deterministic -platform ${srcdir:=.}/../../platforms/cluster.xml --log=xbt_cfg.thresh:warning --cfg=model-check:1 --cfg=model-check/send_determinism:1 --cfg=smpi/send_is_detached_thres:0 --cfg=smpi/running_power:1e9 ./smpi_send_deterministic
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check communication determinism
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> [0.000000] [mc_global/INFO] Expanded states = 520
> [0.000000] [mc_global/INFO] Visited states = 1476
> [0.000000] [mc_global/INFO] Executed transitions = 1312
SG_BEGIN_DECL()
-/** Environment variable name set by `simgrid-mc` to enable MC support in the
- * children MC processes
- */
-#define MC_ENV_VARIABLE "SIMGRIC_MC"
-
/** Check if the given simcall can be resolved
*
* \return `TRUE` or `FALSE`
--- /dev/null
+/* Copyright (c) 2015. 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 <stdlib.h>
+#include <errno.h>
+#include <error.h>
+
+#include <sys/types.h>
+#include <sys/socket.h>
+
+#include <xbt/log.h>
+#include <xbt/sysdep.h>
+
+#include "mc_protocol.h"
+#include "mc_client.h"
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client, mc, "MC client logic");
+
+typedef struct s_mc_client {
+ int active;
+ int fd;
+} s_mc_client_t, mc_client_t;
+
+static s_mc_client_t mc_client;
+
+void MC_client_init(void)
+{
+ mc_client.fd = -1;
+ mc_client.active = 1;
+ char* fd_env = getenv(MC_ENV_SOCKET_FD);
+ if (!fd_env)
+ xbt_die("MC socket not found");
+
+ int fd = atoi(fd_env);
+ XBT_DEBUG("Model-checked application found socket FD %i", fd);
+
+ int type;
+ socklen_t socklen = sizeof(type);
+ if (getsockopt(fd, SOL_SOCKET, SO_TYPE, &type, &socklen) != 0)
+ xbt_die("Could not check socket type: %s", strerror(errno));
+ if (type != SOCK_DGRAM)
+ xbt_die("Unexpected socket type %i", type);
+ XBT_DEBUG("Model-checked application found expected socket type");
+
+ mc_client.fd = fd;
+}
+
+void MC_client_hello(void)
+{
+ XBT_DEBUG("Greeting the MC server");
+ if (MC_protocol_hello(mc_client.fd) != 0)
+ xbt_die("Could not say hello the MC server");
+ XBT_DEBUG("Greeted the MC server");
+}
+
+void MC_client_handle_messages(void)
+{
+ while (1) {
+ XBT_DEBUG("Waiting messages from model-checker");
+ s_mc_message_t message;
+ if (recv(mc_client.fd, &message, sizeof(message), 0) == -1)
+ xbt_die("Could not receive commands from the model-checker: %s",
+ strerror(errno));
+ XBT_DEBUG("Receive message from model-checker");
+ switch (message.type) {
+ case MC_MESSAGE_CONTINUE:
+ return;
+ default:
+ xbt_die("Unexpected message from model-checker %i", message.type);
+ }
+ }
+}
/* 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 <stdio.h>
-#include <errno.h>
+#ifndef MC_CLIENT_H
+#define MC_CLIENT_H
-#include <unistd.h>
+#include <xbt/misc.h>
-#include "mc_base.h"
+SG_BEGIN_DECL()
-int main(int argc, char** argv)
-{
- if (argc < 2)
- xbt_die("Missing arguments.\n");
+void MC_client_init(void);
+void MC_client_hello(void);
+void MC_client_handle_messages(void);
- setenv(MC_ENV_VARIABLE, "1", 1);
- execvp(argv[1], argv+1);
+SG_END_DECL()
- perror("simgrid-mc");
- return 127;
-}
+#endif
/* 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 <string.h>
+
#include "mc_base.h"
#ifndef _XBT_WIN32
#include "mc_unw.h"
#endif
#include "mc_record.h"
-
+#include "mc_protocol.h"
+#include "mc_client.h"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
"Logging specific to MC (global)");
+e_mc_mode_t mc_mode;
+
double *mc_time = NULL;
#ifdef HAVE_MC
mc_model_checker_t mc_model_checker = NULL;
-mc_model_checker_t MC_model_checker_new()
+mc_model_checker_t MC_model_checker_new(pid_t pid, int socket)
{
mc_model_checker_t mc = xbt_new0(s_mc_model_checker_t, 1);
mc->pages = mc_pages_store_new();
mc->fd_clear_refs = -1;
mc->fd_pagemap = -1;
- MC_process_init(&mc->process, getpid());
+ MC_process_init(&mc->process, pid, socket);
return mc;
}
}
void MC_init()
+{
+ if (mc_mode == MC_MODE_NONE) {
+ if (getenv(MC_ENV_SOCKET_FD)) {
+ mc_mode = MC_MODE_CLIENT;
+ } else {
+ mc_mode = MC_MODE_STANDALONE;
+ }
+ }
+
+ MC_init_pid(getpid(), -1);
+
+ if (mc_mode == MC_MODE_CLIENT) {
+ MC_client_init();
+ MC_client_hello();
+ // This will move somehwere else:
+ MC_client_handle_messages();
+ }
+}
+
+void MC_init_pid(pid_t pid, int socket)
{
int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
MC_SET_MC_HEAP;
- mc_model_checker = MC_model_checker_new();
+ mc_model_checker = MC_model_checker_new(pid, socket);
mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
smx_process_t process;
// FIXME, cross-process support (simix_global->process_list)
- xbt_swag_foreach(process, simix_global->process_list) {
- MC_ignore_heap(&(process->process_hookup),
- sizeof(process->process_hookup));
- }
+
+ if (mc_mode == MC_MODE_STANDALONE || mc_mode == MC_MODE_CLIENT) {
+ xbt_swag_foreach(process, simix_global->process_list) {
+ MC_ignore_heap(&(process->process_hookup),
+ sizeof(process->process_hookup));
+ }
+ } else {
+ // TODO
+ }
}
if (raw_mem_set)
#ifndef MC_MODEL_CHECKER_H
#define MC_MODEL_CHECKER_H
+#include <sys/types.h>
+
#include <simgrid_config.h>
#include "mc_forward.h"
SG_BEGIN_DECL()
+typedef enum {
+ MC_MODE_NONE = 0,
+ MC_MODE_STANDALONE,
+ MC_MODE_CLIENT,
+ MC_MODE_SERVER
+} e_mc_mode_t;
+
+extern e_mc_mode_t mc_mode;
+
/** @brief State of the model-checker (global variables for the model checker)
*
* Each part of the state of the model chercker represented as a global
s_mc_process_t process;
};
-mc_model_checker_t MC_model_checker_new(void);
+mc_model_checker_t MC_model_checker_new(pid_t pid, int socket);
void MC_model_checker_delete(mc_model_checker_t mc);
SG_END_DECL()
#ifndef MC_PRIVATE_H
#define MC_PRIVATE_H
+#include <sys/types.h>
+
#include "simgrid_config.h"
#include <stdio.h>
#include <stdint.h>
#include "mc/datatypes.h"
#include "xbt/fifo.h"
#include "xbt/config.h"
+
#include "xbt/function_types.h"
#include "xbt/mmalloc.h"
#include "../simix/smx_private.h"
/********************************* MC Global **********************************/
+/** Initialisation of the model-checker
+ *
+ * @param pid PID of the target process
+ * @param socket FD for the communication socket **in server mode** (or -1 otherwise)
+ */
+void MC_init_pid(pid_t pid, int socket);
+
extern FILE *dot_output;
extern const char* colors[13];
extern xbt_parmap_t parmap;
return p->address_space_class == &mc_process_class;
}
-void MC_process_init(mc_process_t process, pid_t pid)
+void MC_process_init(mc_process_t process, pid_t pid, int sockfd)
{
process->address_space.address_space_class = &mc_process_class;
process->process_flags = MC_PROCESS_NO_FLAG;
+ process->socket = sockfd;
process->pid = pid;
if (pid==getpid())
process->process_flags |= MC_PROCESS_SELF_FLAG;
+ process->running = true;
+ process->status = 0;
process->memory_map = MC_get_memory_map(pid);
process->memory_file = -1;
process->cache_flags = 0;
/** @brief Finds the range of the different memory segments and binary paths */
static void MC_process_init_memory_map_info(mc_process_t process)
{
- XBT_INFO("Get debug information ...");
+ XBT_DEBUG("Get debug information ...");
process->maestro_stack_start = NULL;
process->maestro_stack_end = NULL;
process->object_infos = NULL;
for (i=0; i!=process->object_infos_size; ++i)
MC_post_process_object_info(process, process->object_infos[i]);
- xbt_assert(process->maestro_stack_start, "maestro_stack_start");
- xbt_assert(process->maestro_stack_end, "maestro_stack_end");
+ xbt_assert(process->maestro_stack_start, "Did not find maestro_stack_start");
+ xbt_assert(process->maestro_stack_end, "Did not find maestro_stack_end");
- XBT_INFO("Get debug information done !");
+ XBT_DEBUG("Get debug information done !");
}
mc_object_info_t MC_process_find_object_info(mc_process_t process, const void *addr)
s_mc_address_space_t address_space;
e_mc_process_flags_t process_flags;
pid_t pid;
+ int socket;
+ int status;
+ bool running;
memory_map_t memory_map;
void *maestro_stack_start, *maestro_stack_end;
mc_object_info_t libsimgrid_info;
bool MC_is_process(mc_address_space_t p);
-void MC_process_init(mc_process_t process, pid_t pid);
+void MC_process_init(mc_process_t process, pid_t pid, int sockfd);
void MC_process_clear(mc_process_t process);
/** Refresh the information about the process
--- /dev/null
+/* Copyright (c) 2015. 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 <errno.h>
+#include <string.h>
+
+#include <sys/types.h>
+#include <sys/socket.h>
+
+#include <xbt/log.h>
+
+#include "mc_protocol.h"
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_protocol, mc, "Generic MC protocol logic");
+
+int MC_protocol_send_simple_message(int socket, int type)
+{
+ s_mc_message_t message;
+ message.type = type;
+
+ while (send(socket, &message, sizeof(message), 0) == -1) {
+ if (errno == EINTR)
+ continue;
+ else
+ return errno;
+ }
+ return 0;
+}
+
+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: %s", strerror(e));
+ return 1;
+ }
+
+ s_mc_message_t message;
+ message.type = MC_MESSAGE_NONE;
+
+ while (recv(socket, &message, sizeof(message), 0) == -1) {
+ if (errno == EINTR)
+ continue;
+ else {
+ XBT_ERROR("Could not receive HELLO message: %s", strerror(errno));
+ return 2;
+ }
+ }
+ if (message.type != MC_MESSAGE_HELLO) {
+ XBT_ERROR("Did not receive suitable HELLO message. Who are you?");
+ return 3;
+ }
+
+ return 0;
+}
--- /dev/null
+/* Copyright (c) 2015. 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. */
+
+#ifndef MC_PROTOCOL_H
+#define MC_PROTOCOL_H
+
+#include <xbt/misc.h>
+
+SG_BEGIN_DECL()
+
+// ***** Environment variables for passing context to the model-checked process
+
+/** Environment variable name set by `simgrid-mc` to enable MC support in the
+ * children MC processes
+ */
+#define MC_ENV_VARIABLE "SIMGRIC_MC"
+
+/** Environment variable name used to pass the communication socket */
+#define MC_ENV_SOCKET_FD "SIMGRID_MC_SOCKET_FD"
+
+// ***** Messages
+
+enum {
+ MC_MESSAGE_NONE = 0,
+ MC_MESSAGE_HELLO = 1,
+ MC_MESSAGE_CONTINUE = 2,
+};
+
+typedef struct s_mc_message {
+ int type;
+} s_mc_message_t, *mc_message_t;
+
+/**
+ * @return errno
+ */
+int MC_protocol_send_simple_message(int socket, int type);
+int MC_protocol_hello(int socket);
+
+SG_END_DECL()
+
+#endif
--- /dev/null
+/* Copyright (c) 2015. 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 <memory>
+#include <system_error>
+
+#include <poll.h>
+#include <sys/types.h>
+#include <sys/wait.h>
+#include <sys/socket.h>
+#include <sys/signalfd.h>
+
+#include <xbt/log.h>
+
+#include "mc_model_checker.h"
+#include "mc_protocol.h"
+#include "mc_server.h"
+#include "mc_private.h"
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_server, mc, "MC server logic");
+
+// HArdcoded index for now:
+#define SOCKET_FD_INDEX 0
+#define SIGNAL_FD_INDEX 1
+
+mc_server_t mc_server;
+
+int MC_server_init(pid_t pid, int socket)
+{
+ if (mc_server)
+ xbt_die("MC server already present");
+ mc_mode = MC_MODE_SERVER;
+ mc_server = new s_mc_server(pid, socket);
+ mc_server->start();
+ return 0;
+}
+
+void MC_server_run(void)
+{
+ try {
+ mc_server->resume(&mc_model_checker->process);
+ mc_server->loop();
+ mc_server->shutdown();
+ mc_server->exit();
+ }
+ catch(std::exception& e) {
+ XBT_ERROR(e.what());
+ exit(MC_SERVER_ERROR);
+ }
+}
+
+s_mc_server::s_mc_server(pid_t pid, int socket)
+{
+ this->pid = pid;
+ this->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.
+ */
+ XBT_DEBUG("Greeting the MC client");
+ int res = MC_protocol_hello(socket);
+ if (res != 0)
+ throw std::system_error(res, std::system_category());
+ XBT_DEBUG("Greeted the MC client");
+
+ MC_init_pid(pid, socket);
+
+ // Block SIGCHLD (this will be handled with accept/signalfd):
+ sigset_t set;
+ sigemptyset(&set);
+ sigaddset(&set, SIGCHLD);
+ if (sigprocmask(SIG_BLOCK, &set, NULL) == -1)
+ throw std::system_error(errno, std::system_category());
+
+ sigset_t full_set;
+ sigfillset(&full_set);
+
+ // Prepare data for poll:
+
+ struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
+ socket_pollfd->fd = socket;
+ socket_pollfd->events = POLLIN;
+ socket_pollfd->revents = 0;
+
+ int signal_fd = signalfd(-1, &set, 0);
+ if (signal_fd == -1)
+ throw std::system_error(errno, std::system_category());
+
+ struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
+ signalfd_pollfd->fd = signal_fd;
+ signalfd_pollfd->events = POLLIN;
+ signalfd_pollfd->revents = 0;
+}
+
+void s_mc_server::shutdown()
+{
+ XBT_DEBUG("Shuting down model-checker");
+
+ mc_process_t process = &mc_model_checker->process;
+ int status = process->status;
+ if (process->running) {
+ XBT_DEBUG("Killing process");
+ kill(process->pid, SIGTERM);
+ if (waitpid(process->pid, &status, 0) == -1)
+ throw std::system_error(errno, std::system_category());
+ // TODO, handle the case when the process does not want to die with a timeout
+ process->status = status;
+ }
+}
+
+void s_mc_server::exit()
+{
+ // Finished:
+ int status = mc_model_checker->process.status;
+ if (WIFEXITED(status))
+ ::exit(WEXITSTATUS(status));
+ else if (WIFSIGNALED(status)) {
+ // Try to uplicate the signal of the model-checked process.
+ // This is a temporary hack so we don't try too hard.
+ kill(mc_model_checker->process.pid, WTERMSIG(status));
+ abort();
+ } else {
+ xbt_die("Unexpected status from model-checked process");
+ }
+}
+
+void s_mc_server::resume(mc_process_t process)
+{
+ int socket = process->socket;
+ int res = MC_protocol_send_simple_message(socket, MC_MESSAGE_CONTINUE);
+ if (res)
+ throw std::system_error(res, std::system_category());
+}
+
+static
+void throw_socket_error(int fd)
+{
+ int error = 0;
+ socklen_t errlen = sizeof(error);
+ if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1)
+ error = errno;
+ throw std::system_error(error, std::system_category());
+}
+
+void s_mc_server::handle_events()
+{
+ s_mc_message_t message;
+ struct pollfd* socket_pollfd = &fds[SOCKET_FD_INDEX];
+ struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
+
+ while(poll(fds, 2, -1) == -1) {
+ switch(errno) {
+ case EINTR:
+ continue;
+ default:
+ throw std::system_error(errno, std::system_category());
+ }
+ }
+
+ if (socket_pollfd->revents) {
+ if (socket_pollfd->revents & POLLIN) {
+ ssize_t size = recv(socket_pollfd->fd, &message, sizeof(message), MSG_DONTWAIT);
+ if (size == -1 && errno != EAGAIN)
+ throw std::system_error(errno, std::system_category());
+ else switch(message.type) {
+ default:
+ xbt_die("Unexpected message from model-checked application");
+ }
+ return;
+ }
+ if (socket_pollfd->revents & POLLERR) {
+ throw_socket_error(socket_pollfd->fd);
+ }
+ if (socket_pollfd->revents & POLLHUP)
+ xbt_die("Socket hang up?");
+ }
+
+ if (signalfd_pollfd->revents) {
+ if (signalfd_pollfd->revents & POLLIN) {
+ this->handle_signals();
+ return;
+ }
+ if (signalfd_pollfd->revents & POLLERR) {
+ throw_socket_error(signalfd_pollfd->fd);
+ }
+ if (signalfd_pollfd->revents & POLLHUP)
+ xbt_die("Signalfd hang up?");
+ }
+}
+
+void s_mc_server::loop()
+{
+ while (mc_model_checker->process.running)
+ this->handle_events();
+}
+
+void s_mc_server::handle_signals()
+{
+ struct signalfd_siginfo info;
+ struct pollfd* signalfd_pollfd = &fds[SIGNAL_FD_INDEX];
+ while (1) {
+ ssize_t size = read(signalfd_pollfd->fd, &info, sizeof(info));
+ if (size == -1) {
+ if (errno == EINTR)
+ continue;
+ else
+ throw std::system_error(errno, std::system_category());
+ } else if (size != sizeof(info))
+ return throw std::runtime_error(
+ "Bad communication with model-checked application");
+ else
+ break;
+ }
+ this->on_signal(&info);
+}
+
+void s_mc_server::handle_waitpid()
+{
+ XBT_DEBUG("Check for wait event");
+ int status;
+ pid_t pid;
+ while ((pid = waitpid(-1, &status, WNOHANG)) != 0) {
+ if (pid == -1) {
+ if (errno == ECHILD) {
+ // No more children:
+ if (mc_model_checker->process.running)
+ xbt_die("Inconsistent state");
+ else
+ break;
+ } else {
+ XBT_ERROR("Could not wait for pid: %s", strerror(errno));
+ throw std::system_error(errno, std::system_category());
+ }
+ }
+
+ if (pid == mc_model_checker->process.pid) {
+ if (WIFEXITED(status) || WIFSIGNALED(status)) {
+ XBT_DEBUG("Child process is over");
+ mc_model_checker->process.status = status;
+ mc_model_checker->process.running = false;
+ }
+ }
+ }
+}
+
+void s_mc_server::on_signal(const struct signalfd_siginfo* info)
+{
+ switch(info->ssi_signo) {
+ case SIGCHLD:
+ this->handle_waitpid();
+ break;
+ default:
+ break;
+ }
+}
--- /dev/null
+/* Copyright (c) 2015. 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. */
+
+#ifndef MC_SERVER_H
+#define MC_SERVER_H
+
+#include <xbt/misc.h>
+
+SG_BEGIN_DECL()
+
+#define MC_SERVER_ERROR 127
+
+typedef struct s_mc_server s_mc_server_t, *mc_server_t;
+
+extern mc_server_t mc_server;
+
+/** Initialise MC server
+ *
+ * @param PID of the model-checked process
+ * @param socket file descriptor for communication with the model-checked process
+ * @return 0 on success
+ */
+int MC_server_init(pid_t pid, int socket);
+
+/** Execute the MC server
+ *
+ * @return Status code (can be used with `exit()`)
+ */
+void MC_server_run(void);
+
+SG_END_DECL()
+
+#ifdef __cplusplus
+
+struct s_mc_server {
+private:
+ pid_t pid;
+ int socket;
+ struct pollfd fds[2];
+public:
+ s_mc_server(pid_t pid, int socket);
+ void start();
+ void shutdown();
+ void exit();
+ void resume(mc_process_t process);
+ void loop();
+ void handle_events();
+protected:
+ void handle_signals();
+ void handle_waitpid();
+ void on_signal(const struct signalfd_siginfo* info);
+};
+
+#endif
+
+#endif
if(fp == NULL)
perror("fopen failed");
xbt_assert(fp,
- "Cannot open /proc/self/maps to investigate the memory map of the process. Please report this bug.");
+ "Cannot open %s to investigate the memory map of the process.", path);
setbuf(fp, NULL);
memory_map_t ret = xbt_new0(s_memory_map_t, 1);
/* Create space for a new map region in the region's array and copy the */
/* parsed stuff from the temporal memreg variable */
+ XBT_DEBUG("Found region for %s",
+ memreg.pathname ? memreg.pathname : "(null)");
ret->regions =
xbt_realloc(ret->regions, sizeof(memreg) * (ret->mapsize + 1));
memcpy(ret->regions + ret->mapsize, &memreg, sizeof(memreg));
--- /dev/null
+/* Copyright (c) 2015. 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 <cstdlib>
+#include <cstdio>
+#include <cstring>
+
+#include <signal.h>
+#include <poll.h>
+
+#include <unistd.h>
+
+#include <sys/types.h>
+#include <sys/socket.h>
+#include <sys/wait.h>
+
+#include <xbt/log.h>
+
+#include "simgrid/sg_config.h"
+#include "xbt_modinter.h"
+
+#include "mc_base.h"
+#include "mc_private.h"
+#include "mc_protocol.h"
+#include "mc_server.h"
+#include "mc_model_checker.h"
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
+
+static const bool trace = true;
+
+static int do_child(int socket, char** argv)
+{
+ XBT_DEBUG("Inside the child process PID=%i", (int) getpid());
+ int res;
+
+ // Remove CLOEXEC in order to pass the socket to the exec-ed program:
+ int fdflags = fcntl(socket, F_GETFD, 0);
+ if (fdflags == -1) {
+ std::perror("simgrid-mc");
+ return MC_SERVER_ERROR;
+ }
+ if (fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) == -1) {
+ std::perror("simgrid-mc");
+ return MC_SERVER_ERROR;
+ }
+
+ XBT_DEBUG("CLOEXEC removed on socket %i", socket);
+
+ // Set environment:
+ setenv(MC_ENV_VARIABLE, "1", 1);
+
+ char buffer[64];
+ res = std::snprintf(buffer, sizeof(buffer), "%i", socket);
+ if ((size_t) res >= sizeof(buffer) || res == -1)
+ return MC_SERVER_ERROR;
+ setenv(MC_ENV_SOCKET_FD, buffer, 1);
+
+ execvp(argv[1], argv+1);
+ std::perror("simgrid-mc");
+ return MC_SERVER_ERROR;
+}
+
+static int do_parent(int socket, pid_t child)
+{
+ XBT_DEBUG("Inside the parent process");
+ if (MC_server_init(child, socket))
+ return MC_SERVER_ERROR;
+ XBT_DEBUG("Server initialized");
+ MC_server_run();
+ return 0;
+}
+
+static char** argvdup(int argc, char** argv)
+{
+ char** argv_copy = xbt_new(char*, argc+1);
+ std::memcpy(argv_copy, argv, sizeof(char*) * argc);
+ argv_copy[argc] = NULL;
+ return argv_copy;
+}
+
+int main(int argc, char** argv)
+{
+ // We need to keep the original parameters in order to pass them to the
+ // model-checked process:
+ int argc_copy = argc;
+ char** argv_copy = argvdup(argc, argv);
+ xbt_log_init(&argc_copy, argv_copy);
+ sg_config_init(&argc_copy, argv_copy);
+
+ if (argc < 2)
+ xbt_die("Missing arguments.\n");
+
+ bool server_mode = false;
+ char* env = std::getenv("SIMGRID_MC_MODE");
+ if (env) {
+ if (std::strcmp(env, "server") == 0)
+ server_mode = true;
+ else if (std::strcmp(env, "standalone") == 0)
+ server_mode = false;
+ else
+ XBT_WARN("Unrecognised value for SIMGRID_MC_MODE (server/standalone)");
+ }
+
+ if (!server_mode) {
+ setenv(MC_ENV_VARIABLE, "1", 1);
+ execvp(argv[1], argv+1);
+
+ std::perror("simgrid-mc");
+ return 127;
+ }
+
+ // Create a AF_LOCAL socketpair:
+ int res;
+
+ int sockets[2];
+ res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
+ if (res == -1) {
+ perror("simgrid-mc");
+ return MC_SERVER_ERROR;
+ }
+
+ XBT_DEBUG("Created socketpair");
+
+ pid_t pid = fork();
+ if (pid < 0) {
+ perror("simgrid-mc");
+ return MC_SERVER_ERROR;
+ } else if (pid == 0) {
+ close(sockets[1]);
+ return do_child(sockets[0], argv);
+ } else {
+ close(sockets[0]);
+ return do_parent(sockets[1], pid);
+ }
+
+ return 0;
+}
#include "xbt_modinter.h"
#include "internal_config.h"
#include <math.h>
+#include "../mc/mc_protocol.h"
//#define MM_LEGACY_VERBOSE 1 /* define this to see which version of malloc gets used */
#define XBT_MODINTER_H
#include "xbt/misc.h"
+SG_BEGIN_DECL()
+
/* Modules definitions */
void xbt_backtrace_preinit(void);
void xbt_backtrace_postexit(void);
void *mmalloc_preinit(void);
void mmalloc_postexit(void);
+SG_END_DECL()
#endif /* XBT_MODINTER_H */
s_mc_process_t p;
mc_process_t process = &p;
- MC_process_init(&p, getpid());
+ MC_process_init(&p, getpid(), -1);
test_global_variable(process, process->binary_info, "some_local_variable", &some_local_variable, sizeof(int));
#! ./tesh
$ $SG_TEST_EXENV ${bindir:=.}/dwarf
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
!expect signal SIGABRT
$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random_bug ${srcdir:=.}/../../../examples/platforms/small_platform.xml ${srcdir:=.}/random_bug.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning --cfg=model-check:1 --cfg=model-check/record:1
> [ 0.000000] (0:@) Check a safety property
-> [ 0.000000] (0:@) Get debug information ...
-> [ 0.000000] (0:@) Get debug information done !
> [ 0.000000] (1:app@Tremblay) **************************
> [ 0.000000] (1:app@Tremblay) *** PROPERTY NOT VALID ***
> [ 0.000000] (1:app@Tremblay) **************************
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml -np 3 --log=xbt_cfg.thresh:warning --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-can-deadlock10
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml -np 3 --log=xbt_cfg.thresh:warning --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-can-deadlock4
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --log=xbt_cfg.thresh:warning --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-can-deadlock5
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-can-deadlock6
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-wait-deadlock
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-waitall-deadlock2
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-waitall-deadlock3
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-waitany-deadlock
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/any_src-waitany-deadlock2
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun --log=xbt_cfg.thresh:warning -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/basic-deadlock-comm_create
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/basic-deadlock-comm_dup
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/basic-deadlock-comm_split
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/basic-deadlock
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/bcast-deadlock
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/collective-misorder-allreduce
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/collective-misorder
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/complex-deadlock
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/deadlock-config
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> WARNING: This test depends on the MPI's eager limit. Set it appropriately.
> Initializing (0 of 3)
> (0) is alive on Tremblay
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/finalize-deadlock
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/irecv-deadlock
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/no-error
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/no-error2
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/no-error3-any_src
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
$ ${bindir:=.}/../../../../bin/smpirun -hostfile ../../hostfile -platform ../../../../examples/platforms/small_platform.xml --log=xbt_cfg.thresh:warning -np 3 --cfg=model-check:1 --cfg=smpi/running_power:1e9 --cfg=smpi/coll_selector:mpich ${bindir:=.}/no-error3
> [0.000000] [surf_config/INFO] Switching workstation model to compound since you changed the network and/or cpu model(s)
> [0.000000] [mc_global/INFO] Check a safety property
-> [0.000000] [mc_process/INFO] Get debug information ...
-> [0.000000] [mc_process/INFO] Get debug information done !
> (0) is alive on Tremblay
> (1) is alive on Jupiter
> (2) is alive on Fafard
