model-checker : test data in libsimgrid memory region between each state

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index c377374..60adc47 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -24,7 +24,8 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
   if(s1->num_reg != s2->num_reg)
     return 1;
 
   if(s1->num_reg != s2->num_reg)
     return 1;
 

-  int i;
+  int i, errors=0;
+

   for(i=0 ; i< s1->num_reg ; i++){
     
     if(s1->regions[i]->size != s2->regions[i]->size)
   for(i=0 ; i< s1->num_reg ; i++){
     
     if(s1->regions[i]->size != s2->regions[i]->size)


@@ -33,19 +34,27 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
     if(s1->regions[i]->start_addr != s2->regions[i]->start_addr)
       return 1;
     
     if(s1->regions[i]->start_addr != s2->regions[i]->start_addr)
       return 1;
     

-    XBT_DEBUG("(%d) Snapshot ok before memcmp on data", i);
-    

     if(s1->regions[i]->type != s2->regions[i]->type)
       return 1;
 
     if(s1->regions[i]->type != s2->regions[i]->type)
       return 1;
 

-    if(s1->regions[i]->type == 0){
-      if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0)
-       return 1;
+    if(s1->regions[i]->type == 0){ 
+      if(mmalloc_compare_heap(s1->regions[i]->start_addr, s2->regions[i]->start_addr)){
+       XBT_DEBUG("Different heap (mmalloc_compare)");
+       //sleep(1);
+       errors++; 
+      }
+    }else{
+      if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
+       XBT_DEBUG("Different memcmp for data in libsimgrid (%d)", i);
+       //sleep(2);
+       errors++;
+      }

     }
     
     }
     

+    

   }
 
   }
 

-  return 0;
+  return (errors>0);

 
 }
 
 
 }
 


@@ -173,26 +182,42 @@ int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l){
 }
 
 
 }
 
 

-/********************* Double-DFS stateful without visited state *******************/

 
 
 
 

-void MC_ddfs_stateful_init(xbt_automaton_t a){
+
+/********************* Double-DFS stateless *******************/
+
+void MC_pair_stateless_delete(mc_pair_stateless_t pair){
+  xbt_free(pair->graph_state->proc_status);
+  xbt_free(pair->graph_state);
+  //xbt_free(pair->automaton_state); -> FIXME : à implémenter
+  xbt_free(pair);
+}
+
+mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){
+  mc_pair_stateless_t p = NULL;
+  p = xbt_new0(s_mc_pair_stateless_t, 1);
+  p->automaton_state = st;
+  p->graph_state = sg;
+  mc_stats_pair->expanded_pairs++;
+  return p;
+}
+
+
+
+void MC_ddfs_stateless_init(xbt_automaton_t a){

 
   XBT_DEBUG("**************************************************");
 
   XBT_DEBUG("**************************************************");

-  XBT_DEBUG("Double-DFS stateful without visited state init");
+  XBT_DEBUG("Double-DFS stateless init");

   XBT_DEBUG("**************************************************");
  
   XBT_DEBUG("**************************************************");
  

-  mc_pair_t mc_initial_pair;
-  mc_state_t initial_graph_state;
+  mc_pair_stateless_t mc_initial_pair = NULL;
+  mc_state_t initial_graph_state = NULL;

   smx_process_t process; 
   smx_process_t process; 

-  mc_snapshot_t init_snapshot;

  
   MC_wait_for_requests();
 
   MC_SET_RAW_MEM;
  
   MC_wait_for_requests();
 
   MC_SET_RAW_MEM;

-
-  init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-

   initial_graph_state = MC_state_pair_new();
   xbt_swag_foreach(process, simix_global->process_list){
     if(MC_process_is_enabled(process)){
   initial_graph_state = MC_state_pair_new();
   xbt_swag_foreach(process, simix_global->process_list){
     if(MC_process_is_enabled(process)){


@@ -202,77 +227,79 @@ void MC_ddfs_stateful_init(xbt_automaton_t a){
 
   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); 
 
 
   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); 
 

-  MC_take_snapshot(init_snapshot);
+  initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
+  MC_take_snapshot(initial_snapshot);

 
   MC_UNSET_RAW_MEM; 
 
   unsigned int cursor = 0;
 
   MC_UNSET_RAW_MEM; 
 
   unsigned int cursor = 0;

-  xbt_state_t state = NULL;
+  xbt_state_t state;

 
   xbt_dynar_foreach(a->states, cursor, state){
     if(state->type == -1){
 
   xbt_dynar_foreach(a->states, cursor, state){
     if(state->type == -1){

-    
+      

       MC_SET_RAW_MEM;
       MC_SET_RAW_MEM;

-      mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
-      xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
+      mc_initial_pair = new_pair_stateless(initial_graph_state, state);
+      xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);

       MC_UNSET_RAW_MEM;
       MC_UNSET_RAW_MEM;

-
+      

       if(cursor == 0){
       if(cursor == 0){

-       MC_ddfs_stateful(a, 0, 0);
+       MC_ddfs_stateless(a, 0, 0);

       }else{
       }else{

-       MC_restore_snapshot(init_snapshot);
+       MC_restore_snapshot(initial_snapshot);

        MC_UNSET_RAW_MEM;
        MC_UNSET_RAW_MEM;

-       MC_ddfs_stateful(a, 0, 0);
+       MC_ddfs_stateless(a, 0, 0);

       }
     }else{
       }
     }else{

-       if(state->type == 2){
-    
-        MC_SET_RAW_MEM;
-        mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
-        xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
-        MC_UNSET_RAW_MEM;
-        
-        if(cursor == 0){
-          MC_ddfs_stateful(a, 1, 0);
-        }else{
-          MC_restore_snapshot(init_snapshot);
-          MC_UNSET_RAW_MEM;
-          MC_ddfs_stateful(a, 1, 0);
-        }
-       }
+      if(state->type == 2){
+      
+       MC_SET_RAW_MEM;
+       mc_initial_pair = new_pair_stateless(initial_graph_state, state);
+       xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
+       MC_UNSET_RAW_MEM;
+       
+       if(cursor == 0){
+         MC_ddfs_stateless(a, 1, 0);
+       }else{
+         MC_restore_snapshot(initial_snapshot);
+         MC_UNSET_RAW_MEM;
+         MC_ddfs_stateless(a, 1, 0);
+       }
+      }

     }
   } 
     }
   } 

+

 }
 
 
 }
 
 

-void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
+void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){

 
 

-  smx_process_t process = NULL;
-  mc_pair_t current_pair = NULL;
+  smx_process_t process;
+  mc_pair_stateless_t current_pair = NULL;

 
 

-  if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
+  if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)

     return;
 
     return;
 

