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