model-checker : get bytes used in std_heap instead of chunks used

diff --git a/include/xbt/mmalloc.h b/include/xbt/mmalloc.h
index c259bf6..0a5dade 100644 (file)
--- a/include/xbt/mmalloc.h
+++ b/include/xbt/mmalloc.h
@@ -73,6 +73,6 @@ void mmalloc_backtrace_display(void *addr);
 
 int is_free_area(void *area, xbt_mheap_t heap);
 
-size_t mmalloc_get_chunks_used(xbt_mheap_t);
+size_t mmalloc_get_bytes_used(xbt_mheap_t);
 
 #endif                          /* MMALLOC_H */

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 5fb0655..d0e92b6 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -161,7 +161,7 @@ mc_snapshot_t MC_take_snapshot()
       if (maps->regions[i].pathname == NULL){
         if (reg.start_addr == std_heap){ // only save the std heap (and not the raw one)
           MC_snapshot_add_region(snapshot, 0, reg.start_addr, (char*)reg.end_addr - (char*)reg.start_addr);
-          snapshot->heap_chunks_used = mmalloc_get_chunks_used(std_heap);
+          snapshot->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
           heap = snapshot->regions[snapshot->num_reg - 1]->data;
         }
         i++;

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 711fd83..047e7af 100644 (file)
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -225,16 +225,20 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     #endif
   }
 