-  if(restore == 1){
-    current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
-    MC_restore_snapshot(current_pair->system_state);
+  if(replay == 1){
+    MC_replay_liveness(mc_stack_liveness_stateless);
+    current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));

     xbt_swag_foreach(process, simix_global->process_list){
       if(MC_process_is_enabled(process)){
        MC_state_interleave_process(current_pair->graph_state, process);
       }
     }
     xbt_swag_foreach(process, simix_global->process_list){
       if(MC_process_is_enabled(process)){
        MC_state_interleave_process(current_pair->graph_state, process);
       }
     }

-    MC_UNSET_RAW_MEM;

   }
 
   }
 

-  /* Get current state */
-  current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
-
-
-  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle);
-  XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state));
+  /* Get current pair */
+  current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));

 
 

+  /* Update current state in buchi automaton */

   a->current_state = current_pair->automaton_state;
   a->current_state = current_pair->automaton_state;

+ 
+  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
+  XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state));

 
 

+  

   mc_stats_pair->visited_pairs++;
 
   int value;
   mc_stats_pair->visited_pairs++;
 
   int value;


@@ -280,30 +307,28 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
   smx_req_t req = NULL;
   char *req_str;
 
   smx_req_t req = NULL;
   char *req_str;
 

-  mc_pair_t pair_succ;

   xbt_transition_t transition_succ;
   xbt_transition_t transition_succ;

-  unsigned int cursor;
+  unsigned int cursor = 0;

   int res;
 
   int res;
 

-  xbt_dynar_t successors = NULL;
-
-  mc_pair_t next_pair = NULL;
+  mc_pair_stateless_t next_pair = NULL;
+  mc_pair_stateless_t pair_succ;

   mc_snapshot_t next_snapshot = NULL;
   mc_snapshot_t current_snapshot = NULL;
   mc_snapshot_t next_snapshot = NULL;
   mc_snapshot_t current_snapshot = NULL;

-
-  //sleep(1);
+  
+  xbt_dynar_t successors = NULL;
+  

   MC_SET_RAW_MEM;
   MC_SET_RAW_MEM;

-  successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
+  successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);

   MC_UNSET_RAW_MEM;
   MC_UNSET_RAW_MEM;

-  
-  while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){

 
 

+  while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
+   

     MC_SET_RAW_MEM;
     current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
     MC_take_snapshot(current_snapshot);
     MC_UNSET_RAW_MEM;
     MC_SET_RAW_MEM;
     current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
     MC_take_snapshot(current_snapshot);
     MC_UNSET_RAW_MEM;

-   
-    
+

     /* Debug information */
     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
       req_str = MC_request_to_string(req, value);
     /* Debug information */
     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
       req_str = MC_request_to_string(req, value);


@@ -311,8 +336,10 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
       xbt_free(req_str);
     }
 
       xbt_free(req_str);
     }
 

-    MC_state_set_executed_request(current_pair->graph_state, req, value);
+    //sleep(1);

 
 

+    MC_state_set_executed_request(current_pair->graph_state, req, value);   
+    

     /* Answer the request */
     SIMIX_request_pre(req, value);
 
     /* Answer the request */
     SIMIX_request_pre(req, value);
 


@@ -320,11 +347,11 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
     MC_wait_for_requests();
 
 
     MC_wait_for_requests();
 
 

-    /* Create the new expanded graph_state */

     MC_SET_RAW_MEM;
 
     MC_SET_RAW_MEM;
 

+    /* Create the new expanded graph_state */

     next_graph_state = MC_state_pair_new();
     next_graph_state = MC_state_pair_new();

