[mc] Multiple heap removal (partial)

diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake
index b038e16..abde103 100644 (file)
--- a/buildtools/Cmake/DefinePackages.cmake
+++ b/buildtools/Cmake/DefinePackages.cmake
@@ -620,6 +620,8 @@ set(MC_SRC
   src/mc/mc_dwarf_tagnames.h
   src/mc/mc_hash.cpp
   src/mc/mc_ignore.cpp
   src/mc/mc_dwarf_tagnames.h
   src/mc/mc_hash.cpp
   src/mc/mc_ignore.cpp

+  src/mc/mcer_ignore.cpp
+  src/mc/mcer_ignore.h

   src/mc/mc_ignore.h
   src/mc/mc_liveness.h
   src/mc/mc_location.h
   src/mc/mc_ignore.h
   src/mc/mc_liveness.h
   src/mc/mc_location.h

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index b78bf83..2adb895 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -32,11 +32,9 @@ const char* ModelChecker::get_host_name(const char* hostname)
   // Lookup the host name in the dictionary (or create it):
   xbt_dictelm_t elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
   if (!elt) {
   // Lookup the host name in the dictionary (or create it):
   xbt_dictelm_t elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
   if (!elt) {

-    xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);

     xbt_dict_set(this->hostnames_, hostname, NULL, NULL);
     elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
     assert(elt);
     xbt_dict_set(this->hostnames_, hostname, NULL, NULL);
     elt = xbt_dict_get_elm_or_null(this->hostnames_, hostname);
     assert(elt);

-    mmalloc_set_current_heap(heap);

   }
   return elt->key;
 }
   }
   return elt->key;
 }

diff --git a/src/mc/mc_client_api.cpp b/src/mc/mc_client_api.cpp
index 179033b..f4bed1b 100644 (file)
--- a/src/mc/mc_client_api.cpp
+++ b/src/mc/mc_client_api.cpp
@@ -62,11 +62,6 @@ void MC_ignore(void* addr, size_t size)
     message.size = size;
     MC_client_send_message(&message, sizeof(message));
   }
     message.size = size;
     MC_client_send_message(&message, sizeof(message));
   }

-
-  // TODO, remove this once the migration has been completed
-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-  MC_process_ignore_memory(&mc_model_checker->process(), addr, size);
-  mmalloc_set_current_heap(heap);

 }
 
 }
 }
 
 }

diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp
index bede558..eb87892 100644 (file)
--- a/src/mc/mc_comm_determinism.cpp
+++ b/src/mc/mc_comm_determinism.cpp
@@ -300,8 +300,6 @@ static void MC_modelcheck_comm_determinism_main(void);
 
 static void MC_pre_modelcheck_comm_determinism(void)
 {
 
 static void MC_pre_modelcheck_comm_determinism(void)
 {

-  MC_SET_MC_HEAP;
-

   mc_state_t initial_state = NULL;
   smx_process_t process;
   int i;
   mc_state_t initial_state = NULL;
   smx_process_t process;
   int i;


@@ -327,15 +325,12 @@ static void MC_pre_modelcheck_comm_determinism(void)
   }
 
   initial_state = MC_state_new();
   }
 
   initial_state = MC_state_new();

-  MC_SET_STD_HEAP;

   
   XBT_DEBUG("********* Start communication determinism verification *********");
 
   /* Wait for requests (schedules processes) */
   MC_wait_for_requests();
 
   
   XBT_DEBUG("********* Start communication determinism verification *********");
 
   /* Wait for requests (schedules processes) */
   MC_wait_for_requests();
 

-  MC_SET_MC_HEAP;
-

   /* Get an enabled process and insert it in the interleave set of the initial state */
   MC_EACH_SIMIX_PROCESS(process,
     if (MC_process_is_enabled(process)) {
   /* Get an enabled process and insert it in the interleave set of the initial state */
   MC_EACH_SIMIX_PROCESS(process,
     if (MC_process_is_enabled(process)) {


@@ -344,9 +339,6 @@ static void MC_pre_modelcheck_comm_determinism(void)
   );
 
   xbt_fifo_unshift(mc_stack, initial_state);
   );
 
   xbt_fifo_unshift(mc_stack, initial_state);

-
-  MC_SET_STD_HEAP;
-

 }
 
 static void MC_modelcheck_comm_determinism_main(void)
 }
 
 static void MC_modelcheck_comm_determinism_main(void)


@@ -381,9 +373,7 @@ static void MC_modelcheck_comm_determinism_main(void)
       xbt_free(req_str);
       
       if (dot_output != NULL) {
       xbt_free(req_str);
       
       if (dot_output != NULL) {

-        MC_SET_MC_HEAP;

         req_str = MC_request_get_dot_output(req, value);
         req_str = MC_request_get_dot_output(req, value);

-        MC_SET_STD_HEAP;

       }
 
       MC_state_set_executed_request(state, req, value);
       }
 
       MC_state_set_executed_request(state, req, value);


@@ -398,19 +388,15 @@ static void MC_modelcheck_comm_determinism_main(void)
       /* Answer the request */
       MC_simcall_handle(req, value);    /* After this call req is no longer useful */
 
       /* Answer the request */
       MC_simcall_handle(req, value);    /* After this call req is no longer useful */
 

-      MC_SET_MC_HEAP;

       if(!initial_global_state->initial_communications_pattern_done)
         MC_handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
       else
         MC_handle_comm_pattern(call, req, value, NULL, 0);
       if(!initial_global_state->initial_communications_pattern_done)
         MC_handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
       else
         MC_handle_comm_pattern(call, req, value, NULL, 0);

-      MC_SET_STD_HEAP;

 
       /* Wait for requests (schedules processes) */
       MC_wait_for_requests();
 
       /* Create the new expanded state */
 
       /* Wait for requests (schedules processes) */
       MC_wait_for_requests();
 
       /* Create the new expanded state */

-      MC_SET_MC_HEAP;
-

       next_state = MC_state_new();
 
       if ((visited_state = is_visited_state(next_state)) == NULL) {
       next_state = MC_state_new();
 
       if ((visited_state = is_visited_state(next_state)) == NULL) {


@@ -437,8 +423,6 @@ static void MC_modelcheck_comm_determinism_main(void)
       if (dot_output != NULL)
         xbt_free(req_str);
 
       if (dot_output != NULL)
         xbt_free(req_str);
 

-      MC_SET_STD_HEAP;
-

     } else {
 
       if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth) {
     } else {
 
       if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth) {


@@ -449,8 +433,6 @@ static void MC_modelcheck_comm_determinism_main(void)
         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack));
       }
 
         XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack));
       }
 

