model-checker : add chunks used into snapshot structure and size used into stack...

diff --git a/src/mc/mc_checkpoint.c b/src/mc/mc_checkpoint.c
index 64d8c71..b3dd6ca 100644 (file)
--- a/src/mc/mc_checkpoint.c
+++ b/src/mc/mc_checkpoint.c
@@ -161,6 +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);
           heap = snapshot->regions[nb_reg]->data;
           nb_reg++;
         }
@@ -386,6 +387,7 @@ static xbt_dynar_t take_snapshot_stacks(void *heap){
     mc_snapshot_stack_t st = xbt_new(s_mc_snapshot_stack_t, 1);
     st->local_variables = get_local_variables_values(current_stack->context, heap);
     st->stack_pointer = get_stack_pointer(current_stack->context, heap);
+    st->size_used = current_stack->size - ((char *)st->stack_pointer - (char *)((char *)heap + ((char *)current_stack->address - (char *)std_heap)));
     xbt_dynar_push(res, &st);
   }
 

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 323c11f..81e075e 100644 (file)
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -217,20 +217,20 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
     xbt_os_timer_start(timer);
 
   /* Compare number of blocks/fragments used in each heap */
-  size_t chunks_used1 = mmalloc_get_chunks_used((xbt_mheap_t)s1->regions[heap_index]->data);
-  size_t chunks_used2 = mmalloc_get_chunks_used((xbt_mheap_t)s2->regions[heap_index]->data);
-  if(chunks_used1 != chunks_used2){
+
+  if(s1->heap_chunks_used != s2->heap_chunks_used){
+
     if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
       xbt_os_timer_stop(timer);
       if(ct1 != NULL)
         xbt_dynar_push_as(ct1->chunks_used_comparison_times, double, xbt_os_timer_elapsed(timer));
       if(ct2 != NULL)
         xbt_dynar_push_as(ct2->chunks_used_comparison_times, double, xbt_os_timer_elapsed(timer));
-      XBT_DEBUG("Different number of chunks used in each heap : %zu - %zu", chunks_used1, chunks_used2);
+      XBT_DEBUG("Different number of chunks used in each heap : %zu - %zu", s1->heap_chunks_used, s2->heap_chunks_used);
       errors++;
     }else{
       if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
-        XBT_VERB("Different number of chunks used in each heap : %zu - %zu", chunks_used1, chunks_used2);
+        XBT_VERB("Different number of chunks used in each heap : %zu - %zu", s1->heap_chunks_used, s2->heap_chunks_used);
      
       xbt_os_timer_free(timer);
       xbt_os_timer_stop(global_timer);
@@ -246,26 +246,22 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
       return 1;
     }
   }else{
+
     if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug))
       xbt_os_timer_stop(timer);
   }
   
   if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug))
     xbt_os_timer_start(timer);
-
+  
   /* Compare size of stacks */
+
   unsigned int cursor = 0;
-  void *addr_stack1, *addr_stack2;
-  void *sp1, *sp2;
   size_t size_used1, size_used2;
   int is_diff = 0;
   while(cursor < xbt_dynar_length(stacks_areas)){
-    addr_stack1 = (char *)s1->regions[heap_index]->data + ((char *)((stack_region_t)xbt_dynar_get_as(stacks_areas, cursor, stack_region_t))->address - (char *)std_heap);
-    addr_stack2 = (char *)s2->regions[heap_index]->data + ((char *)((stack_region_t)xbt_dynar_get_as(stacks_areas, cursor, stack_region_t))->address - (char *)std_heap);
-    sp1 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->stack_pointer;
-    sp2 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->stack_pointer;
-    size_used1 = ((stack_region_t)xbt_dynar_get_as(stacks_areas, cursor, stack_region_t))->size - ((char*)sp1 - (char*)addr_stack1);
-    size_used2 = ((stack_region_t)xbt_dynar_get_as(stacks_areas, cursor, stack_region_t))->size - ((char*)sp2 - (char*)addr_stack2);
+    size_used1 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->size_used;
+    size_used2 = ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->size_used;
     if(size_used1 != size_used2){
       if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
         if(is_diff == 0){
@@ -306,6 +302,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
   }
 
   /* Compare binary global variables */
+
   is_diff = compare_global_variables(s1->regions[data_program_index]->type, s1->regions[data_program_index]->data, s2->regions[data_program_index]->data);
   if(is_diff != 0){
     if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
@@ -330,6 +327,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
     
       if(!raw_mem)
         MC_UNSET_RAW_MEM;
+
       return 1;
     }
   }
@@ -338,9 +336,10 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
     if(is_diff == 0)
       xbt_os_timer_stop(timer);
     xbt_os_timer_start(timer);
-  }
+  } 
 
   /* Compare libsimgrid global variables */