-    
+

     /* Get enabled process and insert it in the interleave set of the next graph_state */
     xbt_swag_foreach(process, simix_global->process_list){
       if(MC_process_is_enabled(process)){
     /* Get enabled process and insert it in the interleave set of the next graph_state */
     xbt_swag_foreach(process, simix_global->process_list){
       if(MC_process_is_enabled(process)){


@@ -334,20 +361,26 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
 
     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
     MC_take_snapshot(next_snapshot);
 
     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
     MC_take_snapshot(next_snapshot);

-
+    

     xbt_dynar_reset(successors);
 
     xbt_dynar_reset(successors);
 

-    MC_UNSET_RAW_MEM;
+    if(snapshot_compare(current_snapshot,next_snapshot)){
+      XBT_DEBUG("Different snapshot");
+      //sleep(2);
+      
+    }

 
 

+    MC_UNSET_RAW_MEM;

     
     

-    cursor = 0;
+
+    cursor= 0;

     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 
       res = MC_automaton_evaluate_label(a, transition_succ->label);
     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 
       res = MC_automaton_evaluate_label(a, transition_succ->label);

-       
+

       if(res == 1){ // enabled transition in automaton
        MC_SET_RAW_MEM;
       if(res == 1){ // enabled transition in automaton
        MC_SET_RAW_MEM;

-       next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
+       next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);

        xbt_dynar_push(successors, &next_pair);
        MC_UNSET_RAW_MEM;
       }
        xbt_dynar_push(successors, &next_pair);
        MC_UNSET_RAW_MEM;
       }


@@ -355,128 +388,103 @@ void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
     }
 
     cursor = 0;
     }
 
     cursor = 0;

+   

     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){

-
+      

       res = MC_automaton_evaluate_label(a, transition_succ->label);
        
       res = MC_automaton_evaluate_label(a, transition_succ->label);
        

-      if(res == 2){ // transition always enabled in automaton
+      if(res == 2){ // true transition in automaton

        MC_SET_RAW_MEM;
        MC_SET_RAW_MEM;

-       next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);
+       next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);

        xbt_dynar_push(successors, &next_pair);
        MC_UNSET_RAW_MEM;
       }
 
        xbt_dynar_push(successors, &next_pair);
        MC_UNSET_RAW_MEM;
       }
 

-     

     }
 
    
     if(xbt_dynar_length(successors) == 0){
     }
 
    
     if(xbt_dynar_length(successors) == 0){

-

       MC_SET_RAW_MEM;
       MC_SET_RAW_MEM;

-      next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);
+      next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state);

       xbt_dynar_push(successors, &next_pair);
       MC_UNSET_RAW_MEM;
       xbt_dynar_push(successors, &next_pair);
       MC_UNSET_RAW_MEM;

-       

     }
 
     }
 

-    //XBT_DEBUG("Successors in automaton %lu", xbt_dynar_length(successors));
+    cursor = 0; 

 
 

-    cursor = 0;

     xbt_dynar_foreach(successors, cursor, pair_succ){
     xbt_dynar_foreach(successors, cursor, pair_succ){

-
-      //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
-
+     

       if((search_cycle == 1) && (reached(a, next_snapshot) == 1)){
        XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
        XBT_INFO("|             ACCEPTANCE CYCLE            |");
        XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
        XBT_INFO("Counter-example that violates formula :");
       if((search_cycle == 1) && (reached(a, next_snapshot) == 1)){
        XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
        XBT_INFO("|             ACCEPTANCE CYCLE            |");
        XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
        XBT_INFO("Counter-example that violates formula :");

-       MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
-       MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
+       MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
+       MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);

        MC_print_statistics_pairs(mc_stats_pair);
        exit(0);
       }
        
        MC_print_statistics_pairs(mc_stats_pair);
        exit(0);
       }
        

-      //mc_stats_pair->executed_transitions++;
- 

       MC_SET_RAW_MEM;
       MC_SET_RAW_MEM;

-      xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
+      xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);

       MC_UNSET_RAW_MEM;
 
       MC_UNSET_RAW_MEM;
 

-      MC_ddfs_stateful(a, search_cycle, 0);
-    
-    
+      MC_ddfs_stateless(a, search_cycle, 0);
+
+     

       if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 
       if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 

+       XBT_DEBUG("Acceptance pair %p : graph=%p, automaton=%p(%s)", pair_succ, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);

        int res = set_pair_reached(a, next_snapshot);
        int res = set_pair_reached(a, next_snapshot);

-       XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
-       
+

        MC_SET_RAW_MEM;
        MC_SET_RAW_MEM;

-       xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
+       xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);

        MC_UNSET_RAW_MEM;
        MC_UNSET_RAW_MEM;

+      
+       MC_ddfs_stateless(a, 1, 1);

        
        

-       MC_ddfs_stateful(a, 1, 1);
-

        if(res){
          MC_SET_RAW_MEM;
          xbt_dynar_pop(reached_pairs, NULL);
          MC_UNSET_RAW_MEM;
        }
       }
        if(res){
          MC_SET_RAW_MEM;
          xbt_dynar_pop(reached_pairs, NULL);
          MC_UNSET_RAW_MEM;
        }
       }

-

     }
 
     if(MC_state_interleave_size(current_pair->graph_state) > 0){
     }
 
     if(MC_state_interleave_size(current_pair->graph_state) > 0){

-      XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateful));
-      MC_restore_snapshot(current_snapshot);
-      MC_UNSET_RAW_MEM;
-    }
-
+      XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
+      MC_replay_liveness(mc_stack_liveness_stateless);
+    }    
+   

   }
   }

-

   
   MC_SET_RAW_MEM;
   
   MC_SET_RAW_MEM;

-  xbt_fifo_shift(mc_stack_liveness_stateful);
-  XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);
+  xbt_fifo_shift(mc_stack_liveness_stateless);
+  XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle);

   MC_UNSET_RAW_MEM;
 
 }
 
   MC_UNSET_RAW_MEM;
 
 }
 