-      MC_SET_MC_HEAP;
-

       if (!initial_global_state->initial_communications_pattern_done) 
         initial_global_state->initial_communications_pattern_done = 1;
 
       if (!initial_global_state->initial_communications_pattern_done) 
         initial_global_state->initial_communications_pattern_done = 1;
 


@@ -459,8 +441,6 @@ static void MC_modelcheck_comm_determinism_main(void)
       MC_state_delete(state, !state->in_visited_states ? 1 : 0);
       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 
       MC_state_delete(state, !state->in_visited_states ? 1 : 0);
       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
 

-      MC_SET_STD_HEAP;
-

       visited_state = NULL;
 
       /* Check for deadlocks */
       visited_state = NULL;
 
       /* Check for deadlocks */


@@ -469,14 +449,11 @@ static void MC_modelcheck_comm_determinism_main(void)
         return;
       }
 
         return;
       }
 

-      MC_SET_MC_HEAP;
-

       while ((state = (mc_state_t) xbt_fifo_shift(mc_stack)) != NULL) {
         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
           /* We found a back-tracking point, let's loop */
           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
           xbt_fifo_unshift(mc_stack, state);
       while ((state = (mc_state_t) xbt_fifo_shift(mc_stack)) != NULL) {
         if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
           /* We found a back-tracking point, let's loop */
           XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
           xbt_fifo_unshift(mc_stack, state);

-          MC_SET_STD_HEAP;

 
           MC_replay(mc_stack);
 
 
           MC_replay(mc_stack);
 


@@ -488,14 +465,10 @@ static void MC_modelcheck_comm_determinism_main(void)
           MC_state_delete(state, !state->in_visited_states ? 1 : 0);
         }
       }
           MC_state_delete(state, !state->in_visited_states ? 1 : 0);
         }
       }

-
-      MC_SET_STD_HEAP;

     }
   }
 
   MC_print_statistics(mc_stats);
     }
   }
 
   MC_print_statistics(mc_stats);

-  MC_SET_STD_HEAP;
-

   exit(0);
 }
 
   exit(0);
 }
 


@@ -510,16 +483,11 @@ void MC_modelcheck_comm_determinism(void)
     MC_client_handle_messages();
   }
 
     MC_client_handle_messages();
   }
 

-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-

   /* Create exploration stack */
   mc_stack = xbt_fifo_new();
 
   /* Create exploration stack */
   mc_stack = xbt_fifo_new();
 

-  MC_SET_STD_HEAP;
-

   MC_pre_modelcheck_comm_determinism();
 
   MC_pre_modelcheck_comm_determinism();
 

-  MC_SET_MC_HEAP;

   initial_global_state = xbt_new0(s_mc_global_t, 1);
   initial_global_state->snapshot = MC_take_snapshot(0);
   initial_global_state->initial_communications_pattern_done = 0;
   initial_global_state = xbt_new0(s_mc_global_t, 1);
   initial_global_state->snapshot = MC_take_snapshot(0);
   initial_global_state->initial_communications_pattern_done = 0;


@@ -528,11 +496,7 @@ void MC_modelcheck_comm_determinism(void)
   initial_global_state->recv_diff = NULL;
   initial_global_state->send_diff = NULL;
 
   initial_global_state->recv_diff = NULL;
   initial_global_state->send_diff = NULL;
 

-  MC_SET_STD_HEAP;
-

   MC_modelcheck_comm_determinism_main();
   MC_modelcheck_comm_determinism_main();

-
-  mmalloc_set_current_heap(heap);

 }
 
 }
 }
 
 }

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 7a9ebfd..d6e4ca1 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -144,7 +144,7 @@ void MC_init_pid(pid_t pid, int socket)
   /* Init parmap */
   //parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
 
   /* Init parmap */
   //parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
 

-  MC_SET_STD_HEAP;
+  mmalloc_set_current_heap(std_heap);

 
   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 */
 
   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 */


@@ -286,7 +286,7 @@ void MC_replay(xbt_fifo_t stack)
       MC_restore_snapshot(state->system_state);
       if(_sg_mc_comms_determinism || _sg_mc_send_determinism) 
         MC_restore_communications_pattern(state);
       MC_restore_snapshot(state->system_state);
       if(_sg_mc_comms_determinism || _sg_mc_send_determinism) 
         MC_restore_communications_pattern(state);

-      MC_SET_STD_HEAP;
+      mmalloc_set_current_heap(std_heap);

       return;
     }
   }
       return;
     }
   }


@@ -296,11 +296,11 @@ void MC_replay(xbt_fifo_t stack)
   MC_restore_snapshot(initial_global_state->snapshot);
   /* 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_restore_snapshot(initial_global_state->snapshot);
   /* 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_SET_STD_HEAP;
+  mmalloc_set_current_heap(std_heap);

 
   start_item = xbt_fifo_get_last_item(stack);
   
 
   start_item = xbt_fifo_get_last_item(stack);
   

-  MC_SET_MC_HEAP;
+  mmalloc_set_current_heap(mc_heap);

 
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
     // int n = xbt_dynar_length(incomplete_communications_pattern);
 
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
     // int n = xbt_dynar_length(incomplete_communications_pattern);


@@ -313,7 +313,7 @@ void MC_replay(xbt_fifo_t stack)
     }
   }
 
     }
   }
 

-  MC_SET_STD_HEAP;
+  mmalloc_set_current_heap(std_heap);

 
   /* Traverse the stack from the state at position start and re-execute the transitions */
   for (item = start_item;
 
   /* Traverse the stack from the state at position start and re-execute the transitions */
   for (item = start_item;


@@ -344,10 +344,10 @@ void MC_replay(xbt_fifo_t stack)
 
       MC_simcall_handle(req, value);
 
 
       MC_simcall_handle(req, value);
 

-      MC_SET_MC_HEAP;
+      mmalloc_set_current_heap(mc_heap);

       if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
         MC_handle_comm_pattern(call, req, value, NULL, 1);
       if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
         MC_handle_comm_pattern(call, req, value, NULL, 1);

-      MC_SET_STD_HEAP;
+      mmalloc_set_current_heap(std_heap);

 
       MC_wait_for_requests();
 
 
       MC_wait_for_requests();
 


@@ -384,7 +384,7 @@ void MC_replay_liveness(xbt_fifo_t stack)
     pair = (mc_pair_t) xbt_fifo_get_item_content(item);
     if(pair->graph_state->system_state){
       MC_restore_snapshot(pair->graph_state->system_state);
     pair = (mc_pair_t) xbt_fifo_get_item_content(item);
     if(pair->graph_state->system_state){
       MC_restore_snapshot(pair->graph_state->system_state);

-      MC_SET_STD_HEAP;
+      mmalloc_set_current_heap(std_heap);

       return;
     }
   }
       return;
     }
   }


