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