+/********************* Double-DFS stateful without visited state *******************/

 
 
 
 

-/********************* Double-DFS stateless *******************/
-
-void MC_pair_stateless_delete(mc_pair_stateless_t pair){
-  xbt_free(pair->graph_state->proc_status);
-  xbt_free(pair->graph_state);
-  //xbt_free(pair->automaton_state); -> FIXME : à implémenter
-  xbt_free(pair);
-}
-
-mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){
-  mc_pair_stateless_t p = NULL;
-  p = xbt_new0(s_mc_pair_stateless_t, 1);
-  p->automaton_state = st;
-  p->graph_state = sg;
-  mc_stats_pair->expanded_pairs++;
-  return p;
-}
-
-
-
-void MC_ddfs_stateless_init(xbt_automaton_t a){
+void MC_ddfs_stateful_init(xbt_automaton_t a){

 
   XBT_DEBUG("**************************************************");
 
   XBT_DEBUG("**************************************************");

-  XBT_DEBUG("Double-DFS stateless init");
+  XBT_DEBUG("Double-DFS stateful without visited state init");

   XBT_DEBUG("**************************************************");
  
   XBT_DEBUG("**************************************************");
  

-  mc_pair_stateless_t mc_initial_pair = NULL;
-  mc_state_t initial_graph_state = NULL;
+  mc_pair_t mc_initial_pair;
+  mc_state_t initial_graph_state;

   smx_process_t process; 
   smx_process_t process; 

+  mc_snapshot_t init_snapshot;

  
   MC_wait_for_requests();
 
   MC_SET_RAW_MEM;
  
   MC_wait_for_requests();
 
   MC_SET_RAW_MEM;

+
+  init_snapshot = xbt_new0(s_mc_snapshot_t, 1);
+

   initial_graph_state = MC_state_pair_new();
   xbt_swag_foreach(process, simix_global->process_list){
     if(MC_process_is_enabled(process)){
   initial_graph_state = MC_state_pair_new();
   xbt_swag_foreach(process, simix_global->process_list){
     if(MC_process_is_enabled(process)){


@@ -486,79 +494,77 @@ void MC_ddfs_stateless_init(xbt_automaton_t a){
 
   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); 
 
 
   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL); 
 

-  initial_snapshot = xbt_new0(s_mc_snapshot_t, 1);
-  MC_take_snapshot(initial_snapshot);
+  MC_take_snapshot(init_snapshot);

 
   MC_UNSET_RAW_MEM; 
 
   unsigned int cursor = 0;
 
   MC_UNSET_RAW_MEM; 
 
   unsigned int cursor = 0;

-  xbt_state_t state;
+  xbt_state_t state = NULL;

 
   xbt_dynar_foreach(a->states, cursor, state){
     if(state->type == -1){
 
   xbt_dynar_foreach(a->states, cursor, state){
     if(state->type == -1){

-      
+    

       MC_SET_RAW_MEM;
       MC_SET_RAW_MEM;

-      mc_initial_pair = new_pair_stateless(initial_graph_state, state);
-      xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
+      mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
+      xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);

       MC_UNSET_RAW_MEM;
       MC_UNSET_RAW_MEM;

-      
+

       if(cursor == 0){
       if(cursor == 0){

-       MC_ddfs_stateless(a, 0, 0);
+       MC_ddfs_stateful(a, 0, 0);

       }else{
       }else{

-       MC_restore_snapshot(initial_snapshot);
+       MC_restore_snapshot(init_snapshot);

        MC_UNSET_RAW_MEM;
        MC_UNSET_RAW_MEM;

-       MC_ddfs_stateless(a, 0, 0);
+       MC_ddfs_stateful(a, 0, 0);

       }
     }else{
       }
     }else{

-      if(state->type == 2){
-      
-       MC_SET_RAW_MEM;
-       mc_initial_pair = new_pair_stateless(initial_graph_state, state);
-       xbt_fifo_unshift(mc_stack_liveness_stateless, mc_initial_pair);
-       MC_UNSET_RAW_MEM;
-       
-       if(cursor == 0){
-         MC_ddfs_stateless(a, 1, 0);
-       }else{
-         MC_restore_snapshot(initial_snapshot);
-         MC_UNSET_RAW_MEM;
-         MC_ddfs_stateless(a, 1, 0);
-       }
-      }
+       if(state->type == 2){
+    
+        MC_SET_RAW_MEM;
+        mc_initial_pair = new_pair(init_snapshot, initial_graph_state, state);
+        xbt_fifo_unshift(mc_stack_liveness_stateful, mc_initial_pair);
+        MC_UNSET_RAW_MEM;
+        
+        if(cursor == 0){
+          MC_ddfs_stateful(a, 1, 0);
+        }else{
+          MC_restore_snapshot(init_snapshot);
+          MC_UNSET_RAW_MEM;
+          MC_ddfs_stateful(a, 1, 0);
+        }
+       }

     }
   } 
     }
   } 

-

 }
 
 
 }
 
 

-void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
+void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){

 
 

-  smx_process_t process;
-  mc_pair_stateless_t current_pair = NULL;
+  smx_process_t process = NULL;
+  mc_pair_t current_pair = NULL;

 
 

-  if(xbt_fifo_size(mc_stack_liveness_stateless) == 0)
+  if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)

     return;
 
     return;
 

-  if(replay == 1){
-    MC_replay_liveness(mc_stack_liveness_stateless);
-    current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
+  if(restore == 1){
+    current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
+    MC_restore_snapshot(current_pair->system_state);

     xbt_swag_foreach(process, simix_global->process_list){
       if(MC_process_is_enabled(process)){
        MC_state_interleave_process(current_pair->graph_state, process);
       }
     }
     xbt_swag_foreach(process, simix_global->process_list){
       if(MC_process_is_enabled(process)){
        MC_state_interleave_process(current_pair->graph_state, process);
       }
     }

+    MC_UNSET_RAW_MEM;

   }
 
   }
 

-  /* Get current pair */
-  current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateless));
+  /* Get current state */
+  current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));

 
 