-  /* Compare number of blocks/fragments used in each heap */
-  if(s1->heap_chunks_used != s2->heap_chunks_used){
+  #ifdef MC_DEBUG
+    xbt_os_timer_start(timer);
+  #endif
+
+  /* Compare number of bytes used in each heap */
+  if(s1->heap_bytes_used != s2->heap_bytes_used){
     #ifdef MC_DEBUG
       xbt_os_timer_stop(timer);
-      mc_comp_times->chunks_used_comparison_time = xbt_os_timer_elapsed(timer);
-      XBT_DEBUG("Different number of chunks used in each heap : %zu - %zu", s1->heap_chunks_used, s2->heap_chunks_used);
+      mc_comp_times->bytes_used_comparison_time = xbt_os_timer_elapsed(timer);
+      XBT_DEBUG("Different number of bytes used in each heap : %zu - %zu", s1->heap_bytes_used, s2->heap_bytes_used);
       errors++;
     #else
       #ifdef MC_VERBOSE
-        XBT_VERB("Different number of chunks used in each heap : %zu - %zu", s1->heap_chunks_used, s2->heap_chunks_used);
+        XBT_VERB("Different number of bytes used in each heap : %zu - %zu", s1->heap_bytes_used, s2->heap_bytes_used);
       #endif
 
       xbt_os_timer_free(timer);
@@ -648,7 +652,7 @@ int MC_compare_snapshots(void *s1, void *s2){
 void print_comparison_times(){
   XBT_DEBUG("*** Comparison times ***");
   XBT_DEBUG("- Nb processes : %f", mc_comp_times->nb_processes_comparison_time);
-  XBT_DEBUG("- Nb chunks used : %f", mc_comp_times->chunks_used_comparison_time);
+  XBT_DEBUG("- Nb bytes used : %f", mc_comp_times->bytes_used_comparison_time);
   XBT_DEBUG("- Stacks sizes : %f", mc_comp_times->stacks_sizes_comparison_time);
   XBT_DEBUG("- Binary global variables : %f", mc_comp_times->binary_global_variables_comparison_time);
   XBT_DEBUG("- Libsimgrid global variables : %f", mc_comp_times->libsimgrid_global_variables_comparison_time);

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index c3a3383..555144c 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -49,14 +49,14 @@ static int is_visited_state(){
 
     if(raw_mem_set)
       MC_SET_RAW_MEM;
- 
+
     return 0;
 
   }else{
 
     MC_SET_RAW_MEM;
     
-    size_t current_chunks_used = new_state->system_state->heap_chunks_used;
+    size_t current_bytes_used = new_state->system_state->heap_bytes_used;
 
     unsigned int cursor = 0;
     int previous_cursor = 0, next_cursor = 0;
@@ -64,19 +64,19 @@ static int is_visited_state(){
     int end = xbt_dynar_length(visited_states) - 1;
 
     mc_safety_visited_state_t state_test = NULL;
-    size_t chunks_used_test;
-    int same_chunks_not_found = 1;
+    size_t bytes_used_test;
+    int same_bytes_not_found = 1;
 
-    while(start <= end && same_chunks_not_found){
+    while(start <= end && same_bytes_not_found){
       cursor = (start + end) / 2;
       state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
-      chunks_used_test = state_test->system_state->heap_chunks_used;
-      if(chunks_used_test < current_chunks_used)
+      bytes_used_test = state_test->system_state->heap_bytes_used;
+      if(bytes_used_test < current_bytes_used)
         start = cursor + 1;
-      if(chunks_used_test > current_chunks_used)
+      if(bytes_used_test > current_bytes_used)
         end = cursor - 1; 
-      if(chunks_used_test == current_chunks_used){
-        same_chunks_not_found = 0;
+      if(bytes_used_test == current_bytes_used){
+        same_bytes_not_found = 0;
         if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
           xbt_dynar_remove_at(visited_states, cursor, NULL);
           xbt_dynar_insert_at(visited_states, cursor, &new_state);
@@ -86,12 +86,12 @@ static int is_visited_state(){
             MC_UNSET_RAW_MEM;
           return 1;
         }else{
-          /* Search another state with same number of chunks used */
+          /* Search another state with same number of bytes used */
           previous_cursor = cursor - 1;
           while(previous_cursor >= 0){
             state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_safety_visited_state_t);
-            chunks_used_test = state_test->system_state->heap_chunks_used;
-            if(chunks_used_test != current_chunks_used)
+            bytes_used_test = state_test->system_state->heap_bytes_used;
+            if(bytes_used_test != current_bytes_used)
               break;
             if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
               xbt_dynar_remove_at(visited_states, previous_cursor, NULL);
@@ -107,8 +107,8 @@ static int is_visited_state(){
           next_cursor = cursor + 1;
           while(next_cursor < xbt_dynar_length(visited_states)){
             state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_safety_visited_state_t);
-            chunks_used_test = state_test->system_state->heap_chunks_used;
-            if(chunks_used_test != current_chunks_used)
+            bytes_used_test = state_test->system_state->heap_bytes_used;
+            if(bytes_used_test != current_bytes_used)
               break;
             if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
               xbt_dynar_remove_at(visited_states, next_cursor, NULL);
@@ -126,9 +126,9 @@ static int is_visited_state(){
     }
 
     state_test = (mc_safety_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_safety_visited_state_t);
-    chunks_used_test = state_test->system_state->heap_chunks_used;
+    bytes_used_test = state_test->system_state->heap_bytes_used;
 
-    if(chunks_used_test < current_chunks_used)
+    if(bytes_used_test < current_bytes_used)
       xbt_dynar_insert_at(visited_states, cursor + 1, &new_state);
     else
       xbt_dynar_insert_at(visited_states, cursor, &new_state);

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index bf29aa9..0a8fd2f 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -36,7 +36,7 @@ typedef struct s_mc_mem_region{
 typedef struct s_mc_snapshot{
   unsigned int num_reg;
   int region_type[nb_regions];
-  size_t heap_chunks_used;
+  size_t heap_bytes_used;
   mc_mem_region_t *regions;
   size_t *stack_sizes;
   xbt_dynar_t stacks;
@@ -219,7 +219,7 @@ extern void *end_got_plt_binary;
 
 typedef struct s_mc_comparison_times{
   double nb_processes_comparison_time;
-  double chunks_used_comparison_time;
+  double bytes_used_comparison_time;
   double stacks_sizes_comparison_time;
   double binary_global_variables_comparison_time;
   double libsimgrid_global_variables_comparison_time;

diff --git a/src/xbt/mmalloc/mm_module.c b/src/xbt/mmalloc/mm_module.c
index 07cbe7e..0dfd027 100644 (file)
--- a/src/xbt/mmalloc/mm_module.c
+++ b/src/xbt/mmalloc/mm_module.c
@@ -344,6 +344,24 @@ void mmalloc_postexit(void)
   xbt_mheap_destroy_no_free(__mmalloc_default_mdp);
 }
 
-size_t mmalloc_get_chunks_used(xbt_mheap_t heap){
-  return ((struct mdesc *)heap)->heapstats.chunks_used;
+size_t mmalloc_get_bytes_used(xbt_mheap_t heap){
+  int i = 0, j = 0;
+  int bytes = 0;
+  
+  while(i<=((struct mdesc *)heap)->heaplimit){
+    if(((struct mdesc *)heap)->heapinfo[i].type == 0){
+      if(((struct mdesc *)heap)->heapinfo[i].busy_block.busy_size > 0)
+        bytes += ((struct mdesc *)heap)->heapinfo[i].busy_block.busy_size;
+     
+    }else if(((struct mdesc *)heap)->heapinfo[i].type > 0){
+      for(j=0; j < (size_t) (BLOCKSIZE >> ((struct mdesc *)heap)->heapinfo[i].type); j++){
+        if(((struct mdesc *)heap)->heapinfo[i].busy_frag.frag_size[j] > 0)
+          bytes += ((struct mdesc *)heap)->heapinfo[i].busy_frag.frag_size[j];
+      }
+    }
+    i++; 
+  }
+
+  return bytes;
 }
+