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