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
${LUA_SRC}
${MC_SRC_BASE}
${MC_SRC}
+ ${MC_SIMGRID_MC_SRC}
${MSG_SRC}
${NS3_SRC}
${RNGSTREAM_SRC}
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")
! 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 !
! 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 !
! 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 !
! 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 !
! 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 !
! 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 !
#! ./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 ...
#! ./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 ...
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);
/* 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();
--- /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 <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;
+}
#include <dlfcn.h>
+#include "../../mc/mc_base.h"
#include "mmprivate.h"
#include "xbt_modinter.h"
#include "internal_config.h"
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. */
#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");
void *malloc(size_t n)
{
- if (!__mmalloc_current_heap) {
+ if (!__malloc_use_mmalloc) {
return mm_real_malloc(n);
}
void *calloc(size_t nmemb, size_t size)
{
- if (!__mmalloc_current_heap) {
+ if (!__malloc_use_mmalloc) {
return mm_real_calloc(nmemb, size);
}
void *realloc(void *p, size_t s)
{
- if (!__mmalloc_current_heap) {
+ if (!__malloc_use_mmalloc) {
return mm_real_realloc(p, 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);
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);
#! ./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 !
#!/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 !