X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/50376f845bf79ba752eb226efdeb2a46b2ff88cf..cf9200da17217300a7966654d881f2efdb8e514c:/src/mc/mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 68a564cdaf..5ed07dad5c 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -1,4 +1,5 @@
-/* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved.            */
+/* Copyright (c) 2008-2013. 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. */
@@ -34,9 +35,8 @@ char *_sg_mc_dot_output_file = NULL;
 
 int user_max_depth_reached = 0;
 
-extern int _sg_init_status;
 void _mc_cfg_cb_reduce(const char *name, int pos) {
-  if (_sg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check) {
     xbt_die("You are specifying a reduction strategy after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
   }
   char *val= xbt_cfg_get_string(_sg_cfg_set, name);
@@ -50,41 +50,41 @@ void _mc_cfg_cb_reduce(const char *name, int pos) {
 }
 
 void _mc_cfg_cb_checkpoint(const char *name, int pos) {
-  if (_sg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check) {
     xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
   }
-  _sg_mc_checkpoint = xbt_cfg_get_boolean(_sg_cfg_set, name);
+  _sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
 }
 void _mc_cfg_cb_property(const char *name, int pos) {
-  if (_sg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check) {
     xbt_die("You are specifying a property after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
   }
   _sg_mc_property_file= xbt_cfg_get_string(_sg_cfg_set, name);
 }
 
 void _mc_cfg_cb_timeout(const char *name, int pos) {
-  if (_sg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check) {
     xbt_die("You are specifying a value to enable/disable timeout for wait requests after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
   }
   _sg_mc_timeout= xbt_cfg_get_boolean(_sg_cfg_set, name);
 }
 
 void _mc_cfg_cb_max_depth(const char *name, int pos) {
-  if (_sg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check) {
     xbt_die("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
   }
   _sg_mc_max_depth= xbt_cfg_get_int(_sg_cfg_set, name);
 }
 
 void _mc_cfg_cb_visited(const char *name, int pos) {
-  if (_sg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check) {
     xbt_die("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
   }
   _sg_mc_visited= xbt_cfg_get_int(_sg_cfg_set, name);
 }
 
 void _mc_cfg_cb_dot_output(const char *name, int pos) {
-  if (_sg_init_status && !_sg_do_model_check) {
+  if (_sg_cfg_init_status && !_sg_do_model_check) {
     xbt_die("You are specifying a file name for a dot output of graph state after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
   }
   _sg_mc_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name);
@@ -94,8 +94,8 @@ void _mc_cfg_cb_dot_output(const char *name, int pos) {
 mc_state_t mc_current_state = NULL;
 char mc_replay_mode = FALSE;
 double *mc_time = NULL;
-mc_comparison_times_t mc_comp_times = NULL;
-double mc_snapshot_comparison_time;
+__thread mc_comparison_times_t mc_comp_times = NULL;
+__thread double mc_snapshot_comparison_time;
 mc_stats_t mc_stats = NULL;
 
 /* Safety */
@@ -116,6 +116,8 @@ xbt_dynar_t mc_global_variables_libsimgrid = NULL;
 xbt_dynar_t mc_global_variables_binary = NULL;
 xbt_dict_t mc_variables_type_libsimgrid = NULL;
 xbt_dict_t mc_variables_type_binary = NULL;
+mc_object_info_t mc_libsimgrid_info = NULL;
+mc_object_info_t mc_binary_info = NULL;
 
 /* Ignore mechanism */
 xbt_dynar_t mc_stack_comparison_ignore;
@@ -176,6 +178,24 @@ static void dw_variable_free_voidp(void *t){
   dw_variable_free((dw_variable_t) * (void **) t);
 }
 
+// object_info
+
+mc_object_info_t MC_new_object_info() {
+  mc_object_info_t res = xbt_new(s_mc_object_info_t, 1);
+  res->local_variables = xbt_dict_new_homogeneous(NULL);
+  res->global_variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
+  res->types = xbt_dict_new_homogeneous(NULL);
+  return res;
+}
+
+void MC_free_object_info(mc_object_info_t* info) {
+  xbt_dict_free(&(*info)->local_variables);
+  xbt_dynar_free(&(*info)->global_variables);
+  xbt_dict_free(&(*info)->types);
+  xbt_free(info);
+  info = NULL;
+}
+
 /*************************************************************************/
 
 static dw_location_t MC_dwarf_get_location(xbt_dict_t location_list, char *expr){
@@ -314,9 +334,14 @@ static dw_location_t MC_dwarf_get_location(xbt_dict_t location_list, char *expr)
 
 }
 
+/** @brief Extract the location lists from an ELF file (.debug_loc)
+ *
+ *  @return A map from the offset in the list (in hexadecimal string)
+ *          into a location list (dynar of dw_location_entry_t).
+ */
 static xbt_dict_t MC_dwarf_get_location_list(const char *elf_file){
 
-  char *command = bprintf("objdump -Wo %s", elf_file);
+  char *command = bprintf("LANG=C objdump -Wo %s", elf_file);
 
   FILE *fp = popen(command, "r");
 
@@ -371,8 +396,14 @@ static xbt_dict_t MC_dwarf_get_location_list(const char *elf_file){
     xbt_str_strip_spaces(line);
     split = xbt_str_split(line, " ");
 
+    char *key = NULL;
     while(read != -1 && strcmp("<End", (char *)xbt_dynar_get_as(split, 1, char *)) != 0){
       
+      // Take the key from the first line of the list:
+      if(key==NULL){
+        key = bprintf("%d", (int)strtoul((char *)xbt_dynar_get_as(split, 0, char *), NULL, 16));
+      }
+
       dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1);
       new_entry->lowpc = strtoul((char *)xbt_dynar_get_as(split, 1, char *), NULL, 16);
       new_entry->highpc = strtoul((char *)xbt_dynar_get_as(split, 2, char *), NULL, 16);
@@ -403,7 +434,6 @@ static xbt_dict_t MC_dwarf_get_location_list(const char *elf_file){
     }
 
 
-    char *key = bprintf("%d", (int)strtoul((char *)xbt_dynar_get_as(split, 0, char *), NULL, 16));
     xbt_dict_set(location_list, key, loclist, NULL);
     xbt_free(key);
     
@@ -492,16 +522,22 @@ static int MC_dwarf_get_variable_index(xbt_dynar_t variables, char* var, void *a
 
 }
 
+static mc_object_info_t MC_dwarf_get_variables(const char *elf_file){
 
-static void MC_dwarf_get_variables(const char *elf_file, xbt_dict_t location_list, xbt_dict_t *local_variables, xbt_dynar_t *global_variables, xbt_dict_t *types){
+  xbt_dict_t location_list = MC_dwarf_get_location_list(elf_file);
 
-  char *command = bprintf("objdump -Wi %s", elf_file);
+  char *command = bprintf("LANG=C objdump -Wi %s", elf_file);
   
   FILE *fp = popen(command, "r");
 
   if(fp == NULL)
     perror("popen for objdump failed");
 
+  mc_object_info_t result = MC_new_object_info();
+  xbt_dict_t *local_variables = &result->local_variables;
+  xbt_dynar_t *global_variables = &result->global_variables;
+  xbt_dict_t *types = &result->types;
+
   char *line = NULL, *origin, *abstract_origin, *current_frame = NULL, 
     *subprogram_name = NULL, *subprogram_start = NULL, *subprogram_end = NULL,
     *node_type = NULL, *location_type = NULL, *variable_name = NULL, 
@@ -550,6 +586,8 @@ static void MC_dwarf_get_variables(const char *elf_file, xbt_dict_t location_lis
     node_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
 
     if(strcmp(node_type, "(DW_TAG_subprogram)") == 0){ /* New frame */
+      /* We build/complete a dw_frame_t object
+       * and append it if necessary to the local_variables dictionnary */
 
       dw_frame_t frame = NULL;
 
@@ -665,6 +703,9 @@ static void MC_dwarf_get_variables(const char *elf_file, xbt_dict_t location_lis
         
 
     }else if(strcmp(node_type, "(DW_TAG_variable)") == 0){ /* New variable */
+      /* We build a dw_variable_t object and append it either to
+         the list of variables of the frame (local variable)
+         or to the list of global variables (global variables). */
 
       dw_variable_t var = NULL;
       
@@ -817,6 +858,7 @@ static void MC_dwarf_get_variables(const char *elf_file, xbt_dict_t location_lis
       new_variable = 1;
 
     }else if(strcmp(node_type, "(DW_TAG_inlined_subroutine)") == 0){
+      /* Update the information on the frame (we should duplicate it instead). */
 
       read = xbt_getline(&line, &n, fp);
 
@@ -871,6 +913,8 @@ static void MC_dwarf_get_variables(const char *elf_file, xbt_dict_t location_lis
              || strcmp(node_type, "(DW_TAG_volatile_type)") == 0
              || (is_pointer = !strcmp(node_type, "(DW_TAG_pointer_type)"))){
 
+      /* Create the and add it to the types dictionnary */
+
       if(strcmp(node_type, "(DW_TAG_base_type)") == 0)
         type_type = e_dw_base_type;
       else if(strcmp(node_type, "(DW_TAG_enumeration_type)") == 0)
@@ -1213,8 +1257,10 @@ static void MC_dwarf_get_variables(const char *elf_file, xbt_dict_t location_lis
   xbt_dict_free(&subprograms_origin);
   xbt_free(line);
   xbt_free(command);
+  xbt_dict_free(&location_list);
+
   pclose(fp);
-  
+  return result;
 }
 
 
@@ -1313,11 +1359,11 @@ void MC_ignore_heap(void *address, size_t size){
       if(!raw_mem_set)
         MC_UNSET_RAW_MEM;
       return;
-    }
-    if(current_region->address < address)
+    }else if(current_region->address < address){
       start = cursor + 1;
-    if(current_region->address > address)
-      end = cursor - 1;   
+    }else{
+      end = cursor - 1;
+    }   
   }
 
   if(current_region->address < address)
@@ -1325,10 +1371,8 @@ void MC_ignore_heap(void *address, size_t size){
   else
     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
 
-  MC_UNSET_RAW_MEM;
-
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
 }
 
 void MC_remove_ignore_heap(void *address, size_t size){
@@ -1349,15 +1393,15 @@ void MC_remove_ignore_heap(void *address, size_t size){
     if(region->address == address){
       ignore_found = 1;
       break;
-    }
-    if(region->address < address)
+    }else if(region->address < address){
       start = cursor + 1;
-    if(region->address > address){
+    }else{
       if((char * )region->address <= ((char *)address + size)){
         ignore_found = 1;
         break;
-      }else
+      }else{
         end = cursor - 1;   
+      }
     }
   }
   
@@ -1366,10 +1410,8 @@ void MC_remove_ignore_heap(void *address, size_t size){
     MC_remove_ignore_heap(address, size);
   }
 
-  MC_UNSET_RAW_MEM;
-  
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
 
 }
 
@@ -1379,22 +1421,20 @@ void MC_ignore_global_variable(const char *name){
 
   MC_SET_RAW_MEM;
 
-  if(mc_global_variables_libsimgrid){
+  if(mc_libsimgrid_info){
 
     unsigned int cursor = 0;
     dw_variable_t current_var;
     int start = 0;
-    int end = xbt_dynar_length(mc_global_variables_libsimgrid) - 1;
-    int var_found;
+    int end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
 
     while(start <= end){
       cursor = (start + end) /2;
-      current_var = (dw_variable_t)xbt_dynar_get_as(mc_global_variables_libsimgrid, cursor, dw_variable_t);
+      current_var = (dw_variable_t)xbt_dynar_get_as(mc_libsimgrid_info->global_variables, cursor, dw_variable_t);
       if(strcmp(current_var->name, name) == 0){
-        xbt_dynar_remove_at(mc_global_variables_libsimgrid, cursor, NULL);
+        xbt_dynar_remove_at(mc_libsimgrid_info->global_variables, cursor, NULL);
         start = 0;
-        end = xbt_dynar_length(mc_global_variables_libsimgrid) - 1;
-        break;
+        end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
       }else if(strcmp(current_var->name, name) < 0){
         start = cursor + 1;
       }else{
@@ -1445,10 +1485,8 @@ void MC_ignore_global_variable(const char *name){
     }
   }
 
-  MC_UNSET_RAW_MEM;
-
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
 }
 
 void MC_ignore_local_variable(const char *var_name, const char *frame_name){
@@ -1457,7 +1495,7 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name){
 
   MC_SET_RAW_MEM;
 
-  if(mc_local_variables_libsimgrid){
+  if(mc_libsimgrid_info){
     unsigned int cursor = 0;
     dw_variable_t current_var;
     int start, end;
@@ -1465,7 +1503,24 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name){
       xbt_dict_cursor_t dict_cursor;
       char *current_frame_name;
       dw_frame_t frame;
-      xbt_dict_foreach(mc_local_variables_libsimgrid, dict_cursor, current_frame_name, frame){
+      xbt_dict_foreach(mc_libsimgrid_info->local_variables, dict_cursor, current_frame_name, frame){
+        start = 0;
+        end = xbt_dynar_length(frame->variables) - 1;
+        while(start <= end){
+          cursor = (start + end) / 2;
+          current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t); 
+          if(strcmp(current_var->name, var_name) == 0){
+            xbt_dynar_remove_at(frame->variables, cursor, NULL);
+            start = 0;
+            end = xbt_dynar_length(frame->variables) - 1;
+          }else if(strcmp(current_var->name, var_name) < 0){
+            start = cursor + 1;
+          }else{
+            end = cursor - 1;
+          } 
+        }
+      }
+       xbt_dict_foreach(mc_binary_info->local_variables, dict_cursor, current_frame_name, frame){
         start = 0;
         end = xbt_dynar_length(frame->variables) - 1;
         while(start <= end){
@@ -1483,7 +1538,8 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name){
         }
       }
     }else{
-      xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(mc_local_variables_libsimgrid, frame_name))->variables;
+      xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(
+                                      mc_libsimgrid_info->local_variables, frame_name))->variables;
       start = 0;
       end = xbt_dynar_length(variables_list) - 1;
       while(start <= end){
@@ -1530,30 +1586,34 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name){
             if(!raw_mem_set)
               MC_UNSET_RAW_MEM;
             return;
-          }
-          if(strcmp(current_var->var_name, var_name) < 0)
+          }else if(strcmp(current_var->var_name, var_name) < 0){
             start = cursor + 1;
-          if(strcmp(current_var->var_name, var_name) > 0)
+          }else{
             end = cursor - 1;
-        }
-        if(strcmp(current_var->frame, frame_name) < 0)
+          }
+        }else if(strcmp(current_var->frame, frame_name) < 0){
           start = cursor + 1;
-        if(strcmp(current_var->frame, frame_name) > 0)
+        }else{
           end = cursor - 1;
+        }
       }
 
-      if(strcmp(current_var->frame, frame_name) < 0)
+      if(strcmp(current_var->frame, frame_name) == 0){
+        if(strcmp(current_var->var_name, var_name) < 0){
+          xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
+        }else{
+          xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
+        }
+      }else if(strcmp(current_var->frame, frame_name) < 0){
         xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
-      else
+      }else{
         xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
-
+      }
     }
   }
 
-  MC_UNSET_RAW_MEM;
-  
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
 
 }
 
@@ -1562,6 +1622,7 @@ void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
+
   if(stacks_areas == NULL)
     stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
   
@@ -1573,11 +1634,9 @@ void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
   region->size = size;
   region->block = ((char*)stack - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
   xbt_dynar_push(stacks_areas, &region);
-  
-  MC_UNSET_RAW_MEM;
 
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
 }
 
 void MC_ignore(void *addr, size_t size){
@@ -1593,7 +1652,48 @@ void MC_ignore(void *addr, size_t size){
   region->addr = addr;
   region->size = size;
 
-  xbt_dynar_push(mc_checkpoint_ignore, &region);
+  if(xbt_dynar_is_empty(mc_checkpoint_ignore)){
+    xbt_dynar_push(mc_checkpoint_ignore, &region);
+  }else{
+     
+    unsigned int cursor = 0;
+    int start = 0;
+    int end = xbt_dynar_length(mc_checkpoint_ignore) -1;
+    mc_checkpoint_ignore_region_t current_region = NULL;
+
+    while(start <= end){
+      cursor = (start + end) / 2;
+      current_region = (mc_checkpoint_ignore_region_t)xbt_dynar_get_as(mc_checkpoint_ignore, cursor, mc_checkpoint_ignore_region_t);
+      if(current_region->addr == addr){
+        if(current_region->size == size){
+          checkpoint_ignore_region_free(region);
+          if(!raw_mem_set)
+            MC_UNSET_RAW_MEM;
+          return;
+        }else if(current_region->size < size){
+          start = cursor + 1;
+        }else{
+          end = cursor - 1;
+        }
+      }else if(current_region->addr < addr){
+          start = cursor + 1;
+      }else{
+        end = cursor - 1;
+      }
+    }
+
+     if(current_region->addr == addr){
+       if(current_region->size < size){
+        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
+      }else{
+        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
+      }
+    }else if(current_region->addr < addr){
+       xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
+    }else{
+       xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
+    }
+  }
 
   if(!raw_mem_set)
     MC_UNSET_RAW_MEM;
@@ -1648,26 +1748,19 @@ void MC_init(){
   MC_SET_RAW_MEM;
 
   MC_init_memory_map_info();
-  
-  mc_local_variables_libsimgrid = xbt_dict_new_homogeneous(NULL);
-  mc_local_variables_binary = xbt_dict_new_homogeneous(NULL);
-  mc_global_variables_libsimgrid = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
-  mc_global_variables_binary = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
-  mc_variables_type_libsimgrid = xbt_dict_new_homogeneous(NULL);
-  mc_variables_type_binary = xbt_dict_new_homogeneous(NULL);
 
   XBT_INFO("Get debug information ...");
 
-  /* Get local variables in binary for state equality detection */
-  xbt_dict_t binary_location_list = MC_dwarf_get_location_list(xbt_binary_name);
-  MC_dwarf_get_variables(xbt_binary_name, binary_location_list, &mc_local_variables_binary, &mc_global_variables_binary, &mc_variables_type_binary);
-
-  /* Get local variables in libsimgrid for state equality detection */
-  xbt_dict_t libsimgrid_location_list = MC_dwarf_get_location_list(libsimgrid_path);
-  MC_dwarf_get_variables(libsimgrid_path, libsimgrid_location_list, &mc_local_variables_libsimgrid, &mc_global_variables_libsimgrid, &mc_variables_type_libsimgrid);
+  /* Get local variables for state equality detection */
+  mc_binary_info = MC_dwarf_get_variables(xbt_binary_name);
+  mc_libsimgrid_info = MC_dwarf_get_variables(libsimgrid_path);
 
-  xbt_dict_free(&libsimgrid_location_list);
-  xbt_dict_free(&binary_location_list);
+  mc_local_variables_libsimgrid = mc_libsimgrid_info->local_variables;
+  mc_local_variables_binary = mc_binary_info->local_variables;
+  mc_global_variables_libsimgrid = mc_libsimgrid_info->global_variables;
+  mc_global_variables_binary = mc_binary_info->global_variables;
+  mc_variables_type_libsimgrid = mc_libsimgrid_info->types;
+  mc_variables_type_binary = mc_binary_info->types;
 
   XBT_INFO("Get debug information done !");
 
@@ -1679,6 +1772,9 @@ void MC_init(){
   MC_get_libsimgrid_plt_section();
   MC_get_binary_plt_section();
 
+   /* Init parmap */
+  parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
+
   MC_UNSET_RAW_MEM;
 
    /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
@@ -1701,10 +1797,19 @@ void MC_init(){
   MC_ignore_global_variable("mc_snapshot_comparison_time"); 
   MC_ignore_global_variable("mc_time");
   MC_ignore_global_variable("smpi_current_rank");
-  MC_ignore_global_variable("smx_current_context_serial");
-  MC_ignore_global_variable("smx_current_context_key");
-  MC_ignore_global_variable("sysv_maestro_context");
   MC_ignore_global_variable("counter"); /* Static variable used for tracing */
+  MC_ignore_global_variable("maestro_stack_start");
+  MC_ignore_global_variable("maestro_stack_end");
+
+  MC_ignore_heap(&(simix_global->process_to_run), sizeof(simix_global->process_to_run));
+  MC_ignore_heap(&(simix_global->process_that_ran), sizeof(simix_global->process_that_ran));
+  MC_ignore_heap(simix_global->process_to_run, sizeof(*(simix_global->process_to_run)));
+  MC_ignore_heap(simix_global->process_that_ran, sizeof(*(simix_global->process_that_ran)));
+  
+  smx_process_t process;
+  xbt_swag_foreach(process, simix_global->process_list){
+    MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
+  }
 
   if(raw_mem_set)
     MC_SET_RAW_MEM;
@@ -1810,7 +1915,7 @@ void MC_modelcheck_safety(void)
   MC_SET_RAW_MEM;
   /* Save the initial state */
   initial_state_safety = xbt_new0(s_mc_global_t, 1);
-  initial_state_safety->snapshot = MC_take_snapshot();
+  initial_state_safety->snapshot = MC_take_snapshot(0);
   MC_UNSET_RAW_MEM;
 
   MC_dpor();