@@ -395,7 +395,7 @@ void MC_replay_liveness(xbt_fifo_t stack)
   /* 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  */
   if (!initial_global_state->raw_mem_set)
   /* 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  */
   if (!initial_global_state->raw_mem_set)

-    MC_SET_STD_HEAP;
+    mmalloc_set_current_heap(std_heap);

 
     /* Traverse the stack from the initial state and re-execute the transitions */
     for (item = xbt_fifo_get_last_item(stack);
 
     /* Traverse the stack from the initial state and re-execute the transitions */
     for (item = xbt_fifo_get_last_item(stack);


@@ -440,9 +440,9 @@ void MC_replay_liveness(xbt_fifo_t stack)
   XBT_DEBUG("**** End Replay ****");
 
   if (initial_global_state->raw_mem_set)
   XBT_DEBUG("**** End Replay ****");
 
   if (initial_global_state->raw_mem_set)

-    MC_SET_MC_HEAP;
+    mmalloc_set_current_heap(mc_heap);

   else
   else

-    MC_SET_STD_HEAP;
+    mmalloc_set_current_heap(std_heap);

 
 }
 
 
 }
 


@@ -459,7 +459,7 @@ void MC_dump_stack_safety(xbt_fifo_t stack)
   
   mc_state_t state;
   
   
   mc_state_t state;
   

-  MC_SET_MC_HEAP;
+  mmalloc_set_current_heap(mc_heap);

   while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
     MC_state_delete(state, !state->in_visited_states ? 1 : 0);
   mmalloc_set_current_heap(heap);
   while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
     MC_state_delete(state, !state->in_visited_states ? 1 : 0);
   mmalloc_set_current_heap(heap);

diff --git a/src/mc/mc_ignore.cpp b/src/mc/mc_ignore.cpp
index 1239c3c..5440faf 100644 (file)
--- a/src/mc/mc_ignore.cpp
+++ b/src/mc/mc_ignore.cpp
@@ -24,7 +24,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ignore, mc,
 // structure but they are currently used before the MC initialisation
 // (in standalone mode).
 
 // 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;
 
 /**************************** Structures ******************************/
 extern xbt_dynar_t stacks_areas;
 
 /**************************** Structures ******************************/


@@ -75,136 +75,51 @@ xbt_dynar_t MC_checkpoint_ignore_new(void)
 
 /***********************************************************************/
 
 
 /***********************************************************************/
 

-// Mcer
-void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region)
+// ***** Model-checked
+
+void MC_ignore_heap(void *address, size_t size)

 {
 {

-  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 (mc_mode != MC_MODE_CLIENT)

     return;
     return;

-  }

 
 

-  unsigned int cursor = 0;
-  mc_heap_ignore_region_t current_region = NULL;
-  int start = 0;
-  int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
-
-  // Find the position where we want to insert the mc_heap_ignore_region_t:
-  while (start <= end) {
-    cursor = (start + end) / 2;
-    current_region =
-        (mc_heap_ignore_region_t) xbt_dynar_get_as(mc_heap_comparison_ignore,
-                                                   cursor,
-                                                   mc_heap_ignore_region_t);
-    if (current_region->address == region->address) {
-      heap_ignore_region_free(region);
-      return;
-    } else if (current_region->address < region->address) {
-      start = cursor + 1;
-    } else {
-      end = cursor - 1;
-    }
+  s_mc_heap_ignore_region_t region;
+  memset(&region, 0, sizeof(region));
+  region.address = address;
+  region.size = size;
+  region.block =
+   ((char *) address -
+    (char *) std_heap->heapbase) / BLOCKSIZE + 1;
+  if (std_heap->heapinfo[region.block].type == 0) {
+    region.fragment = -1;
+    std_heap->heapinfo[region.block].busy_block.ignore++;
+  } else {
+    region.fragment =
+        ((uintptr_t) (ADDR2UINT(address) % (BLOCKSIZE))) >> std_heap->
+        heapinfo[region.block].type;
+    std_heap->heapinfo[region.block].busy_frag.ignore[region.fragment]++;

   }
 
   }
 

-  // Insert it mc_heap_ignore_region_t:
-  if (current_region->address < region->address)
-    xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, &region);
-  else
-    xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
-}
-
-// MCed:
-static void MC_heap_region_ignore_send(mc_heap_ignore_region_t region)
-{

   s_mc_ignore_heap_message_t message;
   message.type = MC_MESSAGE_IGNORE_HEAP;
   s_mc_ignore_heap_message_t message;
   message.type = MC_MESSAGE_IGNORE_HEAP;

-  message.region = *region;
+  message.region = region;

   if (MC_protocol_send(mc_client->fd, &message, sizeof(message)))
     xbt_die("Could not send ignored region to MCer");
 }
 
   if (MC_protocol_send(mc_client->fd, &message, sizeof(message)))
     xbt_die("Could not send ignored region to MCer");
 }
 

-// MCed:
-void MC_ignore_heap(void *address, size_t size)
-{
-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
-  mc_heap_ignore_region_t region = xbt_new0(s_mc_heap_ignore_region_t, 1);
-  region->address = address;
-  region->size = size;
-
-  region->block =
-      ((char *) address -
-       (char *) std_heap->heapbase) / BLOCKSIZE + 1;
-
-  if (std_heap->heapinfo[region->block].type == 0) {
-    region->fragment = -1;
-    std_heap->heapinfo[region->block].busy_block.ignore++;
-  } else {
-    region->fragment =
-        ((uintptr_t) (ADDR2UINT(address) % (BLOCKSIZE))) >> std_heap->
-        heapinfo[region->block].type;
-    std_heap->heapinfo[region->block].busy_frag.ignore[region->fragment]++;
-  }
-
-  MC_heap_region_ignore_insert(region);
-
-#if 1
-  if (mc_mode == MC_MODE_CLIENT)
-    MC_heap_region_ignore_send(region);
-#endif
-  mmalloc_set_current_heap(heap);
-}
-

 void MC_remove_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));
