From 3c5b31c9766da42c82473b8c9dbf5910b74f3cb0 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Tue, 3 Feb 2015 11:26:44 +0100 Subject: [PATCH] [mc] Basic infrastructure for a real model-checker process The model checker process communicates with the model-checked application using socket (and wait). Currently it waits for the MCed process initialisation and fetch its system state, DWARF information, etc but does not do anything else. The previous (standalone) mode is currently used by default. The new behaviour is triggered with the SIMGRID_MC_MODE=server environment. The idea is to keep the standalone version at least as long as the new version is not stable/working. --- buildtools/Cmake/DefinePackages.cmake | 8 +- buildtools/Cmake/MakeLib.cmake | 2 +- examples/msg/mc/bugged1.tesh | 2 - examples/msg/mc/bugged1_liveness.tesh | 2 - examples/msg/mc/bugged1_liveness_sparse.tesh | 2 - examples/msg/mc/bugged1_liveness_visited.tesh | 2 - .../mc/bugged1_liveness_visited_sparse.tesh | 2 - examples/msg/mc/bugged2.tesh | 2 - examples/smpi/mc/non_deterministic.tesh | 4 +- examples/smpi/mc/send_deterministic.tesh | 2 - src/mc/mc_base.h | 5 - src/mc/mc_client.c | 75 +++++ src/mc/{simgrid_mc.c => mc_client.h} | 22 +- src/mc/mc_global.c | 46 ++- src/mc/mc_model_checker.h | 13 +- src/mc/mc_private.h | 10 + src/mc/mc_process.c | 13 +- src/mc/mc_process.h | 5 +- src/mc/mc_protocol.c | 58 ++++ src/mc/mc_protocol.h | 44 +++ src/mc/mc_server.cpp | 261 ++++++++++++++++++ src/mc/mc_server.h | 59 ++++ src/mc/memory_map.c | 4 +- src/mc/simgrid_mc.cpp | 141 ++++++++++ src/xbt/mmalloc/mm_legacy.c | 1 + src/xbt_modinter.h | 3 + teshsuite/mc/dwarf/dwarf.c | 2 +- teshsuite/mc/dwarf/dwarf.tesh | 2 - teshsuite/mc/replay/random_bug.tesh | 2 - .../isp/umpire/any_src-can-deadlock10.tesh | 2 - .../isp/umpire/any_src-can-deadlock4.tesh | 2 - .../isp/umpire/any_src-can-deadlock5.tesh | 2 - .../isp/umpire/any_src-can-deadlock6.tesh | 2 - .../isp/umpire/any_src-wait-deadlock.tesh | 2 - .../isp/umpire/any_src-waitall-deadlock2.tesh | 2 - .../isp/umpire/any_src-waitall-deadlock3.tesh | 2 - .../isp/umpire/any_src-waitany-deadlock.tesh | 2 - .../isp/umpire/any_src-waitany-deadlock2.tesh | 2 - .../umpire/basic-deadlock-comm_create.tesh | 2 - .../isp/umpire/basic-deadlock-comm_dup.tesh | 2 - .../isp/umpire/basic-deadlock-comm_split.tesh | 2 - teshsuite/smpi/isp/umpire/basic-deadlock.tesh | 2 - teshsuite/smpi/isp/umpire/bcast-deadlock.tesh | 2 - .../umpire/collective-misorder-allreduce.tesh | 2 - .../smpi/isp/umpire/collective-misorder.tesh | 2 - .../smpi/isp/umpire/complex-deadlock.tesh | 2 - .../smpi/isp/umpire/deadlock-config.tesh | 2 - .../smpi/isp/umpire/finalize-deadlock.tesh | 2 - teshsuite/smpi/isp/umpire/irecv-deadlock.tesh | 2 - teshsuite/smpi/isp/umpire/no-error.tesh | 2 - teshsuite/smpi/isp/umpire/no-error2.tesh | 2 - .../smpi/isp/umpire/no-error3-any_src.tesh | 2 - teshsuite/smpi/isp/umpire/no-error3.tesh | 2 - 53 files changed, 736 insertions(+), 106 deletions(-) create mode 100644 src/mc/mc_client.c rename src/mc/{simgrid_mc.c => mc_client.h} (51%) create mode 100644 src/mc/mc_protocol.c create mode 100644 src/mc/mc_protocol.h create mode 100644 src/mc/mc_server.cpp create mode 100644 src/mc/mc_server.h create mode 100644 src/mc/simgrid_mc.cpp diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake index cb222a5bf7..4f69a870b5 100644 --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@ -641,10 +641,16 @@ set(MC_SRC 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 diff --git a/buildtools/Cmake/MakeLib.cmake b/buildtools/Cmake/MakeLib.cmake index be1613f8f4..91611c92c0 100644 --- a/buildtools/Cmake/MakeLib.cmake +++ b/buildtools/Cmake/MakeLib.cmake @@ -23,7 +23,7 @@ endif() 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 diff --git a/examples/msg/mc/bugged1.tesh b/examples/msg/mc/bugged1.tesh index 45a86acb8c..03f5d54f9b 100644 --- a/examples/msg/mc/bugged1.tesh +++ b/examples/msg/mc/bugged1.tesh @@ -4,8 +4,6 @@ ! 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 diff --git a/examples/msg/mc/bugged1_liveness.tesh b/examples/msg/mc/bugged1_liveness.tesh index d58f08d6ef..b2e56421bc 100644 --- a/examples/msg/mc/bugged1_liveness.tesh +++ b/examples/msg/mc/bugged1_liveness.tesh @@ -4,8 +4,6 @@ ! 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 diff --git a/examples/msg/mc/bugged1_liveness_sparse.tesh b/examples/msg/mc/bugged1_liveness_sparse.tesh index 7e10bbed22..cc378b1a6b 100644 --- a/examples/msg/mc/bugged1_liveness_sparse.tesh +++ b/examples/msg/mc/bugged1_liveness_sparse.tesh @@ -4,8 +4,6 @@ ! 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 diff --git a/examples/msg/mc/bugged1_liveness_visited.tesh b/examples/msg/mc/bugged1_liveness_visited.tesh index 5cc0174b8d..bf01872a9a 100644 --- a/examples/msg/mc/bugged1_liveness_visited.tesh +++ b/examples/msg/mc/bugged1_liveness_visited.tesh @@ -4,8 +4,6 @@ ! 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 diff --git a/examples/msg/mc/bugged1_liveness_visited_sparse.tesh b/examples/msg/mc/bugged1_liveness_visited_sparse.tesh index d05eb7779d..95eea17ad1 100644 --- a/examples/msg/mc/bugged1_liveness_visited_sparse.tesh +++ b/examples/msg/mc/bugged1_liveness_visited_sparse.tesh @@ -4,8 +4,6 @@ ! 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 diff --git a/examples/msg/mc/bugged2.tesh b/examples/msg/mc/bugged2.tesh index 0daf1d5d63..49619cea8f 100644 --- a/examples/msg/mc/bugged2.tesh +++ b/examples/msg/mc/bugged2.tesh @@ -4,8 +4,6 @@ ! 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 diff --git a/examples/smpi/mc/non_deterministic.tesh b/examples/smpi/mc/non_deterministic.tesh index 9a4a6ca804..494c917120 100644 --- a/examples/smpi/mc/non_deterministic.tesh +++ b/examples/smpi/mc/non_deterministic.tesh @@ -1,11 +1,9 @@ #! ./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 ***** diff --git a/examples/smpi/mc/send_deterministic.tesh b/examples/smpi/mc/send_deterministic.tesh index 6c3d51d917..39dccba678 100644 --- a/examples/smpi/mc/send_deterministic.tesh +++ b/examples/smpi/mc/send_deterministic.tesh @@ -4,8 +4,6 @@ $ ../../../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 diff --git a/src/mc/mc_base.h b/src/mc/mc_base.h index 00a453a39d..c21a00bc26 100644 --- a/src/mc/mc_base.h +++ b/src/mc/mc_base.h @@ -14,11 +14,6 @@ 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` diff --git a/src/mc/mc_client.c b/src/mc/mc_client.c new file mode 100644 index 0000000000..2f30581ce3 --- /dev/null +++ b/src/mc/mc_client.c @@ -0,0 +1,75 @@ +/* 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 +#include +#include + +#include +#include + +#include +#include + +#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); + } + } +} diff --git a/src/mc/simgrid_mc.c b/src/mc/mc_client.h similarity index 51% rename from src/mc/simgrid_mc.c rename to src/mc/mc_client.h index 48e61a13c8..d013a172eb 100644 --- a/src/mc/simgrid_mc.c +++ b/src/mc/mc_client.h @@ -4,21 +4,17 @@ /* 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 -#include +#ifndef MC_CLIENT_H +#define MC_CLIENT_H -#include +#include -#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 diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 04017085e3..901bfd6bb2 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -4,6 +4,8 @@ /* 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 + #include "mc_base.h" #ifndef _XBT_WIN32 @@ -34,11 +36,14 @@ #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 @@ -96,13 +101,13 @@ static void MC_init_dot_output() 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; } @@ -114,6 +119,26 @@ void MC_model_checker_delete(mc_model_checker_t 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); @@ -124,7 +149,7 @@ void MC_init() 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); @@ -183,10 +208,15 @@ void MC_init() 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) diff --git a/src/mc/mc_model_checker.h b/src/mc/mc_model_checker.h index 77bbfe00d2..d590e0fc28 100644 --- a/src/mc/mc_model_checker.h +++ b/src/mc/mc_model_checker.h @@ -7,6 +7,8 @@ #ifndef MC_MODEL_CHECKER_H #define MC_MODEL_CHECKER_H +#include + #include #include "mc_forward.h" @@ -14,6 +16,15 @@ 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 @@ -31,7 +42,7 @@ struct s_mc_model_checker { 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() diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index e303ff4eac..7f092a5489 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -7,6 +7,8 @@ #ifndef MC_PRIVATE_H #define MC_PRIVATE_H +#include + #include "simgrid_config.h" #include #include @@ -21,6 +23,7 @@ #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" @@ -44,6 +47,13 @@ extern xbt_dynar_t mc_checkpoint_ignore; /********************************* 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; diff --git a/src/mc/mc_process.c b/src/mc/mc_process.c index b4aace4fde..fd3942043b 100644 --- a/src/mc/mc_process.c +++ b/src/mc/mc_process.c @@ -42,13 +42,16 @@ bool MC_is_process(mc_address_space_t p) 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; @@ -222,7 +225,7 @@ static char* MC_get_lib_name(const char* pathname, struct s_mc_memory_map_re* re /** @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; @@ -299,10 +302,10 @@ static void MC_process_init_memory_map_info(mc_process_t process) 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) diff --git a/src/mc/mc_process.h b/src/mc/mc_process.h index f5fd69f976..b8c551436d 100644 --- a/src/mc/mc_process.h +++ b/src/mc/mc_process.h @@ -46,6 +46,9 @@ struct s_mc_process { 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; @@ -103,7 +106,7 @@ struct s_mc_process { 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 diff --git a/src/mc/mc_protocol.c b/src/mc/mc_protocol.c new file mode 100644 index 0000000000..3396a38396 --- /dev/null +++ b/src/mc/mc_protocol.c @@ -0,0 +1,58 @@ +/* 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 +#include + +#include +#include + +#include + +#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; +} diff --git a/src/mc/mc_protocol.h b/src/mc/mc_protocol.h new file mode 100644 index 0000000000..ba8014500b --- /dev/null +++ b/src/mc/mc_protocol.h @@ -0,0 +1,44 @@ +/* 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 + +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 diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp new file mode 100644 index 0000000000..cc7c5250bb --- /dev/null +++ b/src/mc/mc_server.cpp @@ -0,0 +1,261 @@ +/* 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 +#include + +#include +#include +#include +#include +#include + +#include + +#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; + } +} diff --git a/src/mc/mc_server.h b/src/mc/mc_server.h new file mode 100644 index 0000000000..559d0850b7 --- /dev/null +++ b/src/mc/mc_server.h @@ -0,0 +1,59 @@ +/* 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 + +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 diff --git a/src/mc/memory_map.c b/src/mc/memory_map.c index 0d6a0667cb..337ed9da2c 100644 --- a/src/mc/memory_map.c +++ b/src/mc/memory_map.c @@ -24,7 +24,7 @@ memory_map_t MC_get_memory_map(pid_t pid) 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); @@ -141,6 +141,8 @@ memory_map_t MC_get_memory_map(pid_t pid) /* 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)); diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp new file mode 100644 index 0000000000..982bd8e73c --- /dev/null +++ b/src/mc/simgrid_mc.cpp @@ -0,0 +1,141 @@ +/* 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 +#include +#include + +#include +#include + +#include + +#include +#include +#include + +#include + +#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; +} diff --git a/src/xbt/mmalloc/mm_legacy.c b/src/xbt/mmalloc/mm_legacy.c index a5d57952cf..d4f75a3368 100644 --- a/src/xbt/mmalloc/mm_legacy.c +++ b/src/xbt/mmalloc/mm_legacy.c @@ -16,6 +16,7 @@ #include "xbt_modinter.h" #include "internal_config.h" #include +#include "../mc/mc_protocol.h" //#define MM_LEGACY_VERBOSE 1 /* define this to see which version of malloc gets used */ diff --git a/src/xbt_modinter.h b/src/xbt_modinter.h index 079e050d76..ed497cc7e2 100644 --- a/src/xbt_modinter.h +++ b/src/xbt_modinter.h @@ -10,6 +10,8 @@ #define XBT_MODINTER_H #include "xbt/misc.h" +SG_BEGIN_DECL() + /* Modules definitions */ void xbt_backtrace_preinit(void); void xbt_backtrace_postexit(void); @@ -29,5 +31,6 @@ void xbt_os_thread_mod_postexit(void); void *mmalloc_preinit(void); void mmalloc_postexit(void); +SG_END_DECL() #endif /* XBT_MODINTER_H */ diff --git a/teshsuite/mc/dwarf/dwarf.c b/teshsuite/mc/dwarf/dwarf.c index 997771c337..c7ad31c335 100644 --- a/teshsuite/mc/dwarf/dwarf.c +++ b/teshsuite/mc/dwarf/dwarf.c @@ -128,7 +128,7 @@ int main(int argc, char** argv) 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)); diff --git a/teshsuite/mc/dwarf/dwarf.tesh b/teshsuite/mc/dwarf/dwarf.tesh index 49a59b7de2..0491dadc2d 100644 --- a/teshsuite/mc/dwarf/dwarf.tesh +++ b/teshsuite/mc/dwarf/dwarf.tesh @@ -1,5 +1,3 @@ #! ./tesh $ $SG_TEST_EXENV ${bindir:=.}/dwarf -> [0.000000] [mc_process/INFO] Get debug information ... -> [0.000000] [mc_process/INFO] Get debug information done ! diff --git a/teshsuite/mc/replay/random_bug.tesh b/teshsuite/mc/replay/random_bug.tesh index 35bf5e9860..1b79e51dc7 100644 --- a/teshsuite/mc/replay/random_bug.tesh +++ b/teshsuite/mc/replay/random_bug.tesh @@ -2,8 +2,6 @@ !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) ************************** diff --git a/teshsuite/smpi/isp/umpire/any_src-can-deadlock10.tesh b/teshsuite/smpi/isp/umpire/any_src-can-deadlock10.tesh index be608b9a0d..f10e305761 100644 --- a/teshsuite/smpi/isp/umpire/any_src-can-deadlock10.tesh +++ b/teshsuite/smpi/isp/umpire/any_src-can-deadlock10.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/any_src-can-deadlock4.tesh b/teshsuite/smpi/isp/umpire/any_src-can-deadlock4.tesh index 0c901f65e0..c8857c90be 100644 --- a/teshsuite/smpi/isp/umpire/any_src-can-deadlock4.tesh +++ b/teshsuite/smpi/isp/umpire/any_src-can-deadlock4.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/any_src-can-deadlock5.tesh b/teshsuite/smpi/isp/umpire/any_src-can-deadlock5.tesh index 903cde54c9..0adf72c474 100644 --- a/teshsuite/smpi/isp/umpire/any_src-can-deadlock5.tesh +++ b/teshsuite/smpi/isp/umpire/any_src-can-deadlock5.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/any_src-can-deadlock6.tesh b/teshsuite/smpi/isp/umpire/any_src-can-deadlock6.tesh index 69e33a9f88..0122655faf 100644 --- a/teshsuite/smpi/isp/umpire/any_src-can-deadlock6.tesh +++ b/teshsuite/smpi/isp/umpire/any_src-can-deadlock6.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/any_src-wait-deadlock.tesh b/teshsuite/smpi/isp/umpire/any_src-wait-deadlock.tesh index 944b92b8be..fdd9a5f308 100644 --- a/teshsuite/smpi/isp/umpire/any_src-wait-deadlock.tesh +++ b/teshsuite/smpi/isp/umpire/any_src-wait-deadlock.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/any_src-waitall-deadlock2.tesh b/teshsuite/smpi/isp/umpire/any_src-waitall-deadlock2.tesh index 9818b2cf3a..9678f5f789 100644 --- a/teshsuite/smpi/isp/umpire/any_src-waitall-deadlock2.tesh +++ b/teshsuite/smpi/isp/umpire/any_src-waitall-deadlock2.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/any_src-waitall-deadlock3.tesh b/teshsuite/smpi/isp/umpire/any_src-waitall-deadlock3.tesh index 183a8fec27..c18b734773 100644 --- a/teshsuite/smpi/isp/umpire/any_src-waitall-deadlock3.tesh +++ b/teshsuite/smpi/isp/umpire/any_src-waitall-deadlock3.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/any_src-waitany-deadlock.tesh b/teshsuite/smpi/isp/umpire/any_src-waitany-deadlock.tesh index b2d528e3f4..11814348d1 100644 --- a/teshsuite/smpi/isp/umpire/any_src-waitany-deadlock.tesh +++ b/teshsuite/smpi/isp/umpire/any_src-waitany-deadlock.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/any_src-waitany-deadlock2.tesh b/teshsuite/smpi/isp/umpire/any_src-waitany-deadlock2.tesh index 08134f8c8f..821c2c355e 100644 --- a/teshsuite/smpi/isp/umpire/any_src-waitany-deadlock2.tesh +++ b/teshsuite/smpi/isp/umpire/any_src-waitany-deadlock2.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/basic-deadlock-comm_create.tesh b/teshsuite/smpi/isp/umpire/basic-deadlock-comm_create.tesh index 64dc1be993..f0f433e1a8 100644 --- a/teshsuite/smpi/isp/umpire/basic-deadlock-comm_create.tesh +++ b/teshsuite/smpi/isp/umpire/basic-deadlock-comm_create.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/basic-deadlock-comm_dup.tesh b/teshsuite/smpi/isp/umpire/basic-deadlock-comm_dup.tesh index 2b97ecb067..d7810c8f12 100644 --- a/teshsuite/smpi/isp/umpire/basic-deadlock-comm_dup.tesh +++ b/teshsuite/smpi/isp/umpire/basic-deadlock-comm_dup.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/basic-deadlock-comm_split.tesh b/teshsuite/smpi/isp/umpire/basic-deadlock-comm_split.tesh index 623bdd440e..b540f3ac43 100644 --- a/teshsuite/smpi/isp/umpire/basic-deadlock-comm_split.tesh +++ b/teshsuite/smpi/isp/umpire/basic-deadlock-comm_split.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/basic-deadlock.tesh b/teshsuite/smpi/isp/umpire/basic-deadlock.tesh index 7440523392..e35272ad6e 100644 --- a/teshsuite/smpi/isp/umpire/basic-deadlock.tesh +++ b/teshsuite/smpi/isp/umpire/basic-deadlock.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/bcast-deadlock.tesh b/teshsuite/smpi/isp/umpire/bcast-deadlock.tesh index c867107eea..dbd8f7fa49 100644 --- a/teshsuite/smpi/isp/umpire/bcast-deadlock.tesh +++ b/teshsuite/smpi/isp/umpire/bcast-deadlock.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/collective-misorder-allreduce.tesh b/teshsuite/smpi/isp/umpire/collective-misorder-allreduce.tesh index 0cab131bf3..ab2f74b6ef 100644 --- a/teshsuite/smpi/isp/umpire/collective-misorder-allreduce.tesh +++ b/teshsuite/smpi/isp/umpire/collective-misorder-allreduce.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/collective-misorder.tesh b/teshsuite/smpi/isp/umpire/collective-misorder.tesh index a4e65cb2f1..7bd71e9a53 100644 --- a/teshsuite/smpi/isp/umpire/collective-misorder.tesh +++ b/teshsuite/smpi/isp/umpire/collective-misorder.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/complex-deadlock.tesh b/teshsuite/smpi/isp/umpire/complex-deadlock.tesh index 926e8b01f4..1ccfc3c323 100644 --- a/teshsuite/smpi/isp/umpire/complex-deadlock.tesh +++ b/teshsuite/smpi/isp/umpire/complex-deadlock.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/deadlock-config.tesh b/teshsuite/smpi/isp/umpire/deadlock-config.tesh index b1bc3e60f1..2d2f1d0535 100644 --- a/teshsuite/smpi/isp/umpire/deadlock-config.tesh +++ b/teshsuite/smpi/isp/umpire/deadlock-config.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/finalize-deadlock.tesh b/teshsuite/smpi/isp/umpire/finalize-deadlock.tesh index ccb3011b1d..87c6758afe 100644 --- a/teshsuite/smpi/isp/umpire/finalize-deadlock.tesh +++ b/teshsuite/smpi/isp/umpire/finalize-deadlock.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/irecv-deadlock.tesh b/teshsuite/smpi/isp/umpire/irecv-deadlock.tesh index 16bfaf74f7..a3670b391b 100644 --- a/teshsuite/smpi/isp/umpire/irecv-deadlock.tesh +++ b/teshsuite/smpi/isp/umpire/irecv-deadlock.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/no-error.tesh b/teshsuite/smpi/isp/umpire/no-error.tesh index 791a62892f..987bd1d0f0 100644 --- a/teshsuite/smpi/isp/umpire/no-error.tesh +++ b/teshsuite/smpi/isp/umpire/no-error.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/no-error2.tesh b/teshsuite/smpi/isp/umpire/no-error2.tesh index 21e800287e..9ca59c83ff 100644 --- a/teshsuite/smpi/isp/umpire/no-error2.tesh +++ b/teshsuite/smpi/isp/umpire/no-error2.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/no-error3-any_src.tesh b/teshsuite/smpi/isp/umpire/no-error3-any_src.tesh index 75e8655135..4fc50a3dcd 100644 --- a/teshsuite/smpi/isp/umpire/no-error3-any_src.tesh +++ b/teshsuite/smpi/isp/umpire/no-error3-any_src.tesh @@ -4,8 +4,6 @@ $ ${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 diff --git a/teshsuite/smpi/isp/umpire/no-error3.tesh b/teshsuite/smpi/isp/umpire/no-error3.tesh index 84b8ea8aab..a8a67880f5 100644 --- a/teshsuite/smpi/isp/umpire/no-error3.tesh +++ b/teshsuite/smpi/isp/umpire/no-error3.tesh @@ -4,8 +4,6 @@ $ ${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 -- 2.20.1