model-checker : sorting of visited states according to chunks used

diff --git a/src/mc/mc_compare.c b/src/mc/mc_compare.c
index e27511e..f016ad3 100644 (file)
--- a/src/mc/mc_compare.c
+++ b/src/mc/mc_compare.c
@@ -147,6 +147,21 @@ int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall,
   return snapshot_compare(s1, s2, NULL, NULL);
 }
 
   return snapshot_compare(s1, s2, NULL, NULL);
 }
 

+int get_heap_region_index(mc_snapshot_t s){
+  int i =0;
+  while(i < s->num_reg){
+    switch(s->regions[i]->type){
+    case 0:
+      return i;
+      break;
+    default:
+      i++;
+      break;
+    }
+  }
+  return -1;
+}
+

 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t ct1, mc_comparison_times_t ct2){
 
   int raw_mem = (mmalloc_get_current_heap() == raw_heap);
 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2, mc_comparison_times_t ct1, mc_comparison_times_t ct2){
 
   int raw_mem = (mmalloc_get_current_heap() == raw_heap);

diff --git a/src/mc/mc_dpor.c b/src/mc/mc_dpor.c
index 11cc06c..f797347 100644 (file)
--- a/src/mc/mc_dpor.c
+++ b/src/mc/mc_dpor.c
@@ -41,29 +41,76 @@ static int is_visited_state(){
 
     MC_SET_RAW_MEM;
     
 
     MC_SET_RAW_MEM;
     

-    unsigned int cursor = 0;
+    size_t current_chunks_used = mmalloc_get_chunks_used((xbt_mheap_t)new_state->regions[get_heap_region_index(new_state)]->data);
+
+    unsigned int cursor = 0, previous_cursor = 0, next_cursor = 0;
+    int start = 0;
+    int end = xbt_dynar_length(visited_states) - 1;
+

     mc_snapshot_t state_test = NULL;
     mc_snapshot_t state_test = NULL;

-     
-    xbt_dynar_foreach(visited_states, cursor, state_test){
-      if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug))
-        XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);
-      if(snapshot_compare(new_state, state_test, NULL, NULL) == 0){
-        if(raw_mem_set)
-          MC_SET_RAW_MEM;
-        else
-          MC_UNSET_RAW_MEM;
-        
-        return 1;
-      }   
+    size_t chunks_used_test;
+
+    while(start <= end){
+      cursor = (start + end) / 2;
+      state_test = (mc_snapshot_t)xbt_dynar_get_as(visited_states, cursor, mc_snapshot_t);
+      chunks_used_test = mmalloc_get_chunks_used((xbt_mheap_t)state_test->regions[get_heap_region_index(state_test)]->data);
+      if(chunks_used_test == current_chunks_used){
+        if(snapshot_compare(new_state, state_test, NULL, NULL) == 0){
+          if(raw_mem_set)
+            MC_SET_RAW_MEM;
+          else
+            MC_UNSET_RAW_MEM;
+          return 1;
+        }else{
+          /* Search another state with same number of chunks used */
+          previous_cursor = cursor - 1;
+          while(previous_cursor >= 0){
+            state_test = (mc_snapshot_t)xbt_dynar_get_as(visited_states, previous_cursor, mc_snapshot_t);
+            chunks_used_test = mmalloc_get_chunks_used((xbt_mheap_t)state_test->regions[get_heap_region_index(state_test)]->data);
+            if(chunks_used_test != current_chunks_used)
+              break;
+            if(snapshot_compare(new_state, state_test, NULL, NULL) == 0){
+              if(raw_mem_set)
+                MC_SET_RAW_MEM;
+              else
+                MC_UNSET_RAW_MEM;
+              return 1;
+            }
+            previous_cursor--;
+          }
+          next_cursor = cursor + 1;
+          while(next_cursor < xbt_dynar_length(visited_states)){
+            state_test = (mc_snapshot_t)xbt_dynar_get_as(visited_states, next_cursor, mc_snapshot_t);
+            chunks_used_test = mmalloc_get_chunks_used((xbt_mheap_t)state_test->regions[get_heap_region_index(state_test)]->data);
+            if(chunks_used_test != current_chunks_used)
+              break;
+            if(snapshot_compare(new_state, state_test, NULL, NULL) == 0){
+              if(raw_mem_set)
+                MC_SET_RAW_MEM;
+              else
+                MC_UNSET_RAW_MEM;
+              return 1;
+            }
+            next_cursor++;
+          }
+        }   
+      }
+      if(chunks_used_test < current_chunks_used)
+        start = cursor + 1;
+      if(chunks_used_test > current_chunks_used)
+        end = cursor - 1;

     }
     }

-
+ 

     if(xbt_dynar_length(visited_states) == _sg_mc_visited){
       mc_snapshot_t state_to_remove = NULL;
       xbt_dynar_shift(visited_states, &state_to_remove);
       MC_free_snapshot(state_to_remove);
     }
 
     if(xbt_dynar_length(visited_states) == _sg_mc_visited){
       mc_snapshot_t state_to_remove = NULL;
       xbt_dynar_shift(visited_states, &state_to_remove);
       MC_free_snapshot(state_to_remove);
     }
 

-    xbt_dynar_push(visited_states, &new_state); 
+    if(chunks_used_test < current_chunks_used)
+      xbt_dynar_insert_at(visited_states, cursor + 1, &new_state);
+    else
+      xbt_dynar_insert_at(visited_states, cursor, &new_state);

     
     MC_UNSET_RAW_MEM;
 
     
     MC_UNSET_RAW_MEM;
 

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 382b7c0..895a25b 100644 (file)
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -288,6 +288,8 @@ void MC_init_liveness(void);
 void MC_init_memory_map_info(void);
 void MC_print_comparison_times_statistics(mc_comparison_times_t ct);
 
 void MC_init_memory_map_info(void);
 void MC_print_comparison_times_statistics(mc_comparison_times_t ct);
 

+int get_heap_region_index(mc_snapshot_t s);
+

 /* **** Double-DFS stateless **** */
 
 typedef struct s_mc_pair_stateless{
 /* **** Double-DFS stateless **** */
 
 typedef struct s_mc_pair_stateless{