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     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     create_dump(xbt_dynar_length(reached_pairs));
  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     create_dump(xbt_dynar_length(reached_pairs));
 120
 121     /* New pair reached */
 122     xbt_dynar_push(reached_pairs, &new_pair);
 123
 124     MC_UNSET_RAW_MEM;
 125
 126     if(raw_mem_set)
 127       MC_SET_RAW_MEM;
 128     else
 129       MC_UNSET_RAW_MEM;
 130
 131     compare = 0;
 132
 133     return 0;
 134
 135   }
 136 }
 137
 138
 139 void set_pair_reached(xbt_state_t st){
 140
 141   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 142
 143   MC_SET_RAW_MEM;
 144
 145   mc_pair_reached_t pair = NULL;
 146   pair = xbt_new0(s_mc_pair_reached_t, 1);
 147   pair->nb = xbt_dynar_length(reached_pairs) + 1;
 148   pair->automaton_state = st;
 149   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 150   pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
 151   MC_take_snapshot_liveness(pair->system_state);
 152
 153   /* Get values of propositional symbols */
 154   unsigned int cursor = 0;
 155   xbt_propositional_symbol_t ps = NULL;
 156   int res;
 157   int_f_void_t f;
 158
 159   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 160     f = (int_f_void_t)ps->function;
 161     res = (*f)();
 162     xbt_dynar_push_as(pair->prop_ato, int, res);
 163   }
 164
 165   xbt_dynar_push(reached_pairs, &pair);
 166
 167   MC_UNSET_RAW_MEM;
 168
 169   create_dump(xbt_dynar_length(reached_pairs));
 170
 171   if(raw_mem_set)
 172     MC_SET_RAW_MEM;
 173   else
 174     MC_UNSET_RAW_MEM;
 175
 176 }
 177
 178 void MC_pair_delete(mc_pair_t pair){
 179   xbt_free(pair->graph_state->proc_status);
 180   xbt_free(pair->graph_state);
 181   xbt_free(pair);
 182 }
 183
 184
 185
 186 int MC_automaton_evaluate_label(xbt_exp_label_t l){
 187
 188   switch(l->type){
 189   case 0 : {
 190     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 191     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 192     return (left_res || right_res);
 193   }
 194   case 1 : {
 195     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 196     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 197     return (left_res && right_res);
 198   }
 199   case 2 : {
 200     int res = MC_automaton_evaluate_label(l->u.exp_not);
 201     return (!res);
 202   }
 203   case 3 : {
 204     unsigned int cursor = 0;
 205     xbt_propositional_symbol_t p = NULL;
 206     int_f_void_t f;
 207     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
 208       if(strcmp(p->pred, l->u.predicat) == 0){
 209         f = (int_f_void_t)p->function;
 210         return (*f)();
 211       }
 212     }
 213     return -1;
 214   }
 215   case 4 : {
 216     return 2;
 217   }
 218   default :
 219     return -1;
 220   }
 221 }
 222
 223
 224 /********************* Double-DFS stateless *******************/
 225
 226 void MC_pair_stateless_delete(mc_pair_stateless_t pair){
 227   xbt_free(pair->graph_state->proc_status);
 228   xbt_free(pair->graph_state);
 229   xbt_free(pair);
 230 }
 231
 232 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
 233   mc_pair_stateless_t p = NULL;
 234   p = xbt_new0(s_mc_pair_stateless_t, 1);
 235   p->automaton_state = st;
 236   p->graph_state = sg;
 237   p->requests = r;
 238   mc_stats_pair->expanded_pairs++;
 239   return p;
 240 }
 241
 242 void MC_ddfs_init(void){
 243
 244   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 245
 246   XBT_INFO("**************************************************");
 247   XBT_INFO("Double-DFS init");
 248   XBT_INFO("**************************************************");
 249
 250   mc_pair_stateless_t mc_initial_pair = NULL;
 251   mc_state_t initial_graph_state = NULL;
 252   smx_process_t process;
 253
 254
 255   MC_wait_for_requests();
 256
 257   MC_SET_RAW_MEM;
 258
 259   initial_graph_state = MC_state_pair_new();
 260   xbt_swag_foreach(process, simix_global->process_list){
 261     if(MC_process_is_enabled(process)){
 262       MC_state_interleave_process(initial_graph_state, process);
 263     }
 264   }
 265
 266   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), NULL);
 267   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 268
 269   /* Save the initial state */
 270   initial_snapshot_liveness = xbt_new0(s_mc_snapshot_t, 1);
 271   MC_take_snapshot_liveness(initial_snapshot_liveness);
 272
 273   MC_UNSET_RAW_MEM;
 274
 275   unsigned int cursor = 0;
 276   xbt_state_t state;
 277
 278   xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
 279     if(state->type == -1){
 280
 281       MC_SET_RAW_MEM;
 282       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 283       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 284       MC_UNSET_RAW_MEM;
 285
 286       if(cursor != 0){
 287         MC_restore_snapshot(initial_snapshot_liveness);
 288         MC_UNSET_RAW_MEM;
 289       }
 290
 291       MC_ddfs(0);
 292
 293     }else{
 294       if(state->type == 2){
 295
 296         MC_SET_RAW_MEM;
 297         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 298         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 299         MC_UNSET_RAW_MEM;
 300
 301         set_pair_reached(state);
 302
 303         if(cursor != 0){
 304           MC_restore_snapshot(initial_snapshot_liveness);
 305           MC_UNSET_RAW_MEM;
 306         }
 307
 308         MC_ddfs(1);
 309
 310       }
 311     }
 312   }
 313
 314   if(raw_mem_set)
 315     MC_SET_RAW_MEM;
 316   else
 317     MC_UNSET_RAW_MEM;
 318
 319
 320 }
 321
 322
 323 void MC_ddfs(int search_cycle){
 324
 325   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 326
 327   smx_process_t process;
 328   mc_pair_stateless_t current_pair = NULL;
 329
 330   if(xbt_fifo_size(mc_stack_liveness) == 0)
 331     return;
 332
 333
 334   /* Get current pair */
 335   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 336
 337   /* Update current state in buchi automaton */
 338   _mc_property_automaton->current_state = current_pair->automaton_state;
 339
 340
 341   XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
 342
 343   mc_stats_pair->visited_pairs++;
 344
 345   //sleep(1);
 346
 347   int value;
 348   mc_state_t next_graph_state = NULL;
 349   smx_simcall_t req = NULL;
 350   char *req_str;
 351
 352   xbt_transition_t transition_succ;
 353   unsigned int cursor = 0;
 354   int res;
 355
 356   mc_pair_stateless_t next_pair = NULL;
 357   mc_pair_stateless_t pair_succ;
 358
 359   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
 360
 361     if(current_pair->requests > 0){
 362
 363       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 364
 365         /* Debug information */
 366
 367         req_str = MC_request_to_string(req, value);
 368         XBT_INFO("Execute: %s", req_str);
 369         xbt_free(req_str);
 370
 371         MC_state_set_executed_request(current_pair->graph_state, req, value);
 372
 373         /* Answer the request */
 374         SIMIX_simcall_pre(req, value);
 375
 376         /* Wait for requests (schedules processes) */
 377         MC_wait_for_requests();
 378
 379         MC_SET_RAW_MEM;
 380
 381         /* Create the new expanded graph_state */
 382         next_graph_state = MC_state_pair_new();
 383
 384         /* Get enabled process and insert it in the interleave set of the next graph_state */
 385         xbt_swag_foreach(process, simix_global->process_list){
 386           if(MC_process_is_enabled(process)){
 387             MC_state_interleave_process(next_graph_state, process);
 388           }
 389         }
 390
 391         xbt_dynar_reset(successors);
 392
 393         MC_UNSET_RAW_MEM;
 394
 395
 396         cursor= 0;
 397         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 398
 399           res = MC_automaton_evaluate_label(transition_succ->label);
 400
 401           if(res == 1){ // enabled transition in automaton
 402             MC_SET_RAW_MEM;
 403             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 404             xbt_dynar_push(successors, &next_pair);
 405             MC_UNSET_RAW_MEM;
 406           }
 407
 408         }
 409
 410         cursor = 0;
 411
 412         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 413
 414           res = MC_automaton_evaluate_label(transition_succ->label);
 415
 416           if(res == 2){ // true transition in automaton
 417             MC_SET_RAW_MEM;
 418             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 419             xbt_dynar_push(successors, &next_pair);
 420             MC_UNSET_RAW_MEM;
 421           }
 422
 423         }
 424
 425         cursor = 0;
 426
 427         xbt_dynar_foreach(successors, cursor, pair_succ){
 428
 429           if(search_cycle == 1){
 430
 431             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 432
 433               if(reached(pair_succ->automaton_state)){
 434
 435                 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));
 436
 437                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 438                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 439                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 440                 XBT_INFO("Counter-example that violates formula :");
 441                 MC_show_stack_liveness(mc_stack_liveness);
 442                 MC_dump_stack_liveness(mc_stack_liveness);
 443                 MC_print_statistics_pairs(mc_stats_pair);
 444                 exit(0);
 445
 446               }else{
 447
 448                 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);
 449
 450                 XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 451
 452                 MC_SET_RAW_MEM;
 453                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 454                 MC_UNSET_RAW_MEM;
 455
 456                 MC_ddfs(search_cycle);
 457
 458               }
 459
 460             }else{
 461
 462               MC_SET_RAW_MEM;
 463               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 464               MC_UNSET_RAW_MEM;
 465
 466               MC_ddfs(search_cycle);
 467
 468             }
 469
 470           }else{
 471
 472             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 473
 474               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);
 475
 476               set_pair_reached(pair_succ->automaton_state);
 477
 478               search_cycle = 1;
 479
 480               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 481
 482             }
 483
 484             MC_SET_RAW_MEM;
 485             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 486             MC_UNSET_RAW_MEM;
 487
 488             MC_ddfs(search_cycle);
 489
 490           }
 491
 492
 493           /* Restore system before checking others successors */
 494           if(cursor != (xbt_dynar_length(successors) - 1))
 495             MC_replay_liveness(mc_stack_liveness, 1);
 496
 497
 498         }
 499
 500         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 501           XBT_INFO("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
 502           MC_replay_liveness(mc_stack_liveness, 0);
 503         }
 504       }
 505
 506
 507     }else{  /*No request to execute, search evolution in Büchi automaton */
 508
 509       MC_SET_RAW_MEM;
 510
 511       /* Create the new expanded graph_state */
 512       next_graph_state = MC_state_pair_new();
 513
 514       xbt_dynar_reset(successors);
 515
 516       MC_UNSET_RAW_MEM;
 517
 518
 519       cursor= 0;
 520       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 521
 522         res = MC_automaton_evaluate_label(transition_succ->label);
 523
 524         if(res == 1){ // enabled transition in automaton
 525           MC_SET_RAW_MEM;
 526           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 527           xbt_dynar_push(successors, &next_pair);
 528           MC_UNSET_RAW_MEM;
 529         }
 530
 531       }
 532
 533       cursor = 0;
 534
 535       xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 536
 537         res = MC_automaton_evaluate_label(transition_succ->label);
 538
 539         if(res == 2){ // true transition in automaton
 540           MC_SET_RAW_MEM;
 541           next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 542           xbt_dynar_push(successors, &next_pair);
 543           MC_UNSET_RAW_MEM;
 544         }
 545
 546       }
 547
 548       cursor = 0;
 549
 550       xbt_dynar_foreach(successors, cursor, pair_succ){
 551
 552         if(search_cycle == 1){
 553
 554           if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 555
 556             if(reached(pair_succ->automaton_state)){
 557
 558               XBT_INFO("Next pair (depth = %d) already reached !", xbt_fifo_size(mc_stack_liveness) + 1);
 559
 560               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 561               XBT_INFO("|             ACCEPTANCE CYCLE            |");
 562               XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 563               XBT_INFO("Counter-example that violates formula :");
 564               MC_show_stack_liveness(mc_stack_liveness);
 565               MC_dump_stack_liveness(mc_stack_liveness);
 566               MC_print_statistics_pairs(mc_stats_pair);
 567               exit(0);
 568
 569             }else{
 570
 571               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);
 572
 573               XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 574
 575               MC_SET_RAW_MEM;
 576               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 577               MC_UNSET_RAW_MEM;
 578
 579               MC_ddfs(search_cycle);
 580
 581             }
 582
 583           }else{
 584
 585             MC_SET_RAW_MEM;
 586             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 587             MC_UNSET_RAW_MEM;
 588
 589             MC_ddfs(search_cycle);
 590
 591           }
 592
 593
 594         }else{
 595
 596           if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 597
 598             set_pair_reached(pair_succ->automaton_state);
 599
 600             search_cycle = 1;
 601
 602             XBT_INFO("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 603
 604           }
 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         /* Restore system before checking others successors */
 615         if(cursor != xbt_dynar_length(successors) - 1)
 616           MC_replay_liveness(mc_stack_liveness, 1);
 617
 618
 619       }
 620
 621     }
 622
 623   }else{
 624
 625     XBT_INFO("Max depth reached");
 626
 627   }
 628
 629   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
 630     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) );
 631   }else{
 632     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) );
 633   }
 634
 635
 636   MC_SET_RAW_MEM;
 637   xbt_fifo_shift(mc_stack_liveness);
 638   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 639     xbt_dynar_pop(reached_pairs, NULL);
 640   }
 641   MC_UNSET_RAW_MEM;
 642
 643   if(raw_mem_set)
 644     MC_SET_RAW_MEM;
 645   else
 646     MC_UNSET_RAW_MEM;
 647
 648 }