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 successors;
  15
  16 int create_dump(int pair)
  17 {
  18    // Try to enable core dumps
  19   struct rlimit core_limit;
  20   core_limit.rlim_cur = RLIM_INFINITY;
  21   core_limit.rlim_max = RLIM_INFINITY;
  22
  23   if(setrlimit(RLIMIT_CORE, &core_limit) < 0)
  24     fprintf(stderr, "setrlimit: %s\nWarning: core dumps may be truncated or non-existant\n", strerror(errno));
  25
  26   int status;
  27   switch(fork()){
  28   case 0:
  29     // We are the child process -- run the actual program
  30     xbt_abort();
  31     break;
  32
  33   case -1:
  34     // An error occurred, shouldn't happen
  35     perror("fork");
  36     return -1;
  37
  38   default:
  39     // We are the parent process -- wait for the child process to exit
  40     if(wait(&status) < 0)
  41       perror("wait");
  42     if(WIFSIGNALED(status) && WCOREDUMP(status)){
  43       char *core_name = malloc(20);
  44       sprintf(core_name,"core_%d", pair);
  45       rename("core", core_name);
  46       free(core_name);
  47     }
  48   }
  49
  50   return 0;
  51 }
  52
  53 int reached(xbt_state_t st){
  54
  55   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
  56
  57   MC_SET_RAW_MEM;
  58
  59   mc_pair_reached_t new_pair = NULL;
  60   new_pair = xbt_new0(s_mc_pair_reached_t, 1);
  61   new_pair->nb = xbt_dynar_length(reached_pairs) + 1;
  62   new_pair->automaton_state = st;
  63   new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
  64   new_pair->system_state = MC_take_snapshot_liveness();
  65
  66   /* Get values of propositional symbols */
  67   int res;
  68   int_f_void_t f;
  69   unsigned int cursor = 0;
  70   xbt_propositional_symbol_t ps = NULL;
  71   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
  72     f = (int_f_void_t)ps->function;
  73     res = (*f)();
  74     xbt_dynar_push_as(new_pair->prop_ato, int, res);
  75   }
  76
  77   MC_UNSET_RAW_MEM;
  78
  79   if(xbt_dynar_is_empty(reached_pairs)/* || !compare*/){
  80
  81     MC_SET_RAW_MEM;
  82     /* New pair reached */
  83     xbt_dynar_push(reached_pairs, &new_pair);
  84     MC_UNSET_RAW_MEM;
  85
  86     if(raw_mem_set)
  87       MC_SET_RAW_MEM;
  88
  89     return 0;
  90
  91   }else{
  92
  93     MC_SET_RAW_MEM;
  94
  95     cursor = 0;
  96     mc_pair_reached_t pair_test = NULL;
  97
  98     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
  99       XBT_INFO("Pair reached #%d", pair_test->nb);
 100       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
 101         if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
 102           if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
 103
 104             if(raw_mem_set)
 105               MC_SET_RAW_MEM;
 106             else
 107               MC_UNSET_RAW_MEM;
 108
 109             return 1;
 110           }
 111         }else{
 112           XBT_INFO("Different values of propositional symbols");
 113         }
 114       }else{
 115         XBT_INFO("Different automaton state");
 116       }
 117     }
 118
 119     /* New pair reached */
 120     xbt_dynar_push(reached_pairs, &new_pair);
 121
 122     MC_UNSET_RAW_MEM;
 123
 124     if(raw_mem_set)
 125       MC_SET_RAW_MEM;
 126
 127     compare = 0;
 128
 129     return 0;
 130
 131   }
 132 }
 133
 134
 135 void set_pair_reached(xbt_state_t st){
 136
 137   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 138
 139   MC_SET_RAW_MEM;
 140
 141   mc_pair_reached_t pair = NULL;
 142   pair = xbt_new0(s_mc_pair_reached_t, 1);
 143   pair->nb = xbt_dynar_length(reached_pairs) + 1;
 144   pair->automaton_state = st;
 145   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 146   pair->system_state = MC_take_snapshot_liveness();
 147
 148   /* Get values of propositional symbols */
 149   unsigned int cursor = 0;
 150   xbt_propositional_symbol_t ps = NULL;
 151   int res;
 152   int_f_void_t f;
 153
 154   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 155     f = (int_f_void_t)ps->function;
 156     res = (*f)();
 157     xbt_dynar_push_as(pair->prop_ato, int, res);
 158   }
 159
 160   xbt_dynar_push(reached_pairs, &pair);
 161
 162   MC_UNSET_RAW_MEM;
 163
 164   if(raw_mem_set)
 165     MC_SET_RAW_MEM;
 166
 167 }
 168
 169 void MC_pair_delete(mc_pair_t pair){
 170   xbt_free(pair->graph_state->proc_status);
 171   xbt_free(pair->graph_state);
 172   xbt_free(pair);
 173 }
 174
 175
 176
 177 int MC_automaton_evaluate_label(xbt_exp_label_t l){
 178
 179   switch(l->type){
 180   case 0 : {
 181     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 182     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 183     return (left_res || right_res);
 184   }
 185   case 1 : {
 186     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 187     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 188     return (left_res && right_res);
 189   }
 190   case 2 : {
 191     int res = MC_automaton_evaluate_label(l->u.exp_not);
 192     return (!res);
 193   }
 194   case 3 : {
 195     unsigned int cursor = 0;
 196     xbt_propositional_symbol_t p = NULL;
 197     int_f_void_t f;
 198     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
 199       if(strcmp(p->pred, l->u.predicat) == 0){
 200         f = (int_f_void_t)p->function;
 201         return (*f)();
 202       }
 203     }
 204     return -1;
 205   }
 206   case 4 : {
 207     return 2;
 208   }
 209   default :
 210     return -1;
 211   }
 212 }
 213
 214
 215 /********************* Double-DFS stateless *******************/
 216
 217 void pair_stateless_free(mc_pair_stateless_t pair){
 218   xbt_free(pair->graph_state->system_state);
 219   xbt_free(pair->graph_state->proc_status);
 220   xbt_free(pair->graph_state);
 221   xbt_free(pair);
 222 }
 223
 224 void pair_stateless_free_voidp(void *p){
 225   pair_stateless_free((mc_pair_stateless_t) * (void **) p);
 226 }
 227
 228 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
 229   mc_pair_stateless_t p = NULL;
 230   p = xbt_new0(s_mc_pair_stateless_t, 1);
 231   p->automaton_state = st;
 232   p->graph_state = sg;
 233   p->requests = r;
 234   mc_stats_pair->expanded_pairs++;
 235   return p;
 236 }
 237
 238 void pair_reached_free(mc_pair_reached_t pair){
 239   if(pair){
 240     pair->automaton_state = NULL;
 241     xbt_dynar_free(&(pair->prop_ato));
 242     MC_free_snapshot(pair->system_state);
 243     xbt_free(pair);
 244   }
 245 }
 246
 247 void pair_reached_free_voidp(void *p){
 248   pair_reached_free((mc_pair_reached_t) * (void **) p);
 249 }
 250
 251 void MC_ddfs_init(void){
 252
 253   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 254
 255   XBT_INFO("**************************************************");
 256   XBT_INFO("Double-DFS init");
 257   XBT_INFO("**************************************************");
 258
 259   mc_pair_stateless_t mc_initial_pair = NULL;
 260   mc_state_t initial_graph_state = NULL;
 261   smx_process_t process;
 262
 263
 264   MC_wait_for_requests();
 265
 266   MC_SET_RAW_MEM;
 267
 268   initial_graph_state = MC_state_pair_new();
 269   xbt_swag_foreach(process, simix_global->process_list){
 270     if(MC_process_is_enabled(process)){
 271       MC_state_interleave_process(initial_graph_state, process);
 272     }
 273   }
 274
 275   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), pair_reached_free_voidp);
 276   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 277
 278   /* Save the initial state */
 279   initial_state_liveness = xbt_new0(s_mc_global_t, 1);
 280   initial_state_liveness->initial_snapshot = MC_take_snapshot_liveness();
 281
 282   MC_UNSET_RAW_MEM;
 283
 284   unsigned int cursor = 0;
 285   xbt_state_t state;
 286
 287   xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
 288     if(state->type == -1){
 289
 290       MC_SET_RAW_MEM;
 291       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 292       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 293       MC_UNSET_RAW_MEM;
 294
 295       if(cursor != 0){
 296         MC_restore_snapshot(initial_state_liveness->initial_snapshot);
 297         MC_UNSET_RAW_MEM;
 298       }
 299
 300       MC_ddfs(0);
 301
 302     }else{
 303       if(state->type == 2){
 304
 305         MC_SET_RAW_MEM;
 306         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 307         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 308         MC_UNSET_RAW_MEM;
 309
 310         set_pair_reached(state);
 311
 312         if(cursor != 0){
 313           MC_restore_snapshot(initial_state_liveness->initial_snapshot);
 314           MC_UNSET_RAW_MEM;
 315         }
 316
 317         MC_ddfs(1);
 318
 319       }
 320     }
 321   }
 322
 323   if(raw_mem_set)
 324     MC_SET_RAW_MEM;
 325   else
 326     MC_UNSET_RAW_MEM;
 327
 328
 329 }
 330
 331
 332 void MC_ddfs(int search_cycle){
 333
 334   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 335
 336   smx_process_t process;
 337   mc_pair_stateless_t current_pair = NULL;
 338
 339   if(xbt_fifo_size(mc_stack_liveness) == 0)
 340     return;
 341
 342
 343   /* Get current pair */
 344   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 345
 346   /* Update current state in buchi automaton */
 347   _mc_property_automaton->current_state = current_pair->automaton_state;
 348
 349
 350   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
 351
 352   mc_stats_pair->visited_pairs++;
 353
 354   //sleep(1);
 355
 356   int value;
 357   mc_state_t next_graph_state = NULL;
 358   smx_simcall_t req = NULL;
 359   char *req_str;
 360
 361   xbt_transition_t transition_succ;
 362   unsigned int cursor = 0;
 363   int res;
 364
 365   mc_pair_stateless_t next_pair = NULL;
 366   mc_pair_stateless_t pair_succ;
 367
 368   mc_pair_stateless_t remove_pair;
 369   mc_pair_reached_t remove_pair_reached;
 370
 371   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
 372
 373     if(current_pair->requests > 0){
 374
 375       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 376
 377         /* Debug information */
 378
 379         req_str = MC_request_to_string(req, value);
 380         XBT_DEBUG("Execute: %s", req_str);
 381         xbt_free(req_str);
 382
 383         MC_state_set_executed_request(current_pair->graph_state, req, value);
 384
 385         /* Answer the request */
 386         SIMIX_simcall_pre(req, value);
 387
 388         /* Wait for requests (schedules processes) */
 389         MC_wait_for_requests();
 390
 391         MC_SET_RAW_MEM;
 392
 393         /* Create the new expanded graph_state */
 394         next_graph_state = MC_state_pair_new();
 395
 396         /* Get enabled process and insert it in the interleave set of the next graph_state */
 397
 398         xbt_swag_foreach(process, simix_global->process_list){
 399           if(MC_process_is_enabled(process)){
 400             XBT_DEBUG("Process %lu enabled with simcall : %d", process->pid, (&process->simcall)->call);
 401           }
 402         }
 403
 404         xbt_swag_foreach(process, simix_global->process_list){
 405           if(MC_process_is_enabled(process)){
 406             MC_state_interleave_process(next_graph_state, process);
 407           }
 408         }
 409
 410         xbt_dynar_reset(successors);
 411
 412         MC_UNSET_RAW_MEM;
 413
 414
 415         cursor= 0;
 416         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 417
 418           res = MC_automaton_evaluate_label(transition_succ->label);
 419
 420           if(res == 1){ // enabled transition in automaton
 421             MC_SET_RAW_MEM;
 422             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 423             xbt_dynar_push(successors, &next_pair);
 424             MC_UNSET_RAW_MEM;
 425           }
 426
 427         }
 428
 429         cursor = 0;
 430
 431         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 432
 433           res = MC_automaton_evaluate_label(transition_succ->label);
 434
 435           if(res == 2){ // true transition in automaton
 436             MC_SET_RAW_MEM;
 437             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 438             xbt_dynar_push(successors, &next_pair);
 439             MC_UNSET_RAW_MEM;
 440           }
 441
 442         }
 443
 444         cursor = 0;
 445
 446         xbt_dynar_foreach(successors, cursor, pair_succ){
 447
 448           if(search_cycle == 1){
 449
 450             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 451
 452               if(reached(pair_succ->automaton_state)){
 453
 454                 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));
 455
 456                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 457                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 458                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 459                 XBT_INFO("Counter-example that violates formula :");
 460                 MC_show_stack_liveness(mc_stack_liveness);
 461                 MC_dump_stack_liveness(mc_stack_liveness);
 462                 MC_print_statistics_pairs(mc_stats_pair);
 463                 xbt_abort();
 464
 465               }else{
 466
 467                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 468
 469                 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 470
 471                 MC_SET_RAW_MEM;
 472                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 473                 MC_UNSET_RAW_MEM;
 474
 475                 MC_ddfs(search_cycle);
 476
 477               }
 478
 479             }else{
 480
 481               MC_SET_RAW_MEM;
 482               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 483               MC_UNSET_RAW_MEM;
 484
 485               MC_ddfs(search_cycle);
 486
 487             }
 488
 489           }else{
 490
 491             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 492
 493               XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 494
 495               set_pair_reached(pair_succ->automaton_state);
 496
 497               search_cycle = 1;
 498
 499               XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 500
 501             }
 502
 503             MC_SET_RAW_MEM;
 504             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 505             MC_UNSET_RAW_MEM;
 506
 507             MC_ddfs(search_cycle);
 508
 509           }
 510
 511
 512           /* Restore system before checking others successors */
 513           if(cursor != (xbt_dynar_length(successors) - 1))
 514             MC_replay_liveness(mc_stack_liveness, 1);
 515
 516
 517         }
 518
 519         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 520           XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
 521           MC_replay_liveness(mc_stack_liveness, 0);
 522         }
 523       }
 524
 525
 526     }else{
 527
 528       XBT_DEBUG("No more request to execute in this state, search evolution in Büchi Automaton.");
 529
 530       MC_SET_RAW_MEM;
 531
 532       /* Create the new expanded graph_state */
 533       next_graph_state = MC_state_pair_new();
 534
 535       xbt_dynar_reset(successors);
 536
 537       MC_UNSET_RAW_MEM;
 538
 539
 540       cursor= 0;
 541       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 542
 543         res = MC_automaton_evaluate_label(transition_succ->label);
 544
 545         if(res == 1){ // enabled transition in automaton
 546           MC_SET_RAW_MEM;
 547           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 548           xbt_dynar_push(successors, &next_pair);
 549           MC_UNSET_RAW_MEM;
 550         }
 551
 552       }
 553
 554       cursor = 0;
 555
 556       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 557
 558         res = MC_automaton_evaluate_label(transition_succ->label);
 559
 560         if(res == 2){ // true transition in automaton
 561           MC_SET_RAW_MEM;
 562           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 563           xbt_dynar_push(successors, &next_pair);
 564           MC_UNSET_RAW_MEM;
 565         }
 566
 567       }
 568
 569       cursor = 0;
 570
 571       xbt_dynar_foreach(successors, cursor, pair_succ){
 572
 573         if(search_cycle == 1){
 574
 575           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 576
 577             if(reached(pair_succ->automaton_state)){
 578
 579               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
 580
 581               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 582               XBT_INFO("|             ACCEPTANCE CYCLE            |");
 583               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 584               XBT_INFO("Counter-example that violates formula :");
 585               MC_show_stack_liveness(mc_stack_liveness);
 586               MC_dump_stack_liveness(mc_stack_liveness);
 587               MC_print_statistics_pairs(mc_stats_pair);
 588               exit(0);
 589
 590             }else{
 591
 592               XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 593
 594               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 595
 596               MC_SET_RAW_MEM;
 597               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 598               MC_UNSET_RAW_MEM;
 599
 600               MC_ddfs(search_cycle);
 601
 602             }
 603
 604           }else{
 605
 606             MC_SET_RAW_MEM;
 607             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 608             MC_UNSET_RAW_MEM;
 609
 610             MC_ddfs(search_cycle);
 611
 612           }
 613
 614
 615         }else{
 616
 617           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 618
 619             set_pair_reached(pair_succ->automaton_state);
 620
 621             search_cycle = 1;
 622
 623             XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 624
 625           }
 626
 627           MC_SET_RAW_MEM;
 628           xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 629           MC_UNSET_RAW_MEM;
 630
 631           MC_ddfs(search_cycle);
 632
 633         }
 634
 635         /* Restore system before checking others successors */
 636         if(cursor != xbt_dynar_length(successors) - 1)
 637           MC_replay_liveness(mc_stack_liveness, 1);
 638
 639       }
 640
 641     }
 642
 643   }else{
 644
 645     XBT_DEBUG("Max depth reached");
 646
 647   }
 648
 649   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
 650     XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
 651   }else{
 652     XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
 653   }
 654
 655
 656   MC_SET_RAW_MEM;
 657   remove_pair = xbt_fifo_shift(mc_stack_liveness);
 658   xbt_fifo_remove(mc_stack_liveness, remove_pair);
 659   remove_pair = NULL;
 660   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 661     remove_pair_reached = xbt_dynar_pop_as(reached_pairs, mc_pair_reached_t);
 662     pair_reached_free(remove_pair_reached);
 663     remove_pair_reached = NULL;
 664   }
 665   MC_UNSET_RAW_MEM;
 666
 667   if(raw_mem_set)
 668     MC_SET_RAW_MEM;
 669
 670 }