Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
[mc] New message for stack_area
[simgrid.git] / src / mc / mc_ignore.c
index 5f8ea90..d0c2c37 100644 (file)
@@ -18,7 +18,10 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ignore, mc,
 
 
 /**************************** Global variables ******************************/
-xbt_dynar_t mc_checkpoint_ignore;
+// Those structures live with the MCer and should be moved in the model_checker
+// structure but they are currently used before the MC initialisation
+// (in standalone mode).
+
 extern xbt_dynar_t mc_heap_comparison_ignore;
 extern xbt_dynar_t stacks_areas;
 
@@ -62,19 +65,21 @@ static void checkpoint_ignore_region_free_voidp(void *r)
   checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r);
 }
 
+xbt_dynar_t MC_checkpoint_ignore_new(void)
+{
+  return xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t),
+                        checkpoint_ignore_region_free_voidp);
+}
+
 /***********************************************************************/
 
 void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region)
 {
-  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
   if (mc_heap_comparison_ignore == NULL) {
     mc_heap_comparison_ignore =
         xbt_dynar_new(sizeof(mc_heap_ignore_region_t),
                       heap_ignore_region_free_voidp);
     xbt_dynar_push(mc_heap_comparison_ignore, &region);
-    if (!raw_mem_set)
-      MC_SET_STD_HEAP;
     return;
   }
 
@@ -92,8 +97,6 @@ void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region)
                                                    mc_heap_ignore_region_t);
     if (current_region->address == region->address) {
       heap_ignore_region_free(region);
-      if (!raw_mem_set)
-        MC_SET_STD_HEAP;
       return;
     } else if (current_region->address < region->address) {
       start = cursor + 1;
@@ -107,15 +110,12 @@ void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region)
     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, &region);
   else
     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
-
-  if (!raw_mem_set)
-    MC_SET_STD_HEAP;
 }
 
 void MC_heap_region_ignore_send(mc_heap_ignore_region_t region)
 {
-  s_mc_ignore_region_message_t message;
-  message.type = MC_MESSAGE_IGNORE_REGION;
+  s_mc_ignore_heap_message_t message;
+  message.type = MC_MESSAGE_IGNORE_HEAP;
   message.region = *region;
   if (MC_protocol_send(mc_client->fd, &message, sizeof(message)))
     xbt_die("Could not send ignored region to MCer");
@@ -125,15 +125,10 @@ void MC_heap_region_ignore_send(mc_heap_ignore_region_t region)
 // FIXME, cross-process support? (or make this it is used on the app-side)
 void MC_ignore_heap(void *address, size_t size)
 {
-  if(!std_heap)
-    return;
-
   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
   MC_SET_MC_HEAP;
 
-  mc_heap_ignore_region_t region = NULL;
-  region = xbt_new0(s_mc_heap_ignore_region_t, 1);
+  mc_heap_ignore_region_t region = xbt_new0(s_mc_heap_ignore_region_t, 1);
   region->address = address;
   region->size = size;
 
@@ -164,6 +159,13 @@ void MC_ignore_heap(void *address, size_t size)
 
 void MC_remove_ignore_heap(void *address, size_t size)
 {
+  if (mc_mode == MC_MODE_CLIENT) {
+    s_mc_ignore_memory_message_t message;
+    message.type = MC_MESSAGE_UNIGNORE_HEAP;
+    message.addr = address;
+    message.size = size;
+    MC_client_send_message(&message, sizeof(message));
+  }
 
   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 
@@ -344,6 +346,13 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name)
 
 }
 
+void MC_stack_area_add(stack_region_t stack_area)
+{
+  if (stacks_areas == NULL)
+    stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
+  xbt_dynar_push(stacks_areas, &stack_area);
+}
+
 /** @brief Register a stack in the model checker
  *
  *  The stacks are allocated in the heap. The MC handle them especially
@@ -359,16 +368,10 @@ void MC_new_stack_area(void *stack, smx_process_t process, void *context, size_t
 {
 
   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
   MC_SET_MC_HEAP;
 
-  if (stacks_areas == NULL)
-    stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
-
-  stack_region_t region = NULL;
-  region = xbt_new0(s_stack_region_t, 1);
+  stack_region_t region = xbt_new0(s_stack_region_t, 1);
   region->address = stack;
-  region->process_name = process && process->name ? strdup(process->name) : NULL;
   region->context = context;
   region->size = size;
   region->block =
@@ -381,50 +384,45 @@ void MC_new_stack_area(void *stack, smx_process_t process, void *context, size_t
 #endif
   region->process_index = -1;
 
-  xbt_dynar_push(stacks_areas, &region);
+  if (mc_mode == MC_MODE_CLIENT) {
+    s_mc_stack_region_message_t message;
+    message.type = MC_MESSAGE_STACK_REGION;
+    message.stack_region = *region;
+    MC_client_send_message(&message, sizeof(message));
+  }
+
+  MC_stack_area_add(region);
 
   if (!raw_mem_set)
     MC_SET_STD_HEAP;
 }
 
-void MC_ignore(void *addr, size_t size)
+void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size)
 {
-
-  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
-  MC_SET_MC_HEAP;
-
-  // FIXME, cross-process support
-  if (mc_checkpoint_ignore == NULL)
-    mc_checkpoint_ignore =
-        xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t),
-                      checkpoint_ignore_region_free_voidp);
-
+  xbt_dynar_t checkpoint_ignore = process->checkpoint_ignore;
   mc_checkpoint_ignore_region_t region =
       xbt_new0(s_mc_checkpoint_ignore_region_t, 1);
   region->addr = addr;
   region->size = size;
 
-  if (xbt_dynar_is_empty(mc_checkpoint_ignore)) {
-    xbt_dynar_push(mc_checkpoint_ignore, &region);
+  if (xbt_dynar_is_empty(checkpoint_ignore)) {
+    xbt_dynar_push(checkpoint_ignore, &region);
   } else {
 
     unsigned int cursor = 0;
     int start = 0;
-    int end = xbt_dynar_length(mc_checkpoint_ignore) - 1;
+    int end = xbt_dynar_length(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,
+          (mc_checkpoint_ignore_region_t) xbt_dynar_get_as(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_SET_STD_HEAP;
           return;
         } else if (current_region->size < size) {
           start = cursor + 1;
@@ -440,17 +438,14 @@ void MC_ignore(void *addr, size_t size)
 
     if (current_region->addr == addr) {
       if (current_region->size < size) {
-        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
+        xbt_dynar_insert_at(checkpoint_ignore, cursor + 1, &region);
       } else {
-        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
+        xbt_dynar_insert_at(checkpoint_ignore, cursor, &region);
       }
     } else if (current_region->addr < addr) {
-      xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
+      xbt_dynar_insert_at(checkpoint_ignore, cursor + 1, &region);
     } else {
-      xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
+      xbt_dynar_insert_at(checkpoint_ignore, cursor, &region);
     }
   }
-
-  if (!raw_mem_set)
-    MC_SET_STD_HEAP;
 }