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     return 0;
  87
  88   }else{
  89
  90     MC_SET_RAW_MEM;
  91
  92     cursor = 0;
  93     mc_pair_reached_t pair_test = NULL;
  94
  95     xbt_dynar_foreach(reached_pairs, cursor, pair_test){
  96       XBT_INFO("Pair reached #%d", pair_test->nb);
  97       if(automaton_state_compare(pair_test->automaton_state, st) == 0){
  98         if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
  99           if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
 100
 101             if(raw_mem_set)
 102               MC_SET_RAW_MEM;
 103             else
 104               MC_UNSET_RAW_MEM;
 105
 106             return 1;
 107           }
 108         }else{
 109           XBT_INFO("Different values of propositional symbols");
 110         }
 111       }else{
 112         XBT_INFO("Different automaton state");
 113       }
 114     }
 115
 116     /* New pair reached */
 117     xbt_dynar_push(reached_pairs, &new_pair);
 118
 119     MC_UNSET_RAW_MEM;
 120
 121     if(raw_mem_set)
 122       MC_SET_RAW_MEM;
 123     else
 124       MC_UNSET_RAW_MEM;
 125
 126     compare = 0;
 127
 128     return 0;
 129
 130   }
 131 }
 132
 133
 134 void set_pair_reached(xbt_state_t st){
 135
 136   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 137
 138   MC_SET_RAW_MEM;
 139
 140   mc_pair_reached_t pair = NULL;
 141   pair = xbt_new0(s_mc_pair_reached_t, 1);
 142   pair->nb = xbt_dynar_length(reached_pairs) + 1;
 143   pair->automaton_state = st;
 144   pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
 145   pair->system_state = MC_take_snapshot_liveness();
 146
 147   /* Get values of propositional symbols */
 148   unsigned int cursor = 0;
 149   xbt_propositional_symbol_t ps = NULL;
 150   int res;
 151   int_f_void_t f;
 152
 153   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
 154     f = (int_f_void_t)ps->function;
 155     res = (*f)();
 156     xbt_dynar_push_as(pair->prop_ato, int, res);
 157   }
 158
 159   xbt_dynar_push(reached_pairs, &pair);
 160
 161   MC_UNSET_RAW_MEM;
 162
 163   if(raw_mem_set)
 164     MC_SET_RAW_MEM;
 165   else
 166     MC_UNSET_RAW_MEM;
 167
 168 }
 169
 170 void MC_pair_delete(mc_pair_t pair){
 171   xbt_free(pair->graph_state->proc_status);
 172   xbt_free(pair->graph_state);
 173   xbt_free(pair);
 174 }
 175
 176
 177
 178 int MC_automaton_evaluate_label(xbt_exp_label_t l){
 179
 180   switch(l->type){
 181   case 0 : {
 182     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 183     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 184     return (left_res || right_res);
 185   }
 186   case 1 : {
 187     int left_res = MC_automaton_evaluate_label(l->u.or_and.left_exp);
 188     int right_res = MC_automaton_evaluate_label(l->u.or_and.right_exp);
 189     return (left_res && right_res);
 190   }
 191   case 2 : {
 192     int res = MC_automaton_evaluate_label(l->u.exp_not);
 193     return (!res);
 194   }
 195   case 3 : {
 196     unsigned int cursor = 0;
 197     xbt_propositional_symbol_t p = NULL;
 198     int_f_void_t f;
 199     xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
 200       if(strcmp(p->pred, l->u.predicat) == 0){
 201         f = (int_f_void_t)p->function;
 202         return (*f)();
 203       }
 204     }
 205     return -1;
 206   }
 207   case 4 : {
 208     return 2;
 209   }
 210   default :
 211     return -1;
 212   }
 213 }
 214
 215
 216 /********************* Double-DFS stateless *******************/
 217
 218 void pair_stateless_free(mc_pair_stateless_t pair){
 219   xbt_free(pair);
 220 }
 221
 222 void pair_stateless_free_voidp(void *p){
 223   pair_stateless_free((mc_pair_stateless_t) * (void **) p);
 224 }
 225
 226 mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r){
 227   mc_pair_stateless_t p = NULL;
 228   p = xbt_new0(s_mc_pair_stateless_t, 1);
 229   p->automaton_state = st;
 230   p->graph_state = sg;
 231   p->requests = r;
 232   mc_stats_pair->expanded_pairs++;
 233   return p;
 234 }
 235
 236 void pair_reached_free(mc_pair_reached_t pair){
 237   if(pair){
 238     pair->automaton_state = NULL;
 239     xbt_dynar_free(&(pair->prop_ato));
 240     MC_free_snapshot(pair->system_state);
 241     xbt_free(pair);
 242   }
 243 }
 244
 245 void pair_reached_free_voidp(void *p){
 246   pair_reached_free((mc_pair_reached_t) * (void **) p);
 247 }
 248
 249 void MC_ddfs_init(void){
 250
 251   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 252
 253   XBT_INFO("**************************************************");
 254   XBT_INFO("Double-DFS init");
 255   XBT_INFO("**************************************************");
 256
 257   mc_pair_stateless_t mc_initial_pair = NULL;
 258   mc_state_t initial_graph_state = NULL;
 259   smx_process_t process;
 260
 261
 262   MC_wait_for_requests();
 263
 264   MC_SET_RAW_MEM;
 265
 266   initial_graph_state = MC_state_pair_new();
 267   xbt_swag_foreach(process, simix_global->process_list){
 268     if(MC_process_is_enabled(process)){
 269       MC_state_interleave_process(initial_graph_state, process);
 270     }
 271   }
 272
 273   reached_pairs = xbt_dynar_new(sizeof(mc_pair_reached_t), pair_reached_free_voidp);
 274   successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
 275
 276   /* Save the initial state */
 277   initial_state_liveness = xbt_new0(s_mc_global_t, 1);
 278   initial_state_liveness->initial_snapshot = MC_take_snapshot_liveness();
 279
 280   MC_UNSET_RAW_MEM;
 281
 282   unsigned int cursor = 0;
 283   xbt_state_t state;
 284
 285   xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
 286     if(state->type == -1){
 287
 288       MC_SET_RAW_MEM;
 289       mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 290       xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 291       MC_UNSET_RAW_MEM;
 292
 293       if(cursor != 0){
 294         MC_restore_snapshot(initial_state_liveness->initial_snapshot);
 295         MC_UNSET_RAW_MEM;
 296       }
 297
 298       MC_ddfs(0);
 299
 300     }else{
 301       if(state->type == 2){
 302
 303         MC_SET_RAW_MEM;
 304         mc_initial_pair = new_pair_stateless(initial_graph_state, state, MC_state_interleave_size(initial_graph_state));
 305         xbt_fifo_unshift(mc_stack_liveness, mc_initial_pair);
 306         MC_UNSET_RAW_MEM;
 307
 308         set_pair_reached(state);
 309
 310         if(cursor != 0){
 311           MC_restore_snapshot(initial_state_liveness->initial_snapshot);
 312           MC_UNSET_RAW_MEM;
 313         }
 314
 315         MC_ddfs(1);
 316
 317       }
 318     }
 319   }
 320
 321   if(raw_mem_set)
 322     MC_SET_RAW_MEM;
 323   else
 324     MC_UNSET_RAW_MEM;
 325
 326
 327 }
 328
 329
 330 void MC_ddfs(int search_cycle){
 331
 332   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 333
 334   smx_process_t process;
 335   mc_pair_stateless_t current_pair = NULL;
 336
 337   if(xbt_fifo_size(mc_stack_liveness) == 0)
 338     return;
 339
 340
 341   /* Get current pair */
 342   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 343
 344   /* Update current state in buchi automaton */
 345   _mc_property_automaton->current_state = current_pair->automaton_state;
 346
 347
 348   XBT_DEBUG("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
 349
 350   mc_stats_pair->visited_pairs++;
 351
 352   //sleep(1);
 353
 354   int value;
 355   mc_state_t next_graph_state = NULL;
 356   smx_simcall_t req = NULL;
 357   char *req_str;
 358
 359   xbt_transition_t transition_succ;
 360   unsigned int cursor = 0;
 361   int res;
 362
 363   mc_pair_stateless_t next_pair = NULL;
 364   mc_pair_stateless_t pair_succ;
 365
 366   if(xbt_fifo_size(mc_stack_liveness) < MAX_DEPTH_LIVENESS){
 367
 368     if(current_pair->requests > 0){
 369
 370       while((req = MC_state_get_request(current_pair->graph_state, &value)) != NULL){
 371
 372         /* Debug information */
 373
 374         req_str = MC_request_to_string(req, value);
 375         XBT_DEBUG("Execute: %s", req_str);
 376         xbt_free(req_str);
 377
 378         MC_state_set_executed_request(current_pair->graph_state, req, value);
 379
 380         /* Answer the request */
 381         SIMIX_simcall_pre(req, value);
 382
 383         /* Wait for requests (schedules processes) */
 384         MC_wait_for_requests();
 385
 386         MC_SET_RAW_MEM;
 387
 388         /* Create the new expanded graph_state */
 389         next_graph_state = MC_state_pair_new();
 390
 391         /* Get enabled process and insert it in the interleave set of the next graph_state */
 392         xbt_swag_foreach(process, simix_global->process_list){
 393           if(MC_process_is_enabled(process)){
 394             MC_state_interleave_process(next_graph_state, process);
 395           }
 396         }
 397
 398         xbt_dynar_reset(successors);
 399
 400         MC_UNSET_RAW_MEM;
 401
 402
 403         cursor= 0;
 404         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 405
 406           res = MC_automaton_evaluate_label(transition_succ->label);
 407
 408           if(res == 1){ // enabled transition in automaton
 409             MC_SET_RAW_MEM;
 410             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 411             xbt_dynar_push(successors, &next_pair);
 412             MC_UNSET_RAW_MEM;
 413           }
 414
 415         }
 416
 417         cursor = 0;
 418
 419         xbt_dynar_foreach(current_pair->automaton_state->out, cursor, transition_succ){
 420
 421           res = MC_automaton_evaluate_label(transition_succ->label);
 422
 423           if(res == 2){ // true transition in automaton
 424             MC_SET_RAW_MEM;
 425             next_pair = new_pair_stateless(next_graph_state, transition_succ->dst, MC_state_interleave_size(next_graph_state));
 426             xbt_dynar_push(successors, &next_pair);
 427             MC_UNSET_RAW_MEM;
 428           }
 429
 430         }
 431
 432         cursor = 0;
 433
 434         xbt_dynar_foreach(successors, cursor, pair_succ){
 435
 436           if(search_cycle == 1){
 437
 438             if((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2)){
 439
 440               if(reached(pair_succ->automaton_state)){
 441
 442                 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));
 443
 444                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 445                 XBT_INFO("|             ACCEPTANCE CYCLE            |");
 446                 XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 447                 XBT_INFO("Counter-example that violates formula :");
 448                 MC_show_stack_liveness(mc_stack_liveness);
 449                 MC_dump_stack_liveness(mc_stack_liveness);
 450                 MC_print_statistics_pairs(mc_stats_pair);
 451                 xbt_abort();
 452
 453               }else{
 454
 455                 XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 456
 457                 XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 458
 459                 MC_SET_RAW_MEM;
 460                 xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 461                 MC_UNSET_RAW_MEM;
 462
 463                 MC_ddfs(search_cycle);
 464
 465               }
 466
 467             }else{
 468
 469               MC_SET_RAW_MEM;
 470               xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 471               MC_UNSET_RAW_MEM;
 472
 473               MC_ddfs(search_cycle);
 474
 475             }
 476
 477           }else{
 478
 479             if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
 480
 481               XBT_DEBUG("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
 482
 483               set_pair_reached(pair_succ->automaton_state);
 484
 485               search_cycle = 1;
 486
 487               XBT_DEBUG("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
 488
 489             }
 490
 491             MC_SET_RAW_MEM;
 492             xbt_fifo_unshift(mc_stack_liveness, pair_succ);
 493             MC_UNSET_RAW_MEM;
 494
 495             MC_ddfs(search_cycle);
 496
 497           }
 498
 499
 500           /* Restore system before checking others successors */
 501           if(cursor != (xbt_dynar_length(successors) - 1))
 502             MC_replay_liveness(mc_stack_liveness, 1);
 503
 504
 505         }
 506
 507         if(MC_state_interleave_size(current_pair->graph_state) > 0){
 508           XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
 509           MC_replay_liveness(mc_stack_liveness, 0);
 510         }
 511       }
 512
 513
 514     }
 515
 516   }else{
 517
 518     XBT_DEBUG("Max depth reached");
 519
 520   }
 521
 522   if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
 523     XBT_DEBUG("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
 524   }else{
 525     XBT_DEBUG("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
 526   }
 527
 528
 529   MC_SET_RAW_MEM;
 530   xbt_fifo_shift(mc_stack_liveness);
 531   if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
 532     xbt_dynar_pop(reached_pairs, NULL);
 533   }
 534   MC_UNSET_RAW_MEM;
 535
 536   if(raw_mem_set)
 537     MC_SET_RAW_MEM;
 538   else
 539     MC_UNSET_RAW_MEM;
 540
 541 }