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->binary_global_variables_comparison_times) > 0){
  94     cursor = 0;
  95     total = 0.0;
  96     max = 0.0;
  97     min = xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double);
  98     while(cursor < xbt_dynar_length(ct->binary_global_variables_comparison_times) - 1){
  99       total += xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double);
 100       if(xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double) > max)
 101         max = xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double);
 102       if(xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double) < min)
 103         min = xbt_dynar_get_as(ct->binary_global_variables_comparison_times, cursor, double);
 104       cursor++;
 105     }
 106     XBT_DEBUG("Binary global variables comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->binary_global_variables_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->binary_global_variables_comparison_times), max, min);
 107   }
 108
 109   if(xbt_dynar_length(ct->libsimgrid_global_variables_comparison_times) > 0){
 110     cursor = 0;
 111     total = 0.0;
 112     max = 0.0;
 113     min = xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double);
 114     while(cursor < xbt_dynar_length(ct->libsimgrid_global_variables_comparison_times) - 1){
 115       total += xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double);
 116       if(xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double) > max)
 117         max = xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double);
 118       if(xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double) < min)
 119         min = xbt_dynar_get_as(ct->libsimgrid_global_variables_comparison_times, cursor, double);
 120       cursor++;
 121     }
 122     XBT_DEBUG("Libsimgrid global variables comparison -- Different states : %lu/%d, time (in seconds) : average = %lf, max = %lf, min = %lf", xbt_dynar_length(ct->libsimgrid_global_variables_comparison_times), ct->nb_comparisons, total/xbt_dynar_length(ct->libsimgrid_global_variables_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->binary_global_variables_comparison_times = xbt_dynar_new(sizeof(double), NULL);
 183   ct->libsimgrid_global_variables_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   int 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();
 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_DEBUG("Different values of propositional symbols");
 251         }
 252       }else{
 253         XBT_DEBUG("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   int 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();
 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(_sg_mc_visited == 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();
 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_DEBUG("Different values of propositional symbols");
 374         }
 375       }else{
 376         XBT_DEBUG("Different automaton state");
 377       }
 378     }
 379
 380     if(xbt_dynar_length(visited_pairs) == _sg_mc_visited){
 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     if(pair->comparison_times != NULL){
 484       xbt_dynar_free(&(pair->comparison_times->snapshot_comparison_times));
 485       xbt_dynar_free(&(pair->comparison_times->chunks_used_comparison_times));
 486       xbt_dynar_free(&(pair->comparison_times->stacks_sizes_comparison_times));
 487       xbt_dynar_free(&(pair->comparison_times->binary_global_variables_comparison_times));
 488       xbt_dynar_free(&(pair->comparison_times->libsimgrid_global_variables_comparison_times));
 489       xbt_dynar_free(&(pair->comparison_times->heap_comparison_times));
 490       xbt_dynar_free(&(pair->comparison_times->stacks_comparison_times));
 491     }
 492     MC_free_snapshot(pair->system_state);
 493     xbt_free(pair);
 494   }
 495 }
 496
 497 void pair_reached_free_voidp(void *p){
 498   pair_reached_free((mc_pair_reached_t) * (void **) p);
 499 }
 500
 501 void MC_ddfs_init(void){
 502
 503   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 504
 505   XBT_DEBUG("**************************************************");
 506   XBT_DEBUG("Double-DFS init");
 507   XBT_DEBUG("**************************************************");
 508
 509   mc_pair_stateless_t mc_initial_pair = NULL;
 510   mc_state_t initial_graph_state = NULL;
 511   smx_process_t process;
 512
 513
 514   MC_wait_for_requests();
 515
 516   MC_SET_RAW_MEM;
 517
 518   initial_graph_state = MC_state_pair_new();
 519   xbt_swag_foreach(process, simix_global->process_list){
 520     if(MC_process_is_enabled(process)){
 521       MC_state_interleave_process(initial_graph_state, process);
 522     }
 523   }
 524
 525   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), pair_reached_free_voidp);
 526   visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), pair_visited_free_voidp);
 527   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 528
 529   /* Save the initial state */
 530   initial_state_liveness->snapshot = MC_take_snapshot();
 531
 532   MC_UNSET_RAW_MEM;
 533
 534   unsigned int cursor = 0;
 535   xbt_state_t state;
 536
 537   xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
 538     if(state->type == -1){
 539
 540       MC_SET_RAW_MEM;
 541       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 542       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 543       MC_UNSET_RAW_MEM;
 544
 545       if(cursor != 0){
 546         MC_restore_snapshot(initial_state_liveness->snapshot);
 547         MC_UNSET_RAW_MEM;
 548       }
 549
 550       MC_ddfs(0);
 551
 552     }else{
 553       if(state->type == 2){
 554
 555         MC_SET_RAW_MEM;
 556         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 557         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 558         MC_UNSET_RAW_MEM;
 559
 560         set_pair_reached(state);
 561
 562         if(cursor != 0){
 563           MC_restore_snapshot(initial_state_liveness->snapshot);
 564           MC_UNSET_RAW_MEM;
 565         }
 566
 567         MC_ddfs(1);
 568
 569       }
 570     }
 571   }
 572
 573   if(initial_state_liveness->raw_mem_set)
 574     MC_SET_RAW_MEM;
 575   else
 576     MC_UNSET_RAW_MEM;
 577
 578
 579 }
 580
 581
 582 void MC_ddfs(int search_cycle){
 583
 584   //initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 585
 586   smx_process_t process;
 587   mc_pair_stateless_t current_pair = NULL;
 588
 589   if(xbt_fifo_size(mc_stack_liveness) == 0)
 590     return;
 591
 592
 593   /* Get current pair */
 594   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 595
 596   /* Update current state in buchi automaton */
 597   _mc_property_automaton->current_state = current_pair->automaton_state;
 598
 599
 600   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
 601
 602   mc_stats_pair->visited_pairs++;
 603
 604   //sleep(1);
 605
 606   int value;
 607   mc_state_t next_graph_state = NULL;
 608   smx_simcall_t req = NULL;
 609   char *req_str;
 610
 611   xbt_transition_t transition_succ;
 612   unsigned int cursor = 0;
 613   int res;
 614
 615   mc_pair_stateless_t next_pair = NULL;
 616   mc_pair_stateless_t pair_succ;
 617
 618   mc_pair_stateless_t remove_pair;
 619   mc_pair_reached_t remove_pair_reached;
 620
 621   if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
 622
 623     if(current_pair->requests > 0){
 624
 625       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 626
 627         /* Debug information */
 628
 629         req_str = MC_request_to_string(req, value);
 630         XBT_DEBUG("Execute: %s", req_str);
 631         xbt_free(req_str);
 632
 633         MC_state_set_executed_request(current_pair->graph_state, req, value);
 634
 635         /* Answer the request */
 636         SIMIX_simcall_pre(req, value);
 637
 638         /* Wait for requests (schedules processes) */
 639         MC_wait_for_requests();
 640
 641         MC_SET_RAW_MEM;
 642
 643         /* Create the new expanded graph_state */
 644         next_graph_state = MC_state_pair_new();
 645
 646         /* Get enabled process and insert it in the interleave set of the next graph_state */
 647         xbt_swag_foreach(process, simix_global->process_list){
 648           if(MC_process_is_enabled(process)){
 649             XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call);
 650           }
 651         }
 652
 653         xbt_swag_foreach(process, simix_global->process_list){
 654           if(MC_process_is_enabled(process)){
 655             MC_state_interleave_process(next_graph_state, process);
 656           }
 657         }
 658
 659         xbt_dynar_reset(successors);
 660
 661         MC_UNSET_RAW_MEM;
 662
 663
 664         cursor= 0;
 665         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 666
 667           res = MC_automaton_evaluate_label(transition_succ->label);
 668
 669           if(res == 1){ // enabled transition in automaton
 670             MC_SET_RAW_MEM;
 671             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 672             xbt_dynar_push(successors, &next_pair);
 673             MC_UNSET_RAW_MEM;
 674           }
 675
 676         }
 677
 678         cursor = 0;
 679
 680         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 681
 682           res = MC_automaton_evaluate_label(transition_succ->label);
 683
 684           if(res == 2){ // true transition in automaton
 685             MC_SET_RAW_MEM;
 686             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 687             xbt_dynar_push(successors, &next_pair);
 688             MC_UNSET_RAW_MEM;
 689           }
 690
 691         }
 692
 693         cursor = 0;
 694
 695         xbt_dynar_foreach(successors, cursor, pair_succ){
 696
 697           if(search_cycle == 1){
 698
 699             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 700
 701               if(reached(pair_succ->automaton_state)){
 702
 703                 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));
 704
 705                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 706                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 707                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 708                 XBT_INFO("Counter-example that violates formula :");
 709                 MC_show_stack_liveness(mc_stack_liveness);
 710                 MC_dump_stack_liveness(mc_stack_liveness);
 711                 MC_print_statistics_pairs(mc_stats_pair);
 712                 xbt_abort();
 713
 714               }else{
 715
 716                 if(visited(pair_succ->automaton_state)){
 717
 718                   XBT_DEBUG("Next pair already visited !");
 719                   break;
 720
 721                 }else{
 722
 723                   XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 724
 725                   XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 726
 727                   MC_SET_RAW_MEM;
 728                   xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 729                   MC_UNSET_RAW_MEM;
 730
 731                   MC_ddfs(search_cycle);
 732
 733                 }
 734
 735               }
 736
 737             }else{
 738
 739               if(visited(pair_succ->automaton_state)){
 740
 741                 XBT_DEBUG("Next pair already visited !");
 742                 break;
 743
 744               }else{
 745
 746                 MC_SET_RAW_MEM;
 747                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 748                 MC_UNSET_RAW_MEM;
 749
 750                 MC_ddfs(search_cycle);
 751               }
 752
 753             }
 754
 755           }else{
 756
 757             if(visited(pair_succ->automaton_state)){
 758
 759               XBT_DEBUG("Next pair already visited !");
 760               break;
 761
 762             }else{
 763
 764               if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 765
 766                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 767
 768                 set_pair_reached(pair_succ->automaton_state);
 769
 770                 search_cycle = 1;
 771
 772                 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 773
 774               }
 775
 776               MC_SET_RAW_MEM;
 777               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 778               MC_UNSET_RAW_MEM;
 779
 780               MC_ddfs(search_cycle);
 781
 782             }
 783
 784           }
 785
 786           /* Restore system before checking others successors */
 787           if(cursor != (xbt_dynar_length(successors) - 1))
 788             MC_replay_liveness(mc_stack_liveness, 1);
 789
 790         }
 791
 792         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 793           XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
 794           MC_replay_liveness(mc_stack_liveness, 0);
 795         }
 796       }
 797
 798
 799     }else{
 800
 801       XBT_DEBUG("No more request to execute in this state, search evolution in Büchi Automaton.");
 802
 803       MC_SET_RAW_MEM;
 804
 805       /* Create the new expanded graph_state */
 806       next_graph_state = MC_state_pair_new();
 807
 808       xbt_dynar_reset(successors);
 809
 810       MC_UNSET_RAW_MEM;
 811
 812
 813       cursor= 0;
 814       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 815
 816         res = MC_automaton_evaluate_label(transition_succ->label);
 817
 818         if(res == 1){ // enabled transition in automaton
 819           MC_SET_RAW_MEM;
 820           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 821           xbt_dynar_push(successors, &next_pair);
 822           MC_UNSET_RAW_MEM;
 823         }
 824
 825       }
 826
 827       cursor = 0;
 828
 829       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 830
 831         res = MC_automaton_evaluate_label(transition_succ->label);
 832
 833         if(res == 2){ // true transition in automaton
 834           MC_SET_RAW_MEM;
 835           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 836           xbt_dynar_push(successors, &next_pair);
 837           MC_UNSET_RAW_MEM;
 838         }
 839
 840       }
 841
 842       cursor = 0;
 843
 844       xbt_dynar_foreach(successors, cursor, pair_succ){
 845
 846         if(search_cycle == 1){
 847
 848           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 849
 850             if(reached(pair_succ->automaton_state)){
 851
 852               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
 853
 854               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 855               XBT_INFO("|             ACCEPTANCE CYCLE            |");
 856               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 857               XBT_INFO("Counter-example that violates formula :");
 858               MC_show_stack_liveness(mc_stack_liveness);
 859               MC_dump_stack_liveness(mc_stack_liveness);
 860               MC_print_statistics_pairs(mc_stats_pair);
 861               xbt_abort();
 862
 863             }else{
 864
 865               XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 866
 867               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 868
 869               MC_SET_RAW_MEM;
 870               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 871               MC_UNSET_RAW_MEM;
 872
 873               MC_ddfs(search_cycle);
 874
 875             }
 876
 877           }else{
 878
 879             MC_SET_RAW_MEM;
 880             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 881             MC_UNSET_RAW_MEM;
 882
 883             MC_ddfs(search_cycle);
 884
 885           }
 886
 887
 888         }else{
 889
 890           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 891
 892             set_pair_reached(pair_succ->automaton_state);
 893
 894             search_cycle = 1;
 895
 896             XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 897
 898           }
 899
 900           MC_SET_RAW_MEM;
 901           xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 902           MC_UNSET_RAW_MEM;
 903
 904           MC_ddfs(search_cycle);
 905
 906         }
 907
 908         /* Restore system before checking others successors */
 909         if(cursor != xbt_dynar_length(successors) - 1)
 910           MC_replay_liveness(mc_stack_liveness, 1);
 911
 912       }
 913
 914     }
 915
 916   }else{
 917
 918     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 919     if(current_pair->requests > 0){
 920       XBT_WARN("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
 921       XBT_WARN("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
 922     }
 923
 924   }
 925
 926   if(xbt_fifo_size(mc_stack_liveness) == _sg_mc_max_depth ){
 927     XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
 928   }else{
 929     XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
 930   }
 931
 932
 933   MC_SET_RAW_MEM;
 934   remove_pair = xbt_fifo_shift(mc_stack_liveness);
 935   xbt_fifo_remove(mc_stack_liveness, remove_pair);
 936   remove_pair = NULL;
 937   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 938     remove_pair_reached = xbt_dynar_pop_as(reached_pairs, mc_pair_reached_t);
 939     pair_reached_free(remove_pair_reached);
 940     remove_pair_reached = NULL;
 941   }
 942   MC_UNSET_RAW_MEM;
 943
 944   /*if(initial_state_liveness->raw_mem_set)
 945     MC_SET_RAW_MEM;*/
 946
 947 }