+  if (mc_mode != MC_MODE_CLIENT)

     return;
     return;

-  }
-
-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);

 
 

-  unsigned int cursor = 0;
-  int start = 0;
-  int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
-  mc_heap_ignore_region_t region;
-  int ignore_found = 0;
-
-  while (start <= end) {
-    cursor = (start + end) / 2;
-    region =
-        (mc_heap_ignore_region_t) xbt_dynar_get_as(mc_heap_comparison_ignore,
-                                                   cursor,
-                                                   mc_heap_ignore_region_t);
-    if (region->address == address) {
-      ignore_found = 1;
-      break;
-    } else if (region->address < address) {
-      start = cursor + 1;
-    } else {
-      if ((char *) region->address <= ((char *) address + size)) {
-        ignore_found = 1;
-        break;
-      } else {
-        end = cursor - 1;
-      }
-    }
-  }
-
-  if (ignore_found == 1) {
-    xbt_dynar_remove_at(mc_heap_comparison_ignore, cursor, NULL);
-    MC_remove_ignore_heap(address, size);
-  }
-  mmalloc_set_current_heap(heap);
+  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));

 }
 
 }
 

-// MCer
+// ***** Model-checker:
+

 void MC_ignore_global_variable(const char *name)
 {
   mc_process_t process = &mc_model_checker->process();
 void MC_ignore_global_variable(const char *name)
 {
   mc_process_t process = &mc_model_checker->process();

diff --git a/src/mc/mc_ignore.h b/src/mc/mc_ignore.h
index fef9bcd..a5a6032 100644 (file)
--- a/src/mc/mc_ignore.h
+++ b/src/mc/mc_ignore.h
@@ -12,11 +12,9 @@
 
 SG_BEGIN_DECL();
 
 
 SG_BEGIN_DECL();
 

-void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region);

 void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size);
 void MC_stack_area_add(stack_region_t stack_area);
 
 xbt_dynar_t MC_checkpoint_ignore_new(void);
 
 void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size);
 void MC_stack_area_add(stack_region_t stack_area);
 
 xbt_dynar_t MC_checkpoint_ignore_new(void);
 

-

 SG_END_DECL();
 SG_END_DECL();

diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp
index 41be27f..b7cc85d 100644 (file)
--- a/src/mc/mc_liveness.cpp
+++ b/src/mc/mc_liveness.cpp
@@ -44,9 +44,8 @@ static xbt_dynar_t get_atomic_propositions_values()
   return values;
 }
 
   return values;
 }
 

-static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair) {
-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
+static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair)
+{

   mc_visited_pair_t new_pair = NULL;
   new_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
   new_pair->acceptance_pair = 1;
   mc_visited_pair_t new_pair = NULL;
   new_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
   new_pair->acceptance_pair = 1;


@@ -69,8 +68,6 @@ static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair) {
       // Parallell implementation
       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(acceptance_pairs, min), (max-min)+1, pair);
          if(res != -1){
       // Parallell implementation
       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(acceptance_pairs, min), (max-min)+1, pair);
          if(res != -1){

-         if(!raw_mem_set)
-         MC_SET_STD_HEAP;

          return ((mc_pair_t)xbt_dynar_get_as(acceptance_pairs, (min+res)-1, mc_pair_t))->num;
          } */
 
          return ((mc_pair_t)xbt_dynar_get_as(acceptance_pairs, (min+res)-1, mc_pair_t))->num;
          } */
 


@@ -85,7 +82,6 @@ static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair) {
                 xbt_fifo_shift(mc_stack);
                 if (dot_output != NULL)
                   fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);
                 xbt_fifo_shift(mc_stack);
                 if (dot_output != NULL)
                   fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, pair_test->num, initial_global_state->prev_req);

-                mmalloc_set_current_heap(heap);

                 return NULL;
               }
             }
                 return NULL;
               }
             }


@@ -105,16 +101,12 @@ static mc_visited_pair_t is_reached_acceptance_pair(mc_pair_t pair) {
           xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
       }
     }
           xbt_dynar_insert_at(acceptance_pairs, index, &new_pair);
       }
     }

-

   }
   }

-  mmalloc_set_current_heap(heap);

   return new_pair;
 }
 
 static void remove_acceptance_pair(int pair_num)
 {
   return new_pair;
 }
 
 static void remove_acceptance_pair(int pair_num)
 {

-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-

   unsigned int cursor = 0;
   mc_visited_pair_t pair_test = NULL;
   int pair_found = 0;
   unsigned int cursor = 0;
   mc_visited_pair_t pair_test = NULL;
   int pair_found = 0;


@@ -135,8 +127,6 @@ static void remove_acceptance_pair(int pair_num)
       MC_visited_pair_delete(pair_test);
 
   }
       MC_visited_pair_delete(pair_test);
 
   }

-
-  mmalloc_set_current_heap(heap);

 }
 
 
 }
 
 


@@ -187,8 +177,6 @@ static void MC_pre_modelcheck_liveness(void)
 
   MC_wait_for_requests();
 
 
   MC_wait_for_requests();
 

-  MC_SET_MC_HEAP;
-

   acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
   if(_sg_mc_visited > 0)
     visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
   acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
   if(_sg_mc_visited > 0)
     visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);


@@ -222,12 +210,7 @@ static void MC_pre_modelcheck_liveness(void)
     }
   }
 
     }
   }
 

-  MC_SET_STD_HEAP;
-  

   MC_modelcheck_liveness_main();
   MC_modelcheck_liveness_main();

-
-  if (initial_global_state->raw_mem_set)
-    MC_SET_MC_HEAP;

 }
 
 static void MC_modelcheck_liveness_main(void)
 }
 
 static void MC_modelcheck_liveness_main(void)


