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           }else{
 211             XBT_DEBUG("Different snapshot");
 212           }
 213         }else{
 214           XBT_DEBUG("Different values of propositional symbols");
 215         }
 216       }else{
 217         XBT_DEBUG("Different automaton state");
 218       }
 219     }
 220
 221     MC_free_snapshot(sn);
 222     xbt_dynar_reset(prop_ato);
 223     xbt_free(prop_ato);
 224     MC_UNSET_RAW_MEM;
 225     return 0;
 226
 227   }
 228 }
 229
 230 void set_pair_reached(xbt_state_t st){
 231
 232
 233   MC_SET_RAW_MEM;
 234
 235   mc_pair_reached_t pair = NULL;
 236   pair = xbt_new0(s_mc_pair_reached_t, 1);
 237   pair->automaton_state = st;
 238   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 239   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
 240   MC_take_snapshot_liveness(pair->system_state);
 241
 242   /* Get values of propositional symbols */
 243   unsigned int cursor = 0;
 244   xbt_propositional_symbol_t ps = NULL;
 245   int res;
 246   int (*f)();
 247
 248   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 249     f = ps->function;
 250     res = (*f)();
 251     xbt_dynar_push_as(pair->prop_ato, int, res);
 252   }
 253
 254   xbt_dynar_push(reached_pairs, &pair);
 255
 256   MC_UNSET_RAW_MEM;
 257
 258 }
 259
 260 int reached_hash(xbt_state_t st){
 261
 262
 263   if(xbt_dynar_is_empty(reached_pairs_hash)){
 264
 265     return 0;
 266
 267   }else{
 268
 269     MC_SET_RAW_MEM;
 270
 271     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 272     MC_take_snapshot_liveness(sn);
 273
 274     int j;
 275     unsigned int hash_regions[sn->num_reg];
 276     for(j=0; j<sn->num_reg; j++){
 277       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
 278     }
 279
 280
 281     /* Get values of propositional symbols */
 282     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 283     unsigned int cursor = 0;
 284     xbt_propositional_symbol_t ps = NULL;
 285     int res;
 286     int (*f)();
 287
 288     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 289       f = ps->function;
 290       res = (*f)();
 291       xbt_dynar_push_as(prop_ato, int, res);
 292     }
 293
 294     mc_pair_reached_hash_t pair_test = NULL;
 295
 296     int region_diff = 0;
 297
 298     cursor = 0;
 299
 300     xbt_dynar_foreach(reached_pairs_hash, cursor, pair_test){
 301
 302       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 303         if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 304           for(j=0 ; j< sn->num_reg ; j++){
 305             if(hash_regions[j] != pair_test->hash_regions[j]){
 306               region_diff++;
 307             }
 308           }
 309           if(region_diff == 0){
 310             MC_free_snapshot(sn);
 311             xbt_dynar_reset(prop_ato);
 312             xbt_free(prop_ato);
 313             MC_UNSET_RAW_MEM;
 314             return 1;
 315           }else{
 316             XBT_DEBUG("Different snapshot");
 317           }
 318         }else{
 319           XBT_DEBUG("Different values of propositional symbols");
 320         }
 321       }else{
 322         XBT_DEBUG("Different automaton state");
 323       }
 324
 325       region_diff = 0;
 326     }
 327
 328     MC_free_snapshot(sn);
 329     xbt_dynar_reset(prop_ato);
 330     xbt_free(prop_ato);
 331     MC_UNSET_RAW_MEM;
 332     return 0;
 333
 334   }
 335 }
 336
 337 void set_pair_reached_hash(xbt_state_t st){
 338
 339   MC_SET_RAW_MEM;
 340
 341   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 342   MC_take_snapshot_liveness(sn);
 343
 344   mc_pair_reached_hash_t pair = NULL;
 345   pair = xbt_new0(s_mc_pair_reached_hash_t, 1);
 346   pair->automaton_state = st;
 347   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 348   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
 349
 350   int i;
 351
 352   for(i=0 ; i< sn->num_reg ; i++){
 353     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
 354   }
 355
 356   /* Get values of propositional symbols */
 357   unsigned int cursor = 0;
 358   xbt_propositional_symbol_t ps = NULL;
 359   int res;
 360   int (*f)();
 361
 362   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 363     f = ps->function;
 364     res = (*f)();
 365     xbt_dynar_push_as(pair->prop_ato, int, res);
 366   }
 367
 368   xbt_dynar_push(reached_pairs_hash, &pair);
 369
 370   MC_free_snapshot(sn);
 371
 372   MC_UNSET_RAW_MEM;
 373
 374 }
 375
 376
 377 int visited(xbt_state_t st, int sc){
 378
 379
 380   if(xbt_dynar_is_empty(visited_pairs)){
 381
 382     return 0;
 383
 384   }else{
 385
 386     MC_SET_RAW_MEM;
 387
 388     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 389     MC_take_snapshot_liveness(sn);
 390
 391     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 392
 393     /* Get values of propositional symbols */
 394     unsigned int cursor = 0;
 395     xbt_propositional_symbol_t ps = NULL;
 396     int res;
 397     int (*f)();
 398
 399     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 400       f = ps->function;
 401       res = (*f)();
 402       xbt_dynar_push_as(prop_ato, int, res);
 403     }
 404
 405     cursor = 0;
 406     mc_pair_visited_t pair_test = NULL;
 407
 408     xbt_dynar_foreach(visited_pairs, cursor, pair_test){
 409       if(pair_test->search_cycle == sc) {
 410         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 411           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 412             if(snapshot_compare(pair_test->system_state, sn) == 0){
 413
 414               MC_free_snapshot(sn);
 415               xbt_dynar_reset(prop_ato);
 416               xbt_free(prop_ato);
 417               MC_UNSET_RAW_MEM;
 418
 419               return 1;
 420
 421             }else{
 422               XBT_DEBUG("Different snapshot");
 423             }
 424           }else{
 425             XBT_DEBUG("Different values of propositional symbols");
 426           }
 427         }else{
 428           XBT_DEBUG("Different automaton state");
 429         }
 430       }else{
 431         XBT_DEBUG("Different value of search_cycle");
 432       }
 433     }
 434
 435
 436     MC_free_snapshot(sn);
 437     xbt_dynar_reset(prop_ato);
 438     xbt_free(prop_ato);
 439     MC_UNSET_RAW_MEM;
 440     return 0;
 441
 442   }
 443 }
 444
 445
 446 int visited_hash(xbt_state_t st, int sc){
 447
 448
 449   if(xbt_dynar_is_empty(visited_pairs_hash)){
 450
 451     return 0;
 452
 453   }else{
 454
 455     MC_SET_RAW_MEM;
 456
 457     mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 458     MC_take_snapshot_liveness(sn);
 459
 460     int j;
 461     unsigned int hash_regions[sn->num_reg];
 462     for(j=0; j<sn->num_reg; j++){
 463       hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
 464     }
 465
 466
 467     /* Get values of propositional symbols */
 468     xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
 469     unsigned int cursor = 0;
 470     xbt_propositional_symbol_t ps = NULL;
 471     int res;
 472     int (*f)();
 473
 474     xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 475       f = ps->function;
 476       res = (*f)();
 477       xbt_dynar_push_as(prop_ato, int, res);
 478     }
 479
 480     mc_pair_visited_hash_t pair_test = NULL;
 481
 482     int region_diff = 0;
 483     cursor = 0;
 484
 485     xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
 486
 487       if(pair_test->search_cycle == sc) {
 488         if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 489           if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
 490             for(j=0 ; j< sn->num_reg ; j++){
 491               if(hash_regions[j] != pair_test->hash_regions[j]){
 492                 region_diff++;
 493               }
 494             }
 495             if(region_diff == 0){
 496               MC_free_snapshot(sn);
 497               xbt_dynar_reset(prop_ato);
 498               xbt_free(prop_ato);
 499               MC_UNSET_RAW_MEM;
 500               return 1;
 501             }else{
 502               XBT_DEBUG("Different snapshot");
 503             }
 504           }else{
 505             XBT_DEBUG("Different values of propositional symbols");
 506           }
 507         }else{
 508           XBT_DEBUG("Different automaton state");
 509         }
 510       }else{
 511         XBT_DEBUG("Different value of search_cycle");
 512       }
 513
 514       region_diff = 0;
 515     }
 516
 517     MC_free_snapshot(sn);
 518     xbt_dynar_reset(prop_ato);
 519     xbt_free(prop_ato);
 520     MC_UNSET_RAW_MEM;
 521     return 0;
 522
 523   }
 524 }
 525
 526 void set_pair_visited_hash(xbt_state_t st, int sc){
 527
 528   MC_SET_RAW_MEM;
 529
 530   mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
 531   MC_take_snapshot_liveness(sn);
 532
 533   mc_pair_visited_hash_t pair = NULL;
 534   pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
 535   pair->automaton_state = st;
 536   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 537   pair->search_cycle = sc;
 538   pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
 539
 540   int i;
 541
 542   for(i=0 ; i< sn->num_reg ; i++){
 543     pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
 544   }
 545
 546   /* Get values of propositional symbols */
 547   unsigned int cursor = 0;
 548   xbt_propositional_symbol_t ps = NULL;
 549   int res;
 550   int (*f)();
 551
 552   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 553     f = ps->function;
 554     res = (*f)();
 555     xbt_dynar_push_as(pair->prop_ato, int, res);
 556   }
 557
 558   xbt_dynar_push(visited_pairs_hash, &pair);
 559
 560   MC_free_snapshot(sn);
 561
 562   MC_UNSET_RAW_MEM;
 563
 564 }
 565
 566 void set_pair_visited(xbt_state_t st, int sc){
 567
 568
 569   MC_SET_RAW_MEM;
 570
 571   mc_pair_visited_t pair = NULL;
 572   pair = xbt_new0(s_mc_pair_visited_t, 1);
 573   pair->automaton_state = st;
 574   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 575   pair->search_cycle = sc;
 576   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
 577   MC_take_snapshot_liveness(pair->system_state);
 578
 579
 580   /* Get values of propositional symbols */
 581   unsigned int cursor = 0;
 582   xbt_propositional_symbol_t ps = NULL;
 583   int res;
 584   int (*f)();
 585
 586   xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
 587     f = ps->function;
 588     res = (*f)();
 589     xbt_dynar_push_as(pair->prop_ato, int, res);
 590   }
 591
 592   xbt_dynar_push(visited_pairs, &pair);
 593
 594   MC_UNSET_RAW_MEM;
 595
 596
 597 }
 598
 599 void MC_pair_delete(mc_pair_t pair){
 600   xbt_free(pair->graph_state->proc_status);
 601   xbt_free(pair->graph_state);
 602   xbt_free(pair);
 603 }
 604
 605
 606
 607 int MC_automaton_evaluate_label(xbt_exp_label_t l){
 608
 609   switch(l->type){
 610   case 0 : {
 611     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 612     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 613     return (left_res || right_res);
 614     break;
 615   }
 616   case 1 : {
 617     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 618     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 619     return (left_res && right_res);
 620     break;
 621   }
 622   case 2 : {
 623     int res = MC_automaton_evaluate_label(l->u.exp_not);
 624     return (!res);
 625     break;
 626   }
 627   case 3 : {
 628     unsigned int cursor = 0;
 629     xbt_propositional_symbol_t p = NULL;
 630     int (*f)();
 631     xbt_dynar_foreach(automaton->propositional_symbols, cursor, p){
 632       if(strcmp(p->pred, l->u.predicat) == 0){
 633         f = p->function;
 634         return (*f)();
 635       }
 636     }
 637     return -1;
 638     break;
 639   }
 640   case 4 : {
 641     return 2;
 642     break;
 643   }
 644   default :
 645     return -1;
 646     break;
 647   }
 648 }
 649
 650
 651
 652
 653
 654 /********************* Double-DFS stateless *******************/
 655
 656 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
 657   xbt_free(pair->graph_state->proc_status);
 658   xbt_free(pair->graph_state);
 659   xbt_free(pair);
 660 }
 661
 662 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
 663   mc_pair_stateless_t p = NULL;
 664   p = xbt_new0(s_mc_pair_stateless_t, 1);
 665   p->automaton_state = st;
 666   p->graph_state = sg;
 667   p->requests = r;
 668   mc_stats_pair->expanded_pairs++;
 669   return p;
 670 }
 671
 672 void MC_ddfs_init(void){
 673
 674   XBT_DEBUG("**************************************************");
 675   XBT_DEBUG("Double-DFS init");
 676   XBT_DEBUG("**************************************************");
 677
 678   mc_pair_stateless_t mc_initial_pair = NULL;
 679   mc_state_t initial_graph_state = NULL;
 680   smx_process_t process;
 681
 682   MC_wait_for_requests();
 683
 684   MC_SET_RAW_MEM;
 685
 686   initial_graph_state = MC_state_pair_new();
 687   xbt_swag_foreach(process, simix_global->process_list){
 688     if(MC_process_is_enabled(process)){
 689       MC_state_interleave_process(initial_graph_state, process);
 690     }
 691   }
 692
 693   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
 694   //reached_pairs_hash = xbt_dynar_new(sizeof(mc_pair_reached_hash_t), NULL);
 695   //visited_pairs = xbt_dynar_new(sizeof(mc_pair_visited_t), NULL);
 696   visited_pairs_hash = xbt_dynar_new(sizeof(mc_pair_visited_hash_t), NULL);
 697   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 698
 699   /* Save the initial state */
 700   initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
 701   MC_take_snapshot_to_restore_liveness(initial_snapshot_liveness);
 702
 703   MC_UNSET_RAW_MEM;
 704
 705   unsigned int cursor = 0;
 706   xbt_state_t state;
 707
 708   xbt_dynar_foreach(automaton->states, cursor, state){
 709     if(state->type == -1){
 710
 711       MC_SET_RAW_MEM;
 712       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 713       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 714       MC_UNSET_RAW_MEM;
 715
 716       if(cursor != 0){
 717         MC_restore_snapshot(initial_snapshot_liveness);
 718         MC_UNSET_RAW_MEM;
 719       }
 720
 721       MC_ddfs(0);
 722
 723     }else{
 724       if(state->type == 2){
 725
 726         MC_SET_RAW_MEM;
 727         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 728         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 729         MC_UNSET_RAW_MEM;
 730
 731         set_pair_reached(state);
 732         //set_pair_reached_hash(state);
 733
 734         if(cursor != 0){
 735           MC_restore_snapshot(initial_snapshot_liveness);
 736           MC_UNSET_RAW_MEM;
 737         }
 738
 739         MC_ddfs(1);
 740
 741       }
 742     }
 743   }
 744
 745 }
 746
 747
 748 void MC_ddfs(int search_cycle){
 749
 750   smx_process_t process;
 751   mc_pair_stateless_t current_pair = NULL;
 752
 753   if(xbt_fifo_size(mc_stack_liveness) == 0)
 754     return;
 755
 756
 757   /* Get current pair */
 758   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 759
 760   /* Update current state in buchi automaton */
 761   automaton->current_state = current_pair->automaton_state;
 762
 763
 764   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
 765   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));
 766
 767   mc_stats_pair->visited_pairs++;
 768
 769   sleep(1);
 770
 771   int value;
 772   mc_state_t next_graph_state = NULL;
 773   smx_req_t req = NULL;
 774   char *req_str;
 775
 776   xbt_transition_t transition_succ;
 777   unsigned int cursor = 0;
 778   int res;
 779
 780   mc_pair_stateless_t next_pair = NULL;
 781   mc_pair_stateless_t pair_succ;
 782
 783   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
 784
 785     //set_pair_visited(current_pair->automaton_state, search_cycle);
 786     set_pair_visited_hash(current_pair->automaton_state, search_cycle);
 787
 788     //XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs));
 789     XBT_DEBUG("Visited pairs : %lu", xbt_dynar_length(visited_pairs_hash));
 790
 791     if(current_pair->requests > 0){
 792
 793       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 794
 795         /* Debug information */
 796         if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug)){
 797           req_str = MC_request_to_string(req, value);
 798           XBT_DEBUG("Execute: %s", req_str);
 799           xbt_free(req_str);
 800         }
 801
 802         MC_state_set_executed_request(current_pair->graph_state, req, value);
 803
 804         /* Answer the request */
 805         SIMIX_request_pre(req, value);
 806
 807         /* Wait for requests (schedules processes) */
 808         MC_wait_for_requests();
 809
 810
 811         MC_SET_RAW_MEM;
 812
 813         /* Create the new expanded graph_state */
 814         next_graph_state = MC_state_pair_new();
 815
 816         /* Get enabled process and insert it in the interleave set of the next graph_state */
 817         xbt_swag_foreach(process, simix_global->process_list){
 818           if(MC_process_is_enabled(process)){
 819             MC_state_interleave_process(next_graph_state, process);
 820           }
 821         }
 822
 823         xbt_dynar_reset(successors);
 824
 825         MC_UNSET_RAW_MEM;
 826
 827
 828         cursor= 0;
 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 == 1){ // enabled 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(current_pair->automaton_state->out, cursor, transition_succ){
 845
 846           res = MC_automaton_evaluate_label(transition_succ->label);
 847
 848           if(res == 2){ // true transition in automaton
 849             MC_SET_RAW_MEM;
 850             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 851             xbt_dynar_push(successors, &next_pair);
 852             MC_UNSET_RAW_MEM;
 853           }
 854
 855         }
 856
 857         cursor = 0;
 858
 859         xbt_dynar_foreach(successors, cursor, pair_succ){
 860
 861           if(search_cycle == 1){
 862
 863             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 864
 865               if(reached(pair_succ->automaton_state)){
 866                 //if(reached_hash(pair_succ->automaton_state)){
 867
 868                 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));
 869
 870                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 871                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 872                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 873                 XBT_INFO("Counter-example that violates formula :");
 874                 MC_show_stack_liveness(mc_stack_liveness);
 875                 MC_dump_stack_liveness(mc_stack_liveness);
 876                 MC_print_statistics_pairs(mc_stats_pair);
 877                 exit(0);
 878
 879               }else{
 880
 881                 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);
 882
 883                 set_pair_reached(pair_succ->automaton_state);
 884                 //set_pair_reached_hash(pair_succ->automaton_state);
 885
 886                 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 887                 //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 888
 889                 MC_SET_RAW_MEM;
 890                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 891                 MC_UNSET_RAW_MEM;
 892
 893                 MC_ddfs(search_cycle);
 894
 895               }
 896
 897             }else{
 898
 899               if(!visited_hash(pair_succ->automaton_state, search_cycle)){
 900                 //if(!visited(pair_succ->automaton_state, search_cycle)){
 901
 902                 MC_SET_RAW_MEM;
 903                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 904                 MC_UNSET_RAW_MEM;
 905
 906                 MC_ddfs(search_cycle);
 907
 908               }else{
 909
 910                 XBT_DEBUG("Next pair already visited ! ");
 911
 912               }
 913
 914             }
 915
 916           }else{
 917
 918             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 919
 920               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);
 921
 922               set_pair_reached(pair_succ->automaton_state);
 923               //set_pair_reached_hash(pair_succ->automaton_state);
 924
 925               search_cycle = 1;
 926
 927               XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 928               //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
 929
 930             }
 931
 932             if(!visited_hash(pair_succ->automaton_state, search_cycle)){
 933               //if(!visited(pair_succ->automaton_state, search_cycle)){
 934
 935               MC_SET_RAW_MEM;
 936               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 937               MC_UNSET_RAW_MEM;
 938
 939               MC_ddfs(search_cycle);
 940
 941             }else{
 942
 943               XBT_DEBUG("Next pair already visited ! ");
 944
 945             }
 946
 947           }
 948
 949
 950           /* Restore system before checking others successors */
 951           if(cursor != (xbt_dynar_length(successors) - 1))
 952             MC_replay_liveness(mc_stack_liveness, 1);
 953
 954
 955         }
 956
 957         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 958           XBT_DEBUG("Backtracking to depth %u", xbt_fifo_size(mc_stack_liveness));
 959           MC_replay_liveness(mc_stack_liveness, 0);
 960         }
 961       }
 962
 963
 964     }else{  /*No request to execute, search evolution in Büchi automaton */
 965
 966       MC_SET_RAW_MEM;
 967
 968       /* Create the new expanded graph_state */
 969       next_graph_state = MC_state_pair_new();
 970
 971       xbt_dynar_reset(successors);
 972
 973       MC_UNSET_RAW_MEM;
 974
 975
 976       cursor= 0;
 977       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 978
 979         res = MC_automaton_evaluate_label(transition_succ->label);
 980
 981         if(res == 1){ // enabled transition in automaton
 982           MC_SET_RAW_MEM;
 983           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 984           xbt_dynar_push(successors, &next_pair);
 985           MC_UNSET_RAW_MEM;
 986         }
 987
 988       }
 989
 990       cursor = 0;
 991
 992       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 993
 994         res = MC_automaton_evaluate_label(transition_succ->label);
 995
 996         if(res == 2){ // true transition in automaton
 997           MC_SET_RAW_MEM;
 998           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 999           xbt_dynar_push(successors, &next_pair);
1000           MC_UNSET_RAW_MEM;
1001         }
1002
1003       }
1004
1005       cursor = 0;
1006
1007       xbt_dynar_foreach(successors, cursor, pair_succ){
1008
1009         if(search_cycle == 1){
1010
1011           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
1012
1013             if(reached(pair_succ->automaton_state)){
1014               //if(reached_hash(pair_succ->automaton_state)){
1015
1016               XBT_DEBUG("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
1017
1018               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1019               XBT_INFO("|             ACCEPTANCE CYCLE            |");
1020               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
1021               XBT_INFO("Counter-example that violates formula :");
1022               MC_show_stack_liveness(mc_stack_liveness);
1023               MC_dump_stack_liveness(mc_stack_liveness);
1024               MC_print_statistics_pairs(mc_stats_pair);
1025               exit(0);
1026
1027             }else{
1028
1029               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);
1030
1031               set_pair_reached(pair_succ->automaton_state);
1032               //set_pair_reached_hash(pair_succ->automaton_state);
1033
1034               XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1035               //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1036
1037               MC_SET_RAW_MEM;
1038               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1039               MC_UNSET_RAW_MEM;
1040
1041               MC_ddfs(search_cycle);
1042
1043             }
1044
1045           }else{
1046
1047             if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1048               //if(!visited(pair_succ->automaton_state, search_cycle)){
1049
1050               MC_SET_RAW_MEM;
1051               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1052               MC_UNSET_RAW_MEM;
1053
1054               MC_ddfs(search_cycle);
1055
1056             }else{
1057
1058               XBT_DEBUG("Next pair already visited ! ");
1059
1060             }
1061           }
1062
1063
1064         }else{
1065
1066           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
1067
1068             set_pair_reached(pair_succ->automaton_state);
1069             //set_pair_reached_hash(pair_succ->automaton_state);
1070
1071             search_cycle = 1;
1072
1073             XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
1074             //XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs_hash));
1075
1076           }
1077
1078           if(!visited_hash(pair_succ->automaton_state, search_cycle)){
1079             //if(!visited(pair_succ->automaton_state, search_cycle)){
1080
1081             MC_SET_RAW_MEM;
1082             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
1083             MC_UNSET_RAW_MEM;
1084
1085             MC_ddfs(search_cycle);
1086
1087           }else{
1088
1089             XBT_DEBUG("Next pair already visited ! ");
1090
1091           }
1092
1093         }
1094
1095         /* Restore system before checking others successors */
1096         if(cursor != xbt_dynar_length(successors) - 1)
1097           MC_replay_liveness(mc_stack_liveness, 1);
1098
1099
1100       }
1101
1102     }
1103
1104   }else{
1105
1106     XBT_DEBUG("Max depth reached");
1107
1108   }
1109
1110   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
1111     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) );
1112   }else{
1113     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) );
1114   }
1115
1116
1117   MC_SET_RAW_MEM;
1118   xbt_fifo_shift(mc_stack_liveness);
1119   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
1120     xbt_dynar_pop(reached_pairs, NULL);
1121     //xbt_dynar_pop(reached_pairs_hash, NULL);
1122   }
1123   MC_UNSET_RAW_MEM;
1124
1125
1126
1127 }