Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
merge conflicts
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Tue, 22 Nov 2011 17:05:23 +0000 (18:05 +0100)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Tue, 22 Nov 2011 17:05:23 +0000 (18:05 +0100)
1  2 
buildtools/Cmake/DefinePackages.cmake
include/msg/msg.h
src/mc/mc_global.c
src/mc/memory_map.c
src/msg/msg_global.c
src/simix/smx_smurf.c
src/xbt/dynar.c
src/xbt/mmalloc/mm_legacy.c

@@@ -17,7 -17,6 +17,7 @@@ set(EXTRA_DIS
        src/xbt/backtrace_dummy.c
        src/xbt/setset_private.h
        src/xbt/parmap_private.h
 +      src/xbt/automatonparse_promela.c
        src/xbt/mmalloc/attach.c
        src/xbt/mmalloc/detach.c        
        src/xbt/mmalloc/keys.c
        src/surf/gtnets/gtnets_topology.h
        src/surf/cpu_ti_private.h
        src/surf/surf_routing_private.h
+       src/include/simgrid/platf_interface.h
        src/include/surf/surf_resource.h
        src/include/surf/datatypes.h
        src/include/surf/maxmin.h
        src/include/surf/trace_mgr.h
        src/include/surf/surf.h
-       src/include/surf/surfxml_parse_private.h
+       src/include/surf/surfxml_parse_values.h
        src/include/surf/random_mgr.h
        src/include/surf/surf_resource_lmm.h
        src/include/xbt/wine_dbghelp.h
@@@ -63,8 -63,8 +64,8 @@@
        src/include/mc/datatypes.h
        src/include/mc/mc.h
        src/include/simix/context.h
-       src/msg/private.h
-       src/msg/mailbox.h
+       src/msg/msg_private.h
+       src/msg/msg_mailbox.h
        src/simdag/private.h
        src/simdag/dax.dtd
        src/simdag/dax_dtd.h
@@@ -88,6 -88,7 +89,7 @@@
        src/smpi/private.h
        src/smpi/smpi_mpi_dt_private.h
        src/smpi/README
+       src/mk_supernovae.pl
        
        examples/gras/ping/ping.h
        examples/gras/console/ping.h
@@@ -179,7 -180,6 +181,7 @@@ set(XBT_SR
        src/xbt/parmap.c
        src/xbt/xbt_replay_trace_reader.c
        src/xbt/lib.c
 +      src/xbt/automaton.c
  )
  
  if(HAVE_MMAP)
@@@ -208,11 -208,14 +210,14 @@@ set(SURF_SR
        src/surf/surf_model.c
        src/surf/surf_action.c
        src/surf/surf_routing.c
+       src/surf/surf_routing_none.c
+       src/surf/surf_routing_generic.c
        src/surf/surf_routing_full.c
        src/surf/surf_routing_floyd.c
        src/surf/surf_routing_rulebased.c
        src/surf/surf_routing_dijkstra.c
-       src/surf/surf_routing_none.c
+       src/surf/surf_routing_cluster.c
+       src/surf/surf_routing_vivaldi.c
        src/surf/surf_config.c
        src/surf/maxmin.c
        src/surf/fair_bottleneck.c
        src/surf/random_mgr.c
        src/surf/surf.c
        src/surf/surfxml_parse.c
+       src/surf/surfxml_parseplatf.c
        src/surf/cpu.c
        src/surf/network.c
        src/surf/network_im.c
        src/surf/workstation_ptask_L07.c
        src/surf/cpu_ti.c
        src/surf/cpu_im.c
+       src/surf/sg_platf.c
        src/xbt/xbt_sg_stubs.c
  )
  
@@@ -249,13 -254,13 +256,13 @@@ set(SIMIX_SR
  
  set(MSG_SRC
        src/msg/msg_config.c
-       src/msg/task.c
-       src/msg/host.c
-       src/msg/m_process.c
-       src/msg/gos.c
-       src/msg/global.c
-       src/msg/environment.c
-       src/msg/deployment.c
+       src/msg/msg_task.c
+       src/msg/msg_host.c
+       src/msg/msg_process.c
+       src/msg/msg_gos.c
+       src/msg/msg_global.c
+       src/msg/msg_environment.c
+       src/msg/msg_deployment.c
        src/msg/msg_mailbox.c
        src/msg/msg_actions.c
  )
@@@ -363,7 -368,6 +370,7 @@@ set(MC_SR
        src/mc/mc_dpor.c
        src/mc/mc_request.c
        src/mc/private.h
 +      src/mc/mc_liveness.c
  )
  
  set(RNGSTREAM_SRC
@@@ -406,8 -410,7 +413,9 @@@ set(headers_to_instal
        include/xbt/mmalloc.h
        include/xbt/replay_trace_reader.h
        include/xbt/parmap.h
 +      include/xbt/automaton.h
 +      include/xbt/automatonparse_promela.h
+       include/simgrid/platf.h
        include/mc/modelchecker.h
        include/msg/msg.h
        include/msg/datatypes.h
diff --combined include/msg/msg.h
@@@ -10,8 -10,6 +10,8 @@@
  #include "xbt.h"
  
  #include "msg/datatypes.h"
 +#include "xbt/automaton.h"
 +
  SG_BEGIN_DECL()
  
  
@@@ -22,9 -20,6 +22,9 @@@ XBT_PUBLIC(void) MSG_global_init_args(i
  XBT_PUBLIC(MSG_error_t) MSG_set_channel_number(int number);
  XBT_PUBLIC(int) MSG_get_channel_number(void);
  XBT_PUBLIC(MSG_error_t) MSG_main(void);
 +XBT_PUBLIC(MSG_error_t) MSG_main_stateful(void);
 +XBT_PUBLIC(MSG_error_t) MSG_main_liveness_stateful(xbt_automaton_t a);
 +XBT_PUBLIC(MSG_error_t) MSG_main_liveness_stateless(xbt_automaton_t a, char *prgm);
  XBT_PUBLIC(MSG_error_t) MSG_clean(void);
  XBT_PUBLIC(void) MSG_function_register(const char *name,
                                         xbt_main_func_t code);
@@@ -161,7 -156,6 +161,6 @@@ XBT_PUBLIC(int) MSG_task_Iprobe(m_chann
  XBT_PUBLIC(int) MSG_task_probe_from(m_channel_t channel);
  XBT_PUBLIC(int) MSG_task_probe_from_host(int channel, m_host_t host);
  XBT_PUBLIC(MSG_error_t) MSG_process_sleep(double nb_sec);
- XBT_PUBLIC(MSG_error_t) MSG_get_errno(void);
  
  XBT_PUBLIC(double) MSG_task_get_compute_duration(m_task_t task);
  XBT_PUBLIC(void) MSG_task_set_compute_duration(m_task_t task,
@@@ -182,6 -176,7 +181,7 @@@ XBT_PUBLIC(MSG_error_t
  
  XBT_PUBLIC(MSG_error_t)
      MSG_task_receive(m_task_t * task, const char *alias);
+ #define MSG_task_recv(t,a) MSG_task_receive(t,a)
  
  XBT_PUBLIC(msg_comm_t) MSG_task_isend(m_task_t task, const char *alias);
  XBT_INLINE XBT_PUBLIC(msg_comm_t) MSG_task_isend_with_matching(m_task_t task, const char *alias,
@@@ -236,10 -231,12 +236,12 @@@ MSG_error_t MSG_action_trace_run(char *
  #ifdef MSG_USE_DEPRECATED
  /* these are the functions which are deprecated. Do not use them, they may get removed in future releases */
  #define MSG_TIMEOUT_FAILURE MSG_TIMEOUT
+ #define MSG_TASK_CANCELLED MSG_TASK_CANCELED
  #define MSG_mailbox_put_with_time_out(mailbox, task, timeout) \
          MSG_mailbox_put_with_timeout(mailbox, task, timeout)
  
  #define MSG_process_change_host(h) MSG_process_migrate(MSG_process_self(),h);
+ XBT_PUBLIC(MSG_error_t) MSG_get_errno(void);
  #endif
  
  #include "instr/instr.h"
diff --combined src/mc/mc_global.c
@@@ -1,7 -1,6 +1,7 @@@
  #include <unistd.h>
  #include <sys/types.h>
  #include <sys/wait.h>
 +#include <sys/time.h>
  
  #include "../surf/surf_private.h"
  #include "../simix/private.h"
@@@ -13,32 -12,17 +13,32 @@@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_glob
                                  "Logging specific to MC (global)");
  
  /* MC global data structures */
 -mc_snapshot_t initial_snapshot = NULL;
 -xbt_fifo_t mc_stack = NULL;
 -mc_stats_t mc_stats = NULL;
 +
  mc_state_t mc_current_state = NULL;
  char mc_replay_mode = FALSE;
  double *mc_time = NULL;
 +mc_snapshot_t initial_snapshot = NULL;
 +
 +/* Safety */
 +
 +xbt_fifo_t mc_stack_safety_stateful = NULL;
 +xbt_fifo_t mc_stack_safety_stateless = NULL;
 +mc_stats_t mc_stats = NULL;
 +
 +/* Liveness */
 +
 +xbt_fifo_t mc_stack_liveness_stateful = NULL;
 +mc_stats_pair_t mc_stats_pair = NULL;
 +xbt_fifo_t mc_stack_liveness_stateless = NULL;
 +mc_snapshot_t initial_snapshot_liveness = NULL;
 +
 +
  /**
   *  \brief Initialize the model-checker data structures
   */
 -void MC_init(void)
 +void MC_init_safety_stateless(void)
  {
 +
    /* Check if MC is already initialized */
    if (initial_snapshot)
      return;
@@@ -54,7 -38,7 +54,7 @@@
    mc_stats->state_size = 1;
  
    /* Create exploration stack */
 -  mc_stack = xbt_fifo_new();
 +  mc_stack_safety_stateless = xbt_fifo_new();
  
    MC_UNSET_RAW_MEM;
  
    MC_UNSET_RAW_MEM;
  }
  
 +void MC_init_safety_stateful(void){
 +
 +  
 +   /* Check if MC is already initialized */
 +  if (initial_snapshot)
 +    return;
 +
 +  mc_time = xbt_new0(double, simix_process_maxpid);
 +
 +  /* Initialize the data structures that must be persistent across every
 +     iteration of the model-checker (in RAW memory) */
 +  MC_SET_RAW_MEM;
 +
 +  /* Initialize statistics */
 +  mc_stats = xbt_new0(s_mc_stats_t, 1);
 +  mc_stats->state_size = 1;
 +
 +  /* Create exploration stack */
 +  mc_stack_safety_stateful = xbt_fifo_new();
 +
 +  MC_UNSET_RAW_MEM;
 +
 +  MC_dpor_stateful_init();
 +
 +
 +}
 +
 +void MC_init_liveness_stateful(xbt_automaton_t a){
 +
 +  XBT_DEBUG("Start init mc");
 +  
 +  mc_time = xbt_new0(double, simix_process_maxpid);
 +
 +  /* Initialize the data structures that must be persistent across every
 +     iteration of the model-checker (in RAW memory) */
 +
 +  MC_SET_RAW_MEM;
 +
 +  /* Initialize statistics */
 +  mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
 +  //mc_stats = xbt_new0(s_mc_stats_t, 1);
 +
 +  XBT_DEBUG("Creating snapshot_stack");
 +
 + /* Create exploration stack */
 +  mc_stack_liveness_stateful = xbt_fifo_new();
 +
 +
 +  MC_UNSET_RAW_MEM;
 +
 +  //MC_ddfs_stateful_init(a);
 +  //MC_dpor2_init(a);
 +  //MC_dpor3_init(a);
 +}
 +
 +void MC_init_liveness_stateless(xbt_automaton_t a, char *prgm){
 +
 +  XBT_DEBUG("Start init mc");
 +  
 +  mc_time = xbt_new0(double, simix_process_maxpid);
 +
 +  /* Initialize the data structures that must be persistent across every
 +     iteration of the model-checker (in RAW memory) */
 +
 +  MC_SET_RAW_MEM;
 +
 +  /* Initialize statistics */
 +  mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
 +
 +  XBT_DEBUG("Creating stack");
 +
 + /* Create exploration stack */
 +  mc_stack_liveness_stateless = xbt_fifo_new();
 +
 +  MC_UNSET_RAW_MEM;
 +
 +  MC_ddfs_stateless_init(a, prgm);
 +
 +  
 +}
 +
 +
  void MC_modelcheck(void)
  {
 -  MC_init();
 +  MC_init_safety_stateless();
    MC_dpor();
    MC_exit();
  }
  
 +void MC_modelcheck_stateful(void)
 +{
 +  MC_init_safety_stateful();
 +  MC_dpor_stateful();
 +  MC_exit();
 +}
 +
 +void MC_modelcheck_liveness_stateful(xbt_automaton_t a){
 +  MC_init_liveness_stateful(a);
 +  MC_exit_liveness();
 +}
 +
 +void MC_modelcheck_liveness_stateless(xbt_automaton_t a, char *prgm){
 +  MC_init_liveness_stateless(a, prgm);
 +  MC_exit_liveness();
 +}
 +
 +void MC_exit_liveness(void)
 +{
 +  MC_print_statistics_pairs(mc_stats_pair);
 +  //xbt_free(mc_time);
 +  //MC_memory_exit();
 +  exit(0);
 +}
 +
 +
  void MC_exit(void)
  {
    MC_print_statistics(mc_stats);
    MC_memory_exit();
  }
  
 +
  int MC_random(int min, int max)
  {
    /*FIXME: return mc_current_state->executed_transition->random.value;*/
@@@ -205,7 -80,7 +205,7 @@@ void MC_wait_for_requests(void
    smx_req_t req;
    unsigned int iter;
  
-   while (xbt_dynar_length(simix_global->process_to_run)) {
+   while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
      SIMIX_process_runall();
      xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
        req = &process->request;
@@@ -284,120 -159,16 +284,120 @@@ void MC_replay(xbt_fifo_t stack
    XBT_DEBUG("**** End Replay ****");
  }
  
 +void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
 +{
 +  int value;
 +  char *req_str;
 +  smx_req_t req = NULL, saved_req = NULL;
 +  xbt_fifo_item_t item;
 +  mc_state_t state;
 +  mc_pair_stateless_t pair;
 +  int depth = 1;
 +
 +  XBT_DEBUG("**** Begin Replay ****");
 +
 +  /* Restore the initial state */
 +  MC_restore_snapshot(initial_snapshot_liveness);
 +  /* At the moment of taking the snapshot the raw heap was set, so restoring
 +   * it will set it back again, we have to unset it to continue  */
 +  MC_UNSET_RAW_MEM;
 +
 +  if(all_stack){
 +
 +    item = xbt_fifo_get_last_item(stack);
 +
 +    while(depth <= xbt_fifo_size(stack)){
 +
 +      pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
 +      state = (mc_state_t) pair->graph_state;
 +
 +      if(pair->requests > 0){
 +   
 +      saved_req = MC_state_get_executed_request(state, &value);
 +      //XBT_DEBUG("SavedReq->call %u", saved_req->call);
 +      
 +      if(saved_req != NULL){
 +        /* because we got a copy of the executed request, we have to fetch the  
 +           real one, pointed by the request field of the issuer process */
 +        req = &saved_req->issuer->request;
 +        //XBT_DEBUG("Req->call %u", req->call);
 +      
 +        /* Debug information */
 +        if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
 +          req_str = MC_request_to_string(req, value);
 +          XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
 +          xbt_free(req_str);
 +        }
 +      
 +      }
 + 
 +      SIMIX_request_pre(req, value);
 +      MC_wait_for_requests();
 +      }
 +
 +      depth++;
 +    
 +      /* Update statistics */
 +      mc_stats_pair->visited_pairs++;
 +
 +      item = xbt_fifo_get_prev_item(item);
 +    }
 +
 +  }else{
 +
 +    /* Traverse the stack from the initial state and re-execute the transitions */
 +    for (item = xbt_fifo_get_last_item(stack);
 +       item != xbt_fifo_get_first_item(stack);
 +       item = xbt_fifo_get_prev_item(item)) {
 +
 +      pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
 +      state = (mc_state_t) pair->graph_state;
 +
 +      if(pair->requests > 0){
 +   
 +      saved_req = MC_state_get_executed_request(state, &value);
 +      //XBT_DEBUG("SavedReq->call %u", saved_req->call);
 +      
 +      if(saved_req != NULL){
 +        /* because we got a copy of the executed request, we have to fetch the  
 +           real one, pointed by the request field of the issuer process */
 +        req = &saved_req->issuer->request;
 +        //XBT_DEBUG("Req->call %u", req->call);
 +      
 +        /* Debug information */
 +        if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
 +          req_str = MC_request_to_string(req, value);
 +          XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
 +          xbt_free(req_str);
 +        }
 +      
 +      }
 + 
 +      SIMIX_request_pre(req, value);
 +      MC_wait_for_requests();
 +      }
 +
 +      depth++;
 +    
 +      /* Update statistics */
 +      mc_stats_pair->visited_pairs++;
 +    }
 +  }  
 +
 +  XBT_DEBUG("**** End Replay ****");
 +}
 +
 +
  /**
   * \brief Dumps the contents of a model-checker's stack and shows the actual
   *        execution trace
   * \param stack The stack to dump
  */
 -void MC_dump_stack(xbt_fifo_t stack)
 +void MC_dump_stack_safety_stateless(xbt_fifo_t stack)
  {
    mc_state_t state;
  
 -  MC_show_stack(stack);
 +  MC_show_stack_safety_stateless(stack);
  
    MC_SET_RAW_MEM;
    while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
    MC_UNSET_RAW_MEM;
  }
  
 -void MC_show_stack(xbt_fifo_t stack)
 +
 +void MC_show_stack_safety_stateless(xbt_fifo_t stack)
  {
    int value;
    mc_state_t state;
@@@ -437,117 -207,9 +437,117 @@@ void MC_show_deadlock(smx_req_t req
    XBT_INFO("%s", req_str);
    xbt_free(req_str);*/
    XBT_INFO("Counter-example execution trace:");
 -  MC_dump_stack(mc_stack);
 +  MC_dump_stack_safety_stateless(mc_stack_safety_stateless);
 +}
 +
 +void MC_show_deadlock_stateful(smx_req_t req)
 +{
 +  /*char *req_str = NULL;*/
 +  XBT_INFO("**************************");
 +  XBT_INFO("*** DEAD-LOCK DETECTED ***");
 +  XBT_INFO("**************************");
 +  XBT_INFO("Locked request:");
 +  /*req_str = MC_request_to_string(req);
 +  XBT_INFO("%s", req_str);
 +  xbt_free(req_str);*/
 +  XBT_INFO("Counter-example execution trace:");
 +  MC_show_stack_safety_stateful(mc_stack_safety_stateful);
 +}
 +
 +void MC_dump_stack_safety_stateful(xbt_fifo_t stack)
 +{
 +  //mc_state_ws_t state;
 +
 +  MC_show_stack_safety_stateful(stack);
 +
 +  /*MC_SET_RAW_MEM;
 +  while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
 +    MC_state_delete(state);
 +    MC_UNSET_RAW_MEM;*/
 +}
 +
 +
 +void MC_show_stack_safety_stateful(xbt_fifo_t stack)
 +{
 +  int value;
 +  mc_state_ws_t state;
 +  xbt_fifo_item_t item;
 +  smx_req_t req;
 +  char *req_str = NULL;
 +  
 +  for (item = xbt_fifo_get_last_item(stack);
 +       (item ? (state = (mc_state_ws_t) (xbt_fifo_get_item_content(item)))
 +        : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 +    req = MC_state_get_executed_request(state->graph_state, &value);
 +    if(req){
 +      req_str = MC_request_to_string(req, value);
 +      XBT_INFO("%s", req_str);
 +      xbt_free(req_str);
 +    }
 +  }
 +}
 +
 +void MC_show_stack_liveness_stateful(xbt_fifo_t stack){
 +  int value;
 +  mc_pair_t pair;
 +  xbt_fifo_item_t item;
 +  smx_req_t req;
 +  char *req_str = NULL;
 +  
 +  for (item = xbt_fifo_get_last_item(stack);
 +       (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
 +        : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 +    req = MC_state_get_executed_request(pair->graph_state, &value);
 +    if(req){
 +      req_str = MC_request_to_string(req, value);
 +      XBT_INFO("%s", req_str);
 +      xbt_free(req_str);
 +    }
 +  }
  }
  
 +void MC_dump_stack_liveness_stateful(xbt_fifo_t stack){
 +  mc_pair_t pair;
 +
 +  MC_SET_RAW_MEM;
 +  while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
 +    MC_pair_delete(pair);
 +  MC_UNSET_RAW_MEM;
 +}
 +
 +void MC_show_stack_liveness_stateless(xbt_fifo_t stack){
 +  int value;
 +  mc_pair_stateless_t pair;
 +  xbt_fifo_item_t item;
 +  smx_req_t req;
 +  char *req_str = NULL;
 +  
 +  for (item = xbt_fifo_get_last_item(stack);
 +       (item ? (pair = (mc_pair_stateless_t) (xbt_fifo_get_item_content(item)))
 +        : (NULL)); item = xbt_fifo_get_prev_item(item)) {
 +    req = MC_state_get_executed_request(pair->graph_state, &value);
 +    if(req){
 +      if(pair->requests>0){
 +      req_str = MC_request_to_string(req, value);
 +      XBT_INFO("%s", req_str);
 +      xbt_free(req_str);
 +      }else{
 +      XBT_INFO("End of system requests but evolution in B├╝chi automaton");
 +      }
 +    }
 +  }
 +}
 +
 +void MC_dump_stack_liveness_stateless(xbt_fifo_t stack){
 +  mc_pair_stateless_t pair;
 +
 +  MC_SET_RAW_MEM;
 +  while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL)
 +    MC_pair_stateless_delete(pair);
 +  MC_UNSET_RAW_MEM;
 +}
 +
 +
  void MC_print_statistics(mc_stats_t stats)
  {
    XBT_INFO("State space size ~= %lu", stats->state_size);
       (double)stats->expanded_states / stats->state_size); */
  }
  
 +void MC_print_statistics_pairs(mc_stats_pair_t stats)
 +{
 +  XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
 +  XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
 +  //XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
 +  XBT_INFO("Expanded / Visited = %lf",
 +        (double) stats->visited_pairs / stats->expanded_pairs);
 +  /*XBT_INFO("Exploration coverage = %lf",
 +     (double)stats->expanded_states / stats->state_size); */
 +}
 +
  void MC_assert(int prop)
  {
    if (MC_IS_ENABLED && !prop) {
      XBT_INFO("*** PROPERTY NOT VALID ***");
      XBT_INFO("**************************");
      XBT_INFO("Counter-example execution trace:");
 -    MC_dump_stack(mc_stack);
 +    MC_dump_stack_safety_stateless(mc_stack_safety_stateless);
 +    MC_print_statistics(mc_stats);
 +    xbt_abort();
 +  }
 +}
 +
 +void MC_assert_stateful(int prop)
 +{
 +  if (MC_IS_ENABLED && !prop) {
 +    XBT_INFO("**************************");
 +    XBT_INFO("*** PROPERTY NOT VALID ***");
 +    XBT_INFO("**************************");
 +    XBT_INFO("Counter-example execution trace:");
 +    MC_dump_stack_safety_stateful(mc_stack_safety_stateful);
      MC_print_statistics(mc_stats);
      xbt_abort();
    }
  }
  
 +void MC_assert_pair_stateful(int prop){
 +  if (MC_IS_ENABLED && !prop) {
 +    XBT_INFO("**************************");
 +    XBT_INFO("*** PROPERTY NOT VALID ***");
 +    XBT_INFO("**************************");
 +    //XBT_INFO("Counter-example execution trace:");
 +    MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
 +    //MC_dump_snapshot_stack(mc_snapshot_stack);
 +    MC_print_statistics_pairs(mc_stats_pair);
 +    xbt_abort();
 +  }
 +}
 +
 +void MC_assert_pair_stateless(int prop){
 +  if (MC_IS_ENABLED && !prop) {
 +    XBT_INFO("**************************");
 +    XBT_INFO("*** PROPERTY NOT VALID ***");
 +    XBT_INFO("**************************");
 +    //XBT_INFO("Counter-example execution trace:");
 +    MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
 +    //MC_dump_snapshot_stack(mc_snapshot_stack);
 +    MC_print_statistics_pairs(mc_stats_pair);
 +    xbt_abort();
 +  }
 +}
 +
  void MC_process_clock_add(smx_process_t process, double amount)
  {
    mc_time[process->pid] += amount;
diff --combined src/mc/memory_map.c
@@@ -2,9 -2,6 +2,9 @@@
  #include "private.h"
  #include <stdlib.h>
  
 +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_memory_map, mc,
 +                                "Logging specific to algorithms for memory_map");
 +
  memory_map_t get_memory_map(void)
  {
    FILE *fp;                     /* File pointer to process's proc maps file */
    xbt_assert(fp,
                "Cannot open /proc/self/maps to investigate the memory map of the process. Please report this bug.");
  
 +  //XBT_DEBUG("/proc/self/maps");
 +
    ret = xbt_new0(s_memory_map_t, 1);
  
    /* Read one line at the time, parse it and add it to the memory map to be returned */
    while ((read = getline(&line, &n, fp)) != -1) {
  
 +    XBT_DEBUG("%s", line);
 +
      /* Wipeout the new line character */
      line[read - 1] = '\0';
  
          xbt_realloc(ret->regions, sizeof(memreg) * (ret->mapsize + 1));
      memcpy(ret->regions + ret->mapsize, &memreg, sizeof(memreg));
      ret->mapsize++;
 +
    }
  
-   if (line)
-     free(line);
+   free(line);
  
    return ret;
  }
diff --combined src/msg/msg_global.c
@@@ -4,13 -4,13 +4,13 @@@
  /* 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 "msg/private.h"
+ #include "msg_private.h"
+ #include "msg_mailbox.h"
  #include "mc/mc.h"
  #include "xbt/sysdep.h"
  #include "xbt/log.h"
  #include "xbt/virtu.h"
  #include "xbt/ex.h"             /* ex_backtrace_display */
- #include "mailbox.h"
  
  XBT_LOG_NEW_DEFAULT_SUBCATEGORY(msg_kernel, msg,
                                  "Logging specific to MSG (kernel)");
@@@ -153,51 -153,6 +153,51 @@@ MSG_error_t MSG_main(void
    return MSG_OK;
  }
  
 +MSG_error_t MSG_main_stateful(void)
 +{
 +  /* Clean IO before the run */
 +  fflush(stdout);
 +  fflush(stderr);
 +
 +  if (MC_IS_ENABLED) {
 +    MC_modelcheck_stateful();
 +  }
 +  else {
 +    SIMIX_run();
 +  }
 +  return MSG_OK;
 +}
 +
 +MSG_error_t MSG_main_liveness_stateful(xbt_automaton_t a)
 +{
 +  /* Clean IO before the run */
 +  fflush(stdout);
 +  fflush(stderr);
 +
 +  if (MC_IS_ENABLED) {
 +    MC_modelcheck_liveness_stateful(a);
 +  }
 +  else {
 +    SIMIX_run();
 +  }
 +  return MSG_OK;
 +}
 +
 +MSG_error_t MSG_main_liveness_stateless(xbt_automaton_t a, char *prgm)
 +{
 +  /* Clean IO before the run */
 +  fflush(stdout);
 +  fflush(stderr);
 +
 +  if (MC_IS_ENABLED) {
 +    MC_modelcheck_liveness_stateless(a, prgm);
 +  }
 +  else {
 +    SIMIX_run();
 +  }
 +  return MSG_OK;
 +}
 +
  /** \ingroup msg_simulation
   * \brief Kill all running process
  
@@@ -223,6 -178,7 +223,7 @@@ int MSG_process_killall(int reset_PIDs
   */
  MSG_error_t MSG_clean(void)
  {
+   XBT_DEBUG("Closing MSG");
  
  #ifdef HAVE_TRACING
    TRACE_surf_release();
diff --combined src/simix/smx_smurf.c
@@@ -5,24 -5,25 +5,25 @@@
  XBT_LOG_NEW_DEFAULT_SUBCATEGORY(simix_smurf, simix,
                                  "Logging specific to SIMIX (SMURF)");
  
- /* FIXME: we may want to save the initialization of issuer... */
  XBT_INLINE smx_req_t SIMIX_req_mine()
  {
    smx_process_t issuer = SIMIX_process_self();
    return &issuer->request;
  }
  
- void SIMIX_request_push()
+ /**
+  * \brief Makes the current process do a request to the kernel and yields
+  * until completion.
+  * \param self the current process
+  */
+ void SIMIX_request_push(smx_process_t self)
  {
-   smx_process_t issuer = SIMIX_process_self();
-   if (issuer != simix_global->maestro_process){
-     issuer->request.issuer = issuer;
-     XBT_DEBUG("Yield process '%s' on request of type %s (%d)", issuer->name,
-         SIMIX_request_name(issuer->request.call), issuer->request.call);
-     SIMIX_process_yield();
+   if (self != simix_global->maestro_process) {
+     XBT_DEBUG("Yield process '%s' on request of type %s (%d)", self->name,
+         SIMIX_request_name(self->request.call), self->request.call);
+     SIMIX_process_yield(self);
    } else {
-     SIMIX_request_pre(&issuer->request, 0);
+     SIMIX_request_pre(&self->request, 0);
    }
  }
  
@@@ -483,7 -484,6 +484,7 @@@ void SIMIX_request_pre(smx_req_t req, i
            SIMIX_host_get_name(SIMIX_process_get_host(req->issuer))
            );
        break;
 +
    }
  }
  
diff --combined src/xbt/dynar.c
@@@ -152,11 -152,11 +152,11 @@@ _xbt_dynar_remove_at(xbt_dynar_t const 
      if (dynar->elmsize <= SIZEOF_MAX) {
        char elm[SIZEOF_MAX];
        _xbt_dynar_get_elm(elm, dynar, idx);
-       (*dynar->free_f) (elm);
+       dynar->free_f(elm);
      } else {
        char *elm = malloc(dynar->elmsize);
        _xbt_dynar_get_elm(elm, dynar, idx);
-       (*dynar->free_f) (elm);
+       dynar->free_f(elm);
        free(elm);
      }
    }
@@@ -259,7 -259,6 +259,6 @@@ XBT_INLINE void xbt_dynar_reset(xbt_dyn
      _dynar_map(dynar, dynar->free_f);
    }
    /*
-      if (dynar->data)
       free(dynar->data);
  
       dynar->size = 0;
@@@ -331,7 -330,7 +330,7 @@@ XBT_INLINE unsigned long xbt_dynar_leng
    return (dynar ? (unsigned long) dynar->used : (unsigned long) 0);
  }
  
 -/**@brief check if a dynar is empty
 + /**@brief check if a dynar is empty
   *
   *\param dynar the dynat we want to check
   */
@@@ -460,7 -459,7 +459,7 @@@ xbt_dynar_replace(xbt_dynar_t dynar
    if (idx < dynar->used && dynar->free_f) {
      void *const old_object = _xbt_dynar_elm(dynar, idx);
  
-     (*(dynar->free_f)) (old_object);
+     dynar->free_f(old_object);
    }
  
    _xbt_dynar_set(dynar, idx, object);
@@@ -675,7 -674,7 +674,7 @@@ static void _dynar_map(const xbt_dynar_
  
    for (i = 0; i < used; i++) {
      char* elm = (char*) data + i * elmsize;
-     (*op) (elm);
+     op(elm);
    }
  }
  
@@@ -1003,7 -1002,7 +1002,7 @@@ XBT_TEST_UNIT("insert",test_dynar_inser
                       "The retrieved value is not the same than the injected one (%d!=%d)",
                       cursor, cpt);
    }
-   xbt_test_assert(xbt_dynar_length(d) == 0,
+   xbt_test_assert(xbt_dynar_is_empty(d),
                     "There is still %lu elements in the dynar after removing everything",
                     xbt_dynar_length(d));
    xbt_dynar_free(&d);
                       "The retrieved value is not the same than the injected one (%d!=%d)",
                       cursor, cpt);
    }
-   xbt_test_assert(xbt_dynar_length(d) == 0,
+   xbt_test_assert(xbt_dynar_is_empty(d),
                     "There is still %lu elements in the dynar after removing everything",
                     xbt_dynar_length(d));
    xbt_dynar_free(&d);
@@@ -1324,7 -1323,7 +1323,7 @@@ static void pusher_f(void *a
  static void poper_f(void *a)
  {
    xbt_dynar_t d = (xbt_dynar_t) a;
-   int i;
+   volatile int i;
    int data;
    xbt_ex_t e;
  
@@@ -9,9 -9,6 +9,9 @@@
  #include "mmprivate.h"
  #include "gras_config.h"
  
 +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(xbt_mm_legacy, xbt,
 +                                "Logging specific to mm_legacy in mmalloc");
 +
  static void *__mmalloc_current_heap = NULL;     /* The heap we are currently using. */
  
  #include "xbt_modinter.h"
@@@ -74,8 -71,7 +74,7 @@@ void *realloc(void *p, size_t s
      else
        ret = mmalloc(mdp, s);
    } else {
-     if (p)
-       mfree(mdp, p);
+     mfree(mdp, p);
    }
    UNLOCK(mdp);
  
@@@ -167,249 -163,3 +166,249 @@@ void mmalloc_postexit(void
    //  mmalloc_detach(__mmalloc_default_mdp);
    mmalloc_pre_detach(__mmalloc_default_mdp);
  }
 +
 +int mmalloc_compare_heap(void *h1, void *h2){
 +
 +  if(h1 == NULL && h2 == NULL){
 +    XBT_DEBUG("Malloc descriptors null");
 +    return 0;
 +  }
 + 
 +
 +  /* Heapstats */
 +
 +  struct mstats ms1 = mmstats(h1);
 +  struct mstats ms2 = mmstats(h2);
 +
 +  if(ms1.bytes_total !=  ms2.bytes_total){
 +    XBT_DEBUG("Different total size of the heap");
 +    return 1;
 +  }
 +
 +  if(ms1.chunks_used !=  ms2.chunks_used){
 +    XBT_DEBUG("Different chunks allocated by the user");
 +    return 1;
 +  }
 +
 +  if(ms1.bytes_used !=  ms2.bytes_used){
 +    XBT_DEBUG("Different byte total of user-allocated chunks");
 +    return 1;
 +  }
 +
 +  if(ms1.bytes_free !=  ms2.bytes_free){
 +    XBT_DEBUG("Different byte total of chunks in the free list");
 +    return 1;
 +  }
 +
 +  if(ms1.chunks_free !=  ms2.chunks_free){
 +    XBT_DEBUG("Different chunks in the free list");
 +    return 1;
 +  }
 +
 +  struct mdesc *mdp1, *mdp2;
 +  mdp1 = MD_TO_MDP(h1);
 +  mdp2 = MD_TO_MDP(h2);
 +  
 +  if(mmalloc_compare_mdesc(mdp1, mdp2))
 +    return 1;
 +  
 +
 +  return 0;
 +}
 +
 +int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
 +
 +  struct mdesc* mdp;
 +  
 +
 +  if(mdp1->headersize != mdp2->headersize){
 +    XBT_DEBUG("Different size of the file header for the mapped files");
 +    return 1;
 +  }
 +
 +  if(mdp1->refcount != mdp2->refcount){
 +    XBT_DEBUG("Different number of processes that attached the heap");
 +    return 1;
 +  }
 + 
 +  if(strcmp(mdp1->magic, mdp2->magic) != 0){
 +    XBT_DEBUG("Different magic number");
 +    return 1;
 +  }
 +
 +  if(mdp1->flags != mdp2->flags){
 +    XBT_DEBUG("Different flags");
 +    return 1;
 +  }
 +
 +  if(mdp1->heapsize != mdp2->heapsize){
 +    XBT_DEBUG("Different number of info entries");
 +    return 1;
 +  }
 +
 +  // XBT_DEBUG("Heap size : %Zu", mdp1->heapsize);
 +
 +  if(mdp1->heapbase != mdp2->heapbase){
 +    XBT_DEBUG("Different first block of the heap");
 +    return 1;
 +  }
 +
 +
 +  if(mdp1->heapindex != mdp2->heapindex){
 +    XBT_DEBUG("Different index for the heap table");
 +    return 1;
 +  }
 +
 +  //XBT_DEBUG("Heap index : %Zu", mdp1->heapindex);
 +
 +  if(mdp1->base != mdp2->base){
 +    XBT_DEBUG("Different base address of the memory region");
 +    return 1;
 +  }
 +
 +  if(mdp1->breakval != mdp2->breakval){
 +    XBT_DEBUG("Different current location in the memory region");
 +    return 1;
 +  }
 +
 +  if(mdp1->top != mdp2->top){
 +    XBT_DEBUG("Different end of the current location in the memory region");
 +    return 1;
 +  }
 +  
 +  if(mdp1->heaplimit != mdp2->heaplimit){
 +    XBT_DEBUG("Different limit of valid info table indices");
 +    return 1;
 +  }
 +
 +  //XBT_DEBUG("Heap limit : %Zu", mdp1->heaplimit);
 +
 +
 +  if(mdp1->fd != mdp2->fd){
 +    XBT_DEBUG("Different file descriptor for the file to which this malloc heap is mapped");
 +    return 1;
 +  }
 +
 +  if(mdp1->saved_errno != mdp2->saved_errno){
 +    XBT_DEBUG("Different errno");
 +    return 1;
 +  }
 +
 +  if(mdp1->version != mdp2->version){
 +    XBT_DEBUG("Different version of the mmalloc package");
 +    return 1;
 +  }
 +
 + 
 +  size_t block_free1, block_free2 , next_block_free, first_block_free ;
 +  size_t i, j;
 +  void *addr_block1, *addr_block2;
 +
 + 
 +
 +  /* Search index of the first free block */
 +
 +  block_free1 = mdp1->heapindex; 
 +  block_free2 = mdp2->heapindex;
 +
 +  while(mdp1->heapinfo[block_free1].free.prev != 0){
 +    block_free1 = mdp1->heapinfo[block_free1].free.prev;
 +  }
 +
 +  while(mdp2->heapinfo[block_free2].free.prev != 0){
 +    block_free2 = mdp1->heapinfo[block_free2].free.prev;
 +  }
 +
 +  if(block_free1 !=  block_free2){
 +    XBT_DEBUG("Different first free block");
 +    return 1;
 +  }
 +
 +  first_block_free = block_free1;
 +
 +  if(mdp1->heapinfo[block_free1].free.size != mdp2->heapinfo[block_free2].free.size){ 
 +    XBT_DEBUG("Different size (in blocks) of the first free cluster");
 +    return 1;
 +  }
 +
 +  /* Check busy blocks (circular checking)*/
 +
 +  i = block_free1 + mdp1->heapinfo[block_free1].free.size;
 +  next_block_free = mdp1->heapinfo[block_free1].free.next;
 +
 +  if(next_block_free == 0)
 +    next_block_free = mdp1->heaplimit;
 +
 +
 +  while(i != first_block_free){
 +
 +    while(i<next_block_free){
 +
 +      j = i;
 +
 +      if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){
 +      XBT_DEBUG("Different type of busy block");
 +      return 1;
 +      }else{
 +      if(i == 0)
 +        j++;
 +      mdp = mdp1;
 +      addr_block1 = ADDRESS(j);
 +      mdp = mdp2;
 +      addr_block2 = ADDRESS(j); 
 +      switch(mdp1->heapinfo[i].busy.type){
 +      case 0 :
 +        if(mdp1->heapinfo[i].busy.info.size != mdp2->heapinfo[i].busy.info.size){
 +          XBT_DEBUG("Different size of a large cluster");
 +          return 1;
 +        }else{
 +          XBT_DEBUG("Block : %Zu", i);
 +          if(memcmp(addr_block1, addr_block2, (mdp1->heapinfo[i].busy.info.size * BLOCKSIZE)) != 0){
 +            XBT_DEBUG("Different data in block %Zu", i);
 +            return 1;
 +          } 
 +        }
 +        i = i+mdp1->heapinfo[i].busy.info.size;
 +        break;
 +      default :         
 +        if(mdp1->heapinfo[i].busy.info.frag.nfree != mdp2->heapinfo[i].busy.info.frag.nfree){
 +          XBT_DEBUG("Different free fragments in a fragmented block");
 +          return 1;
 +        }else{
 +          if(mdp1->heapinfo[i].busy.info.frag.first != mdp2->heapinfo[i].busy.info.frag.first){
 +            XBT_DEBUG("Different first free fragments of the block");
 +            return 1; 
 +          }else{
 +            if(memcmp(addr_block1, addr_block2, BLOCKSIZE) != 0){
 +              XBT_DEBUG("Different data in fragmented block %Zu", i);
 +              return 1;
 +            } 
 +          }
 +        }
 +        i++;
 +        break;
 +      }
 +      }
 +    }
 +
 +     
 +    block_free1 = mdp1->heapinfo[block_free1].free.next;
 +    next_block_free = mdp1->heapinfo[block_free1].free.next;
 +    if(i != first_block_free){
 +      if(block_free1 != 0)
 +      i = block_free1 + mdp1->heapinfo[block_free1].free.size;
 +      else
 +      i = 0;
 +    }
 +      
 +  }
 +  
 +  return 0;   
 +  
 +  
 +}
 +
 + 
 +  
 +  
 +