@@ -277,16 +260,12 @@ static void MC_modelcheck_liveness_main(void)
       if ((current_pair->exploration_started == 0) && (visited_num = is_visited_pair(reached_pair, current_pair)) != -1) {
 
         if (dot_output != NULL){
       if ((current_pair->exploration_started == 0) && (visited_num = is_visited_pair(reached_pair, current_pair)) != -1) {
 
         if (dot_output != NULL){

-          MC_SET_MC_HEAP;

           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, visited_num, initial_global_state->prev_req);
           fflush(dot_output);
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, visited_num, initial_global_state->prev_req);
           fflush(dot_output);

-          MC_SET_STD_HEAP;

         }
 
         XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);
         }
 
         XBT_DEBUG("Pair already visited (equal to pair %d), exploration on the current path stopped.", visited_num);

-        MC_SET_MC_HEAP;

         current_pair->requests = 0;
         current_pair->requests = 0;

-        MC_SET_STD_HEAP;

         goto backtracking;
         
       }else{
         goto backtracking;
         
       }else{


@@ -294,7 +273,6 @@ static void MC_modelcheck_liveness_main(void)
         req = MC_state_get_request(current_pair->graph_state, &value);
 
          if (dot_output != NULL) {
         req = MC_state_get_request(current_pair->graph_state, &value);
 
          if (dot_output != NULL) {

-           MC_SET_MC_HEAP;

            if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
              fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, current_pair->num, initial_global_state->prev_req);
              xbt_free(initial_global_state->prev_req);
            if (initial_global_state->prev_pair != 0 && initial_global_state->prev_pair != current_pair->num) {
              fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_global_state->prev_pair, current_pair->num, initial_global_state->prev_req);
              xbt_free(initial_global_state->prev_req);


@@ -304,7 +282,6 @@ static void MC_modelcheck_liveness_main(void)
            if (current_pair->search_cycle)
              fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
            fflush(dot_output);
            if (current_pair->search_cycle)
              fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
            fflush(dot_output);

-           MC_SET_STD_HEAP;

          }
 
          char* req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX); 
          }
 
          char* req_str = MC_request_to_string(req, value, MC_REQUEST_SIMIX); 


@@ -325,8 +302,6 @@ static void MC_modelcheck_liveness_main(void)
          /* Wait for requests (schedules processes) */
          MC_wait_for_requests();
 
          /* Wait for requests (schedules processes) */
          MC_wait_for_requests();
 

-         MC_SET_MC_HEAP;
-

          current_pair->requests--;
          current_pair->exploration_started = 1;
 
          current_pair->requests--;
          current_pair->exploration_started = 1;
 


@@ -363,9 +338,7 @@ static void MC_modelcheck_liveness_main(void)
            }
            cursor--;
          }
            }
            cursor--;
          }

-         
-         MC_SET_STD_HEAP;
-        
+

       } /* End of visited_pair test */
       
     } else {
       } /* End of visited_pair test */
       
     } else {


@@ -374,8 +347,6 @@ static void MC_modelcheck_liveness_main(void)
       if(visited_num == -1)
         XBT_DEBUG("No more request to execute. Looking for backtracking point.");
     
       if(visited_num == -1)
         XBT_DEBUG("No more request to execute. Looking for backtracking point.");
     

-      MC_SET_MC_HEAP;
-    

       xbt_dynar_free(&prop_values);
     
       /* Traverse the stack backwards until a pair with a non empty interleave
       xbt_dynar_free(&prop_values);
     
       /* Traverse the stack backwards until a pair with a non empty interleave


@@ -385,7 +356,6 @@ static void MC_modelcheck_liveness_main(void)
           /* We found a backtracking point */
           XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
           xbt_fifo_unshift(mc_stack, current_pair);
           /* We found a backtracking point */
           XBT_DEBUG("Backtracking to depth %d", current_pair->depth);
           xbt_fifo_unshift(mc_stack, current_pair);

-          MC_SET_STD_HEAP;

           MC_replay_liveness(mc_stack);
           XBT_DEBUG("Backtracking done");
           break;
           MC_replay_liveness(mc_stack);
           XBT_DEBUG("Backtracking done");
           break;


@@ -397,8 +367,7 @@ static void MC_modelcheck_liveness_main(void)
           MC_pair_delete(current_pair);
         }
       }
           MC_pair_delete(current_pair);
         }
       }

-    
-      MC_SET_STD_HEAP;
+

     } /* End of if (current_pair->requests > 0) else ... */
     
   } /* End of while(xbt_fifo_size(mc_stack) > 0) */
     } /* End of if (current_pair->requests > 0) else ... */
     
   } /* End of while(xbt_fifo_size(mc_stack) > 0) */


@@ -416,24 +385,17 @@ void MC_modelcheck_liveness(void)
   XBT_DEBUG("Starting the liveness algorithm");
   _sg_mc_liveness = 1;
 
   XBT_DEBUG("Starting the liveness algorithm");
   _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);
 
   /* 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);
   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_mmalloc.h b/src/mc/mc_mmalloc.h
index b59d7d7..6aa7d61 100644 (file)
--- a/src/mc/mc_mmalloc.h
+++ b/src/mc/mc_mmalloc.h
@@ -35,9 +35,6 @@ extern xbt_mheap_t mc_heap;
 /*   size_t bytes_free;            /\* Byte total of chunks in the free list. *\/ */
 /* }; */
 
 /*   size_t bytes_free;            /\* Byte total of chunks in the free list. *\/ */
 /* }; */
 

-#define MC_SET_MC_HEAP    mmalloc_set_current_heap(mc_heap)
-#define MC_SET_STD_HEAP  mmalloc_set_current_heap(std_heap)
-

 SG_END_DECL()
 
 #endif
 SG_END_DECL()
 
 #endif

diff --git a/src/mc/mc_process.cpp b/src/mc/mc_process.cpp
index 31e79cf..5dbbddd 100644 (file)
--- a/src/mc/mc_process.cpp
+++ b/src/mc/mc_process.cpp
@@ -157,9 +157,7 @@ void MC_process_refresh_heap(mc_process_t process)
   assert(!MC_process_is_self(process));
   // Read/dereference/refresh the std_heap pointer:
   if (!process->heap) {
   assert(!MC_process_is_self(process));
   // Read/dereference/refresh the std_heap pointer:
   if (!process->heap) {

-    xbt_mheap_t oldheap  = mmalloc_set_current_heap(mc_heap);

     process->heap = (struct mdesc*) malloc(sizeof(struct mdesc));
     process->heap = (struct mdesc*) malloc(sizeof(struct mdesc));

-    mmalloc_set_current_heap(oldheap);

   }
   MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
     process->heap, process->heap_address, sizeof(struct mdesc),
   }
   MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
     process->heap, process->heap_address, sizeof(struct mdesc),


