src/mc/mc_liveness.c

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