model-checker : get times elapsed for snasphot comparison

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index 0333aff..aec9b8c 100644 (file)
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -202,6 +202,14 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     }
   }
 
+  xbt_os_timer_t global_timer = xbt_os_timer_new();
+  xbt_os_timer_t timer = xbt_os_timer_new();
+
+  xbt_os_timer_start(global_timer);
+
+  if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug))
+    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);
@@ -212,12 +220,28 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     }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_os_timer_free(timer);
+      xbt_os_timer_stop(global_timer);
+      xbt_dynar_push_as(initial_state_liveness->snapshot_comparison_times, double, xbt_os_timer_elapsed(timer));
+      xbt_os_timer_free(global_timer);
+
       if(!raw_mem_set)
         MC_UNSET_RAW_MEM;
+
       return 1;
     }
   }
 
+  if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+    xbt_os_timer_stop(timer);
+    xbt_dynar_push_as(initial_state_liveness->chunks_used_comparison_times, double, xbt_os_timer_elapsed(timer));
+
+    XBT_DEBUG("Chunks used comparison : %f", xbt_os_timer_elapsed(timer));
+    
+    xbt_os_timer_start(timer);
+  }
+
   /* Compare size of stacks */
   unsigned int cursor = 0;
   void *addr_stack1, *addr_stack2;
@@ -237,6 +261,12 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       }else{
         if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
           XBT_VERB("Different size used in stacks : %zu - %zu", size_used1, size_used2);
+ 
+        xbt_os_timer_free(timer);
+        xbt_os_timer_stop(global_timer);
+        xbt_dynar_push_as(initial_state_liveness->snapshot_comparison_times, double, xbt_os_timer_elapsed(timer));
+        xbt_os_timer_free(global_timer);
+
         if(!raw_mem_set)
           MC_UNSET_RAW_MEM;
         return 1;
@@ -245,6 +275,14 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     cursor++;
   }
 
+  if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+    xbt_os_timer_stop(timer);
+    xbt_dynar_push_as(initial_state_liveness->stacks_sizes_comparison_times, double, xbt_os_timer_elapsed(timer));
+
+    XBT_DEBUG("Stacks sizes comparison : %f", xbt_os_timer_elapsed(timer));
+    
+    xbt_os_timer_start(timer);
+  }
 
   /* Compare program data segment(s) */
   i = data_program_index;
@@ -256,6 +294,12 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       }else{
         if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
           XBT_VERB("Different memcmp for data in program"); 
+
+        xbt_os_timer_free(timer);
+        xbt_os_timer_stop(global_timer);
+        xbt_dynar_push_as(initial_state_liveness->snapshot_comparison_times, double, xbt_os_timer_elapsed(timer));
+        xbt_os_timer_free(global_timer);
+
         if(!raw_mem_set)
           MC_UNSET_RAW_MEM;
         return 1;
@@ -264,6 +308,15 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     i++;
   }
 
+  if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+    xbt_os_timer_stop(timer);
+    xbt_dynar_push_as(initial_state_liveness->program_data_segment_comparison_times, double, xbt_os_timer_elapsed(timer));
+
+    XBT_DEBUG("Program data segment comparison : %f", xbt_os_timer_elapsed(timer));
+    
+    xbt_os_timer_start(timer);
+  }
+
   /* Compare libsimgrid data segment(s) */
   i = data_libsimgrid_index;
   while(i < s1->num_reg && s1->regions[i]->type == 1){
@@ -274,6 +327,12 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       }else{
         if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
           XBT_VERB("Different memcmp for data in libsimgrid");
+         
+        xbt_os_timer_free(timer);
+        xbt_os_timer_stop(global_timer);
+        xbt_dynar_push_as(initial_state_liveness->snapshot_comparison_times, double, xbt_os_timer_elapsed(timer));
+        xbt_os_timer_free(global_timer);
+        
         if(!raw_mem_set)
           MC_UNSET_RAW_MEM;
         return 1;
@@ -282,6 +341,15 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     i++;
   }
 