@@ -175,11 +173,7 @@ void MC_process_refresh_malloc_info(mc_process_t process)
   // Refresh process->heapinfo:
   size_t malloc_info_bytesize =
     (process->heap->heaplimit + 1) * sizeof(malloc_info);
   // Refresh process->heapinfo:
   size_t malloc_info_bytesize =
     (process->heap->heaplimit + 1) * sizeof(malloc_info);

-
-  xbt_mheap_t heap  = mmalloc_set_current_heap(mc_heap);

   process->heap_info = (malloc_info*) realloc(process->heap_info, malloc_info_bytesize);
   process->heap_info = (malloc_info*) realloc(process->heap_info, malloc_info_bytesize);

-  mmalloc_set_current_heap(heap);
-

   MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
     process->heap_info,
     process->heap->heapinfo, malloc_info_bytesize,
   MC_process_read(process, MC_ADDRESS_SPACE_READ_FLAGS_NONE,
     process->heap_info,
     process->heap->heapinfo, malloc_info_bytesize,

diff --git a/src/mc/mc_safety.cpp b/src/mc/mc_safety.cpp
index f05de06..2e89053 100644 (file)
--- a/src/mc/mc_safety.cpp
+++ b/src/mc/mc_safety.cpp
@@ -40,13 +40,10 @@ static int is_exploration_stack_state(mc_state_t current_state){
  */
 static void MC_pre_modelcheck_safety()
 {
  */
 static void MC_pre_modelcheck_safety()
 {

-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-

   if (_sg_mc_visited > 0)
     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
 
   mc_state_t initial_state = MC_state_new();
   if (_sg_mc_visited > 0)
     visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp);
 
   mc_state_t initial_state = MC_state_new();

-  MC_SET_STD_HEAP;

 
   XBT_DEBUG("**************************************************");
   XBT_DEBUG("Initial state");
 
   XBT_DEBUG("**************************************************");
   XBT_DEBUG("Initial state");


@@ -54,8 +51,6 @@ static void MC_pre_modelcheck_safety()
   /* Wait for requests (schedules processes) */
   MC_wait_for_requests();
 
   /* Wait for requests (schedules processes) */
   MC_wait_for_requests();
 

-  MC_SET_MC_HEAP;
-

   /* Get an enabled process and insert it in the interleave set of the initial state */
   smx_process_t process;
   MC_EACH_SIMIX_PROCESS(process,
   /* Get an enabled process and insert it in the interleave set of the initial state */
   smx_process_t process;
   MC_EACH_SIMIX_PROCESS(process,


@@ -67,7 +62,6 @@ static void MC_pre_modelcheck_safety()
   );
 
   xbt_fifo_unshift(mc_stack, initial_state);
   );
 
   xbt_fifo_unshift(mc_stack, initial_state);

-  mmalloc_set_current_heap(heap);

 }
 
 
 }
 
 


@@ -107,9 +101,7 @@ static void MC_modelcheck_safety_main(void)
       xbt_free(req_str);
 
       if (dot_output != NULL) {
       xbt_free(req_str);
 
       if (dot_output != NULL) {

-        MC_SET_MC_HEAP;

         req_str = MC_request_get_dot_output(req, value);
         req_str = MC_request_get_dot_output(req, value);

-        MC_SET_STD_HEAP;

       }
 
       MC_state_set_executed_request(state, req, value);
       }
 
       MC_state_set_executed_request(state, req, value);


@@ -123,8 +115,6 @@ static void MC_modelcheck_safety_main(void)
       MC_wait_for_requests();
 
       /* Create the new expanded state */
       MC_wait_for_requests();
 
       /* Create the new expanded state */

-      MC_SET_MC_HEAP;
-

       next_state = MC_state_new();
 
       if(_sg_mc_termination && is_exploration_stack_state(next_state)){
       next_state = MC_state_new();
 
       if(_sg_mc_termination && is_exploration_stack_state(next_state)){


@@ -159,8 +149,6 @@ static void MC_modelcheck_safety_main(void)
       if (dot_output != NULL)
         xbt_free(req_str);
 
       if (dot_output != NULL)
         xbt_free(req_str);
 

-      MC_SET_STD_HEAP;
-

       /* Let's loop again */
 
       /* The interleave set is empty or the maximum depth is reached, let's back-track */
       /* Let's loop again */
 
       /* The interleave set is empty or the maximum depth is reached, let's back-track */


@@ -181,15 +169,11 @@ static void MC_modelcheck_safety_main(void)
 
       }
 
 
       }
 

-      MC_SET_MC_HEAP;
-

       /* Trash the current state, no longer needed */
       xbt_fifo_shift(mc_stack);
       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
       MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 
       /* Trash the current state, no longer needed */
       xbt_fifo_shift(mc_stack);
       XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
       MC_state_delete(state, !state->in_visited_states ? 1 : 0);
 

-      MC_SET_STD_HEAP;
-

       visited_state = NULL;
 
       /* Check for deadlocks */
       visited_state = NULL;
 
       /* Check for deadlocks */


@@ -198,7 +182,6 @@ static void MC_modelcheck_safety_main(void)
         return;
       }
 
         return;
       }
 

-      MC_SET_MC_HEAP;

       /* Traverse the stack backwards until a state with a non empty interleave
          set is found, deleting all the states that have it empty in the way.
          For each deleted state, check if the request that has generated it 
       /* Traverse the stack backwards until a state with a non empty interleave
          set is found, deleting all the states that have it empty in the way.
          For each deleted state, check if the request that has generated it 


@@ -261,12 +244,9 @@ static void MC_modelcheck_safety_main(void)
           MC_state_delete(state, !state->in_visited_states ? 1 : 0);
         }
       }
           MC_state_delete(state, !state->in_visited_states ? 1 : 0);
         }
       }

-      MC_SET_STD_HEAP;

     }
   }
   MC_print_statistics(mc_stats);
     }
   }
   MC_print_statistics(mc_stats);

-  MC_SET_STD_HEAP;
-

   return;
 }
 
   return;
 }
 


@@ -287,25 +267,17 @@ void MC_modelcheck_safety(void)
 
   _sg_mc_safety = 1;
 
 
   _sg_mc_safety = 1;
 

-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-

   /* Create exploration stack */
   mc_stack = xbt_fifo_new();
 
   /* Create exploration stack */
   mc_stack = xbt_fifo_new();
 

