X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/3299a47e6bfb29938ceddb8e429d6d2105aabb04..eb5b6b0c3c4d9a38bb205b2c8bc9aeeba8674a25:/src/mc/mc_liveness.c

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 2ff658db94..cd1603bbc8 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -1,4 +1,4 @@
-/* Copyright (c) 2011-2013. The SimGrid Team.
+/* Copyright (c) 2011-2014. The SimGrid Team.
  * All rights reserved.                                                     */
 
 /* This program is free software; you can redistribute it and/or modify it
@@ -36,11 +36,15 @@ static xbt_dynar_t get_atomic_propositions_values(){
   return values;
 }
 
+/** \brief Find a suitable subrange of candidate duplicates for a given state
+ *
+ *  See mc_dpor.c with a similar (same?) function.
+ */
 static int get_search_interval(xbt_dynar_t all_pairs, mc_visited_pair_t pair, int *min, int *max){
 
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 
-  MC_SET_RAW_MEM;
+  MC_SET_MC_HEAP;
 
   int cursor = 0, previous_cursor, next_cursor;
   mc_visited_pair_t pair_test;
@@ -78,23 +82,23 @@ static int get_search_interval(xbt_dynar_t all_pairs, mc_visited_pair_t pair, in
           next_cursor++;
         }
         if(!raw_mem_set)
-          MC_UNSET_RAW_MEM;
+          MC_SET_STD_HEAP;
         return -1;
       }
      }
   }
 
   if(!raw_mem_set)
-    MC_UNSET_RAW_MEM;
+    MC_SET_STD_HEAP;
 
   return cursor;
 }
 
 static mc_visited_pair_t is_reached_acceptance_pair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){
 
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 
-  MC_SET_RAW_MEM;
+  MC_SET_MC_HEAP;
   
   mc_visited_pair_t pair = NULL;
   pair = MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
@@ -114,12 +118,15 @@ static mc_visited_pair_t is_reached_acceptance_pair(int pair_num, xbt_automaton_
     index = get_search_interval(acceptance_pairs, pair, &min, &max);
 
     if(min != -1 && max != -1){ // Acceptance pair with same number of processes and same heap bytes used exists
+
+      // 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_UNSET_RAW_MEM;
+          MC_SET_STD_HEAP;
         return ((mc_pair_t)xbt_dynar_get_as(acceptance_pairs, (min+res)-1, mc_pair_t))->num;
         }*/
+
       cursor = min;
       while(cursor <= max){
         pair_test = (mc_visited_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_visited_pair_t);
@@ -133,7 +140,7 @@ static mc_visited_pair_t is_reached_acceptance_pair(int pair_num, xbt_automaton_
                 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, pair_test->num, initial_state_liveness->prev_req);
 
               if(!raw_mem_set)
-                MC_UNSET_RAW_MEM;
+                MC_SET_STD_HEAP;
 
               return NULL;
             }
@@ -157,7 +164,7 @@ static mc_visited_pair_t is_reached_acceptance_pair(int pair_num, xbt_automaton_
   }
 
   if(!raw_mem_set)
-    MC_UNSET_RAW_MEM;
+    MC_SET_STD_HEAP;
 
   return pair;
  
@@ -165,9 +172,9 @@ static mc_visited_pair_t is_reached_acceptance_pair(int pair_num, xbt_automaton_
 
 static void remove_acceptance_pair(int pair_num){
 
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 
-  MC_SET_RAW_MEM;
+  MC_SET_MC_HEAP;
 
   unsigned int cursor = 0;
   mc_visited_pair_t pair_test = NULL;
@@ -189,17 +196,20 @@ static void remove_acceptance_pair(int pair_num){
   }
 
   if(!raw_mem_set)
-    MC_UNSET_RAW_MEM;
+    MC_SET_STD_HEAP;
 }
 
+/** \brief Checks whether a given state has already been visited by the algorithm.
+ *
+ */
 static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){
 
   if(_sg_mc_visited == 0)
     return -1;
 
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 
-  MC_SET_RAW_MEM;
+  MC_SET_MC_HEAP;
 
   mc_visited_pair_t new_pair = NULL;
 
@@ -247,7 +257,7 @@ static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_s
           }
         }
         if(!raw_mem_set)
-          MC_UNSET_RAW_MEM;
+          MC_SET_STD_HEAP;
         return pair->other_num;
         }*/
       cursor = min;
@@ -275,7 +285,7 @@ static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_s
                   MC_visited_pair_delete(pair_test);
                 }
                 if(!raw_mem_set)
-                  MC_UNSET_RAW_MEM;
+                  MC_SET_STD_HEAP;
                 return new_pair->other_num;
               }
             }
@@ -319,7 +329,7 @@ static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_s
   }
 
   if(!raw_mem_set)
-    MC_UNSET_RAW_MEM;
+    MC_SET_STD_HEAP;
   
   return -1;
 }
@@ -364,7 +374,7 @@ static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l, xbt_dynar_t
 
 void MC_ddfs_init(void){
 
-  initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 
   XBT_DEBUG("**************************************************");
   XBT_DEBUG("Double-DFS init");
@@ -378,7 +388,7 @@ void MC_ddfs_init(void){
   MC_ignore_heap(simix_global->process_to_run->data, 0);
   MC_ignore_heap(simix_global->process_that_ran->data, 0);
 
-  MC_SET_RAW_MEM;
+  MC_SET_MC_HEAP;
 
   acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL); 
   visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL); 