-  /* Update current state in buchi automaton */
-  a->current_state = current_pair->automaton_state;
- 
-  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateless), search_cycle);
+
+  XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness_stateful), search_cycle);

   XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state));
 
   XBT_DEBUG("Pair : graph=%p, automaton=%p(%s), %u interleave", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id,MC_state_interleave_size(current_pair->graph_state));
 

-  
+  a->current_state = current_pair->automaton_state;
+

   mc_stats_pair->visited_pairs++;
 
   int value;
   mc_stats_pair->visited_pairs++;
 
   int value;


@@ -566,23 +572,30 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
   smx_req_t req = NULL;
   char *req_str;
 
   smx_req_t req = NULL;
   char *req_str;
 

+  mc_pair_t pair_succ;

   xbt_transition_t transition_succ;
   xbt_transition_t transition_succ;

-  unsigned int cursor = 0;
+  unsigned int cursor;

   int res;
 
   int res;
 

-  mc_pair_stateless_t next_pair = NULL;
-  mc_pair_stateless_t pair_succ;
-  mc_snapshot_t next_snapshot = NULL;
-  

   xbt_dynar_t successors = NULL;
   xbt_dynar_t successors = NULL;

-  
+
+  mc_pair_t next_pair = NULL;
+  mc_snapshot_t next_snapshot = NULL;
+  mc_snapshot_t current_snapshot = NULL;
+
+  //sleep(1);

   MC_SET_RAW_MEM;
   MC_SET_RAW_MEM;

-  successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
+  successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);

   MC_UNSET_RAW_MEM;
   MC_UNSET_RAW_MEM;

-
+  

   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
   while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){

-   

 
 

+    MC_SET_RAW_MEM;
+    current_snapshot = xbt_new0(s_mc_snapshot_t, 1);
+    MC_take_snapshot(current_snapshot);
+    MC_UNSET_RAW_MEM;
+   
+    

     /* Debug information */
     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
       req_str = MC_request_to_string(req, value);
     /* Debug information */
     if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
       req_str = MC_request_to_string(req, value);


@@ -590,10 +603,8 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
       xbt_free(req_str);
     }
 
       xbt_free(req_str);
     }
 

-    //sleep(1);
+    MC_state_set_executed_request(current_pair->graph_state, req, value);

 
 

-    MC_state_set_executed_request(current_pair->graph_state, req, value);   
-    

     /* Answer the request */
     SIMIX_request_pre(req, value);
 
     /* Answer the request */
     SIMIX_request_pre(req, value);
 


@@ -601,11 +612,11 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
     MC_wait_for_requests();
 
 
     MC_wait_for_requests();
 
 

+    /* Create the new expanded graph_state */

     MC_SET_RAW_MEM;
 
     MC_SET_RAW_MEM;
 

-    /* Create the new expanded graph_state */

     next_graph_state = MC_state_pair_new();
     next_graph_state = MC_state_pair_new();

-
+    

     /* Get enabled process and insert it in the interleave set of the next graph_state */
     xbt_swag_foreach(process, simix_global->process_list){
       if(MC_process_is_enabled(process)){
     /* Get enabled process and insert it in the interleave set of the next graph_state */
     xbt_swag_foreach(process, simix_global->process_list){
       if(MC_process_is_enabled(process)){


@@ -615,20 +626,20 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
 
     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
     MC_take_snapshot(next_snapshot);
 
     next_snapshot = xbt_new0(s_mc_snapshot_t, 1);
     MC_take_snapshot(next_snapshot);

-    
+

     xbt_dynar_reset(successors);
 
     MC_UNSET_RAW_MEM;
     xbt_dynar_reset(successors);
 
     MC_UNSET_RAW_MEM;

-    

 
 

-    cursor= 0;
+    
+    cursor = 0;

     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 
       res = MC_automaton_evaluate_label(a, transition_succ->label);
     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 
       res = MC_automaton_evaluate_label(a, transition_succ->label);

-
+       

       if(res == 1){ // enabled transition in automaton
        MC_SET_RAW_MEM;
       if(res == 1){ // enabled transition in automaton
        MC_SET_RAW_MEM;

-       next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
+       next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);

        xbt_dynar_push(successors, &next_pair);
        MC_UNSET_RAW_MEM;
       }
        xbt_dynar_push(successors, &next_pair);
        MC_UNSET_RAW_MEM;
       }


@@ -636,80 +647,89 @@ void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int replay){
     }
 
     cursor = 0;
     }
 
     cursor = 0;

-   

     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
     xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){

-      
+

       res = MC_automaton_evaluate_label(a, transition_succ->label);
        
       res = MC_automaton_evaluate_label(a, transition_succ->label);
        

-      if(res == 2){ // enabled transition in automaton
+      if(res == 2){ // transition always enabled in automaton

        MC_SET_RAW_MEM;
        MC_SET_RAW_MEM;

-       next_pair = new_pair_stateless(next_graph_state, transition_succ->dst);
+       next_pair = new_pair(next_snapshot,next_graph_state, transition_succ->dst);

        xbt_dynar_push(successors, &next_pair);
        MC_UNSET_RAW_MEM;
       }
 
        xbt_dynar_push(successors, &next_pair);
        MC_UNSET_RAW_MEM;
       }
 

+     

     }
 
    
     if(xbt_dynar_length(successors) == 0){
     }
 
    
     if(xbt_dynar_length(successors) == 0){

+

       MC_SET_RAW_MEM;
       MC_SET_RAW_MEM;

-      next_pair = new_pair_stateless(next_graph_state, current_pair->automaton_state);
+      next_pair = new_pair(next_snapshot, next_graph_state, current_pair->automaton_state);

       xbt_dynar_push(successors, &next_pair);
       MC_UNSET_RAW_MEM;
       xbt_dynar_push(successors, &next_pair);
       MC_UNSET_RAW_MEM;

+       

     }
 
     }
 

