model-checker : store heap_bytes_used and number of processes directly in mc_visited_...

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 06e03d9..de9b988 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -25,6 +25,22 @@ static void visited_state_free_voidp(void *s){
   visited_state_free((mc_visited_state_t) * (void **) s);
 }
 
+static mc_visited_state_t visited_state_new(){
+
+  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->nb_processes = xbt_swag_size(simix_global->process_list);
+  new_state->system_state = MC_take_snapshot();
+  new_state->num = mc_stats->expanded_states - 1;
+
+  return new_state;
+  
+}
+
+/* Dichotomic search in visited_states dynar. 
+ * States are ordered by the number of processes then the number of bytes used in std_heap */
+
 static int is_visited_state(){
 
   if(_sg_mc_visited == 0)
@@ -33,12 +49,7 @@ static int is_visited_state(){
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
-
-  mc_visited_state_t new_state = NULL;
-  new_state = xbt_new0(s_mc_visited_state_t, 1);
-  new_state->system_state = MC_take_snapshot();
-  new_state->num = mc_stats->expanded_states;
-
+  mc_visited_state_t new_state = visited_state_new();
   MC_UNSET_RAW_MEM;
   
   if(xbt_dynar_is_empty(visited_states)){
@@ -56,7 +67,8 @@ static int is_visited_state(){
 
     MC_SET_RAW_MEM;
     
-    size_t current_bytes_used = new_state->system_state->heap_bytes_used;
+    size_t current_bytes_used = new_state->heap_bytes_used;
+    int current_nb_processes = new_state->nb_processes;
 
     unsigned int cursor = 0;
     int previous_cursor = 0, next_cursor = 0;
@@ -65,71 +77,79 @@ static int is_visited_state(){
 
     mc_visited_state_t state_test = NULL;
     size_t bytes_used_test;
-    int same_bytes_not_found = 1;
+    int nb_processes_test;
+    int same_processes_and_bytes_not_found = 1;
 
-    while(start <= end && same_bytes_not_found){
+    while(start <= end && same_processes_and_bytes_not_found){
       cursor = (start + end) / 2;
       state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
-      bytes_used_test = state_test->system_state->heap_bytes_used;
-      if(bytes_used_test < current_bytes_used)
+      bytes_used_test = state_test->heap_bytes_used;
+      nb_processes_test = state_test->nb_processes;
+      if(nb_processes_test < current_nb_processes)
         start = cursor + 1;
-      if(bytes_used_test > current_bytes_used)
+      if(nb_processes_test > current_nb_processes)
         end = cursor - 1; 
-      if(bytes_used_test == current_bytes_used){
-        same_bytes_not_found = 0;
-        if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
-          xbt_dynar_remove_at(visited_states, cursor, NULL);
-          xbt_dynar_insert_at(visited_states, cursor, &new_state);
-          XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
-          if(raw_mem_set)
-            MC_SET_RAW_MEM;
-          else
-            MC_UNSET_RAW_MEM;
-          return state_test->num;
-        }else{
-          /* Search another state with same number of bytes used */
-          previous_cursor = cursor - 1;
-          while(previous_cursor >= 0){
-            state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_visited_state_t);
-            bytes_used_test = state_test->system_state->heap_bytes_used;
-            if(bytes_used_test != current_bytes_used)
-              break;
-            if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
-              xbt_dynar_remove_at(visited_states, previous_cursor, NULL);
-              xbt_dynar_insert_at(visited_states, previous_cursor, &new_state);
-              XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
-              if(raw_mem_set)
-                MC_SET_RAW_MEM;
-              else
-                MC_UNSET_RAW_MEM;
-              return state_test->num;
+      if(nb_processes_test == current_nb_processes){
+        if(bytes_used_test < current_bytes_used)
+          start = cursor + 1;
+        if(bytes_used_test > current_bytes_used)
+          end = cursor - 1;
+        if(bytes_used_test == current_bytes_used){
+          same_processes_and_bytes_not_found = 0;
+          if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
+            xbt_dynar_remove_at(visited_states, cursor, NULL);
+            xbt_dynar_insert_at(visited_states, cursor, &new_state);
+            XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
+            if(raw_mem_set)
+              MC_SET_RAW_MEM;
+            else
+              MC_UNSET_RAW_MEM;
+            return state_test->num;
+          }else{
+            /* Search another state with same number of bytes used in std_heap */
+            previous_cursor = cursor - 1;
+            while(previous_cursor >= 0){
+              state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_visited_state_t);
+              bytes_used_test = state_test->system_state->heap_bytes_used;
+              if(bytes_used_test != current_bytes_used)
+                break;
+              if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
+                xbt_dynar_remove_at(visited_states, previous_cursor, NULL);
+                xbt_dynar_insert_at(visited_states, previous_cursor, &new_state);
+                XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
+                if(raw_mem_set)
+                  MC_SET_RAW_MEM;
+                else
+                  MC_UNSET_RAW_MEM;
+                return state_test->num;
+              }
+              previous_cursor--;
             }
-            previous_cursor--;
-          }
-          next_cursor = cursor + 1;
-          while(next_cursor < xbt_dynar_length(visited_states)){
-            state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_visited_state_t);
-            bytes_used_test = state_test->system_state->heap_bytes_used;
-            if(bytes_used_test != current_bytes_used)
-              break;
-            if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
-              xbt_dynar_remove_at(visited_states, next_cursor, NULL);
-              xbt_dynar_insert_at(visited_states, next_cursor, &new_state);
-              XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
-              if(raw_mem_set)
-                MC_SET_RAW_MEM;
-              else
-                MC_UNSET_RAW_MEM;
-              return state_test->num;
+            next_cursor = cursor + 1;
+            while(next_cursor < xbt_dynar_length(visited_states)){
+              state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, next_cursor, mc_visited_state_t);
+              bytes_used_test = state_test->system_state->heap_bytes_used;
+              if(bytes_used_test != current_bytes_used)
+                break;
+              if(snapshot_compare(new_state->system_state, state_test->system_state) == 0){
+                xbt_dynar_remove_at(visited_states, next_cursor, NULL);
+                xbt_dynar_insert_at(visited_states, next_cursor, &new_state);
+                XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
+                if(raw_mem_set)
+                  MC_SET_RAW_MEM;
+                else
+                  MC_UNSET_RAW_MEM;
+                return state_test->num;
+              }
+              next_cursor++;
             }
-            next_cursor++;
-          }
-        }   
+          }   
+        }
       }
     }
 
     state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