+  if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+    xbt_os_timer_stop(timer);
+    xbt_dynar_push_as(initial_state_liveness->libsimgrid_data_segment_comparison_times, double, xbt_os_timer_elapsed(timer));
+
+    XBT_DEBUG("Libsimgrid data segment comparison : %f", xbt_os_timer_elapsed(timer));
+    
+    xbt_os_timer_start(timer);
+  }
+
   /* 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);
@@ -296,18 +364,33 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
       errors++;
     }else{
 
+      xbt_os_timer_free(timer);
       xbt_dynar_free(&stacks1);
       xbt_dynar_free(&stacks2);
       xbt_dynar_free(&equals);
  
       if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
         XBT_VERB("Different heap (mmalloc_compare)");
+       
+      xbt_os_timer_stop(global_timer);
+      xbt_dynar_push_as(initial_state_liveness->snapshot_comparison_times, double, xbt_os_timer_elapsed(timer));
+      xbt_os_timer_free(global_timer);
+
       if(!raw_mem_set)
         MC_UNSET_RAW_MEM;
       return 1;
     } 
   }
 
+  if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+    xbt_os_timer_stop(timer);
+    xbt_dynar_push_as(initial_state_liveness->heap_comparison_times, double, xbt_os_timer_elapsed(timer));
+
+    XBT_DEBUG("Heap comparison : %f", xbt_os_timer_elapsed(timer));
+    
+    xbt_os_timer_start(timer);
+  }
+
   /* Stacks comparison */
   cursor = 0;
   stack_region_t stack_region1, stack_region2;
@@ -334,6 +417,11 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
           if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_verbose))
             XBT_VERB("Different local variables between stacks %d", cursor + 1);
           
+          xbt_os_timer_free(timer);
+          xbt_os_timer_stop(global_timer);
+          xbt_dynar_push_as(initial_state_liveness->snapshot_comparison_times, double, xbt_os_timer_elapsed(timer));
+          xbt_os_timer_free(global_timer);
+          
           if(!raw_mem_set)
             MC_UNSET_RAW_MEM;
 
@@ -347,6 +435,20 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
   xbt_dynar_free(&stacks1);
   xbt_dynar_free(&stacks2);
   xbt_dynar_free(&equals);
+
+  if(XBT_LOG_ISENABLED(mc_compare, xbt_log_priority_debug)){
+    xbt_os_timer_stop(timer);
+    xbt_dynar_push_as(initial_state_liveness->stacks_comparison_times, double, xbt_os_timer_elapsed(timer));
+
+    XBT_DEBUG("Stacks comparison : %f", xbt_os_timer_elapsed(timer));
+    
+    xbt_os_timer_free(timer);
+  }
+
+  xbt_os_timer_stop(global_timer);
+  xbt_dynar_push_as(initial_state_liveness->snapshot_comparison_times, double, xbt_os_timer_elapsed(timer));
+  xbt_os_timer_free(global_timer);
+
   if(!raw_mem_set)
     MC_UNSET_RAW_MEM;
 

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 8108d3d..a42b115 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -204,6 +204,13 @@ void MC_init_liveness(){
   MC_get_local_variables(ls_path, libsimgrid_location_list, &mc_local_variables);
 
   initial_state_liveness = xbt_new0(s_mc_global_t, 1);
+  initial_state_liveness->snapshot_comparison_times = xbt_dynar_new(sizeof(double), NULL);
+  initial_state_liveness->chunks_used_comparison_times = xbt_dynar_new(sizeof(double), NULL);
+  initial_state_liveness->stacks_sizes_comparison_times = xbt_dynar_new(sizeof(double), NULL);
+  initial_state_liveness->program_data_segment_comparison_times = xbt_dynar_new(sizeof(double), NULL);
+  initial_state_liveness->libsimgrid_data_segment_comparison_times = xbt_dynar_new(sizeof(double), NULL);
+  initial_state_liveness->heap_comparison_times = xbt_dynar_new(sizeof(double), NULL);
+  initial_state_liveness->stacks_comparison_times = xbt_dynar_new(sizeof(double), NULL);
 
   MC_UNSET_RAW_MEM;
 

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 61dc577..f07cd97 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -44,6 +44,13 @@ typedef struct s_mc_snapshot_stack{
 
 typedef struct s_mc_global_t{
   mc_snapshot_t initial_snapshot;
+  xbt_dynar_t snapshot_comparison_times;
+  xbt_dynar_t chunks_used_comparison_times;
+  xbt_dynar_t stacks_sizes_comparison_times;
+  xbt_dynar_t program_data_segment_comparison_times;
+  xbt_dynar_t libsimgrid_data_segment_comparison_times;
+  xbt_dynar_t heap_comparison_times;
+  xbt_dynar_t stacks_comparison_times;
 }s_mc_global_t, *mc_global_t;
 
 void MC_take_snapshot(mc_snapshot_t);