@@ -387,7 +397,7 @@ void MC_ddfs_init(void){
   initial_state_liveness->snapshot = MC_take_snapshot(0);
   initial_state_liveness->prev_pair = 0;
 
-  MC_UNSET_RAW_MEM; 
+  MC_SET_STD_HEAP;
   
   unsigned int cursor = 0;
   xbt_automaton_state_t automaton_state;
@@ -395,7 +405,7 @@ void MC_ddfs_init(void){
   xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state){
     if(automaton_state->type == -1){ /* Initial automaton state */
       
-      MC_SET_RAW_MEM;
+      MC_SET_MC_HEAP;
 
       initial_pair = MC_pair_new();
       initial_pair->automaton_state = automaton_state;
@@ -414,21 +424,21 @@ void MC_ddfs_init(void){
 
       xbt_fifo_unshift(mc_stack_liveness, initial_pair);
 
-      MC_UNSET_RAW_MEM;
+      MC_SET_STD_HEAP;
       
       MC_ddfs();
       
       if(cursor != 0){
         MC_restore_snapshot(initial_state_liveness->snapshot);
-        MC_UNSET_RAW_MEM;
+        MC_SET_STD_HEAP;
       } 
     }
   }
 
   if(initial_state_liveness->raw_mem_set)
-    MC_SET_RAW_MEM;
+    MC_SET_MC_HEAP;
   else
-    MC_UNSET_RAW_MEM;
+    MC_SET_STD_HEAP;
   
 
 }
@@ -492,16 +502,16 @@ void MC_ddfs(){
 
       if((visited_num = is_visited_pair(reached_pair, current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) != -1){
 
-        MC_SET_RAW_MEM;
+        MC_SET_MC_HEAP;
         if(dot_output != NULL)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, visited_num, initial_state_liveness->prev_req);
-        MC_UNSET_RAW_MEM;
+        MC_SET_STD_HEAP;
               
       }else{  
 
         while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 
-          MC_SET_RAW_MEM;
+          MC_SET_MC_HEAP;
           if(dot_output != NULL){
             if(initial_state_liveness->prev_pair != 0 && initial_state_liveness->prev_pair != current_pair->num){
               fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", initial_state_liveness->prev_pair, current_pair->num, initial_state_liveness->prev_req);
@@ -509,7 +519,7 @@ void MC_ddfs(){
             }
             initial_state_liveness->prev_pair = current_pair->num;
           }
-          MC_UNSET_RAW_MEM;
+          MC_SET_STD_HEAP;
 
           /* Debug information */
           if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
@@ -518,13 +528,13 @@ void MC_ddfs(){
             xbt_free(req_str);
           }
 
-          MC_SET_RAW_MEM;
+          MC_SET_MC_HEAP;
           if(dot_output != NULL){
             initial_state_liveness->prev_req = MC_request_get_dot_output(req, value);
             if(current_pair->search_cycle)
               fprintf(dot_output, "%d [shape=doublecircle];\n", current_pair->num);
           }
-          MC_UNSET_RAW_MEM; 
+          MC_SET_STD_HEAP;
           
           MC_state_set_executed_request(current_pair->graph_state, req, value);  
           mc_stats->executed_transitions++;
@@ -535,9 +545,9 @@ void MC_ddfs(){
           /* Wait for requests (schedules processes) */
           MC_wait_for_requests();
 
-          MC_SET_RAW_MEM;
+          MC_SET_MC_HEAP;
           prop_values = get_atomic_propositions_values();
-          MC_UNSET_RAW_MEM;
+          MC_SET_STD_HEAP;
 
           int new_pair = 0;
          
@@ -552,7 +562,7 @@ void MC_ddfs(){
               if(new_pair)
                 MC_replay_liveness(mc_stack_liveness, 1); 
 
-              MC_SET_RAW_MEM;
+              MC_SET_MC_HEAP;
 
               next_pair = MC_pair_new();
               next_pair->graph_state = MC_state_new();
@@ -576,7 +586,7 @@ void MC_ddfs(){
               if(mc_stats->expanded_pairs%1000000 == 0)
                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 
-              MC_UNSET_RAW_MEM;
+              MC_SET_STD_HEAP;
 
               new_pair = 1;
 
@@ -597,7 +607,7 @@ void MC_ddfs(){
               if(new_pair)
                 MC_replay_liveness(mc_stack_liveness, 1); 
             
-              MC_SET_RAW_MEM;
+              MC_SET_MC_HEAP;
             
               next_pair = MC_pair_new();
               next_pair->graph_state = MC_state_new();
@@ -621,7 +631,7 @@ void MC_ddfs(){
               if(mc_stats->expanded_pairs%1000000 == 0)
                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
             
-              MC_UNSET_RAW_MEM;
+              MC_SET_STD_HEAP;
 
               new_pair = 1;
 
@@ -660,7 +670,7 @@ void MC_ddfs(){
   }
 
   
-  MC_SET_RAW_MEM;
+  MC_SET_MC_HEAP;
   xbt_dynar_free(&prop_values);
   current_pair = xbt_fifo_shift(mc_stack_liveness);
   if(xbt_fifo_size(mc_stack_liveness) != _sg_mc_max_depth -1 && current_pair->requests > 0 && current_pair->search_cycle){
@@ -668,6 +678,6 @@ void MC_ddfs(){
   }
   MC_pair_delete(current_pair);
 
-  MC_UNSET_RAW_MEM;
+  MC_SET_STD_HEAP;
 
 }