-    bytes_used_test = state_test->system_state->heap_bytes_used;
+    bytes_used_test = state_test->heap_bytes_used;
 
     if(bytes_used_test < current_bytes_used)
       xbt_dynar_insert_at(visited_states, cursor + 1, &new_state);

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index ac9b74d..f19a670 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -136,19 +136,14 @@ static void set_acceptance_pair_reached(xbt_automaton_state_t st){
     
 }
 
-static int is_visited_pair(xbt_automaton_state_t st){
-
-  if(_sg_mc_visited == 0)
-    return 0;
-
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-
-  MC_SET_RAW_MEM;
+static mc_visited_pair_t visited_pair_new(xbt_automaton_state_t as){
 
   mc_visited_pair_t new_pair = NULL;
   new_pair = xbt_new0(s_mc_visited_pair_t, 1);
-  new_pair->automaton_state = st;
+  new_pair->automaton_state = as;
   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
+  new_pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
+  new_pair->nb_processes = xbt_swag_size(simix_global->process_list);
   new_pair->system_state = MC_take_snapshot();  
   
   /* Get values of propositional symbols */
@@ -161,64 +156,164 @@ static int is_visited_pair(xbt_automaton_state_t st){
     res = f();
     xbt_dynar_push_as(new_pair->prop_ato, int, res);
   }
-  
+
+  return new_pair;
+
+}
+
+static int is_visited_pair(xbt_automaton_state_t as){
+
+  if(_sg_mc_visited == 0)
+    return -1;
+
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_SET_RAW_MEM;
+  mc_visited_pair_t new_pair = visited_pair_new(as);
   MC_UNSET_RAW_MEM;
-  
+
   if(xbt_dynar_is_empty(visited_pairs)){
 
     MC_SET_RAW_MEM;
-    /* New pair visited */
     xbt_dynar_push(visited_pairs, &new_pair); 
     MC_UNSET_RAW_MEM;
 
     if(raw_mem_set)
       MC_SET_RAW_MEM;
- 
-    return 0;
+
+    return -1;
 
   }else{
 
     MC_SET_RAW_MEM;
     
-    cursor = 0;
+    size_t current_bytes_used = new_pair->heap_bytes_used;
+    int current_nb_processes = new_pair->nb_processes;
+
+    unsigned int cursor = 0;
+    int previous_cursor = 0, next_cursor = 0;
+    int start = 0;
+    int end = xbt_dynar_length(visited_pairs) - 1;
+
     mc_visited_pair_t pair_test = NULL;
-     
-    xbt_dynar_foreach(visited_pairs, cursor, pair_test){
-      if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
-        XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);
-      if(xbt_automaton_state_compare(pair_test->automaton_state, st) == 0){
-        if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
-          if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
-            if(raw_mem_set)
-              MC_SET_RAW_MEM;
-            else
-              MC_UNSET_RAW_MEM;
-            
-            return 1;
-          }   
-        }else{
-          XBT_DEBUG("Different values of propositional symbols");
+    size_t bytes_used_test;
+    int nb_processes_test;
+    int same_processes_and_bytes_not_found = 1;
+
+    while(start <= end && same_processes_and_bytes_not_found){
+      cursor = (start + end) / 2;
+      pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
+      bytes_used_test = pair_test->heap_bytes_used;
+      nb_processes_test = pair_test->nb_processes;
+      if(nb_processes_test < current_nb_processes)
+        start = cursor + 1;
+      if(nb_processes_test > current_nb_processes)
+        end = cursor - 1; 
+      if(nb_processes_test == current_nb_processes){
+        if(bytes_used_test < current_bytes_used)
+          start = cursor + 1;
+        if(bytes_used_test > current_bytes_used)
+          end = cursor - 1;
+        if(bytes_used_test == current_bytes_used){
+          same_processes_and_bytes_not_found = 0;
+          if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
+            if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
+              if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
+                xbt_dynar_remove_at(visited_pairs, cursor, NULL);
+                xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
+                XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
+                if(raw_mem_set)
+                  MC_SET_RAW_MEM;
+                else
+                  MC_UNSET_RAW_MEM;
+                return pair_test->num;
+              }
+            }
+          }
+          /* Search another pair with same number of bytes used in std_heap */
+          previous_cursor = cursor - 1;
+          while(previous_cursor >= 0){
+            pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, previous_cursor, mc_visited_pair_t);
+            bytes_used_test = pair_test->system_state->heap_bytes_used;
+            if(bytes_used_test != current_bytes_used)
+              break;
+            if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
+              if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){  
+                if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
+                  xbt_dynar_remove_at(visited_pairs, previous_cursor, NULL);
+                  xbt_dynar_insert_at(visited_pairs, previous_cursor, &new_pair);
+                  XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
+                  if(raw_mem_set)
+                    MC_SET_RAW_MEM;
+                  else
+                    MC_UNSET_RAW_MEM;
+                  return pair_test->num;
+                }
+              }
+            }
+            previous_cursor--;
+          }
+          next_cursor = cursor + 1;
+          while(next_cursor < xbt_dynar_length(visited_pairs)){
+            pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, next_cursor, mc_visited_pair_t);
+            bytes_used_test = pair_test->system_state->heap_bytes_used;
+            if(bytes_used_test != current_bytes_used)
+              break;
+            if(xbt_automaton_state_compare(pair_test->automaton_state, as) == 0){
+              if(xbt_automaton_propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
+                if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
+                  xbt_dynar_remove_at(visited_pairs, next_cursor, NULL);
+                  xbt_dynar_insert_at(visited_pairs, next_cursor, &new_pair);
+                  XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_pair->num, pair_test->num);
+                  if(raw_mem_set)
+                    MC_SET_RAW_MEM;
+                  else
+                    MC_UNSET_RAW_MEM;
+                  return pair_test->num;
+                }
+              }
+            }
+            next_cursor++;
+          }
         }
