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