src/mc/mc_liveness.c

   1 #include "private.h"
   2 #include "unistd.h"
   3
   4 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
   5                                 "Logging specific to algorithms for liveness properties verification");
   6
   7 xbt_dynar_t reached_pairs;
   8 xbt_dynar_t reached_pairs_hash;
   9 xbt_dynar_t visited_pairs;
  10 xbt_dynar_t visited_pairs_hash;
  11 xbt_dynar_t successors;
  12
  13
  14 /* fast implementation of djb2 algorithm */
  15 unsigned int hash_region(char *str, int str_len){
  16
  17   int c;
  18   register unsigned int hash = 5381;
  19
  20   while (str_len--) {
  21     c = *str++;
  22     hash = ((hash << 5) + hash) + c;    /* hash * 33 + c */
  23   }
  24
  25   return hash;
  26
  27 }
  28
  29 int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
  30
  31
  32   if(s1->num_reg != s2->num_reg){
  33     XBT_DEBUG("Different num_reg (s1 = %d, s2 = %d)", s1->num_reg, s2->num_reg);
  34     return 1;
  35   }
  36
  37   int i;
  38   int errors = 0;
  39
  40   for(i=0 ; i< s1->num_reg ; i++){
  41
  42     if(s1->regions[i]->type != s2->regions[i]->type){
  43       if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
  44         XBT_DEBUG("Different type of region");
  45         errors++;
  46       }else{
  47         return 1;
  48       }
  49     }
  50
  51     switch(s1->regions[i]->type){
  52     case 0:
  53       if(s1->regions[i]->size != s2->regions[i]->size){
  54         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
  55           XBT_DEBUG("Different size of heap (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
  56           errors++;
  57         }else{
  58           return 1;
  59         }
  60       }
  61       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
  62         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
  63           XBT_DEBUG("Different start addr of heap (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
  64           errors++;
  65         }else{
  66           return 1;
  67         }
  68       }
  69       if(mmalloc_compare_heap(s1->regions[i]->data, s2->regions[i]->data)){
  70         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
  71           XBT_DEBUG("Different heap (mmalloc_compare)");
  72           errors++;
  73         }else{
  74           return 1;
  75         }
  76       }
  77       break;
  78     case 1 :
  79       if(s1->regions[i]->size != s2->regions[i]->size){
  80         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
  81           XBT_DEBUG("Different size of libsimgrid (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
  82           errors++;
  83         }else{
  84           return 1;
  85         }
  86       }
  87       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
  88         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
  89           XBT_DEBUG("Different start addr of libsimgrid (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
  90           errors++;
  91         }else{
  92           return 1;
  93         }
  94       }
  95       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
  96         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
  97           XBT_DEBUG("Different memcmp for data in libsimgrid");
  98           errors++;
  99         }else{
 100           return 1;
 101         }
 102       }
 103       break;
 104       /*case 2:
 105       if(s1->regions[i]->size != s2->regions[i]->size){
 106         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 107           XBT_DEBUG("Different size of program (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
 108           errors++;
 109         }else{
 110           return 1;
 111         }
 112       }
 113       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
 114         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 115           XBT_DEBUG("Different start addr of program (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
 116           errors++;
 117         }else{
 118           return 1;
 119         }
 120       }
 121       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
 122         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 123           XBT_DEBUG("Different memcmp for data in program");
 124           errors++;
 125         }else{
 126           return 1;
 127         }
 128       }
 129       break;*/
 130     case 3:
 131       if(s1->regions[i]->size != s2->regions[i]->size){
 132         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 133           XBT_DEBUG("Different size of stack (s1 = %zu, s2 = %zu)", s1->regions[i]->size, s2->regions[i]->size);
 134           errors++;
 135         }else{
 136           return 1;
 137         }
 138       }
 139       if(s1->regions[i]->start_addr != s2->regions[i]->start_addr){
 140         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 141           XBT_DEBUG("Different start addr of stack (s1 = %p, s2 = %p)", s1->regions[i]->start_addr, s2->regions[i]->start_addr);
 142           errors++;
 143         }else{
 144           return 1;
 145         }
 146       }
 147       if(memcmp(s1->regions[i]->data, s2->regions[i]->data, s1->regions[i]->size) != 0){
 148         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 149           XBT_DEBUG("Different memcmp for data in stack");
 150           errors++;
 151         }else{
 152           return 1;
 153         }
 154       }
 155       break;
 156     default:
 157       break;
 158     }
 159   }
 160
 161   if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 162     return (errors>0);
 163   }else{
 164     return 0;
 165   }
 166
 167 }
 168
 169 int reached(xbt_state_t st){
 170
 171
 172   if(xbt_dynar_is_empty(reached_pairs)){
 173
 174     return 0;
 175
 176   }else{
 177
 178     MC_SET_RAW_MEM;
 179
 180     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 181     MC_take_snapshot_liveness(sn);
 182
 183     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 184     int res;
 185     int (*f)();
 186
 187     /* Get values of propositional symbols */
 188     unsigned int cursor = 0;
 189     xbt_propositional_symbol_t ps = NULL;
 190     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 191       f = ps->function;
 192       res = (*f)();
 193       xbt_dynar_push_as(prop_ato, int, res);
 194     }
 195
 196     cursor = 0;
 197     mc_pair_reached_t pair_test = NULL;
 198
 199
 200     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
 201       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 202         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 203           XBT_DEBUG("Pair reached %d", cursor+1);
 204           if(snapshot_compare(pair_test->system_state, sn) == 0){
 205             MC_free_snapshot(sn);
 206             xbt_dynar_reset(prop_ato);
 207             xbt_free(prop_ato);
 208             MC_UNSET_RAW_MEM;
 209             return 1;
 210           }
 211         }
 212       }
 213     }
 214
 215     MC_free_snapshot(sn);
 216     xbt_dynar_reset(prop_ato);
 217     xbt_free(prop_ato);
 218     MC_UNSET_RAW_MEM;
 219     return 0;
 220
 221   }
 222 }
 223
 224 void set_pair_reached(xbt_state_t st){
 225
 226
 227   MC_SET_RAW_MEM;
 228
 229   mc_pair_reached_t pair = NULL;
 230   pair = xbt_new0(s_mc_pair_reached_t, 1);
 231   pair->automaton_state = st;
 232   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 233   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
 234   MC_take_snapshot_liveness(pair->system_state);
 235
 236   /* Get values of propositional symbols */
 237   unsigned int cursor = 0;
 238   xbt_propositional_symbol_t ps = NULL;
 239   int res;
 240   int (*f)();
 241
 242   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 243     f = ps->function;
 244     res = (*f)();
 245     xbt_dynar_push_as(pair->prop_ato, int, res);
 246   }
 247
 248   xbt_dynar_push(reached_pairs, &pair);
 249
 250   MC_UNSET_RAW_MEM;
 251
 252 }
 253
 254 int reached_hash(xbt_state_t st){
 255
 256
 257   if(xbt_dynar_is_empty(reached_pairs_hash)){
 258
 259     return 0;
 260
 261   }else{
 262
 263     MC_SET_RAW_MEM;
 264
 265     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 266     MC_take_snapshot_liveness(sn);
 267
 268     int j;
 269     unsigned int hash_regions[sn->num_reg];
 270     for(j=0; j<sn->num_reg; j++){
 271       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
 272     }
 273
 274
 275     /* Get values of propositional symbols */
 276     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 277     unsigned int cursor = 0;
 278     xbt_propositional_symbol_t ps = NULL;
 279     int res;
 280     int (*f)();
 281
 282     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 283       f = ps->function;
 284       res = (*f)();
 285       xbt_dynar_push_as(prop_ato, int, res);
 286     }
 287
 288     mc_pair_reached_hash_t pair_test = NULL;
 289
 290     int region_diff = 0;
 291
 292     cursor = 0;
 293
 294     xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
 295
 296       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 297         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 298           for(j=0 ; j< sn->num_reg ; j++){
 299             if(hash_regions[j] != pair_test->hash_regions[j]){
 300               region_diff++;
 301             }
 302           }
 303           if(region_diff == 0){
 304             MC_free_snapshot(sn);
 305             xbt_dynar_reset(prop_ato);
 306             xbt_free(prop_ato);
 307             MC_UNSET_RAW_MEM;
 308             return 1;
 309           }
 310         }
 311       }
 312
 313
 314       region_diff = 0;
 315     }
 316
 317     MC_free_snapshot(sn);
 318     xbt_dynar_reset(prop_ato);
 319     xbt_free(prop_ato);
 320     MC_UNSET_RAW_MEM;
 321     return 0;
 322
 323   }
 324 }
 325
 326 void set_pair_reached_hash(xbt_state_t st){
 327
 328   MC_SET_RAW_MEM;
 329
 330   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 331   MC_take_snapshot_liveness(sn);
 332
 333   mc_pair_reached_hash_t pair = NULL;
 334   pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
 335   pair->automaton_state = st;
 336   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 337   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
 338
 339   int i;
 340
 341   for(i=0 ; i< sn->num_reg ; i++){
 342     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
 343   }
 344
 345   /* Get values of propositional symbols */
 346   unsigned int cursor = 0;
 347   xbt_propositional_symbol_t ps = NULL;
 348   int res;
 349   int (*f)();
 350
 351   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 352     f = ps->function;
 353     res = (*f)();
 354     xbt_dynar_push_as(pair->prop_ato, int, res);
 355   }
 356
 357   xbt_dynar_push(reached_pairs_hash, &pair);
 358
 359   MC_free_snapshot(sn);
 360
 361   MC_UNSET_RAW_MEM;
 362
 363 }
 364
 365
 366 int visited(xbt_state_t st, int sc){
 367
 368
 369   if(xbt_dynar_is_empty(visited_pairs)){
 370
 371     return 0;
 372
 373   }else{
 374
 375     MC_SET_RAW_MEM;
 376
 377     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 378     MC_take_snapshot_liveness(sn);
 379
 380     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 381
 382     /* Get values of propositional symbols */
 383     unsigned int cursor = 0;
 384     xbt_propositional_symbol_t ps = NULL;
 385     int res;
 386     int (*f)();
 387
 388     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 389       f = ps->function;
 390       res = (*f)();
 391       xbt_dynar_push_as(prop_ato, int, res);
 392     }
 393
 394     cursor = 0;
 395     mc_pair_visited_t pair_test = NULL;
 396
 397     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
 398       if(pair_test->search_cycle == sc) {
 399         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 400           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 401             if(snapshot_compare(pair_test->system_state, sn) == 0){
 402
 403               MC_free_snapshot(sn);
 404               xbt_dynar_reset(prop_ato);
 405               xbt_free(prop_ato);
 406               MC_UNSET_RAW_MEM;
 407
 408               return 1;
 409
 410             }
 411           }
 412         }
 413       }
 414     }
 415
 416
 417     MC_free_snapshot(sn);
 418     xbt_dynar_reset(prop_ato);
 419     xbt_free(prop_ato);
 420     MC_UNSET_RAW_MEM;
 421     return 0;
 422
 423   }
 424 }
 425
 426
 427 int visited_hash(xbt_state_t st, int sc){
 428
 429
 430   if(xbt_dynar_is_empty(visited_pairs_hash)){
 431
 432     return 0;
 433
 434   }else{
 435
 436     MC_SET_RAW_MEM;
 437
 438     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 439     MC_take_snapshot_liveness(sn);
 440
 441     int j;
 442     unsigned int hash_regions[sn->num_reg];
 443     for(j=0; j<sn->num_reg; j++){
 444       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
 445     }
 446
 447
 448     /* Get values of propositional symbols */
 449     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 450     unsigned int cursor = 0;
 451     xbt_propositional_symbol_t ps = NULL;
 452     int res;
 453     int (*f)();
 454
 455     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 456       f = ps->function;
 457       res = (*f)();
 458       xbt_dynar_push_as(prop_ato, int, res);
 459     }
 460
 461     mc_pair_visited_hash_t pair_test = NULL;
 462
 463     int region_diff = 0;
 464     cursor = 0;
 465
 466     xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
 467
 468       if(pair_test->search_cycle == sc) {
 469         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 470           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 471             for(j=0 ; j< sn->num_reg ; j++){
 472               if(hash_regions[j] != pair_test->hash_regions[j]){
 473                 region_diff++;
 474               }
 475             }
 476             if(region_diff == 0){
 477               MC_free_snapshot(sn);
 478               xbt_dynar_reset(prop_ato);
 479               xbt_free(prop_ato);
 480               MC_UNSET_RAW_MEM;
 481               return 1;
 482             }
 483           }
 484         }
 485       }
 486
 487       region_diff = 0;
 488     }
 489
 490     MC_free_snapshot(sn);
 491     xbt_dynar_reset(prop_ato);
 492     xbt_free(prop_ato);
 493     MC_UNSET_RAW_MEM;
 494     return 0;
 495
 496   }
 497 }
 498
 499 void set_pair_visited_hash(xbt_state_t st, int sc){
 500
 501   MC_SET_RAW_MEM;
 502
 503   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 504   MC_take_snapshot_liveness(sn);
 505
 506   mc_pair_visited_hash_t pair = NULL;
 507   pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
 508   pair->automaton_state = st;
 509   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 510   pair->search_cycle = sc;
 511   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
 512
 513   int i;
 514
 515   for(i=0 ; i< sn->num_reg ; i++){
 516     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
 517   }
 518
 519   /* Get values of propositional symbols */
 520   unsigned int cursor = 0;
 521   xbt_propositional_symbol_t ps = NULL;
 522   int res;
 523   int (*f)();
 524
 525   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 526     f = ps->function;
 527     res = (*f)();
 528     xbt_dynar_push_as(pair->prop_ato, int, res);
 529   }
 530
 531   xbt_dynar_push(visited_pairs_hash, &pair);
 532
 533   MC_free_snapshot(sn);
 534
 535   MC_UNSET_RAW_MEM;
 536
 537 }
 538
 539 void set_pair_visited(xbt_state_t st, int sc){
 540
 541
 542   MC_SET_RAW_MEM;
 543
 544   mc_pair_visited_t pair = NULL;
 545   pair = xbt_new0(s_mc_pair_visited_t, 1);
 546   pair->automaton_state = st;
 547   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 548   pair->search_cycle = sc;
 549   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
 550   MC_take_snapshot_liveness(pair->system_state);
 551
 552
 553   /* Get values of propositional symbols */
 554   unsigned int cursor = 0;
 555   xbt_propositional_symbol_t ps = NULL;
 556   int res;
 557   int (*f)();
 558
 559   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 560     f = ps->function;
 561     res = (*f)();
 562     xbt_dynar_push_as(pair->prop_ato, int, res);
 563   }
 564
 565   xbt_dynar_push(visited_pairs, &pair);
 566
 567   MC_UNSET_RAW_MEM;
 568
 569
 570 }
 571
 572 void MC_pair_delete(mc_pair_t pair){
 573   xbt_free(pair->graph_state->proc_status);
 574   xbt_free(pair->graph_state);
 575   xbt_free(pair);
 576 }
 577
 578
 579
 580 int MC_automaton_evaluate_label(xbt_exp_label_t l){
 581
 582   switch(l->type){
 583   case 0 : {
 584     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 585     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 586     return (left_res || right_res);
 587     break;
 588   }
 589   case 1 : {
 590     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 591     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 592     return (left_res && right_res);
 593     break;
 594   }
 595   case 2 : {
 596     int res = MC_automaton_evaluate_label(l->u.exp_not);
 597     return (!res);
 598     break;
 599   }
 600   case 3 : {
 601     unsigned int cursor = 0;
 602     xbt_propositional_symbol_t p = NULL;
 603     int (*f)();
 604     xbt_dynar_foreach(automaton->propositional_symbols, cursor, p){
 605       if(strcmp(p->pred, l->u.predicat) == 0){
 606         f = p->function;
 607         return (*f)();
 608       }
 609     }
 610     return -1;
 611     break;
 612   }
 613   case 4 : {
 614     return 2;
 615     break;
 616   }
 617   default :
 618     return -1;
 619   }
 620 }
 621
 622
 623
 624
 625
 626 /********************* Double-DFS stateless *******************/
 627
 628 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
 629   xbt_free(pair->graph_state->proc_status);
 630   xbt_free(pair->graph_state);
 631   xbt_free(pair);
 632 }
 633
 634 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
 635   mc_pair_stateless_t p = NULL;
 636   p = xbt_new0(s_mc_pair_stateless_t, 1);
 637   p->automaton_state = st;
 638   p->graph_state = sg;
 639   p->requests = r;
 640   mc_stats_pair->expanded_pairs++;
 641   return p;
 642 }
 643
 644 void MC_ddfs_init(void){
 645
 646   XBT_DEBUG("**************************************************");
 647   XBT_DEBUG("Double-DFS init");
 648   XBT_DEBUG("**************************************************");
 649
 650   mc_pair_stateless_t mc_initial_pair = NULL;
 651   mc_state_t initial_graph_state = NULL;
 652   smx_process_t process;
 653
 654   MC_wait_for_requests();
 655
 656   MC_SET_RAW_MEM;
 657
 658   initial_graph_state = MC_state_pair_new();
 659   xbt_swag_foreach(process, simix_global->process_list){
 660     if(MC_process_is_enabled(process)){
 661       MC_state_interleave_process(initial_graph_state, process);
 662     }
 663   }
 664
 665   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
 666   //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
 667   //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
 668   visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
 669   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 670
 671   /* Save the initial state */
 672   initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
 673   MC_take_snapshot_to_restore_liveness(initial_snapshot_liveness);
 674
 675   MC_UNSET_RAW_MEM;
 676
 677   unsigned int cursor = 0;
 678   xbt_state_t state;
 679
 680   xbt_dynar_foreach(automaton->states, cursor, state){
 681     if(state->type == -1){
 682
 683       MC_SET_RAW_MEM;
 684       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 685       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 686       MC_UNSET_RAW_MEM;
 687
 688       if(cursor != 0){
 689         MC_restore_snapshot(initial_snapshot_liveness);
 690         MC_UNSET_RAW_MEM;
 691       }
 692
 693       MC_ddfs(0);
 694
 695     }else{
 696       if(state->type == 2){
 697
 698         MC_SET_RAW_MEM;
 699         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 700         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 701         MC_UNSET_RAW_MEM;
 702
 703         set_pair_reached(state);
 704         //set_pair_reached_hash(state);
 705
 706         if(cursor != 0){
 707           MC_restore_snapshot(initial_snapshot_liveness);
 708           MC_UNSET_RAW_MEM;
 709         }
 710
 711         MC_ddfs(1);
 712
 713       }
 714     }
 715   }
 716
 717 }
 718
 719
 720 void MC_ddfs(int search_cycle){
 721
 722   smx_process_t process;
 723   mc_pair_stateless_t current_pair = NULL;
 724
 725   if(xbt_fifo_size(mc_stack_liveness) == 0)
 726     return;
 727
 728
 729   /* Get current pair */
 730   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 731
 732   /* Update current state in buchi automaton */
 733   automaton->current_state = current_pair->automaton_state;
 734
 735
 736   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
 737   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));
 738
 739   mc_stats_pair->visited_pairs++;
 740
 741   sleep(1);
 742
 743   int value;
 744   mc_state_t next_graph_state = NULL;
 745   smx_req_t req = NULL;
 746   char *req_str;
 747
 748   xbt_transition_t transition_succ;
 749   unsigned int cursor = 0;
 750   int res;
 751
 752   mc_pair_stateless_t next_pair = NULL;
 753   mc_pair_stateless_t pair_succ;
 754
 755   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
 756
 757     //set_pair_visited(current_pair->automaton_state, search_cycle);
 758     set_pair_visited_hash(current_pair->automaton_state, search_cycle);
 759
 760     //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
 761     XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
 762
 763     if(current_pair->requests > 0){
 764
 765       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 766
 767         /* Debug information */
 768         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 769           req_str = MC_request_to_string(req, value);
 770           XBT_DEBUG("Execute: %s", req_str);
 771           xbt_free(req_str);
 772         }
 773
 774         MC_state_set_executed_request(current_pair->graph_state, req, value);
 775
 776         /* Answer the request */
 777         SIMIX_request_pre(req, value);
 778
 779         /* Wait for requests (schedules processes) */
 780         MC_wait_for_requests();
 781
 782
 783         MC_SET_RAW_MEM;
 784
 785         /* Create the new expanded graph_state */
 786         next_graph_state = MC_state_pair_new();
 787
 788         /* Get enabled process and insert it in the interleave set of the next graph_state */
 789         xbt_swag_foreach(process, simix_global->process_list){
 790           if(MC_process_is_enabled(process)){
 791             MC_state_interleave_process(next_graph_state, process);
 792           }
 793         }
 794
 795         xbt_dynar_reset(successors);
 796
 797         MC_UNSET_RAW_MEM;
 798
 799
 800         cursor= 0;
 801         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 802
 803           res = MC_automaton_evaluate_label(transition_succ->label);
 804
 805           if(res == 1){ // enabled transition in automaton
 806             MC_SET_RAW_MEM;
 807             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 808             xbt_dynar_push(successors, &next_pair);
 809             MC_UNSET_RAW_MEM;
 810           }
 811
 812         }
 813
 814         cursor = 0;
 815
 816         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 817
 818           res = MC_automaton_evaluate_label(transition_succ->label);
 819
 820           if(res == 2){ // true transition in automaton
 821             MC_SET_RAW_MEM;
 822             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 823             xbt_dynar_push(successors, &next_pair);
 824             MC_UNSET_RAW_MEM;
 825           }
 826
 827         }
 828
 829         cursor = 0;
 830
 831         xbt_dynar_foreach(successors, cursor, pair_succ){
 832
 833           if(search_cycle == 1){
 834
 835             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 836
 837               if(reached(pair_succ->automaton_state)){
 838                 //if(reached_hash(pair_succ->automaton_state)){
 839
 840                 XBT_DEBUG("Next pair (depth = %d, %d interleave) already reached !", xbt_fifo_size(mc_stack_liveness) + 1, MC_state_interleave_size(pair_succ->graph_state));
 841
 842                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 843                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 844                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 845                 XBT_INFO("Counter-example that violates formula :");
 846                 MC_show_stack_liveness(mc_stack_liveness);
 847                 MC_dump_stack_liveness(mc_stack_liveness);
 848                 MC_print_statistics_pairs(mc_stats_pair);
 849                 exit(0);
 850
 851               }else{
 852
 853                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 854
 855                 set_pair_reached(pair_succ->automaton_state);
 856                 //set_pair_reached_hash(pair_succ->automaton_state);
 857
 858                 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 859                 //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 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               if(!visited_hash(pair_succ->automaton_state, search_cycle)){
 872                 //if(!visited(pair_succ->automaton_state, search_cycle)){
 873
 874                 MC_SET_RAW_MEM;
 875                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 876                 MC_UNSET_RAW_MEM;
 877
 878                 MC_ddfs(search_cycle);
 879
 880               }else{
 881
 882                 XBT_DEBUG("Next pair already visited ! ");
 883
 884               }
 885
 886             }
 887
 888           }else{
 889
 890             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 891
 892               XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
 893
 894               set_pair_reached(pair_succ->automaton_state);
 895               //set_pair_reached_hash(pair_succ->automaton_state);
 896
 897               search_cycle = 1;
 898
 899               XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 900               //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 901
 902             }
 903
 904             if(!visited_hash(pair_succ->automaton_state, search_cycle)){
 905               //if(!visited(pair_succ->automaton_state, search_cycle)){
 906
 907               MC_SET_RAW_MEM;
 908               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 909               MC_UNSET_RAW_MEM;
 910
 911               MC_ddfs(search_cycle);
 912
 913             }else{
 914
 915               XBT_DEBUG("Next pair already visited ! ");
 916
 917             }
 918
 919           }
 920
 921
 922           /* Restore system before checking others successors */
 923           if(cursor != (xbt_dynar_length(successors) - 1))
 924             MC_replay_liveness(mc_stack_liveness, 1);
 925
 926
 927         }
 928
 929         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 930           XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness));
 931           MC_replay_liveness(mc_stack_liveness, 0);
 932         }
 933       }
 934
 935
 936     }else{  /*No request to execute, search evolution in Büchi automaton */
 937
 938       MC_SET_RAW_MEM;
 939
 940       /* Create the new expanded graph_state */
 941       next_graph_state = MC_state_pair_new();
 942
 943       xbt_dynar_reset(successors);
 944
 945       MC_UNSET_RAW_MEM;
 946
 947
 948       cursor= 0;
 949       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 950
 951         res = MC_automaton_evaluate_label(transition_succ->label);
 952
 953         if(res == 1){ // enabled transition in automaton
 954           MC_SET_RAW_MEM;
 955           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 956           xbt_dynar_push(successors, &next_pair);
 957           MC_UNSET_RAW_MEM;
 958         }
 959
 960       }
 961
 962       cursor = 0;
 963
 964       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 965
 966         res = MC_automaton_evaluate_label(transition_succ->label);
 967
 968         if(res == 2){ // true transition in automaton
 969           MC_SET_RAW_MEM;
 970           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 971           xbt_dynar_push(successors, &next_pair);
 972           MC_UNSET_RAW_MEM;
 973         }
 974
 975       }
 976
 977       cursor = 0;
 978
 979       xbt_dynar_foreach(successors, cursor, pair_succ){
 980
 981         if(search_cycle == 1){
 982
 983           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 984
 985             if(reached(pair_succ->automaton_state)){
 986               //if(reached_hash(pair_succ->automaton_state)){
 987
 988               XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
 989
 990               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 991               XBT_INFO("|             ACCEPTANCE CYCLE            |");
 992               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 993               XBT_INFO("Counter-example that violates formula :");
 994               MC_show_stack_liveness(mc_stack_liveness);
 995               MC_dump_stack_liveness(mc_stack_liveness);
 996               MC_print_statistics_pairs(mc_stats_pair);
 997               exit(0);
 998
 999             }else{
1000
1001               XBT_DEBUG("Next pair (depth = %d) -> Acceptance pair : graph=%p, automaton=%p(%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->graph_state, pair_succ->automaton_state, pair_succ->automaton_state->id);
1002
1003               set_pair_reached(pair_succ->automaton_state);
1004               //set_pair_reached_hash(pair_succ->automaton_state);
1005
1006               XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1007               //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1008
1009               MC_SET_RAW_MEM;
1010               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1011               MC_UNSET_RAW_MEM;
1012
1013               MC_ddfs(search_cycle);
1014
1015             }
1016
1017           }else{
1018
1019             if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1020               //if(!visited(pair_succ->automaton_state, search_cycle)){
1021
1022               MC_SET_RAW_MEM;
1023               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1024               MC_UNSET_RAW_MEM;
1025
1026               MC_ddfs(search_cycle);
1027
1028             }else{
1029
1030               XBT_DEBUG("Next pair already visited ! ");
1031
1032             }
1033           }
1034
1035
1036         }else{
1037
1038           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1039
1040             set_pair_reached(pair_succ->automaton_state);
1041             //set_pair_reached_hash(pair_succ->automaton_state);
1042
1043             search_cycle = 1;
1044
1045             XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1046             //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1047
1048           }
1049
1050           if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1051             //if(!visited(pair_succ->automaton_state, search_cycle)){
1052
1053             MC_SET_RAW_MEM;
1054             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1055             MC_UNSET_RAW_MEM;
1056
1057             MC_ddfs(search_cycle);
1058
1059           }else{
1060
1061             XBT_DEBUG("Next pair already visited ! ");
1062
1063           }
1064
1065         }
1066
1067         /* Restore system before checking others successors */
1068         if(cursor != xbt_dynar_length(successors) - 1)
1069           MC_replay_liveness(mc_stack_liveness, 1);
1070
1071
1072       }
1073
1074     }
1075
1076   }else{
1077
1078     XBT_DEBUG("Max depth reached");
1079
1080   }
1081
1082   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
1083     XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u, depth = %d) shifted in stack, maximum depth reached", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
1084   }else{
1085     XBT_DEBUG("Pair (graph=%p, automaton =%p, search_cycle = %u, depth = %d) shifted in stack", current_pair->graph_state, current_pair->automaton_state, search_cycle, xbt_fifo_size(mc_stack_liveness) );
1086   }
1087
1088
1089   MC_SET_RAW_MEM;
1090   xbt_fifo_shift(mc_stack_liveness);
1091   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
1092     xbt_dynar_pop(reached_pairs, NULL);
1093     //xbt_dynar_pop(reached_pairs_hash, NULL);
1094   }
1095   MC_UNSET_RAW_MEM;
1096
1097
1098
1099 }