From 152ae176ced6c0cf415a15a491476488389ce2ab Mon Sep 17 00:00:00 2001
From: Gabriel Corona <gabriel.corona@loria.fr>
Date: Tue, 7 Apr 2015 12:59:10 +0200
Subject: [PATCH] [mc] Move liveness in MCer process

---
 examples/msg/mc/bugged1_liveness.c            |  8 +--
 examples/msg/mc/bugged1_liveness.tesh         | 14 ++---
 examples/msg/mc/bugged1_liveness_sparse.tesh  | 13 +++--
 examples/msg/mc/bugged1_liveness_visited.tesh |  3 +-
 .../mc/bugged1_liveness_visited_sparse.tesh   |  2 +-
 examples/msg/mc/bugged2_liveness.c            |  1 -
 include/xbt/ex.h                              |  3 +-
 src/mc/mc_global.c                            | 55 ++++++-------------
 src/mc/mc_liveness.c                          | 42 ++++++++++++--
 src/mc/mc_liveness.h                          |  1 -
 src/mc/mc_server.cpp                          |  5 ++
 src/mc/mc_server.h                            |  2 +
 src/mc/mc_visited.c                           |  3 +-
 src/mc/simgrid_mc.cpp                         | 16 +-----
 src/msg/msg_mailbox.c                         |  2 +-
 15 files changed, 85 insertions(+), 85 deletions(-)