-    cursor = 0; 
+    //XBT_DEBUG("Successors in automaton %lu", xbt_dynar_length(successors));

 
 

+    cursor = 0;

     xbt_dynar_foreach(successors, cursor, pair_succ){
     xbt_dynar_foreach(successors, cursor, pair_succ){

-     
+
+      //XBT_DEBUG("Search visited pair : graph=%p, automaton=%p", pair_succ->graph_state, pair_succ->automaton_state);
+

       if((search_cycle == 1) && (reached(a, next_snapshot) == 1)){
        XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
        XBT_INFO("|             ACCEPTANCE CYCLE            |");
        XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
        XBT_INFO("Counter-example that violates formula :");
       if((search_cycle == 1) && (reached(a, next_snapshot) == 1)){
        XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
        XBT_INFO("|             ACCEPTANCE CYCLE            |");
        XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
        XBT_INFO("Counter-example that violates formula :");

-       MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
-       MC_dump_stack_liveness_stateless(mc_stack_liveness_stateless);
+       MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
+       MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);

        MC_print_statistics_pairs(mc_stats_pair);
        exit(0);
       }
        
        MC_print_statistics_pairs(mc_stats_pair);
        exit(0);
       }
        

+      //mc_stats_pair->executed_transitions++;
+ 

       MC_SET_RAW_MEM;
       MC_SET_RAW_MEM;

-      xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
+      xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);

       MC_UNSET_RAW_MEM;
 
       MC_UNSET_RAW_MEM;
 

-      MC_ddfs_stateless(a, search_cycle, 0);
-
-     
+      MC_ddfs_stateful(a, search_cycle, 0);
+    
+    

       if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 
       if((search_cycle == 0) && ((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 

-       XBT_DEBUG("Acceptance pair %p : graph=%p, automaton=%p(%s)", pair_succ, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);

        int res = set_pair_reached(a, next_snapshot);
        int res = set_pair_reached(a, next_snapshot);

-
+       XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
+       

        MC_SET_RAW_MEM;
        MC_SET_RAW_MEM;

-       xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
+       xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);

        MC_UNSET_RAW_MEM;
        MC_UNSET_RAW_MEM;

-      
-       MC_ddfs_stateless(a, 1, 1);

        
        

+       MC_ddfs_stateful(a, 1, 1);
+

        if(res){
          MC_SET_RAW_MEM;
          xbt_dynar_pop(reached_pairs, NULL);
          MC_UNSET_RAW_MEM;
        }
       }
        if(res){
          MC_SET_RAW_MEM;
          xbt_dynar_pop(reached_pairs, NULL);
          MC_UNSET_RAW_MEM;
        }
       }

+

     }
 
     if(MC_state_interleave_size(current_pair->graph_state) > 0){
     }
 
     if(MC_state_interleave_size(current_pair->graph_state) > 0){

-      XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateless));
-      MC_replay_liveness(mc_stack_liveness_stateless);
-    }    
-   
+      XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness_stateful));
+      MC_restore_snapshot(current_snapshot);
+      MC_UNSET_RAW_MEM;
+    }
+

   }
   }

+

   
   MC_SET_RAW_MEM;
   
   MC_SET_RAW_MEM;

-  xbt_fifo_shift(mc_stack_liveness_stateless);
-  XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle);
+  xbt_fifo_shift(mc_stack_liveness_stateful);
+  XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in stack", current_pair->graph_state, current_pair->automaton_state);

   MC_UNSET_RAW_MEM;
 
 }
   MC_UNSET_RAW_MEM;
 
 }

-

diff --git a/src/mc/memory_map.c b/src/mc/memory_map.c
index fa49689..9e987f0 100644 (file)
--- a/src/mc/memory_map.c
+++ b/src/mc/memory_map.c
@@ -144,14 +144,15 @@ memory_map_t get_memory_map(void)
     ret->mapsize++;
 
     if(XBT_LOG_ISENABLED(mc_memory_map, xbt_log_priority_debug)){
     ret->mapsize++;
 
     if(XBT_LOG_ISENABLED(mc_memory_map, xbt_log_priority_debug)){

-
-      if (memreg.pathname == NULL){
-       if (memreg.start_addr == std_heap){ 
-         XBT_DEBUG("New region in snapshot : %s", backup_line); 
-       }
-      } else {
-       if (!memcmp(basename(memreg.pathname), "libsimgrid", 10)){
-         XBT_DEBUG("New region in snapshot : %s", backup_line); 
+      if ((memreg.prot & PROT_WRITE)){
+       if (memreg.pathname == NULL){
+         if (memreg.start_addr == std_heap){ 
+           XBT_DEBUG("New region in snapshot : %s", backup_line); 
+         }
+       } else {
+         if (!memcmp(basename(memreg.pathname), "libsimgrid", 10)){
+           XBT_DEBUG("New region in snapshot : %s", backup_line); 
+         }

        }
       }
     }
        }
       }
     }