+
   is_diff = compare_global_variables(s1->regions[data_libsimgrid_index]->type, s1->regions[data_libsimgrid_index]->data, s2->regions[data_libsimgrid_index]->data);
   if(is_diff != 0){
     if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
@@ -365,6 +364,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
     
       if(!raw_mem)
         MC_UNSET_RAW_MEM;
+
       return 1;
     }
   }  
@@ -376,6 +376,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
   }
 
   /* Compare heap */
+
   xbt_dynar_t stacks1 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
   xbt_dynar_t stacks2 = xbt_dynar_new(sizeof(stack_region_t), stack_region_free_voidp);
   xbt_dynar_t equals = xbt_dynar_new(sizeof(heap_equality_t), heap_equality_free_voidp);
@@ -411,6 +412,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
 
       if(!raw_mem)
         MC_UNSET_RAW_MEM;
+
       return 1;
     } 
   }else{
@@ -422,9 +424,11 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
     xbt_os_timer_start(timer);
 
   /* Stacks comparison */
+
   cursor = 0;
   stack_region_t stack_region1, stack_region2;
   int diff = 0, diff_local = 0;
+  void *sp1, *sp2;
   is_diff = 0;
 
   while(cursor < xbt_dynar_length(stacks1)){
@@ -474,8 +478,6 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t c
     cursor++;
   }
 
-  XBT_VERB("Chunks used after comparison of stacks : %zu", mmalloc_get_chunks_used(raw_heap));
-
   xbt_dynar_free(&stacks1);
   xbt_dynar_free(&stacks2);
   xbt_dynar_free(&equals);

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 017b0d0..b7a3569 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -56,7 +56,7 @@ static int is_visited_state(){
 
     MC_SET_RAW_MEM;
     
-    size_t current_chunks_used = mmalloc_get_chunks_used((xbt_mheap_t)(new_state->system_state)->regions[get_heap_region_index(new_state->system_state)]->data);
+    size_t current_chunks_used = new_state->system_state->heap_chunks_used;
 
     unsigned int cursor = 0;
     int previous_cursor = 0, next_cursor = 0;
@@ -70,7 +70,7 @@ static int is_visited_state(){
     while(start <= end && same_chunks_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 = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data);
+      chunks_used_test = state_test->system_state->heap_chunks_used;
       if(chunks_used_test < current_chunks_used)
         start = cursor + 1;
       if(chunks_used_test > current_chunks_used)
@@ -90,7 +90,7 @@ static int is_visited_state(){
           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 = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data);
+            chunks_used_test = state_test->system_state->heap_chunks_used;
             if(chunks_used_test != current_chunks_used)
               break;
             if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 0){
@@ -107,7 +107,7 @@ 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 = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data);
+            chunks_used_test = state_test->system_state->heap_chunks_used;
             if(chunks_used_test != current_chunks_used)
               break;
             if(snapshot_compare(new_state->system_state, state_test->system_state, NULL, NULL) == 0){
@@ -126,7 +126,7 @@ 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 = mmalloc_get_chunks_used((xbt_mheap_t)(state_test->system_state)->regions[get_heap_region_index(state_test->system_state)]->data);
+    chunks_used_test = state_test->system_state->heap_chunks_used;
 
     if(chunks_used_test < current_chunks_used)
       xbt_dynar_insert_at(visited_states, cursor + 1, &new_state);

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 84af06d..240839c 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -33,6 +33,7 @@ typedef struct s_mc_mem_region{
 
 typedef struct s_mc_snapshot{
   unsigned int num_reg;
+  size_t heap_chunks_used;
   mc_mem_region_t *regions;
   xbt_dynar_t stacks;
 } s_mc_snapshot_t, *mc_snapshot_t;
@@ -40,6 +41,7 @@ typedef struct s_mc_snapshot{
 typedef struct s_mc_snapshot_stack{
   xbt_strbuff_t local_variables;
   void *stack_pointer;
+  size_t size_used;
 }s_mc_snapshot_stack_t, *mc_snapshot_stack_t;
 
 typedef struct s_mc_global_t{