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 = xbt_new0(s_mc_snapshot_t, 1);
  65   MC_take_snapshot_liveness(new_pair->system_state);
  66
  67   /* Get values of propositional symbols */
  68   int res;
  69   int_f_void_t f;
  70   unsigned int cursor = 0;
  71   xbt_propositional_symbol_t ps = NULL;
  72   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
  73     f = (int_f_void_t)ps->function;
  74     res = (*f)();
  75     xbt_dynar_push_as(new_pair->prop_ato, int, res);
  76   }
  77
  78   MC_UNSET_RAW_MEM;
  79
  80   if(xbt_dynar_is_empty(reached_pairs) || !compare){
  81
  82     MC_SET_RAW_MEM;
  83     /* New pair reached */
  84     xbt_dynar_push(reached_pairs, &new_pair);
  85     MC_UNSET_RAW_MEM;
  86
  87     return 0;
  88
  89   }else{
  90
  91     MC_SET_RAW_MEM;
  92
  93     cursor = 0;
  94     mc_pair_reached_t pair_test = NULL;
  95
  96     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
  97       XBT_INFO("Pair reached #%d", pair_test->nb);
  98       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
  99         if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
 100           if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
 101
 102             if(raw_mem_set)
 103               MC_SET_RAW_MEM;
 104             else
 105               MC_UNSET_RAW_MEM;
 106
 107             return 1;
 108           }
 109         }else{
 110           XBT_INFO("Different values of propositional symbols");
 111         }
 112       }else{
 113         XBT_INFO("Different automaton state");
 114       }
 115     }
 116
 117     /* New pair reached */
 118     xbt_dynar_push(reached_pairs, &new_pair);
 119
 120     MC_UNSET_RAW_MEM;
 121
 122     if(raw_mem_set)
 123       MC_SET_RAW_MEM;
 124     else
 125       MC_UNSET_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 = xbt_new0(s_mc_snapshot_t, 1);
 147   MC_take_snapshot_liveness(pair->system_state);
 148
 149   /* Get values of propositional symbols */
 150   unsigned int cursor = 0;
 151   xbt_propositional_symbol_t ps = NULL;
 152   int res;
 153   int_f_void_t f;
 154
 155   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 156     f = (int_f_void_t)ps->function;
 157     res = (*f)();
 158     xbt_dynar_push_as(pair->prop_ato, int, res);
 159   }
 160
 161   xbt_dynar_push(reached_pairs, &pair);
 162
 163   MC_UNSET_RAW_MEM;
 164
 165   if(raw_mem_set)
 166     MC_SET_RAW_MEM;
 167   else
 168     MC_UNSET_RAW_MEM;
 169
 170 }
 171
 172 void MC_pair_delete(mc_pair_t pair){
 173   xbt_free(pair->graph_state->proc_status);
 174   xbt_free(pair->graph_state);
 175   xbt_free(pair);
 176 }
 177
 178
 179
 180 int MC_automaton_evaluate_label(xbt_exp_label_t l){
 181
 182   switch(l->type){
 183   case 0 : {
 184     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 185     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 186     return (left_res || right_res);
 187   }
 188   case 1 : {
 189     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 190     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 191     return (left_res && right_res);
 192   }
 193   case 2 : {
 194     int res = MC_automaton_evaluate_label(l->u.exp_not);
 195     return (!res);
 196   }
 197   case 3 : {
 198     unsigned int cursor = 0;
 199     xbt_propositional_symbol_t p = NULL;
 200     int_f_void_t f;
 201     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
 202       if(strcmp(p->pred, l->u.predicat) == 0){
 203         f = (int_f_void_t)p->function;
 204         return (*f)();
 205       }
 206     }
 207     return -1;
 208   }
 209   case 4 : {
 210     return 2;
 211   }
 212   default :
 213     return -1;
 214   }
 215 }
 216
 217
 218 /********************* Double-DFS stateless *******************/
 219
 220 void pair_stateless_free(mc_pair_stateless_t pair){
 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_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
 280   MC_take_snapshot_liveness(initial_snapshot_liveness);
 281
 282   MC_UNSET_RAW_MEM;
 283
 284   /* Get .plt section (start and end addresses) for data libsimgrid and data program comparison */
 285   get_libsimgrid_plt_section();
 286   get_binary_plt_section();
 287
 288   unsigned int cursor = 0;
 289   xbt_state_t state;
 290
 291   xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
 292     if(state->type == -1){
 293
 294       MC_SET_RAW_MEM;
 295       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 296       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 297       MC_UNSET_RAW_MEM;
 298
 299       if(cursor != 0){
 300         MC_restore_snapshot(initial_snapshot_liveness);
 301         MC_UNSET_RAW_MEM;
 302       }
 303
 304       MC_ddfs(0);
 305
 306     }else{
 307       if(state->type == 2){
 308
 309         MC_SET_RAW_MEM;
 310         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 311         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 312         MC_UNSET_RAW_MEM;
 313
 314         set_pair_reached(state);
 315
 316         if(cursor != 0){
 317           MC_restore_snapshot(initial_snapshot_liveness);
 318           MC_UNSET_RAW_MEM;
 319         }
 320
 321         MC_ddfs(1);
 322
 323       }
 324     }
 325   }
 326
 327   if(raw_mem_set)
 328     MC_SET_RAW_MEM;
 329   else
 330     MC_UNSET_RAW_MEM;
 331
 332
 333 }
 334
 335
 336 void MC_ddfs(int search_cycle){
 337
 338   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 339
 340   smx_process_t process;
 341   mc_pair_stateless_t current_pair = NULL;
 342
 343   if(xbt_fifo_size(mc_stack_liveness) == 0)
 344     return;
 345
 346
 347   /* Get current pair */
 348   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 349
 350   /* Update current state in buchi automaton */
 351   _mc_property_automaton->current_state = current_pair->automaton_state;
 352
 353
 354   XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
 355
 356   mc_stats_pair->visited_pairs++;
 357
 358   //sleep(1);
 359
 360   int value;
 361   mc_state_t next_graph_state = NULL;
 362   smx_simcall_t req = NULL;
 363   char *req_str;
 364
 365   xbt_transition_t transition_succ;
 366   unsigned int cursor = 0;
 367   int res;
 368
 369   mc_pair_stateless_t next_pair = NULL;
 370   mc_pair_stateless_t pair_succ;
 371
 372   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
 373
 374     if(current_pair->requests > 0){
 375
 376       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 377
 378         /* Debug information */
 379
 380         req_str = MC_request_to_string(req, value);
 381         XBT_INFO("Execute: %s", req_str);
 382         xbt_free(req_str);
 383
 384         MC_state_set_executed_request(current_pair->graph_state, req, value);
 385
 386         /* Answer the request */
 387         SIMIX_simcall_pre(req, value);
 388
 389         /* Wait for requests (schedules processes) */
 390         MC_wait_for_requests();
 391
 392         MC_SET_RAW_MEM;
 393
 394         /* Create the new expanded graph_state */
 395         next_graph_state = MC_state_pair_new();
 396
 397         /* Get enabled process and insert it in the interleave set of the next graph_state */
 398         xbt_swag_foreach(process, simix_global->process_list){
 399           if(MC_process_is_enabled(process)){
 400             MC_state_interleave_process(next_graph_state, process);
 401           }
 402         }
 403
 404         xbt_dynar_reset(successors);
 405
 406         MC_UNSET_RAW_MEM;
 407
 408
 409         cursor= 0;
 410         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 411
 412           res = MC_automaton_evaluate_label(transition_succ->label);
 413
 414           if(res == 1){ // enabled transition in automaton
 415             MC_SET_RAW_MEM;
 416             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 417             xbt_dynar_push(successors, &next_pair);
 418             MC_UNSET_RAW_MEM;
 419           }
 420
 421         }
 422
 423         cursor = 0;
 424
 425         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 426
 427           res = MC_automaton_evaluate_label(transition_succ->label);
 428
 429           if(res == 2){ // true transition in automaton
 430             MC_SET_RAW_MEM;
 431             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 432             xbt_dynar_push(successors, &next_pair);
 433             MC_UNSET_RAW_MEM;
 434           }
 435
 436         }
 437
 438         cursor = 0;
 439
 440         xbt_dynar_foreach(successors, cursor, pair_succ){
 441
 442           if(search_cycle == 1){
 443
 444             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 445
 446               if(reached(pair_succ->automaton_state)){
 447
 448                 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));
 449
 450                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 451                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 452                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 453                 XBT_INFO("Counter-example that violates formula :");
 454                 MC_show_stack_liveness(mc_stack_liveness);
 455                 MC_dump_stack_liveness(mc_stack_liveness);
 456                 MC_print_statistics_pairs(mc_stats_pair);
 457                 exit(0);
 458
 459               }else{
 460
 461                 XBT_INFO("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 462
 463                 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 464
 465                 MC_SET_RAW_MEM;
 466                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 467                 MC_UNSET_RAW_MEM;
 468
 469                 MC_ddfs(search_cycle);
 470
 471               }
 472
 473             }else{
 474
 475               MC_SET_RAW_MEM;
 476               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 477               MC_UNSET_RAW_MEM;
 478
 479               MC_ddfs(search_cycle);
 480
 481             }
 482
 483           }else{
 484
 485             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 486
 487               XBT_INFO("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 488
 489               set_pair_reached(pair_succ->automaton_state);
 490
 491               search_cycle = 1;
 492
 493               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 494
 495             }
 496
 497             MC_SET_RAW_MEM;
 498             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 499             MC_UNSET_RAW_MEM;
 500
 501             MC_ddfs(search_cycle);
 502
 503           }
 504
 505
 506           /* Restore system before checking others successors */
 507           if(cursor != (xbt_dynar_length(successors) - 1))
 508             MC_replay_liveness(mc_stack_liveness, 1);
 509
 510
 511         }
 512
 513         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 514           XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
 515           MC_replay_liveness(mc_stack_liveness, 0);
 516         }
 517       }
 518
 519
 520     }else{  /*No request to execute, search evolution in Büchi automaton */
 521
 522       MC_SET_RAW_MEM;
 523
 524       /* Create the new expanded graph_state */
 525       next_graph_state = MC_state_pair_new();
 526
 527       xbt_dynar_reset(successors);
 528
 529       MC_UNSET_RAW_MEM;
 530
 531
 532       cursor= 0;
 533       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 534
 535         res = MC_automaton_evaluate_label(transition_succ->label);
 536
 537         if(res == 1){ // enabled transition in automaton
 538           MC_SET_RAW_MEM;
 539           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 540           xbt_dynar_push(successors, &next_pair);
 541           MC_UNSET_RAW_MEM;
 542         }
 543
 544       }
 545
 546       cursor = 0;
 547
 548       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 549
 550         res = MC_automaton_evaluate_label(transition_succ->label);
 551
 552         if(res == 2){ // true transition in automaton
 553           MC_SET_RAW_MEM;
 554           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 555           xbt_dynar_push(successors, &next_pair);
 556           MC_UNSET_RAW_MEM;
 557         }
 558
 559       }
 560
 561       cursor = 0;
 562
 563       xbt_dynar_foreach(successors, cursor, pair_succ){
 564
 565         if(search_cycle == 1){
 566
 567           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 568
 569             if(reached(pair_succ->automaton_state)){
 570
 571               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
 572
 573               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 574               XBT_INFO("|             ACCEPTANCE CYCLE            |");
 575               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 576               XBT_INFO("Counter-example that violates formula :");
 577               MC_show_stack_liveness(mc_stack_liveness);
 578               MC_dump_stack_liveness(mc_stack_liveness);
 579               MC_print_statistics_pairs(mc_stats_pair);
 580               exit(0);
 581
 582             }else{
 583
 584               XBT_INFO("Next pair (depth = %d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 585
 586               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 587
 588               MC_SET_RAW_MEM;
 589               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 590               MC_UNSET_RAW_MEM;
 591
 592               MC_ddfs(search_cycle);
 593
 594             }
 595
 596           }else{
 597
 598             MC_SET_RAW_MEM;
 599             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 600             MC_UNSET_RAW_MEM;
 601
 602             MC_ddfs(search_cycle);
 603
 604           }
 605
 606
 607         }else{
 608
 609           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 610
 611             set_pair_reached(pair_succ->automaton_state);
 612
 613             search_cycle = 1;
 614
 615             XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 616
 617           }
 618
 619           MC_SET_RAW_MEM;
 620           xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 621           MC_UNSET_RAW_MEM;
 622
 623           MC_ddfs(search_cycle);
 624
 625         }
 626
 627         /* Restore system before checking others successors */
 628         if(cursor != xbt_dynar_length(successors) - 1)
 629           MC_replay_liveness(mc_stack_liveness, 1);
 630
 631
 632       }
 633
 634     }
 635
 636   }else{
 637
 638     XBT_INFO("Max depth reached");
 639
 640   }
 641
 642   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
 643     XBT_INFO("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
 644   }else{
 645     XBT_INFO("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
 646   }
 647
 648
 649   MC_SET_RAW_MEM;
 650   xbt_fifo_shift(mc_stack_liveness);
 651   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 652     xbt_dynar_pop(reached_pairs, NULL);
 653   }
 654   MC_UNSET_RAW_MEM;
 655
 656   if(raw_mem_set)
 657     MC_SET_RAW_MEM;
 658   else
 659     MC_UNSET_RAW_MEM;
 660
 661 }