-  MC_SET_STD_HEAP;
-

   MC_pre_modelcheck_safety();
 
   MC_pre_modelcheck_safety();
 

-  MC_SET_MC_HEAP;

   /* Save the initial state */
   initial_global_state = xbt_new0(s_mc_global_t, 1);
   initial_global_state->snapshot = MC_take_snapshot(0);
   /* Save the initial state */
   initial_global_state = xbt_new0(s_mc_global_t, 1);
   initial_global_state->snapshot = MC_take_snapshot(0);

-  MC_SET_STD_HEAP;

 
   MC_modelcheck_safety_main();
 
 
   MC_modelcheck_safety_main();
 

-  mmalloc_set_current_heap(heap);
-

   xbt_abort();
   //MC_exit();
 }
   xbt_abort();
   //MC_exit();
 }

diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp
index deffb42..cf45be1 100644 (file)
--- a/src/mc/mc_server.cpp
+++ b/src/mc/mc_server.cpp
@@ -20,6 +20,7 @@
 #include "mc_server.h"
 #include "mc_private.h"
 #include "mc_ignore.h"
 #include "mc_server.h"
 #include "mc_private.h"
 #include "mc_ignore.h"

+#include "mcer_ignore.h"

 
 extern "C" {
 
 
 extern "C" {
 


@@ -186,7 +187,7 @@ bool s_mc_server::handle_events()
           if (size != sizeof(message))
             xbt_die("Broken messsage");
           memcpy(&message, buffer, sizeof(message));
           if (size != sizeof(message))
             xbt_die("Broken messsage");
           memcpy(&message, buffer, sizeof(message));

-          MC_remove_ignore_heap(message.addr, message.size);
+          MC_heap_region_ignore_remove(message.addr, message.size);

           break;
         }
 
           break;
         }
 

diff --git a/src/mc/mc_smx.cpp b/src/mc/mc_smx.cpp
index 12d9216..b203933 100644 (file)
--- a/src/mc/mc_smx.cpp
+++ b/src/mc/mc_smx.cpp
@@ -19,11 +19,7 @@ static
 void MC_smx_process_info_clear(mc_smx_process_info_t p)
 {
   p->hostname = NULL;
 void MC_smx_process_info_clear(mc_smx_process_info_t p)
 {
   p->hostname = NULL;

-
-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);

   free(p->name);
   free(p->name);

-  mmalloc_set_current_heap(heap);
-

   p->name = NULL;
 }
 
   p->name = NULL;
 }
 


@@ -93,8 +89,6 @@ void MC_process_smx_refresh(mc_process_t process)
   if (process->cache_flags & MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES)
     return;
 
   if (process->cache_flags & MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES)
     return;
 

-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-

   // TODO, avoid to reload `&simix_global`, `simix_global`, `*simix_global`
 
   // simix_global_p = REMOTE(simix_global);
   // TODO, avoid to reload `&simix_global`, `simix_global`, `*simix_global`
 
   // simix_global_p = REMOTE(simix_global);


@@ -112,7 +106,6 @@ void MC_process_smx_refresh(mc_process_t process)
     process, process->smx_old_process_infos, simix_global.process_to_destroy);
 
   process->cache_flags |= MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES;
     process, process->smx_old_process_infos, simix_global.process_to_destroy);
 
   process->cache_flags |= MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES;

-  mmalloc_set_current_heap(heap);

 }
 
 /** Get the issuer of a simcall (`req->issuer`)
 }
 
 /** Get the issuer of a simcall (`req->issuer`)


@@ -212,9 +205,7 @@ const char* MC_smx_process_get_name(smx_process_t p)
 
   mc_smx_process_info_t info = MC_smx_process_get_info(p);
   if (!info->name) {
 
   mc_smx_process_info_t info = MC_smx_process_get_info(p);
   if (!info->name) {

-    xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);

     info->name = MC_process_read_string(process, p->name);
     info->name = MC_process_read_string(process, p->name);

-    mmalloc_set_current_heap(heap);

   }
   return info->name;
 }
   }
   return info->name;
 }

diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp
index 968965f..bd6cb0a 100644 (file)
--- a/src/mc/mc_visited.cpp
+++ b/src/mc/mc_visited.cpp
@@ -147,9 +147,6 @@ void MC_visited_pair_delete(mc_visited_pair_t p)
  */
 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
 {
  */
 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
 {

-
-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-

   int cursor = 0, previous_cursor;
   int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
   void *ref_test;
   int cursor = 0, previous_cursor;
   int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
   void *ref_test;


@@ -219,13 +216,10 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
           *max = next_cursor;
           next_cursor++;
         }
           *max = next_cursor;
           next_cursor++;
         }

-        mmalloc_set_current_heap(heap);

         return -1;
       }
     }
   }
         return -1;
       }
     }
   }

-
-  mmalloc_set_current_heap(heap);

   return cursor;
 }
 
   return cursor;
 }
 


@@ -257,8 +251,6 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
     }
   }
 
     }
   }
 

-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-

   mc_visited_state_t new_state = visited_state_new();
   graph_state->system_state = new_state->system_state;
   graph_state->in_visited_states = 1;
   mc_visited_state_t new_state = visited_state_new();
   graph_state->system_state = new_state->system_state;
   graph_state->in_visited_states = 1;


@@ -267,7 +259,6 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
   if (xbt_dynar_is_empty(visited_states)) {
 
     xbt_dynar_push(visited_states, &new_state);
   if (xbt_dynar_is_empty(visited_states)) {
 
     xbt_dynar_push(visited_states, &new_state);

-    mmalloc_set_current_heap(heap);

     return NULL;
 
   } else {
     return NULL;
 
   } else {


@@ -295,8 +286,6 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
          XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
          xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
          xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
          XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
          xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
          xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);

-         if(!raw_mem_set)
-         MC_SET_STD_HEAP;

          return new_state->other_num;
          } */
 
          return new_state->other_num;
          } */
 