diff --git a/examples/msg/mc/bugged1_liveness.c b/examples/msg/mc/bugged1_liveness.c
index c5e9820a3b..5a0d66b78a 100644
--- a/examples/msg/mc/bugged1_liveness.c
+++ b/examples/msg/mc/bugged1_liveness.c
@@ -39,7 +39,6 @@ static void garbage_stack(void) {
 
 int coordinator(int argc, char *argv[])
 {
-
   int CS_used = 0;   
   msg_task_t task = NULL, answer = NULL; 
   xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);
@@ -151,22 +150,21 @@ static int raw_client(int argc, char *argv[])
 
 int main(int argc, char *argv[])
 {
-
   MSG_init(&argc, argv);
-
   char **options = &argv[1];
 
-  MSG_config("model-check/property","promela_bugged1_liveness");
   MC_automaton_new_propositional_symbol_pointer("r", &r);
   MC_automaton_new_propositional_symbol_pointer("cs", &cs);
 
   const char* platform_file = options[0];
   const char* application_file = options[1];
-  
+
   MSG_create_environment(platform_file);
+
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", raw_client);
   MSG_launch_application(application_file);
+
   MSG_main();
 
   return 0;
diff --git a/examples/msg/mc/bugged1_liveness.tesh b/examples/msg/mc/bugged1_liveness.tesh
index dc3c3a7be1..5cb0cf00eb 100644
--- a/examples/msg/mc/bugged1_liveness.tesh
+++ b/examples/msg/mc/bugged1_liveness.tesh
@@ -2,7 +2,7 @@
 
 ! expect signal SIGABRT
 ! 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
+$ ${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/property:promela_bugged1_liveness
 > [  0.000000] (0:@) Check the liveness property promela_bugged1_liveness
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (3:client@Fafard) Ask the request
@@ -12,7 +12,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.
 > [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
 > [  0.000000] (3:client@Fafard) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [  0.000000] (0:@) Pair 22 already reached (equal to pair 10) !
+> [  0.000000] (0:@) Pair 23 already reached (equal to pair 11) !
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
 > [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
@@ -37,8 +37,8 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.
 > [  0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
 > [  0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only))
 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
-> [  0.000000] (0:@) Expanded pairs = 22
-> [  0.000000] (0:@) Visited pairs = 20
-> [  0.000000] (0:@) Executed transitions = 20
-> [  0.000000] (0:@) Counter-example depth : 21
-
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) Expanded pairs = 23
+> [  0.000000] (0:@) Visited pairs = 21
+> [  0.000000] (0:@) Executed transitions = 21
+> [  0.000000] (0:@) Counter-example depth : 22
diff --git a/examples/msg/mc/bugged1_liveness_sparse.tesh b/examples/msg/mc/bugged1_liveness_sparse.tesh
index 1ad6da3b2e..72d4e722e1 100644
--- 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:=.}/../../../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
+$ ${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 --cfg=model-check/property:promela_bugged1_liveness
 > [  0.000000] (0:@) Check the liveness property promela_bugged1_liveness
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (3:client@Fafard) Ask the request
@@ -12,7 +12,7 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.
 > [  0.000000] (1:coordinator@Tremblay) CS release. resource now idle
 > [  0.000000] (3:client@Fafard) Ask the request
 > [  0.000000] (1:coordinator@Tremblay) CS idle. Grant immediatly
-> [  0.000000] (0:@) Pair 22 already reached (equal to pair 10) !
+> [  0.000000] (0:@) Pair 23 already reached (equal to pair 11) !
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
 > [  0.000000] (0:@) |             ACCEPTANCE CYCLE            |
 > [  0.000000] (0:@) *-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*
@@ -37,7 +37,8 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.
 > [  0.000000] (0:@) [(3)Fafard (client)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
 > [  0.000000] (0:@) [(3)Fafard (client)] iSend(src=(3)Fafard (client), buff=(verbose only), size=(verbose only))
 > [  0.000000] (0:@) [(1)Tremblay (coordinator)] Wait(comm=(verbose only) [(3)Fafard (client)-> (1)Tremblay (coordinator)])
-> [  0.000000] (0:@) Expanded pairs = 22
-> [  0.000000] (0:@) Visited pairs = 20
-> [  0.000000] (0:@) Executed transitions = 20
-> [  0.000000] (0:@) Counter-example depth : 21
+> [  0.000000] (0:@) [(1)Tremblay (coordinator)] iSend(src=(1)Tremblay (coordinator), buff=(verbose only), size=(verbose only))
+> [  0.000000] (0:@) Expanded pairs = 23
+> [  0.000000] (0:@) Visited pairs = 21
+> [  0.000000] (0:@) Executed transitions = 21
+> [  0.000000] (0:@) Counter-example depth : 22
diff --git a/examples/msg/mc/bugged1_liveness_visited.tesh b/examples/msg/mc/bugged1_liveness_visited.tesh
index 859e793af3..daaa02eff4 100644
--- 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:=.}/../../../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
+$ ${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/property:promela_bugged1_liveness
 > [  0.000000] (0:@) Check the liveness property promela_bugged1_liveness
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (3:client@Fafard) Ask the request
@@ -128,4 +128,3 @@ $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${srcdir:=.
 > [  0.000000] (0:@) Visited pairs = 201
 > [  0.000000] (0:@) Executed transitions = 207
 > [  0.000000] (0:@) Counter-example depth : 51
-
diff --git a/examples/msg/mc/bugged1_liveness_visited_sparse.tesh b/examples/msg/mc/bugged1_liveness_visited_sparse.tesh
index 1750e8b638..77e64a4128 100644
--- 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:=.}/../../../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
+$ ${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  --cfg=model-check/property:promela_bugged1_liveness
 > [  0.000000] (0:@) Check the liveness property promela_bugged1_liveness
 > [  0.000000] (2:client@Boivin) Ask the request
 > [  0.000000] (3:client@Fafard) Ask the request
diff --git a/examples/msg/mc/bugged2_liveness.c b/examples/msg/mc/bugged2_liveness.c
index 25e2dedd2e..ee5519f272 100644
--- a/examples/msg/mc/bugged2_liveness.c
+++ b/examples/msg/mc/bugged2_liveness.c
@@ -97,7 +97,6 @@ int main(int argc, char *argv[])
   
   MSG_init(&argc, argv);
 
-  MSG_config("model-check/property","promela_bugged2_liveness");
   MC_automaton_new_propositional_symbol_pointer("cs", &cs);
   
   MSG_create_environment("../msg_platform.xml");
diff --git a/include/xbt/ex.h b/include/xbt/ex.h
index a72f16b120..ab26a72a12 100644
--- a/include/xbt/ex.h
+++ b/include/xbt/ex.h
@@ -323,9 +323,8 @@ XBT_PUBLIC( void )__xbt_ex_terminate_default(xbt_ex_t * e);
     { \
         xbt_running_ctx_t *__xbt_ex_ctx_ptr = __xbt_running_ctx_fetch(); \
         int __ex_cleanup = 0; \
-        __ex_mctx_t *__ex_mctx_en; \
         __ex_mctx_t __ex_mctx_me; \
-        __ex_mctx_en = __xbt_ex_ctx_ptr->ctx_mctx; \
+        __ex_mctx_t * __ex_mctx_en = __xbt_ex_ctx_ptr->ctx_mctx; \
         __xbt_ex_ctx_ptr->ctx_mctx = &__ex_mctx_me; \
         if (__ex_mctx_save(&__ex_mctx_me)) { \
             if (1)
diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 53235a47d7..690ca5af4e 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -21,6 +21,7 @@
 #include "xbt/fifo.h"
 #include "xbt/automaton.h"
 #include "xbt/dict.h"
+#include "mc_server.h"
 
 #ifdef HAVE_MC
 #include <libunwind.h>
@@ -151,7 +152,7 @@ void MC_init_pid(pid_t pid, int socket)
 
   MC_SET_STD_HEAP;
 
-  if (_sg_mc_visited > 0 || _sg_mc_liveness  || _sg_mc_termination) {
+  if (_sg_mc_visited > 0 || _sg_mc_liveness  || _sg_mc_termination || mc_mode == MC_MODE_SERVER) {
     /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
     MC_ignore_local_variable("e", "*");
     MC_ignore_local_variable("__ex_cleanup", "*");
@@ -243,44 +244,19 @@ static void MC_modelcheck_comm_determinism_init(void)
   mmalloc_set_current_heap(heap);
 }
 
-static void MC_modelcheck_liveness_init()
-{
-  _sg_mc_liveness = 1;
-
-  MC_init();
-  if (mc_mode == MC_MODE_CLIENT) {
-    // This will move somehwere else:
-    MC_client_handle_messages();
-  }
-
-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
-  /* Create exploration stack */
-  mc_stack = xbt_fifo_new();
-
-  /* Create the initial state */
-  initial_global_state = xbt_new0(s_mc_global_t, 1);
-
-  MC_SET_STD_HEAP;
-
-  MC_pre_modelcheck_liveness();
-
-  /* We're done */
-  MC_print_statistics(mc_stats);
-  xbt_free(mc_time);
-
-  mmalloc_set_current_heap(heap);
-
-}
-
 void MC_do_the_modelcheck_for_real()
 {
   MC_init_mode();
 
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
-    XBT_INFO("Check communication determinism");
-    mc_reduce_kind = e_mc_reduce_none;
-    MC_modelcheck_comm_determinism_init();
+    // TODO, move this part in the MCer process
+    if (mc_mode == MC_MODE_SERVER)
+      MC_server_loop(mc_server);
+    else {
+      XBT_INFO("Check communication determinism");
+      mc_reduce_kind = e_mc_reduce_none;
+      MC_modelcheck_comm_determinism_init();
+    }
   }
 
   else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
@@ -308,9 +284,14 @@ void MC_do_the_modelcheck_for_real()
   else {
     if (mc_reduce_kind == e_mc_reduce_unset)
       mc_reduce_kind = e_mc_reduce_none;
-    XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
-    MC_automaton_load(_sg_mc_property_file);
-    MC_modelcheck_liveness_init();
+    if (mc_mode == MC_MODE_SERVER || mc_mode == MC_MODE_STANDALONE) {
+      XBT_INFO("Check the liveness property %s", _sg_mc_property_file);
+      MC_automaton_load(_sg_mc_property_file);
+      MC_modelcheck_liveness();
+    } else {
+      MC_init();
+      MC_client_main_loop();
+    }
   }
 }
 
diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index c648c6739e..8be4044836 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -15,6 +15,7 @@
 #include "mc_private.h"
 #include "mc_record.h"
 #include "mc_smx.h"
+#include "mc_client.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
@@ -171,13 +172,17 @@ static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l,
   }
 }
 
-void MC_pre_modelcheck_liveness(void) {
+static void MC_modelcheck_liveness_main(void);
 
+static void MC_pre_modelcheck_liveness(void)
+{
   initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 
   mc_pair_t initial_pair = NULL;
   smx_process_t process;
 
+  // TODO, fix this
+  MC_wait_for_requests();
   MC_wait_for_requests();
 
   MC_SET_MC_HEAP;
@@ -217,13 +222,13 @@ void MC_pre_modelcheck_liveness(void) {
 
   MC_SET_STD_HEAP;
   
-  MC_modelcheck_liveness();
+  MC_modelcheck_liveness_main();
 
   if (initial_global_state->raw_mem_set)
     MC_SET_MC_HEAP;
 }
 
-void MC_modelcheck_liveness()
+static void MC_modelcheck_liveness_main(void)
 {
   smx_process_t process = NULL;
   mc_pair_t current_pair = NULL;
@@ -243,9 +248,10 @@ void MC_modelcheck_liveness()
     /* Update current state in buchi automaton */
     _mc_property_automaton->current_state = current_pair->automaton_state;
 
-    XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size %d, pair_num %d)",
+    XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d, interleave size = %d, pair_num = %d, requests = %d)",
        current_pair->depth, current_pair->search_cycle,
-       MC_state_interleave_size(current_pair->graph_state), current_pair->num);
+       MC_state_interleave_size(current_pair->graph_state), current_pair->num,
+       current_pair->requests);
 
     if (current_pair->requests > 0) {
 
@@ -396,3 +402,29 @@ void MC_modelcheck_liveness()
   } /* End of while(xbt_fifo_size(mc_stack) > 0) */
   
 }
+
+void MC_modelcheck_liveness(void)
+{
+  XBT_DEBUG("Starting the liveness algorithm");
+  xbt_assert(mc_mode == MC_MODE_SERVER);
+  _sg_mc_liveness = 1;
+
+  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
+
+  /* Create exploration stack */
+  mc_stack = xbt_fifo_new();
+
+  /* Create the initial state */
+  initial_global_state = xbt_new0(s_mc_global_t, 1);
+
+  MC_SET_STD_HEAP;
+
+  MC_pre_modelcheck_liveness();
+
+  /* We're done */
+  MC_print_statistics(mc_stats);
+  xbt_free(mc_time);
+
+  mmalloc_set_current_heap(heap);
+
+}
diff --git a/src/mc/mc_liveness.h b/src/mc/mc_liveness.h
index e0f102f458..fa5a246b1e 100644
--- a/src/mc/mc_liveness.h
+++ b/src/mc/mc_liveness.h
@@ -50,7 +50,6 @@ void mc_pair_free_voidp(void *p);
 mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state);
 void MC_visited_pair_delete(mc_visited_pair_t p);
 
-void MC_pre_modelcheck_liveness(void);
 void MC_modelcheck_liveness(void);
 void MC_show_stack_liveness(xbt_fifo_t stack);
 void MC_dump_stack_liveness(xbt_fifo_t stack);
diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp
index 869dd75818..4b8da8b53a 100644
--- a/src/mc/mc_server.cpp
+++ b/src/mc/mc_server.cpp
@@ -355,3 +355,8 @@ void MC_server_simcall_handle(mc_process_t process, unsigned long pid, int value
       return;
   }
 }
+
+void MC_server_loop(mc_server_t server)
+{
+  server->loop();
+}
diff --git a/src/mc/mc_server.h b/src/mc/mc_server.h
index b6677d98da..860cfac3f9 100644
--- a/src/mc/mc_server.h
+++ b/src/mc/mc_server.h
@@ -28,6 +28,8 @@ extern mc_server_t mc_server;
 void MC_server_wait_client(mc_process_t process);
 void MC_server_simcall_handle(mc_process_t process, unsigned long pid, int value);
 
+void MC_server_loop(mc_server_t server);
+
 SG_END_DECL()
 
 #ifdef __cplusplus
diff --git a/src/mc/mc_visited.c b/src/mc/mc_visited.c
index cf37ea6ef3..c644abf4b4 100644
--- a/src/mc/mc_visited.c
+++ b/src/mc/mc_visited.c
@@ -54,8 +54,7 @@ void visited_state_free_voidp(void *s)
 static mc_visited_state_t visited_state_new()
 {
   mc_process_t process = &(mc_model_checker->process);
-  mc_visited_state_t new_state = NULL;
-  new_state = xbt_new0(s_mc_visited_state_t, 1);
+  mc_visited_state_t new_state = xbt_new0(s_mc_visited_state_t, 1);
   new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
     MC_process_get_heap(process)->heaplimit,
     MC_process_get_malloc_info(process));
diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp
index b70091d5f7..0c8899bbee 100644
--- a/src/mc/simgrid_mc.cpp
+++ b/src/mc/simgrid_mc.cpp
@@ -77,21 +77,7 @@ static int do_parent(int socket, pid_t child)
     mc_server = new s_mc_server(child, socket);
     mc_server->start();
     MC_init_pid(child, socket);
-
-    if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
-      mc_server->loop();
-    }
-
-    else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') {
-      if (mc_reduce_kind == e_mc_reduce_unset)
-        mc_reduce_kind = e_mc_reduce_dpor;
-      MC_do_the_modelcheck_for_real();
-    }
-
-    else {
-      mc_server->loop();
-    }
-
+    MC_do_the_modelcheck_for_real();
     mc_server->shutdown();
     mc_server->exit();
   }
diff --git a/src/msg/msg_mailbox.c b/src/msg/msg_mailbox.c
index 53f99df9df..d7ae79962d 100644
--- a/src/msg/msg_mailbox.c
+++ b/src/msg/msg_mailbox.c
@@ -167,7 +167,6 @@ msg_error_t
 MSG_mailbox_put_with_timeout(msg_mailbox_t mailbox, msg_task_t task,
                              double timeout)
 {
-  xbt_ex_t e;
   msg_error_t ret = MSG_OK;
   simdata_task_t t_simdata = NULL;
   msg_process_t process = MSG_process_self();
@@ -204,6 +203,7 @@ MSG_mailbox_put_with_timeout(msg_mailbox_t mailbox, msg_task_t task,
 
   p_simdata->waiting_task = task;
 
+  xbt_ex_t e;
   /* Try to send it by calling SIMIX network layer */
   TRY {
     smx_synchro_t comm = NULL; /* MC needs the comm to be set to NULL during the simix call  */
-- 
2.20.1