-      }else{
-        XBT_DEBUG("Different automaton state");
       }
     }
 
-    if(xbt_dynar_length(visited_pairs) == _sg_mc_visited){
-      xbt_dynar_remove_at(visited_pairs, 0, NULL);
+    pair_test = (mc_visited_pair_t)xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
+    bytes_used_test = pair_test->heap_bytes_used;
+
+    if(bytes_used_test < current_bytes_used)
+      xbt_dynar_insert_at(visited_pairs, cursor + 1, &new_pair);
+    else
+      xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
+
+    if(xbt_dynar_length(visited_pairs) > _sg_mc_visited){
+      int min = mc_stats->expanded_states;
+      unsigned int cursor2 = 0;
+      unsigned int index = 0;
+      xbt_dynar_foreach(visited_pairs, cursor2, pair_test){
+        if(pair_test->num < min){
+          index = cursor2;
+          min = pair_test->num;
+        }
+      }
+      xbt_dynar_remove_at(visited_pairs, index, NULL);
     }
 
-    /* New pair visited */
-    xbt_dynar_push(visited_pairs, &new_pair); 
+    /*cursor = 0;
+    xbt_dynar_foreach(visited_pairs, cursor, pair_test){
+      fprintf(stderr, "Visited pair %d, nb_processes %d and heap_bytes_used %zu\n", pair_test->num, pair_test->nb_processes, pair_test->heap_bytes_used);
+      }*/
     
     MC_UNSET_RAW_MEM;
 
     if(raw_mem_set)
       MC_SET_RAW_MEM;
     
-    return 0;
+    return -1;
     
   }
