X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/3a54b6d1aef3110883b46f912b3a4eeb5c9fb087..32fce378217eb6c3ea29b936cac8e231e4e3b184:/src/mc/mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 970ef80e3f..430da06f13 100644
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -138,9 +138,6 @@ void MC_do_the_modelcheck_for_real() {
   mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
   MC_UNSET_RAW_MEM;
   
-  if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
-    MC_init_dot_output();
-
   if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
     if (mc_reduce_kind==e_mc_reduce_unset)
       mc_reduce_kind=e_mc_reduce_dpor;
@@ -213,6 +210,9 @@ void MC_init(){
   MC_ignore_stack("next_context", "smx_ctx_sysv_suspend_serial");
   MC_ignore_stack("i", "smx_ctx_sysv_suspend_serial");
 
+  /* Ignore local variable about time used for tracing */
+  MC_ignore_stack("start_time", "*"); 
+
   MC_ignore_data_bss(&mc_comp_times, sizeof(mc_comp_times));
   MC_ignore_data_bss(&mc_snapshot_comparison_time, sizeof(mc_snapshot_comparison_time)); 
   MC_ignore_data_bss(&mc_time, sizeof(mc_time));
@@ -269,6 +269,9 @@ void MC_modelcheck_safety(void)
   /* Create exploration stack */
   mc_stack_safety = xbt_fifo_new();
 
+  if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
+    MC_init_dot_output();
+
   MC_UNSET_RAW_MEM;
 
   if(_sg_mc_visited > 0){
@@ -320,6 +323,9 @@ void MC_modelcheck_liveness(){
   /* Create the initial state */
   initial_state_liveness = xbt_new0(s_mc_global_t, 1);
 
+  if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
+    MC_init_dot_output();
+  
   MC_UNSET_RAW_MEM;
 
   MC_ddfs_init();
@@ -336,13 +342,6 @@ void MC_modelcheck_liveness(){
 
 void MC_exit(void)
 {
-  MC_SET_RAW_MEM;
-  if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
-    fprintf(dot_output, "}\n");
-    fclose(dot_output);
-  }
-  MC_UNSET_RAW_MEM;
-
   xbt_free(mc_time);
   MC_memory_exit();
   xbt_abort();
@@ -406,11 +405,12 @@ void MC_replay(xbt_fifo_t stack, int start)
 {
   int raw_mem = (mmalloc_get_current_heap() == raw_heap);
 
-  int value, i = 1;
+  int value, i = 1, count = 1;
   char *req_str;
   smx_simcall_t req = NULL, saved_req = NULL;
   xbt_fifo_item_t item, start_item;
   mc_state_t state;
+  smx_process_t process = NULL;
 
   XBT_DEBUG("**** Begin Replay ****");
 
@@ -430,6 +430,19 @@ void MC_replay(xbt_fifo_t stack, int start)
     }
   }
 
+  MC_SET_RAW_MEM;
+  xbt_dict_reset(first_enabled_state);
+  xbt_swag_foreach(process, simix_global->process_list){
+    if(MC_process_is_enabled(process)){
+      char *key = bprintf("%lu", process->pid);
+      char *data = bprintf("%d", count);
+      xbt_dict_set(first_enabled_state, key, data, NULL);
+      xbt_free(key);
+    }
+  }
+  MC_UNSET_RAW_MEM;
+  
+
   /* Traverse the stack from the state at position start and re-execute the transitions */
   for (item = start_item;
        item != xbt_fifo_get_first_item(stack);
@@ -438,6 +451,12 @@ void MC_replay(xbt_fifo_t stack, int start)
     state = (mc_state_t) xbt_fifo_get_item_content(item);
     saved_req = MC_state_get_executed_request(state, &value);
    
+    MC_SET_RAW_MEM;
+    char *key = bprintf("%lu", saved_req->issuer->pid);
+    xbt_dict_remove(first_enabled_state, key); 
+    xbt_free(key);
+    MC_UNSET_RAW_MEM;
+   
     if(saved_req){
       /* because we got a copy of the executed request, we have to fetch the  
          real one, pointed by the request field of the issuer process */
@@ -450,14 +469,32 @@ void MC_replay(xbt_fifo_t stack, int start)
         xbt_free(req_str);
       }
     }
-         
+    
     SIMIX_simcall_pre(req, value);
     MC_wait_for_requests();
+
+    count++;
+
+    MC_SET_RAW_MEM;
+    /* Insert in dict all enabled processes */
+    xbt_swag_foreach(process, simix_global->process_list){
+      if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
+        char *key = bprintf("%lu", process->pid);
+        if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
+          char *data = bprintf("%d", count);
+          xbt_dict_set(first_enabled_state, key, data, NULL);
+        }
+        xbt_free(key);
+      }
+    }
+    MC_UNSET_RAW_MEM;
          
     /* Update statistics */
     mc_stats->visited_states++;
     mc_stats->executed_transitions++;
+
   }
+
   XBT_DEBUG("**** End Replay ****");
 
   if(raw_mem)
@@ -527,7 +564,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
       depth++;
     
       /* Update statistics */
-      mc_stats->visited_states++;
+      mc_stats->visited_pairs++;
       mc_stats->executed_transitions++;
 
       item = xbt_fifo_get_prev_item(item);
@@ -570,7 +607,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
       depth++;
     
       /* Update statistics */
-      mc_stats->visited_states++;
+      mc_stats->visited_pairs++;
       mc_stats->executed_transitions++;
     }
   }  
@@ -692,14 +729,20 @@ void MC_dump_stack_liveness(xbt_fifo_t stack){
 
 void MC_print_statistics(mc_stats_t stats)
 {
-  //XBT_INFO("State space size ~= %lu", stats->state_size);
-  XBT_INFO("Expanded states = %lu", stats->expanded_states);
-  XBT_INFO("Visited states = %lu", stats->visited_states);
+  if(stats->expanded_pairs == 0){
+    XBT_INFO("Expanded states = %lu", stats->expanded_states);
+    XBT_INFO("Visited states = %lu", stats->visited_states);
+  }else{
+    XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
+    XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
+  }
   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
-  XBT_INFO("Expanded / Visited = %lf",
-           (double) stats->visited_states / stats->expanded_states);
-  /*XBT_INFO("Exploration coverage = %lf",
-    (double)stats->expanded_states / stats->state_size); */
+  MC_SET_RAW_MEM;
+  if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
+    fprintf(dot_output, "}\n");
+    fclose(dot_output);
+  }
+  MC_UNSET_RAW_MEM;
 }
 
 void MC_assert(int prop)
@@ -806,10 +849,10 @@ void MC_ignore_heap(void *address, size_t size){
   
   if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
     region->fragment = -1;
-    ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore = 1;
+    ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore++;
   }else{
     region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
-    ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment] = 1;
+    ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment]++;
   }
   
   if(mc_heap_comparison_ignore == NULL){
@@ -821,7 +864,7 @@ void MC_ignore_heap(void *address, size_t size){
   }
 
   unsigned int cursor = 0;
-  mc_heap_ignore_region_t current_region;
+  mc_heap_ignore_region_t current_region = NULL;
   int start = 0;
   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;