diff --git a/src/xbt/mmalloc/mm_legacy.c b/src/xbt/mmalloc/mm_legacy.c
index 3b581c7..b2814b3 100644 (file)
--- a/src/xbt/mmalloc/mm_legacy.c
+++ b/src/xbt/mmalloc/mm_legacy.c
@@ -256,7 +256,7 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
     return 1;
   }
 
     return 1;
   }
 

-  XBT_DEBUG("Heap index : %d", mdp1->heapindex);
+  //XBT_DEBUG("Heap index : %d", mdp1->heapindex);

 
   if(mdp1->base != mdp2->base){
     XBT_DEBUG("Different base address of the memory region");
 
   if(mdp1->base != mdp2->base){
     XBT_DEBUG("Different base address of the memory region");


@@ -299,13 +299,15 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
  
   size_t block_free1, start1, block_free2 , start2, block_busy1, block_busy2 ;
   unsigned int i;
  
   size_t block_free1, start1, block_free2 , start2, block_busy1, block_busy2 ;
   unsigned int i;

+  void *addr_block1, *addr_block2;
+  struct mdesc* mdp;

 
   start1 = block_free1 = mdp1->heapindex; 
   start2 = block_free2 = mdp2->heapindex;
   block_busy1 = start1 + mdp1->heapinfo[start1].free.size;
   block_busy2 = start2 + mdp2->heapinfo[start2].free.size;
 
 
   start1 = block_free1 = mdp1->heapindex; 
   start2 = block_free2 = mdp2->heapindex;
   block_busy1 = start1 + mdp1->heapinfo[start1].free.size;
   block_busy2 = start2 + mdp2->heapinfo[start2].free.size;
 

-  //XBT_DEBUG("Block busy : %d - %d", block_busy1, block_busy2);
+  XBT_DEBUG("Block busy : %d - %d", block_busy1, block_busy2);

 
 
   if(mdp1->heapinfo[start1].free.size != mdp2->heapinfo[start2].free.size){ // <=> check block_busy
 
 
   if(mdp1->heapinfo[start1].free.size != mdp2->heapinfo[start2].free.size){ // <=> check block_busy


@@ -322,17 +324,36 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
 
     }else{
    
 
     }else{
    

-      for(i=block_busy1 ; i<mdp1->heapinfo[start1].free.next ; i++){
+      i=block_busy1 ;
+
+      XBT_DEBUG("Next free : %d", mdp1->heapinfo[start1].free.next);
+
+
+      while(i<mdp1->heapinfo[start1].free.next){
+
+       XBT_DEBUG("i (block busy) : %d", i);
+

        if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){
          XBT_DEBUG("Different type of busy block");
          return 1;
        }else{
        if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){
          XBT_DEBUG("Different type of busy block");
          return 1;
        }else{

+         mdp = mdp1;
+         addr_block1 = ADDRESS(i);
+         mdp = mdp2;
+         addr_block2 = ADDRESS(i); 

          switch(mdp1->heapinfo[i].busy.type){
          case 0 :
            if(mdp1->heapinfo[i].busy.info.size != mdp2->heapinfo[i].busy.info.size){
              XBT_DEBUG("Different size of a large cluster");
              return 1;
          switch(mdp1->heapinfo[i].busy.type){
          case 0 :
            if(mdp1->heapinfo[i].busy.info.size != mdp2->heapinfo[i].busy.info.size){
              XBT_DEBUG("Different size of a large cluster");
              return 1;

+           }else{
+             XBT_DEBUG("Blocks %d : %p - %p / Data size : %d (%d blocks)", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE),mdp->heapinfo[i].busy.info.size );       
+             if(memcmp(addr_block1, addr_block2, mdp1->heapinfo[i].busy.info.size * BLOCKSIZE) != 0){
+               XBT_DEBUG("Different data in block %d", i);
+               return 1;
+             } 

            }
            }

+           i = i + mdp1->heapinfo[i].busy.info.size;

            break;
          default :       
            if(mdp1->heapinfo[i].busy.info.frag.nfree != mdp2->heapinfo[i].busy.info.frag.nfree){
            break;
          default :       
            if(mdp1->heapinfo[i].busy.info.frag.nfree != mdp2->heapinfo[i].busy.info.frag.nfree){


@@ -342,68 +363,97 @@ int mmalloc_compare_mdesc(struct mdesc *mdp1, struct mdesc *mdp2){
              if(mdp1->heapinfo[i].busy.info.frag.first != mdp2->heapinfo[i].busy.info.frag.first){
                XBT_DEBUG("Different first free fragments of the block");
                return 1; 
              if(mdp1->heapinfo[i].busy.info.frag.first != mdp2->heapinfo[i].busy.info.frag.first){
                XBT_DEBUG("Different first free fragments of the block");
                return 1; 

+             }else{
+               if(memcmp(addr_block1, addr_block2, BLOCKSIZE) != 0){
+                 XBT_DEBUG("Different data in block %d", i);
+                 return 1;
+               } 

              }
            }
              }
            }

+           i++;

            break;
          }
        } 
       }
            break;
          }
        } 
       }

-    }

 
 

-    block_free1 = mdp1->heapinfo[start1].free.next;
-    block_free2 = mdp2->heapinfo[start2].free.next;

 
 

-    //XBT_DEBUG("Index of next free cluster : %d", block_free1);
+      block_free1 = mdp1->heapinfo[start1].free.next;
+      block_free2 = mdp2->heapinfo[start2].free.next;
+
+      //XBT_DEBUG("Index of next free cluster : %d", block_free1);

 
 

-    while((block_free1 != start1) && (block_free2 != start2)){ 
+      while((block_free1 != start1) && (block_free2 != start2)){ 

 
 

-      block_busy1 = block_free1 + mdp1->heapinfo[block_free1].free.size;
-      block_busy2 = block_free2 + mdp2->heapinfo[block_free2].free.size;
+       block_busy1 = block_free1 + mdp1->heapinfo[block_free1].free.size;
+       block_busy2 = block_free2 + mdp2->heapinfo[block_free2].free.size;

 
 

-      if(block_busy1 != block_busy2){
-       XBT_DEBUG("Different index of busy block");
-       return 1;
-      }else{
+       if(block_busy1 != block_busy2){
+         XBT_DEBUG("Different index of busy block");
+         return 1;
+       }else{

 
 

-       //XBT_DEBUG("Index of next busy block : %d - %d", block_busy1, block_busy2);
-       //XBT_DEBUG("Index of next free cluster : %d", mdp1->heapinfo[block_free1].free.next);
+         XBT_DEBUG("Index of next busy block : %d - %d", block_busy1, block_busy2);
+         XBT_DEBUG("Index of next free cluster : %d", mdp1->heapinfo[block_free1].free.next);

        
        

-       for(i=block_busy1 ; i<mdp1->heapinfo[block_free1].free.next ; i++){
-         if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){
-           XBT_DEBUG("Different type of busy block");
-           return 1;
-         }else{
-           switch(mdp1->heapinfo[i].busy.type){
-           case 0 :
-             if(mdp1->heapinfo[i].busy.info.size != mdp2->heapinfo[i].busy.info.size){
-               XBT_DEBUG("Different size of a large cluster");
-               return 1;
-             }
-             break;
-           default :     
-             if(mdp1->heapinfo[i].busy.info.frag.nfree != mdp2->heapinfo[i].busy.info.frag.nfree){
-               XBT_DEBUG("Different free fragments in a fragmented block");
-               return 1;
-             }else{
-               if(mdp1->heapinfo[i].busy.info.frag.first != mdp2->heapinfo[i].busy.info.frag.first){
-                 XBT_DEBUG("Different first free fragments of the block");
-                 return 1; 
+         i = block_busy1;
+
+         while(i<mdp1->heapinfo[block_free1].free.next){
+
+           XBT_DEBUG("i (block busy) : %d", i);
+
+           if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){
+             XBT_DEBUG("Different type of busy block");
+             return 1;
+           }else{
+             mdp = mdp1;
+             addr_block1 = ADDRESS(i);
+             mdp = mdp2;
+             addr_block2 = ADDRESS(i); 
+             switch(mdp1->heapinfo[i].busy.type){
+             case 0 :
+               if(mdp1->heapinfo[i].busy.info.size != mdp2->heapinfo[i].busy.info.size){
+                 XBT_DEBUG("Different size of a large cluster");
+                 return 1;
+               }else{
+                 XBT_DEBUG("Blocks %d : %p - %p / Data size : %d", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE));                
+                 //XBT_DEBUG("Size of large cluster %d", mdp->heapinfo[i].busy.info.size);
+                 if(memcmp(addr_block1, addr_block2, (mdp1->heapinfo[i].busy.info.size * BLOCKSIZE)) != 0){
+                   XBT_DEBUG("Different data in block %d", i);
+                   return 1;
+                 } 
+               }
+               i = i+mdp1->heapinfo[i].busy.info.size;
+               break;
+             default :   
+               if(mdp1->heapinfo[i].busy.info.frag.nfree != mdp2->heapinfo[i].busy.info.frag.nfree){
+                 XBT_DEBUG("Different free fragments in a fragmented block");
+                 return 1;
+               }else{
+                 if(mdp1->heapinfo[i].busy.info.frag.first != mdp2->heapinfo[i].busy.info.frag.first){
+                   XBT_DEBUG("Different first free fragments of the block");
+                   return 1; 
+                 }else{
+                   if(memcmp(addr_block1, addr_block2, BLOCKSIZE) != 0){
+                     XBT_DEBUG("Different data in fragmented block %d", i);
+                     return 1;
+                   } 
+                 }

                }
                }

+               i++;
+               break;

              }
              }

-             break;
-           }
-         } 
+           } 
+         }

        }
        }

-      }

 
 

-      block_free1 = mdp1->heapinfo[block_free1].free.next;
-      block_free2 = mdp2->heapinfo[block_free2].free.next;
+       block_free1 = mdp1->heapinfo[block_free1].free.next;
+       block_free2 = mdp2->heapinfo[block_free2].free.next;

       
       

-    } 
+      } 

     
     

-  }
-  
+    }

   
   

+      }

   return 0;   
   
   
   return 0;