+ 
 }
 
 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l){
@@ -419,7 +514,8 @@ void MC_ddfs(int search_cycle){
           xbt_free(req_str);
         }
 
-        MC_state_set_executed_request(current_pair->graph_state, req, value);   
+        MC_state_set_executed_request(current_pair->graph_state, req, value);  
+        mc_stats->executed_transitions++;
 
         /* Answer the request */
         SIMIX_simcall_pre(req, value);
@@ -502,7 +598,7 @@ void MC_ddfs(int search_cycle){
 
               }else{
 
-                if(is_visited_pair(pair_succ->automaton_state)){
+                if(is_visited_pair(pair_succ->automaton_state) != -1){
 
                   XBT_DEBUG("Next pair already visited !");
                   break;
@@ -525,7 +621,7 @@ void MC_ddfs(int search_cycle){
 
             }else{
 
-              if(is_visited_pair(pair_succ->automaton_state)){
+              if(is_visited_pair(pair_succ->automaton_state) != -1){
 
                 XBT_DEBUG("Next pair already visited !");
                 break;
@@ -543,7 +639,7 @@ void MC_ddfs(int search_cycle){
 
           }else{
 
-            if(is_visited_pair(pair_succ->automaton_state)){
+            if(is_visited_pair(pair_succ->automaton_state) != -1){
 
               XBT_DEBUG("Next pair already visited !");
               break;
@@ -586,6 +682,8 @@ void MC_ddfs(int search_cycle){
 
  
     }else{
+
+      mc_stats->executed_transitions++;
       
       XBT_DEBUG("No more request to execute in this state, search evolution in Büchi Automaton.");
 
@@ -651,7 +749,7 @@ void MC_ddfs(int search_cycle){
 
             }else{
 
-              if(is_visited_pair(pair_succ->automaton_state)){
+              if(is_visited_pair(pair_succ->automaton_state) != -1){
                 
                 XBT_DEBUG("Next pair already visited !");
                 break;
@@ -674,7 +772,7 @@ void MC_ddfs(int search_cycle){
 
           }else{
             
-            if(is_visited_pair(pair_succ->automaton_state)){
+            if(is_visited_pair(pair_succ->automaton_state) != -1){
               
               XBT_DEBUG("Next pair already visited !");
               break;
@@ -694,7 +792,7 @@ void MC_ddfs(int search_cycle){
 
         }else{
       
-          if(is_visited_pair(pair_succ->automaton_state)){
+          if(is_visited_pair(pair_succ->automaton_state) != -1){
 
             XBT_DEBUG("Next pair already visited !");
             break;

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 6a46fd6..15deac2 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -265,6 +265,8 @@ void MC_dpor(void);
 
 typedef struct s_mc_visited_state{
   mc_snapshot_t system_state;
+  size_t heap_bytes_used;
+  int nb_processes;
   int num;
 }s_mc_visited_state_t, *mc_visited_state_t;
 
@@ -297,6 +299,8 @@ typedef struct s_mc_visited_pair{
   xbt_dynar_t prop_ato;
   mc_snapshot_t system_state;
   int num;
+  size_t heap_bytes_used;
+  int nb_processes;
 }s_mc_visited_pair_t, *mc_visited_pair_t;
 
 mc_pair_t MC_pair_new(mc_state_t sg, xbt_automaton_state_t st, int r);