[mc] Create a separate simgrid-mc program

We create a separate program for the model-checker. The goal is that
this program will:

  - prepare the environment for the child/main process (environment
    variables, maybe LD_PRELOAD a library, pass file descriptors);

  - hold all the model-checker state;

  - communicate with the child process;

  - handle some part of the snapshoting/restoration logic;

  - handle the state comparison logic.

Currently it only enables the custom heap in the child process.

diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake
index fcb29a8..79bc327 100644 (file)
--- a/buildtools/Cmake/DefinePackages.cmake
+++ b/buildtools/Cmake/DefinePackages.cmake
@@ -640,6 +640,9 @@ set(MC_SRC
   src/mc/memory_map.c
   )
 
+set(MC_SIMGRID_MC_SRC
+  src/mc/simgrid_mc.c)
+
 set(headers_to_install
   include/instr/instr.h
   include/msg/datatypes.h

diff --git a/buildtools/Cmake/Distrib.cmake b/buildtools/Cmake/Distrib.cmake
index 428db7c..53f9e09 100644 (file)
--- a/buildtools/Cmake/Distrib.cmake
+++ b/buildtools/Cmake/Distrib.cmake
@@ -205,6 +205,7 @@ set(source_to_pack
   ${LUA_SRC}
   ${MC_SRC_BASE}
   ${MC_SRC}
+  ${MC_SIMGRID_MC_SRC}
   ${MSG_SRC}
   ${NS3_SRC}
   ${RNGSTREAM_SRC}

diff --git a/buildtools/Cmake/MakeLib.cmake b/buildtools/Cmake/MakeLib.cmake
index 9f15a91..9518d4c 100644 (file)
--- a/buildtools/Cmake/MakeLib.cmake
+++ b/buildtools/Cmake/MakeLib.cmake
@@ -22,6 +22,14 @@ endif()
 
 add_dependencies(simgrid maintainer_files)
 
+if(enable_model-checking)
+  add_executable(simgrid-mc "${MC_SIMGRID_MC_SRC}")
+  target_link_libraries(simgrid-mc simgrid)
+  set_target_properties(simgrid-mc
+    PROPERTIES
+      RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}/bin")
+endif()
+
 # Compute the dependencies of SimGrid
 #####################################
 set(SIMGRID_DEP "-lm")

diff --git a/examples/msg/mc/bugged1.tesh b/examples/msg/mc/bugged1.tesh
index 3feaf55..45a86ac 100644 (file)
--- a/examples/msg/mc/bugged1.tesh
+++ b/examples/msg/mc/bugged1.tesh
@@ -2,7 +2,7 @@
 
 ! expect signal SIGABRT
 ! timeout 20
-$ ${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
+$ ${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 !

diff --git a/examples/msg/mc/bugged1_liveness.tesh b/examples/msg/mc/bugged1_liveness.tesh
index 3bf495c..d58f08d 100644 (file)
--- a/examples/msg/mc/bugged1_liveness.tesh
+++ b/examples/msg/mc/bugged1_liveness.tesh
@@ -2,7 +2,7 @@
 
 ! expect signal SIGABRT
 ! timeout 20
-$ ${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
+$ ${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 !

diff --git a/examples/msg/mc/bugged1_liveness_sparse.tesh b/examples/msg/mc/bugged1_liveness_sparse.tesh
index a87f36a..7e10bbe 100644 (file)
--- a/examples/msg/mc/bugged1_liveness_sparse.tesh
+++ b/examples/msg/mc/bugged1_liveness_sparse.tesh
@@ -2,7 +2,7 @@
 
 ! expect signal SIGABRT
 ! timeout 60
-$ ${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
+$ ${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 !

diff --git a/examples/msg/mc/bugged1_liveness_visited.tesh b/examples/msg/mc/bugged1_liveness_visited.tesh
index 790bec1..5cc0174 100644 (file)
--- a/examples/msg/mc/bugged1_liveness_visited.tesh
+++ b/examples/msg/mc/bugged1_liveness_visited.tesh
@@ -2,7 +2,7 @@
 
 ! expect signal SIGABRT
 ! timeout 90
-$ ${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
+$ ${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 !

diff --git a/examples/msg/mc/bugged1_liveness_visited_sparse.tesh b/examples/msg/mc/bugged1_liveness_visited_sparse.tesh
index ff082be..d05eb77 100644 (file)
--- a/examples/msg/mc/bugged1_liveness_visited_sparse.tesh
+++ b/examples/msg/mc/bugged1_liveness_visited_sparse.tesh
@@ -2,7 +2,7 @@
 
 ! expect signal SIGABRT
 ! timeout 90
-$ ${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
+$ ${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 !

diff --git a/examples/msg/mc/bugged2.tesh b/examples/msg/mc/bugged2.tesh
index 3909db5..0daf1d5 100644 (file)
--- a/examples/msg/mc/bugged2.tesh
+++ b/examples/msg/mc/bugged2.tesh
@@ -2,7 +2,7 @@
 
 ! expect signal SIGABRT
 ! timeout 20
-$ ${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
+$ ${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 !

diff --git a/examples/smpi/mc/non_deterministic.tesh b/examples/smpi/mc/non_deterministic.tesh
index 176ee34..9a4a6ca 100644 (file)
--- a/examples/smpi/mc/non_deterministic.tesh
+++ b/examples/smpi/mc/non_deterministic.tesh
@@ -1,7 +1,7 @@
 #! ./tesh
 
 ! timeout 60
-$ ../../../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
+$ ${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
 > [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 ...

diff --git a/examples/smpi/mc/send_deterministic.tesh b/examples/smpi/mc/send_deterministic.tesh
index 363b1c3..6c3d51d 100644 (file)
--- a/examples/smpi/mc/send_deterministic.tesh
+++ b/examples/smpi/mc/send_deterministic.tesh
@@ -1,7 +1,7 @@
 #! ./tesh
 
 ! timeout 60
-$ ../../../smpi_script/bin/smpirun -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
+$ ../../../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 ...

diff --git a/src/mc/mc_base.h b/src/mc/mc_base.h
index c462414..7027a93 100644 (file)
--- a/src/mc/mc_base.h
+++ b/src/mc/mc_base.h
@@ -14,6 +14,10 @@
 
 SG_BEGIN_DECL()
 
+// This variable is set by simgrid-mc in order to enable MC support in the
+// children MC processes:
+#define MC_ENV_VARIABLE "SIMGRIC_MC"
+
 int MC_request_is_enabled(smx_simcall_t req);
 int MC_request_is_visible(smx_simcall_t req);
 void MC_wait_for_requests(void);

diff --git a/src/mc/mc_memory.c b/src/mc/mc_memory.c
index 6d9700e..bc0617a 100644 (file)
--- a/src/mc/mc_memory.c
+++ b/src/mc/mc_memory.c
@@ -26,8 +26,9 @@ xbt_mheap_t mc_heap = NULL;           /* memory persistent over the MC rollbacks
 /* It creates the two heap regions: std_heap and mc_heap */
 void MC_memory_init()
 {
-  mmalloc_ensure_using_mm(
-    xbt_dynar_length(xbt_cmdline), xbt_dynar_get_ptr(xbt_cmdline, 0));
+  if (!malloc_use_mmalloc()) {
+    xbt_die("Model-checking support is not enabled: run with simgrid-mc.");
+  }
 
   /* Create the first region HEAP_OFFSET bytes after the heap break address */
   std_heap = mmalloc_get_default_md();

diff --git a/src/mc/simgrid_mc.c b/src/mc/simgrid_mc.c
new file mode 100644 (file)
index 0000000..48e61a1
--- /dev/null
+++ b/src/mc/simgrid_mc.c
@@ -0,0 +1,24 @@
+/* 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 <stdio.h>
+#include <errno.h>
+
+#include <unistd.h>
+
+#include "mc_base.h"
+
+int main(int argc, char** argv)
+{
+  if (argc < 2)
+    xbt_die("Missing arguments.\n");
+
+  setenv(MC_ENV_VARIABLE, "1", 1);
+  execvp(argv[1], argv+1);
+
+  perror("simgrid-mc");
+  return 127;
+}

diff --git a/src/xbt/mmalloc/mm_legacy.c b/src/xbt/mmalloc/mm_legacy.c
index b5457e1..a5d5795 100644 (file)
--- a/src/xbt/mmalloc/mm_legacy.c
+++ b/src/xbt/mmalloc/mm_legacy.c
@@ -11,6 +11,7 @@
 
 #include <dlfcn.h>
 
+#include "../../mc/mc_base.h"
 #include "mmprivate.h"
 #include "xbt_modinter.h"
 #include "internal_config.h"
@@ -24,6 +25,12 @@
    backwards compatibility with the non-mmap'd version. */
 xbt_mheap_t __mmalloc_default_mdp = NULL;
 
+static int __malloc_use_mmalloc;
+
+int malloc_use_mmalloc(void)
+{
+  return __malloc_use_mmalloc;
+}
 
 static xbt_mheap_t __mmalloc_current_heap = NULL;     /* The heap we are currently using. */
 
@@ -61,35 +68,12 @@ static mm_realloc_t mm_real_realloc = mm_fake_realloc;
 
 #define GET_HEAP() __mmalloc_current_heap
 
-static const char* env_name = "SIMGRID_MALLOC_USE_MM";
-
-int mmalloc_exec_using_mm(int argc, const char** argv)
-{
-  char** argv2 = (char**) malloc(sizeof(char*) * (argc+1));
-  memcpy(argv2, argv, sizeof(char*) * argc);
-  argv2[argc] = NULL;
-  if (setenv(env_name, "1", 1) >= 0) {
-    execv(argv[0], argv2);
-  }
-  unsetenv(env_name);
-  fprintf(stderr, "Could not restart with mm malloc\n");
-  free(argv2);
-  return -1;
-}
-
-void mmalloc_ensure_using_mm(int argc, const char** argv)
-{
-  if (!__mmalloc_default_mdp) {
-    mmalloc_exec_using_mm(argc, argv);
-  }
-}
-
 /** Constructor functions used to initialize the malloc implementation
  */
 static void __attribute__((constructor(101))) mm_legacy_constructor()
 {
-  bool use_mm = getenv(env_name);
-  if (use_mm) {
+  __malloc_use_mmalloc = getenv(MC_ENV_VARIABLE) ? 1 : 0;
+  if (__malloc_use_mmalloc) {
     __mmalloc_current_heap = mmalloc_preinit();
   } else {
     mm_real_realloc  = (mm_realloc_t) dlsym(RTLD_NEXT, "realloc");
@@ -101,7 +85,7 @@ static void __attribute__((constructor(101))) mm_legacy_constructor()
 
 void *malloc(size_t n)
 {
-  if (!__mmalloc_current_heap) {
+  if (!__malloc_use_mmalloc) {
     return mm_real_malloc(n);
   }
 
@@ -117,7 +101,7 @@ void *malloc(size_t n)
 
 void *calloc(size_t nmemb, size_t size)
 {
-  if (!__mmalloc_current_heap) {
+  if (!__malloc_use_mmalloc) {
     return mm_real_calloc(nmemb, size);
   }
 
@@ -137,7 +121,7 @@ void *calloc(size_t nmemb, size_t size)
 
 void *realloc(void *p, size_t s)
 {
-  if (!__mmalloc_current_heap) {
+  if (!__malloc_use_mmalloc) {
     return mm_real_realloc(p, s);
   }
 
@@ -153,14 +137,14 @@ void *realloc(void *p, size_t s)
 
 void free(void *p)
 {
-  if (!p)
-    return;
-
-  if (!__mmalloc_current_heap) {
+  if (!__malloc_use_mmalloc) {
     mm_real_free(p);
     return;
   }
 
+  if (!p)
+    return;
+
   xbt_mheap_t mdp = GET_HEAP();
   LOCK(mdp);
   mfree(mdp, p);

diff --git a/src/xbt/mmalloc/mmprivate.h b/src/xbt/mmalloc/mmprivate.h
index 67c5bba..8a40c48 100644 (file)
--- a/src/xbt/mmalloc/mmprivate.h
+++ b/src/xbt/mmalloc/mmprivate.h
@@ -321,6 +321,8 @@ static inline int mmalloc_get_increment(malloc_info* heapinfo) {
 
 void mmcheck(xbt_mheap_t heap);
 
+int malloc_use_mmalloc(void);
+
 int mmalloc_exec_using_mm(int argc, const char** argv);
 void mmalloc_ensure_using_mm(int argc, const char** argv);
 

diff --git a/teshsuite/mc/dwarf/dwarf.tesh b/teshsuite/mc/dwarf/dwarf.tesh
index 49a59b7..6e47a34 100644 (file)
--- a/teshsuite/mc/dwarf/dwarf.tesh
+++ b/teshsuite/mc/dwarf/dwarf.tesh
@@ -1,5 +1,5 @@
 #! ./tesh
 
-$ $SG_TEST_EXENV ${bindir:=.}/dwarf
+$ $SG_TEST_EXENV ${bindir:=.}/../../../bin/simgrid-mc ${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 7993567..35bf5e9 100644 (file)
--- a/teshsuite/mc/replay/random_bug.tesh
+++ b/teshsuite/mc/replay/random_bug.tesh
@@ -1,6 +1,6 @@
 #!/usr/bin/env tesh
 !expect signal SIGABRT
-$ ${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
+$ ${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 !