src/mc/mc_liveness.c

   1 /* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "mc_private.h"
   7 #include <unistd.h>
   8 #include <sys/wait.h>
   9
  10 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
  11                                 "Logging specific to algorithms for liveness properties verification");
  12
  13 xbt_dynar_t reached_pairs;
  14 xbt_dynar_t visited_pairs;
  15 xbt_dynar_t successors;
  16
  17 int create_dump(int pair)
  18 {
  19    // Try to enable core dumps
  20   struct rlimit core_limit;
  21   core_limit.rlim_cur = RLIM_INFINITY;
  22   core_limit.rlim_max = RLIM_INFINITY;
  23
  24   if(setrlimit(RLIMIT_CORE, &core_limit) < 0)
  25     fprintf(stderr, "setrlimit: %s\nWarning: core dumps may be truncated or non-existant\n", strerror(errno));
  26
  27   int status;
  28   switch(fork()){
  29   case 0:
  30     // We are the child process -- run the actual program
  31     xbt_abort();
  32     break;
  33
  34   case -1:
  35     // An error occurred, shouldn't happen
  36     perror("fork");
  37     return -1;
  38
  39   default:
  40     // We are the parent process -- wait for the child process to exit
  41     if(wait(&status) < 0)
  42       perror("wait");
  43     if(WIFSIGNALED(status) && WCOREDUMP(status)){
  44       char *core_name = malloc(20);
  45       sprintf(core_name,"core_%d", pair);
  46       rename("core", core_name);
  47       free(core_name);
  48     }
  49   }
  50
  51   return 0;
  52 }
  53
  54 void MC_print_comparison_times_statistics(mc_comparison_times_t ct){
  55
  56   XBT_DEBUG("Comparisons done : %d", ct->nb_comparisons);
  57
  58   double total, min, max;
  59   unsigned int cursor;
  60
  61   if(xbt_dynar_length(ct->chunks_used_comparison_times) > 0){
  62     cursor = 0;
  63     total = 0.0;
  64     max = 0.0;
  65     min = xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double);
  66     while(cursor < xbt_dynar_length(ct->chunks_used_comparison_times) - 1){
  67       total += xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double);
  68       if(xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double) > max)
  69         max = xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double);
  70       if(xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double) < min)
  71         min = xbt_dynar_get_as(ct->chunks_used_comparison_times, cursor, double);
  72       cursor++;
  73     }
  74     XBT_DEBUG("Chunks used comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->chunks_used_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->chunks_used_comparison_times), max, min);
  75   }
  76
  77   if(xbt_dynar_length(ct->stacks_sizes_comparison_times) > 0){
  78     cursor = 0;
  79     total = 0.0;
  80     max = 0.0;
  81     min = xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double);
  82     while(cursor < xbt_dynar_length(ct->stacks_sizes_comparison_times) - 1){
  83       total += xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double);
  84       if(xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double) > max)
  85         max = xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double);
  86       if(xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double) < min)
  87         min = xbt_dynar_get_as(ct->stacks_sizes_comparison_times, cursor, double);
  88       cursor++;
  89     }
  90     XBT_DEBUG("Stacks sizes comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->stacks_sizes_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->stacks_sizes_comparison_times), max, min);
  91   }
  92
  93   if(xbt_dynar_length(ct->program_data_segment_comparison_times) > 0){
  94     cursor = 0;
  95     total = 0.0;
  96     max = 0.0;
  97     min = xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double);
  98     while(cursor < xbt_dynar_length(ct->program_data_segment_comparison_times) - 1){
  99       total += xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double);
 100       if(xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double) > max)
 101         max = xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double);
 102       if(xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double) < min)
 103         min = xbt_dynar_get_as(ct->program_data_segment_comparison_times, cursor, double);
 104       cursor++;
 105     }
 106     XBT_DEBUG("Program data/bss segments comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->program_data_segment_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->program_data_segment_comparison_times), max, min);
 107   }
 108
 109   if(xbt_dynar_length(ct->libsimgrid_data_segment_comparison_times) > 0){
 110     cursor = 0;
 111     total = 0.0;
 112     max = 0.0;
 113     min = xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double);
 114     while(cursor < xbt_dynar_length(ct->libsimgrid_data_segment_comparison_times) - 1){
 115       total += xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double);
 116       if(xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double) > max)
 117         max = xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double);
 118       if(xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double) < min)
 119         min = xbt_dynar_get_as(ct->libsimgrid_data_segment_comparison_times, cursor, double);
 120       cursor++;
 121     }
 122     XBT_DEBUG("Libsimgrid data/bss segments comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->libsimgrid_data_segment_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->libsimgrid_data_segment_comparison_times), max, min);
 123   }
 124
 125   if(xbt_dynar_length(ct->heap_comparison_times) > 0){
 126     cursor = 0;
 127     total = 0.0;
 128     max = 0.0;
 129     min = xbt_dynar_get_as(ct->heap_comparison_times, cursor, double);
 130     while(cursor < xbt_dynar_length(ct->heap_comparison_times) - 1){
 131       total += xbt_dynar_get_as(ct->heap_comparison_times, cursor, double);
 132       if(xbt_dynar_get_as(ct->heap_comparison_times, cursor, double) > max)
 133         max = xbt_dynar_get_as(ct->heap_comparison_times, cursor, double);
 134       if(xbt_dynar_get_as(ct->heap_comparison_times, cursor, double) < min)
 135         min = xbt_dynar_get_as(ct->heap_comparison_times, cursor, double);
 136       cursor++;
 137     }
 138     XBT_DEBUG("Heap comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->heap_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->heap_comparison_times), max, min);
 139   }
 140
 141   if(xbt_dynar_length(ct->stacks_comparison_times) > 0){
 142     cursor = 0;
 143     total = 0.0;
 144     max = 0.0;
 145     min = xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double);
 146     while(cursor < xbt_dynar_length(ct->stacks_comparison_times) - 1){
 147       total += xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double);
 148       if(xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double) > max)
 149         max = xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double);
 150       if(xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double) < min)
 151         min = xbt_dynar_get_as(ct->stacks_comparison_times, cursor, double);
 152       cursor++;
 153     }
 154     XBT_DEBUG("Stacks comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->stacks_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->stacks_comparison_times), max, min);
 155   }
 156
 157   if(xbt_dynar_length(ct->snapshot_comparison_times) > 0){
 158     cursor = 0;
 159     total = 0.0;
 160     max = 0.0;
 161     min = xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double);
 162     while(cursor < xbt_dynar_length(ct->snapshot_comparison_times) - 1){
 163       total += xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double);
 164       if(xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double) > max)
 165         max = xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double);
 166       if(xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double) < min)
 167         min = xbt_dynar_get_as(ct->snapshot_comparison_times, cursor, double);
 168       cursor++;
 169     }
 170     XBT_DEBUG("Snapshot comparison (Whole funnel) -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->snapshot_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->snapshot_comparison_times), max, min);
 171   }
 172
 173 }
 174
 175 mc_comparison_times_t new_comparison_times(){
 176   mc_comparison_times_t ct = NULL;
 177   ct = xbt_new0(s_mc_comparison_times_t, 1);
 178   ct->nb_comparisons = 0;
 179   ct->snapshot_comparison_times = xbt_dynar_new(sizeof(double), NULL);
 180   ct->chunks_used_comparison_times = xbt_dynar_new(sizeof(double), NULL);
 181   ct->stacks_sizes_comparison_times = xbt_dynar_new(sizeof(double), NULL);
 182   ct->program_data_segment_comparison_times = xbt_dynar_new(sizeof(double), NULL);
 183   ct->libsimgrid_data_segment_comparison_times = xbt_dynar_new(sizeof(double), NULL);
 184   ct->heap_comparison_times = xbt_dynar_new(sizeof(double), NULL);
 185   ct->stacks_comparison_times = xbt_dynar_new(sizeof(double), NULL);
 186   return ct;
 187 }
 188
 189 int reached(xbt_state_t st){
 190
 191   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 192
 193   MC_SET_RAW_MEM;
 194
 195   mc_pair_reached_t new_pair = NULL;
 196   new_pair = xbt_new0(s_mc_pair_reached_t, 1);
 197   new_pair->nb = xbt_dynar_length(reached_pairs) + 1;
 198   new_pair->automaton_state = st;
 199   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 200   new_pair->comparison_times = new_comparison_times();
 201   new_pair->system_state = MC_take_snapshot_liveness();
 202
 203   /* Get values of propositional symbols */
 204   int res;
 205   int_f_void_t f;
 206   unsigned int cursor = 0;
 207   xbt_propositional_symbol_t ps = NULL;
 208   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 209     f = (int_f_void_t)ps->function;
 210     res = (*f)();
 211     xbt_dynar_push_as(new_pair->prop_ato, int, res);
 212   }
 213
 214   MC_UNSET_RAW_MEM;
 215
 216   if(xbt_dynar_is_empty(reached_pairs)/* || !compare*/){
 217
 218     MC_SET_RAW_MEM;
 219     /* New pair reached */
 220     xbt_dynar_push(reached_pairs, &new_pair);
 221     MC_UNSET_RAW_MEM;
 222
 223     if(raw_mem_set)
 224       MC_SET_RAW_MEM;
 225
 226     return 0;
 227
 228   }else{
 229
 230     MC_SET_RAW_MEM;
 231
 232     cursor = 0;
 233     mc_pair_reached_t pair_test = NULL;
 234
 235     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
 236       if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
 237         XBT_DEBUG("****** Pair reached #%d ******", pair_test->nb);
 238       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 239         if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
 240           if(snapshot_compare(new_pair->system_state, pair_test->system_state, new_pair->comparison_times, pair_test->comparison_times) == 0){
 241
 242             if(raw_mem_set)
 243               MC_SET_RAW_MEM;
 244             else
 245               MC_UNSET_RAW_MEM;
 246
 247             return 1;
 248           }
 249         }else{
 250           XBT_INFO("Different values of propositional symbols");
 251         }
 252       }else{
 253         XBT_INFO("Different automaton state");
 254       }
 255       if(pair_test->comparison_times != NULL && XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 256         XBT_DEBUG("*** Comparison times statistics ***");
 257         MC_print_comparison_times_statistics(pair_test->comparison_times);
 258       }
 259     }
 260
 261     /* New pair reached */
 262     xbt_dynar_push(reached_pairs, &new_pair);
 263
 264     MC_UNSET_RAW_MEM;
 265
 266     if(raw_mem_set)
 267       MC_SET_RAW_MEM;
 268
 269     compare = 0;
 270
 271     return 0;
 272
 273   }
 274 }
 275
 276
 277 void set_pair_reached(xbt_state_t st){
 278
 279   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 280
 281   MC_SET_RAW_MEM;
 282
 283   mc_pair_reached_t pair = NULL;
 284   pair = xbt_new0(s_mc_pair_reached_t, 1);
 285   pair->nb = xbt_dynar_length(reached_pairs) + 1;
 286   pair->automaton_state = st;
 287   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 288   pair->comparison_times = new_comparison_times();
 289   pair->system_state = MC_take_snapshot_liveness();
 290
 291   /* Get values of propositional symbols */
 292   unsigned int cursor = 0;
 293   xbt_propositional_symbol_t ps = NULL;
 294   int res;
 295   int_f_void_t f;
 296
 297   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 298     f = (int_f_void_t)ps->function;
 299     res = (*f)();
 300     xbt_dynar_push_as(pair->prop_ato, int, res);
 301   }
 302
 303   xbt_dynar_push(reached_pairs, &pair);
 304
 305   MC_UNSET_RAW_MEM;
 306
 307   if(raw_mem_set)
 308     MC_SET_RAW_MEM;
 309
 310 }
 311
 312 int visited(xbt_state_t st){
 313
 314   if(_surf_mc_stateful == 0)
 315     return 0;
 316
 317   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 318
 319   MC_SET_RAW_MEM;
 320
 321   mc_pair_visited_t new_pair = NULL;
 322   new_pair = xbt_new0(s_mc_pair_visited_t, 1);
 323   new_pair->automaton_state = st;
 324   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 325   new_pair->system_state = MC_take_snapshot_liveness();
 326
 327   /* Get values of propositional symbols */
 328   int res;
 329   int_f_void_t f;
 330   unsigned int cursor = 0;
 331   xbt_propositional_symbol_t ps = NULL;
 332   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 333     f = (int_f_void_t)ps->function;
 334     res = (*f)();
 335     xbt_dynar_push_as(new_pair->prop_ato, int, res);
 336   }
 337
 338   MC_UNSET_RAW_MEM;
 339
 340   if(xbt_dynar_is_empty(visited_pairs)){
 341
 342     MC_SET_RAW_MEM;
 343     /* New pair visited */
 344     xbt_dynar_push(visited_pairs, &new_pair);
 345     MC_UNSET_RAW_MEM;
 346
 347     if(raw_mem_set)
 348       MC_SET_RAW_MEM;
 349
 350     return 0;
 351
 352   }else{
 353
 354     MC_SET_RAW_MEM;
 355
 356     cursor = 0;
 357     mc_pair_visited_t pair_test = NULL;
 358
 359     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
 360       if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
 361         XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);
 362       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 363         if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
 364           if(snapshot_compare(new_pair->system_state, pair_test->system_state, NULL, NULL) == 0){
 365             if(raw_mem_set)
 366               MC_SET_RAW_MEM;
 367             else
 368               MC_UNSET_RAW_MEM;
 369
 370             return 1;
 371           }
 372         }else{
 373           XBT_INFO("Different values of propositional symbols");
 374         }
 375       }else{
 376         XBT_INFO("Different automaton state");
 377       }
 378     }
 379
 380     if(xbt_dynar_length(visited_pairs) == _surf_mc_stateful){
 381       xbt_dynar_remove_at(visited_pairs, 0, NULL);
 382     }
 383
 384     /* New pair visited */
 385     xbt_dynar_push(visited_pairs, &new_pair);
 386
 387     MC_UNSET_RAW_MEM;
 388
 389     if(raw_mem_set)
 390       MC_SET_RAW_MEM;
 391
 392     return 0;
 393
 394   }
 395 }
 396
 397 void MC_pair_delete(mc_pair_t pair){
 398   xbt_free(pair->graph_state->proc_status);
 399   xbt_free(pair->graph_state);
 400   xbt_free(pair);
 401 }
 402
 403
 404
 405 int MC_automaton_evaluate_label(xbt_exp_label_t l){
 406
 407   switch(l->type){
 408   case 0 : {
 409     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 410     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 411     return (left_res || right_res);
 412   }
 413   case 1 : {
 414     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 415     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 416     return (left_res && right_res);
 417   }
 418   case 2 : {
 419     int res = MC_automaton_evaluate_label(l->u.exp_not);
 420     return (!res);
 421   }
 422   case 3 : {
 423     unsigned int cursor = 0;
 424     xbt_propositional_symbol_t p = NULL;
 425     int_f_void_t f;
 426     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
 427       if(strcmp(p->pred, l->u.predicat) == 0){
 428         f = (int_f_void_t)p->function;
 429         return (*f)();
 430       }
 431     }
 432     return -1;
 433   }
 434   case 4 : {
 435     return 2;
 436   }
 437   default :
 438     return -1;
 439   }
 440 }
 441
 442
 443 /********************* Double-DFS stateless *******************/
 444
 445 void pair_visited_free(mc_pair_visited_t pair){
 446   if(pair){
 447     pair->automaton_state = NULL;
 448     xbt_dynar_free(&(pair->prop_ato));
 449     MC_free_snapshot(pair->system_state);
 450     xbt_free(pair);
 451   }
 452 }
 453
 454 void pair_visited_free_voidp(void *p){
 455   pair_visited_free((mc_pair_visited_t) * (void **) p);
 456 }
 457
 458 void pair_stateless_free(mc_pair_stateless_t pair){
 459   xbt_free(pair->graph_state->system_state);
 460   xbt_free(pair->graph_state->proc_status);
 461   xbt_free(pair->graph_state);
 462   xbt_free(pair);
 463 }
 464
 465 void pair_stateless_free_voidp(void *p){
 466   pair_stateless_free((mc_pair_stateless_t) * (void **) p);
 467 }
 468
 469 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
 470   mc_pair_stateless_t p = NULL;
 471   p = xbt_new0(s_mc_pair_stateless_t, 1);
 472   p->automaton_state = st;
 473   p->graph_state = sg;
 474   p->requests = r;
 475   mc_stats_pair->expanded_pairs++;
 476   return p;
 477 }
 478
 479 void pair_reached_free(mc_pair_reached_t pair){
 480   if(pair){
 481     pair->automaton_state = NULL;
 482     xbt_dynar_free(&(pair->prop_ato));
 483     MC_free_snapshot(pair->system_state);
 484     xbt_free(pair);
 485   }
 486 }
 487
 488 void pair_reached_free_voidp(void *p){
 489   pair_reached_free((mc_pair_reached_t) * (void **) p);
 490 }
 491
 492 void MC_ddfs_init(void){
 493
 494   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 495
 496   XBT_INFO("**************************************************");
 497   XBT_INFO("Double-DFS init");
 498   XBT_INFO("**************************************************");
 499
 500   mc_pair_stateless_t mc_initial_pair = NULL;
 501   mc_state_t initial_graph_state = NULL;
 502   smx_process_t process;
 503
 504
 505   MC_wait_for_requests();
 506
 507   MC_SET_RAW_MEM;
 508
 509   initial_graph_state = MC_state_pair_new();
 510   xbt_swag_foreach(process, simix_global->process_list){
 511     if(MC_process_is_enabled(process)){
 512       MC_state_interleave_process(initial_graph_state, process);
 513     }
 514   }
 515
 516   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), pair_reached_free_voidp);
 517   visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), pair_visited_free_voidp);
 518   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 519
 520   /* Save the initial state */
 521   initial_state_liveness->initial_snapshot = MC_take_snapshot_liveness();
 522
 523   MC_UNSET_RAW_MEM;
 524
 525   unsigned int cursor = 0;
 526   xbt_state_t state;
 527
 528   xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
 529     if(state->type == -1){
 530
 531       MC_SET_RAW_MEM;
 532       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 533       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 534       MC_UNSET_RAW_MEM;
 535
 536       if(cursor != 0){
 537         MC_restore_snapshot(initial_state_liveness->initial_snapshot);
 538         MC_UNSET_RAW_MEM;
 539       }
 540
 541       MC_ddfs(0);
 542
 543     }else{
 544       if(state->type == 2){
 545
 546         MC_SET_RAW_MEM;
 547         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 548         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 549         MC_UNSET_RAW_MEM;
 550
 551         set_pair_reached(state);
 552
 553         if(cursor != 0){
 554           MC_restore_snapshot(initial_state_liveness->initial_snapshot);
 555           MC_UNSET_RAW_MEM;
 556         }
 557
 558         MC_ddfs(1);
 559
 560       }
 561     }
 562   }
 563
 564   if(raw_mem_set)
 565     MC_SET_RAW_MEM;
 566   else
 567     MC_UNSET_RAW_MEM;
 568
 569
 570 }
 571
 572
 573 void MC_ddfs(int search_cycle){
 574
 575   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 576
 577   smx_process_t process;
 578   mc_pair_stateless_t current_pair = NULL;
 579
 580   if(xbt_fifo_size(mc_stack_liveness) == 0)
 581     return;
 582
 583
 584   /* Get current pair */
 585   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 586
 587   /* Update current state in buchi automaton */
 588   _mc_property_automaton->current_state = current_pair->automaton_state;
 589
 590
 591   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
 592
 593   mc_stats_pair->visited_pairs++;
 594
 595   //sleep(1);
 596
 597   int value;
 598   mc_state_t next_graph_state = NULL;
 599   smx_simcall_t req = NULL;
 600   char *req_str;
 601
 602   xbt_transition_t transition_succ;
 603   unsigned int cursor = 0;
 604   int res;
 605
 606   mc_pair_stateless_t next_pair = NULL;
 607   mc_pair_stateless_t pair_succ;
 608
 609   mc_pair_stateless_t remove_pair;
 610   mc_pair_reached_t remove_pair_reached;
 611
 612   if(xbt_fifo_size(mc_stack_liveness) < _surf_mc_max_depth){
 613
 614     if(current_pair->requests > 0){
 615
 616       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 617
 618         /* Debug information */
 619
 620         req_str = MC_request_to_string(req, value);
 621         XBT_DEBUG("Execute: %s", req_str);
 622         xbt_free(req_str);
 623
 624         MC_state_set_executed_request(current_pair->graph_state, req, value);
 625
 626         /* Answer the request */
 627         SIMIX_simcall_pre(req, value);
 628
 629         /* Wait for requests (schedules processes) */
 630         MC_wait_for_requests();
 631
 632         MC_SET_RAW_MEM;
 633
 634         /* Create the new expanded graph_state */
 635         next_graph_state = MC_state_pair_new();
 636
 637         /* Get enabled process and insert it in the interleave set of the next graph_state */
 638
 639         xbt_swag_foreach(process, simix_global->process_list){
 640           if(MC_process_is_enabled(process)){
 641             XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call);
 642           }
 643         }
 644
 645         xbt_swag_foreach(process, simix_global->process_list){
 646           if(MC_process_is_enabled(process)){
 647             MC_state_interleave_process(next_graph_state, process);
 648           }
 649         }
 650
 651         xbt_dynar_reset(successors);
 652
 653         MC_UNSET_RAW_MEM;
 654
 655
 656         cursor= 0;
 657         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 658
 659           res = MC_automaton_evaluate_label(transition_succ->label);
 660
 661           if(res == 1){ // enabled transition in automaton
 662             MC_SET_RAW_MEM;
 663             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 664             xbt_dynar_push(successors, &next_pair);
 665             MC_UNSET_RAW_MEM;
 666           }
 667
 668         }
 669
 670         cursor = 0;
 671
 672         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 673
 674           res = MC_automaton_evaluate_label(transition_succ->label);
 675
 676           if(res == 2){ // true transition in automaton
 677             MC_SET_RAW_MEM;
 678             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 679             xbt_dynar_push(successors, &next_pair);
 680             MC_UNSET_RAW_MEM;
 681           }
 682
 683         }
 684
 685         cursor = 0;
 686
 687         xbt_dynar_foreach(successors, cursor, pair_succ){
 688
 689           if(search_cycle == 1){
 690
 691             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 692
 693               if(reached(pair_succ->automaton_state)){
 694
 695                 XBT_INFO("Next pair (depth = %d, %u interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
 696
 697                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 698                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 699                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 700                 XBT_INFO("Counter-example that violates formula :");
 701                 MC_show_stack_liveness(mc_stack_liveness);
 702                 MC_dump_stack_liveness(mc_stack_liveness);
 703                 MC_print_statistics_pairs(mc_stats_pair);
 704                 xbt_abort();
 705
 706               }else{
 707
 708                 if(visited(pair_succ->automaton_state)){
 709
 710                   XBT_DEBUG("Next pair already visited !");
 711                   break;
 712
 713                 }else{
 714
 715                   XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 716
 717                   XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 718
 719                   MC_SET_RAW_MEM;
 720                   xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 721                   MC_UNSET_RAW_MEM;
 722
 723                   MC_ddfs(search_cycle);
 724
 725                 }
 726
 727               }
 728
 729             }else{
 730
 731               if(visited(pair_succ->automaton_state)){
 732
 733                 XBT_DEBUG("Next pair already visited !");
 734                 break;
 735
 736               }else{
 737
 738                 MC_SET_RAW_MEM;
 739                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 740                 MC_UNSET_RAW_MEM;
 741
 742                 MC_ddfs(search_cycle);
 743               }
 744
 745             }
 746
 747           }else{
 748
 749             if(visited(pair_succ->automaton_state)){
 750
 751               XBT_DEBUG("Next pair already visited !");
 752               break;
 753
 754             }else{
 755
 756               if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 757
 758                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 759
 760                 set_pair_reached(pair_succ->automaton_state);
 761
 762                 search_cycle = 1;
 763
 764                 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 765
 766               }
 767
 768               MC_SET_RAW_MEM;
 769               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 770               MC_UNSET_RAW_MEM;
 771
 772               MC_ddfs(search_cycle);
 773
 774             }
 775
 776           }
 777
 778           /* Restore system before checking others successors */
 779           if(cursor != (xbt_dynar_length(successors) - 1))
 780             MC_replay_liveness(mc_stack_liveness, 1);
 781
 782         }
 783
 784         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 785           XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
 786           MC_replay_liveness(mc_stack_liveness, 0);
 787         }
 788       }
 789
 790
 791     }else{
 792
 793       XBT_DEBUG("No more request to execute in this state, search evolution in Büchi Automaton.");
 794
 795       MC_SET_RAW_MEM;
 796
 797       /* Create the new expanded graph_state */
 798       next_graph_state = MC_state_pair_new();
 799
 800       xbt_dynar_reset(successors);
 801
 802       MC_UNSET_RAW_MEM;
 803
 804
 805       cursor= 0;
 806       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 807
 808         res = MC_automaton_evaluate_label(transition_succ->label);
 809
 810         if(res == 1){ // enabled transition in automaton
 811           MC_SET_RAW_MEM;
 812           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 813           xbt_dynar_push(successors, &next_pair);
 814           MC_UNSET_RAW_MEM;
 815         }
 816
 817       }
 818
 819       cursor = 0;
 820
 821       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 822
 823         res = MC_automaton_evaluate_label(transition_succ->label);
 824
 825         if(res == 2){ // true transition in automaton
 826           MC_SET_RAW_MEM;
 827           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 828           xbt_dynar_push(successors, &next_pair);
 829           MC_UNSET_RAW_MEM;
 830         }
 831
 832       }
 833
 834       cursor = 0;
 835
 836       xbt_dynar_foreach(successors, cursor, pair_succ){
 837
 838         if(search_cycle == 1){
 839
 840           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 841
 842             if(reached(pair_succ->automaton_state)){
 843
 844               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
 845
 846               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 847               XBT_INFO("|             ACCEPTANCE CYCLE            |");
 848               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 849               XBT_INFO("Counter-example that violates formula :");
 850               MC_show_stack_liveness(mc_stack_liveness);
 851               MC_dump_stack_liveness(mc_stack_liveness);
 852               MC_print_statistics_pairs(mc_stats_pair);
 853               exit(0);
 854
 855             }else{
 856
 857               XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 858
 859               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 860
 861               MC_SET_RAW_MEM;
 862               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 863               MC_UNSET_RAW_MEM;
 864
 865               MC_ddfs(search_cycle);
 866
 867             }
 868
 869           }else{
 870
 871             MC_SET_RAW_MEM;
 872             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 873             MC_UNSET_RAW_MEM;
 874
 875             MC_ddfs(search_cycle);
 876
 877           }
 878
 879
 880         }else{
 881
 882           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 883
 884             set_pair_reached(pair_succ->automaton_state);
 885
 886             search_cycle = 1;
 887
 888             XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 889
 890           }
 891
 892           MC_SET_RAW_MEM;
 893           xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 894           MC_UNSET_RAW_MEM;
 895
 896           MC_ddfs(search_cycle);
 897
 898         }
 899
 900         /* Restore system before checking others successors */
 901         if(cursor != xbt_dynar_length(successors) - 1)
 902           MC_replay_liveness(mc_stack_liveness, 1);
 903
 904       }
 905
 906     }
 907
 908   }else{
 909
 910     XBT_DEBUG("Max depth reached");
 911
 912   }
 913
 914   if(xbt_fifo_size(mc_stack_liveness) == _surf_mc_max_depth ){
 915     XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
 916   }else{
 917     XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
 918   }
 919
 920
 921   MC_SET_RAW_MEM;
 922   remove_pair = xbt_fifo_shift(mc_stack_liveness);
 923   xbt_fifo_remove(mc_stack_liveness, remove_pair);
 924   remove_pair = NULL;
 925   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 926     remove_pair_reached = xbt_dynar_pop_as(reached_pairs, mc_pair_reached_t);
 927     pair_reached_free(remove_pair_reached);
 928     remove_pair_reached = NULL;
 929   }
 930   MC_UNSET_RAW_MEM;
 931
 932   if(raw_mem_set)
 933     MC_SET_RAW_MEM;
 934
 935 }