X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/adcfb1a36dc3a193da6b595829fef2d7f4c9a4dd..50b36cfb6864e719576327d1289cf9ba31d652da:/src/mc/mc_visited.c

diff --git a/src/mc/mc_visited.c b/src/mc/mc_visited.c
index 765a48ad51..941a780abd 100644
--- a/src/mc/mc_visited.c
+++ b/src/mc/mc_visited.c
@@ -19,13 +19,13 @@ xbt_dynar_t visited_pairs;
 xbt_dynar_t visited_states;
 
 static int is_exploration_stack_state(mc_visited_state_t state){
-  xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
+  xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
   while (item) {
     if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
       ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
       return 1;
     }
-    item = xbt_fifo_get_prev_item(item);
+    item = xbt_fifo_get_next_item(item);
   }
   return 0;
 }
@@ -51,9 +51,12 @@ void visited_state_free_voidp(void *s)
  */
 static mc_visited_state_t visited_state_new()
 {
+  mc_process_t process = &(mc_model_checker->process);
   mc_visited_state_t new_state = NULL;
   new_state = xbt_new0(s_mc_visited_state_t, 1);
-  new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
+  new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
+    MC_process_get_heap(process)->heaplimit,
+    MC_process_get_malloc_info(process));
   new_state->nb_processes = xbt_swag_size(simix_global->process_list);
   new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
   new_state->num = mc_stats->expanded_states;
@@ -61,13 +64,17 @@ static mc_visited_state_t visited_state_new()
   return new_state;
 }
 
-mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_snapshot_t system_state)
+mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state)
 {
+  mc_process_t process = &(mc_model_checker->process);
   mc_visited_pair_t pair = NULL;
   pair = xbt_new0(s_mc_visited_pair_t, 1);
-  pair->graph_state = MC_state_new();
-  pair->graph_state->system_state = (system_state == NULL) ? MC_take_snapshot(pair_num) : system_state;
-  pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
+  pair->graph_state = graph_state;
+  if(pair->graph_state->system_state == NULL)
+    pair->graph_state->system_state = MC_take_snapshot(pair_num);
+  pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
+    MC_process_get_heap(process)->heaplimit,
+    MC_process_get_malloc_info(process));
   pair->nb_processes = xbt_swag_size(simix_global->process_list);
   pair->automaton_state = automaton_state;
   pair->num = pair_num;
@@ -75,7 +82,6 @@ mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automa
   pair->acceptance_removed = 0;
   pair->visited_removed = 0;
   pair->acceptance_pair = 0;
-  pair->in_exploration_stack = 1;
   pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
   unsigned int cursor = 0;
   int value;
@@ -85,13 +91,13 @@ mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automa
 }
 
 static int is_exploration_stack_pair(mc_visited_pair_t pair){
-  xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
+  xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
   while (item) {
     if (((mc_pair_t)xbt_fifo_get_item_content(item))->num == pair->num){
       ((mc_pair_t)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
       return 1;
     }
-    item = xbt_fifo_get_prev_item(item);
+    item = xbt_fifo_get_next_item(item);
   }
   return 0;
 }
@@ -99,7 +105,8 @@ static int is_exploration_stack_pair(mc_visited_pair_t pair){
 void MC_visited_pair_delete(mc_visited_pair_t p)
 {
   p->automaton_state = NULL;
-  MC_state_delete(p->graph_state, !is_exploration_stack_pair(p));
+  if( !is_exploration_stack_pair(p))
+    MC_state_delete(p->graph_state, 1);
   xbt_dynar_free(&(p->atomic_propositions));
   xbt_free(p);
   p = NULL;
@@ -124,9 +131,7 @@ void MC_visited_pair_delete(mc_visited_pair_t p)
 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
 {
 
-  int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
-  MC_SET_MC_HEAP;
+  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 
   int cursor = 0, previous_cursor, next_cursor;
   int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
@@ -197,16 +202,13 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
           *max = next_cursor;
           next_cursor++;
         }
-        if (!mc_mem_set)
-          MC_SET_STD_HEAP;
+        mmalloc_set_current_heap(heap);
         return -1;
       }
     }
   }
 
-  if (!mc_mem_set)
-    MC_SET_STD_HEAP;
-
+  mmalloc_set_current_heap(heap);
   return cursor;
 }
 
@@ -228,7 +230,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
      are incomplete and they cannot be analyzed and compared with the initial pattern. */
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
     int current_process = 1;
-    while (current_process < simix_process_maxpid) {
+    while (current_process < MC_smx_get_maxpid()) {
       if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
         XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
         partial_comm = 1;
@@ -238,9 +240,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
     }
   }
 
-  int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
-  MC_SET_MC_HEAP;
+  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 
   mc_visited_state_t new_state = visited_state_new();
   graph_state->system_state = new_state->system_state;
@@ -250,10 +250,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
   if (xbt_dynar_is_empty(visited_states)) {
 
     xbt_dynar_push(visited_states, &new_state);
-
-    if (!mc_mem_set)
-      MC_SET_STD_HEAP;
-
+    mmalloc_set_current_heap(heap);
     return NULL;
 
   } else {
@@ -310,8 +307,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
             xbt_dynar_insert_at(visited_states, cursor, &new_state);
             XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
 
-            if (!mc_mem_set)
-              MC_SET_STD_HEAP;
+            mmalloc_set_current_heap(heap);
             return state_test;
           }
           cursor++;
@@ -359,11 +355,8 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state)
       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
     }
 
-    if (!mc_mem_set)
-      MC_SET_STD_HEAP;
-
+    mmalloc_set_current_heap(heap);
     return NULL;
-
   }
 }
 
@@ -375,14 +368,12 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
   if (_sg_mc_visited == 0)
     return -1;
 
-  int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
-  MC_SET_MC_HEAP;
+  xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 
   mc_visited_pair_t new_visited_pair = NULL;
 
   if (visited_pair == NULL) {
-    new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state->system_state);
+    new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
   } else {
     new_visited_pair = visited_pair;
   }
@@ -451,8 +442,7 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
               } else {
                 MC_visited_pair_delete(pair_test);
               }
-              if (!mc_mem_set)
-                MC_SET_STD_HEAP;
+              mmalloc_set_current_heap(heap);
               return new_visited_pair->other_num;
             }
           }
@@ -494,8 +484,6 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
 
   }
 
-  if (!mc_mem_set)
-    MC_SET_STD_HEAP;
-
+  mmalloc_set_current_heap(heap);
   return -1;
 }