@@ -325,7 +314,6 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
             xbt_dynar_insert_at(visited_states, cursor, &new_state);
             XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
 
             xbt_dynar_insert_at(visited_states, cursor, &new_state);
             XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
 

-            mmalloc_set_current_heap(heap);

             return state_test;
           }
           cursor++;
             return state_test;
           }
           cursor++;


@@ -373,7 +361,6 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
     }
 
       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
     }
 

-    mmalloc_set_current_heap(heap);

     return NULL;
   }
 }
     return NULL;
   }
 }


@@ -386,8 +373,6 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
   if (_sg_mc_visited == 0)
     return -1;
 
   if (_sg_mc_visited == 0)
     return -1;
 

-  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-

   mc_visited_pair_t new_visited_pair = NULL;
 
   if (visited_pair == NULL) {
   mc_visited_pair_t new_visited_pair = NULL;
 
   if (visited_pair == NULL) {


@@ -433,8 +418,6 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
          MC_pair_delete(pair_test);
          }
          }
          MC_pair_delete(pair_test);
          }
          }

-         if(!raw_mem_set)
-         MC_SET_STD_HEAP;

          return pair->other_num;
          } */
       cursor = min;
          return pair->other_num;
          } */
       cursor = min;


@@ -460,7 +443,6 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
               } else {
                 MC_visited_pair_delete(pair_test);
               }
               } else {
                 MC_visited_pair_delete(pair_test);
               }

-              mmalloc_set_current_heap(heap);

               return new_visited_pair->other_num;
             }
           }
               return new_visited_pair->other_num;
             }
           }


@@ -501,8 +483,6 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
     }
 
   }
     }
 
   }

-
-  mmalloc_set_current_heap(heap);

   return -1;
 }
 
   return -1;
 }
 

diff --git a/src/mc/mcer_ignore.cpp b/src/mc/mcer_ignore.cpp
new file mode 100644 (file)
index 0000000..d813e73
--- /dev/null
+++ b/src/mc/mcer_ignore.cpp
@@ -0,0 +1,97 @@
+/* Copyright (c) 2008-2015. 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. */
+
+#include "internal_config.h"
+#include "mc_object_info.h"
+#include "mc/mc_private.h"
+#include "smpi/private.h"
+#include "mc/mc_snapshot.h"
+#include "mc/mc_ignore.h"
+#include "mc/mc_protocol.h"
+#include "mc/mc_client.h"
+
+extern "C" {
+
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mcer_ignore, mc,
+                                "Logging specific to MC ignore mechanism");
+
+extern xbt_dynar_t mc_heap_comparison_ignore;
+
+void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region)
+{
+  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);
+    return;
+  }
+
+  unsigned int cursor = 0;
+  mc_heap_ignore_region_t current_region = NULL;
+  int start = 0;
+  int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
+
+  // Find the position where we want to insert the mc_heap_ignore_region_t:
+  while (start <= end) {
+    cursor = (start + end) / 2;
+    current_region =
+        (mc_heap_ignore_region_t) xbt_dynar_get_as(mc_heap_comparison_ignore,
+                                                   cursor,
+                                                   mc_heap_ignore_region_t);
+    if (current_region->address == region->address) {
+      heap_ignore_region_free(region);
+      return;
+    } else if (current_region->address < region->address) {
+      start = cursor + 1;
+    } else {
+      end = cursor - 1;
+    }
+  }
+
+  // Insert it mc_heap_ignore_region_t:
+  if (current_region->address < region->address)
+    xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, &region);
+  else
+    xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
+}
+
+void MC_heap_region_ignore_remove(void *address, size_t size)
+{
+  unsigned int cursor = 0;
+  int start = 0;
+  int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
+  mc_heap_ignore_region_t region;
+  int ignore_found = 0;
+
+  while (start <= end) {
+    cursor = (start + end) / 2;
+    region =
+        (mc_heap_ignore_region_t) xbt_dynar_get_as(mc_heap_comparison_ignore,
+                                                   cursor,
+                                                   mc_heap_ignore_region_t);
+    if (region->address == address) {
+      ignore_found = 1;
+      break;
+    } else if (region->address < address) {
+      start = cursor + 1;
+    } else {
+      if ((char *) region->address <= ((char *) address + size)) {
+        ignore_found = 1;
+        break;
+      } else {
+        end = cursor - 1;
+      }
+    }
+  }
+
+  if (ignore_found == 1) {
+    xbt_dynar_remove_at(mc_heap_comparison_ignore, cursor, NULL);
+    MC_remove_ignore_heap(address, size);
+  }
+}
+
+}

diff --git a/src/mc/mcer_ignore.h b/src/mc/mcer_ignore.h
new file mode 100644 (file)
index 0000000..9329362
--- /dev/null
+++ b/src/mc/mcer_ignore.h
@@ -0,0 +1,18 @@
+/* Copyright (c) 2015. 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. */
+
+#include <xbt/dynar.h>
+
+#include "mc/datatypes.h"
+#include "mc/mc_process.h"
+
+#include "xbt/misc.h"           /* SG_BEGIN_DECL */
+
+SG_BEGIN_DECL();
+
+void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region);
+void MC_heap_region_ignore_remove(void *address, size_t size);
+
+SG_END_DECL();

diff --git a/src/xbt/log.c b/src/xbt/log.c
index 42a2178..7cde20d 100644 (file)
--- a/src/xbt/log.c
+++ b/src/xbt/log.c
@@ -641,6 +641,7 @@ static void xbt_log_connect_categories(void)
   XBT_LOG_CONNECT(mc_dwarf);
   XBT_LOG_CONNECT(mc_hash);
   XBT_LOG_CONNECT(mc_ignore);
   XBT_LOG_CONNECT(mc_dwarf);
   XBT_LOG_CONNECT(mc_hash);
   XBT_LOG_CONNECT(mc_ignore);

+  XBT_LOG_CONNECT(mcer_ignore);

   XBT_LOG_CONNECT(mc_liveness);
   XBT_LOG_CONNECT(mc_memory);
   XBT_LOG_CONNECT(mc_memory_map);
   XBT_LOG_CONNECT(mc_liveness);
   XBT_LOG_CONNECT(mc_memory);
   XBT_LOG_CONNECT(mc_memory_map);