src/mc/mc_ignore.cpp

   1 /* Copyright (c) 2008-2014. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #include "internal_config.h"
   8 #include "mc_object_info.h"
   9 #include "mc_private.h"
  10 #include "smpi/private.h"
  11 #include "mc/mc_snapshot.h"
  12 #include "mc_ignore.h"
  13 #include "mc_protocol.h"
  14 #include "mc_client.h"
  15
  16 extern "C" {
  17
  18 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ignore, mc,
  19                                 "Logging specific to MC ignore mechanism");
  20
  21
  22 /**************************** Global variables ******************************/
  23 // Those structures live with the MCer and should be moved in the model_checker
  24 // structure but they are currently used before the MC initialisation
  25 // (in standalone mode).
  26
  27
  28 extern xbt_dynar_t stacks_areas;
  29
  30 /**************************** Structures ******************************/
  31 typedef struct s_mc_stack_ignore_variable {
  32   char *var_name;
  33   char *frame;
  34 } s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t;
  35
  36 /**************************** Free functions ******************************/
  37
  38 static void stack_ignore_variable_free(mc_stack_ignore_variable_t v)
  39 {
  40   xbt_free(v->var_name);
  41   xbt_free(v->frame);
  42   xbt_free(v);
  43 }
  44
  45 static void stack_ignore_variable_free_voidp(void *v)
  46 {
  47   stack_ignore_variable_free((mc_stack_ignore_variable_t) * (void **) v);
  48 }
  49
  50 static void checkpoint_ignore_region_free(mc_checkpoint_ignore_region_t r)
  51 {
  52   xbt_free(r);
  53 }
  54
  55 static void checkpoint_ignore_region_free_voidp(void *r)
  56 {
  57   checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r);
  58 }
  59
  60 xbt_dynar_t MC_checkpoint_ignore_new(void)
  61 {
  62   return xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t),
  63                         checkpoint_ignore_region_free_voidp);
  64 }
  65
  66 /***********************************************************************/
  67
  68 // ***** Model-checked
  69
  70 void MC_ignore_heap(void *address, size_t size)
  71 {
  72   if (mc_mode != MC_MODE_CLIENT)
  73     return;
  74
  75   s_mc_heap_ignore_region_t region;
  76   memset(&region, 0, sizeof(region));
  77   region.address = address;
  78   region.size = size;
  79   region.block =
  80    ((char *) address -
  81     (char *) std_heap->heapbase) / BLOCKSIZE + 1;
  82   if (std_heap->heapinfo[region.block].type == 0) {
  83     region.fragment = -1;
  84     std_heap->heapinfo[region.block].busy_block.ignore++;
  85   } else {
  86     region.fragment =
  87         ((uintptr_t) (ADDR2UINT(address) % (BLOCKSIZE))) >> std_heap->
  88         heapinfo[region.block].type;
  89     std_heap->heapinfo[region.block].busy_frag.ignore[region.fragment]++;
  90   }
  91
  92   s_mc_ignore_heap_message_t message;
  93   message.type = MC_MESSAGE_IGNORE_HEAP;
  94   message.region = region;
  95   if (MC_protocol_send(mc_client->fd, &message, sizeof(message)))
  96     xbt_die("Could not send ignored region to MCer");
  97 }
  98
  99 void MC_remove_ignore_heap(void *address, size_t size)
 100 {
 101   if (mc_mode != MC_MODE_CLIENT)
 102     return;
 103
 104   s_mc_ignore_memory_message_t message;
 105   message.type = MC_MESSAGE_UNIGNORE_HEAP;
 106   message.addr = address;
 107   message.size = size;
 108   MC_client_send_message(&message, sizeof(message));
 109 }
 110
 111 void MC_ignore_global_variable(const char *name)
 112 {
 113   // TODO, send a message to the model_checker
 114   xbt_die("Unimplemented");
 115 }
 116
 117 void MC_stack_area_add(stack_region_t stack_area)
 118 {
 119   if (stacks_areas == NULL)
 120     stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
 121   xbt_dynar_push(stacks_areas, &stack_area);
 122 }
 123
 124 /** @brief Register a stack in the model checker
 125  *
 126  *  The stacks are allocated in the heap. The MC handle them especially
 127  *  when we analyse/compare the content of the heap so it must be told where
 128  *  they are with this function.
 129  *
 130  *  @param stack
 131  *  @param process Process owning the stack
 132  *  @param context
 133  *  @param size    Size of the stack
 134  */
 135 void MC_new_stack_area(void *stack, smx_process_t process, void *context, size_t size)
 136 {
 137   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 138
 139   stack_region_t region = xbt_new0(s_stack_region_t, 1);
 140   region->address = stack;
 141   region->context = context;
 142   region->size = size;
 143   region->block =
 144       ((char *) stack -
 145        (char *) std_heap->heapbase) / BLOCKSIZE + 1;
 146 #ifdef HAVE_SMPI
 147   if (smpi_privatize_global_variables && process) {
 148     region->process_index = smpi_process_index_of_smx_process(process);
 149   } else
 150 #endif
 151   region->process_index = -1;
 152
 153   if (mc_mode == MC_MODE_CLIENT) {
 154     s_mc_stack_region_message_t message;
 155     message.type = MC_MESSAGE_STACK_REGION;
 156     message.stack_region = *region;
 157     MC_client_send_message(&message, sizeof(message));
 158   }
 159
 160   MC_stack_area_add(region);
 161
 162   mmalloc_set_current_heap(heap);
 163 }
 164
 165 void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size)
 166 {
 167   xbt_dynar_t checkpoint_ignore = process->checkpoint_ignore;
 168   mc_checkpoint_ignore_region_t region =
 169       xbt_new0(s_mc_checkpoint_ignore_region_t, 1);
 170   region->addr = addr;
 171   region->size = size;
 172
 173   if (xbt_dynar_is_empty(checkpoint_ignore)) {
 174     xbt_dynar_push(checkpoint_ignore, &region);
 175   } else {
 176
 177     unsigned int cursor = 0;
 178     int start = 0;
 179     int end = xbt_dynar_length(checkpoint_ignore) - 1;
 180     mc_checkpoint_ignore_region_t current_region = NULL;
 181
 182     while (start <= end) {
 183       cursor = (start + end) / 2;
 184       current_region =
 185           (mc_checkpoint_ignore_region_t) xbt_dynar_get_as(checkpoint_ignore,
 186                                                            cursor,
 187                                                            mc_checkpoint_ignore_region_t);
 188       if (current_region->addr == addr) {
 189         if (current_region->size == size) {
 190           checkpoint_ignore_region_free(region);
 191           return;
 192         } else if (current_region->size < size) {
 193           start = cursor + 1;
 194         } else {
 195           end = cursor - 1;
 196         }
 197       } else if (current_region->addr < addr) {
 198         start = cursor + 1;
 199       } else {
 200         end = cursor - 1;
 201       }
 202     }
 203
 204     if (current_region->addr == addr) {
 205       if (current_region->size < size) {
 206         xbt_dynar_insert_at(checkpoint_ignore, cursor + 1, &region);
 207       } else {
 208         xbt_dynar_insert_at(checkpoint_ignore, cursor, &region);
 209       }
 210     } else if (current_region->addr < addr) {
 211       xbt_dynar_insert_at(checkpoint_ignore, cursor + 1, &region);
 212     } else {
 213       xbt_dynar_insert_at(checkpoint_ignore, cursor, &region);
 214     }
 215   }
 216 }
 217
 218 }