src/mc/mc_liveness.c

   1 /* Copyright (c) 2011-2014. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #include <unistd.h>
   8 #include <sys/wait.h>
   9
  10 #include <xbt/dynar.h>
  11 #include <xbt/automaton.h>
  12
  13 #include "mc_request.h"
  14 #include "mc_liveness.h"
  15 #include "mc_private.h"
  16 #include "mc_record.h"
  17
  18 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
  19                                 "Logging specific to algorithms for liveness properties verification");
  20
  21 /********* Global variables *********/
  22
  23 xbt_dynar_t acceptance_pairs;
  24 xbt_dynar_t successors;
  25 xbt_parmap_t parmap;
  26
  27 /********* Static functions *********/
  28
  29 static xbt_dynar_t get_atomic_propositions_values()
  30 {
  31   int res;
  32   int_f_void_t f;
  33   unsigned int cursor = 0;
  34   xbt_automaton_propositional_symbol_t ps = NULL;
  35   xbt_dynar_t values = xbt_dynar_new(sizeof(int), NULL);
  36   // FIXME, cross-process support
  37   xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps) {
  38     f = (int_f_void_t) ps->function;
  39     res = f();
  40     xbt_dynar_push_as(values, int, res);
  41   }
  42
  43   return values;
  44 }
  45
  46
  47 static mc_visited_pair_t is_reached_acceptance_pair(int pair_num,
  48                                                     xbt_automaton_state_t
  49                                                     automaton_state,
  50                                                     xbt_dynar_t
  51                                                     atomic_propositions)
  52 {
  53   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
  54
  55   mc_visited_pair_t pair = NULL;
  56   pair = MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
  57   pair->acceptance_pair = 1;
  58
  59   if (xbt_dynar_is_empty(acceptance_pairs)) {
  60
  61     xbt_dynar_push(acceptance_pairs, &pair);
  62
  63   } else {
  64
  65     int min = -1, max = -1, index;
  66     //int res;
  67     mc_visited_pair_t pair_test;
  68     int cursor;
  69
  70     index = get_search_interval(acceptance_pairs, pair, &min, &max);
  71
  72     if (min != -1 && max != -1) {       // Acceptance pair with same number of processes and same heap bytes used exists
  73
  74       // Parallell implementation
  75       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(acceptance_pairs, min), (max-min)+1, pair);
  76          if(res != -1){
  77          if(!raw_mem_set)
  78          MC_SET_STD_HEAP;
  79          return ((mc_pair_t)xbt_dynar_get_as(acceptance_pairs, (min+res)-1, mc_pair_t))->num;
  80          } */
  81
  82       cursor = min;
  83       while (cursor <= max) {
  84         pair_test =
  85             (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, cursor,
  86                                                  mc_visited_pair_t);
  87         if (xbt_automaton_state_compare
  88             (pair_test->automaton_state, pair->automaton_state) == 0) {
  89           if (xbt_automaton_propositional_symbols_compare_value
  90               (pair_test->atomic_propositions,
  91                pair->atomic_propositions) == 0) {
  92             if (snapshot_compare(pair_test, pair) == 0) {
  93               XBT_INFO("Pair %d already reached (equal to pair %d) !",
  94                        pair->num, pair_test->num);
  95
  96               xbt_fifo_shift(mc_stack);
  97               if (dot_output != NULL)
  98                 fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
  99                         initial_global_state->prev_pair, pair_test->num,
 100                         initial_global_state->prev_req);
 101               mmalloc_set_current_heap(heap);
 102               return NULL;
 103             }
 104           }
 105         }
 106         cursor++;
 107       }
 108       xbt_dynar_insert_at(acceptance_pairs, min, &pair);
 109     } else {
 110       pair_test =
 111           (mc_visited_pair_t) xbt_dynar_get_as(acceptance_pairs, index,
 112                                                mc_visited_pair_t);
 113       if (pair_test->nb_processes < pair->nb_processes) {
 114         xbt_dynar_insert_at(acceptance_pairs, index + 1, &pair);
 115       } else {
 116         if (pair_test->heap_bytes_used < pair->heap_bytes_used)
 117           xbt_dynar_insert_at(acceptance_pairs, index + 1, &pair);
 118         else
 119           xbt_dynar_insert_at(acceptance_pairs, index, &pair);
 120       }
 121     }
 122
 123   }
 124   mmalloc_set_current_heap(heap);
 125   return pair;
 126 }
 127
 128 static void remove_acceptance_pair(int pair_num)
 129 {
 130   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 131
 132   unsigned int cursor = 0;
 133   mc_visited_pair_t pair_test = NULL;
 134
 135   xbt_dynar_foreach(acceptance_pairs, cursor, pair_test) {
 136     if (pair_test->num == pair_num) {
 137       break;
 138     }
 139   }
 140
 141   xbt_dynar_remove_at(acceptance_pairs, cursor, &pair_test);
 142
 143   pair_test->acceptance_removed = 1;
 144
 145   if (_sg_mc_visited == 0) {
 146     MC_visited_pair_delete(pair_test);
 147   } else if (pair_test->visited_removed == 1) {
 148     MC_visited_pair_delete(pair_test);
 149   }
 150
 151   mmalloc_set_current_heap(heap);
 152 }
 153
 154
 155 static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l,
 156                                        xbt_dynar_t atomic_propositions_values)
 157 {
 158
 159   switch (l->type) {
 160   case 0:{
 161       int left_res =
 162           MC_automaton_evaluate_label(l->u.or_and.left_exp,
 163                                       atomic_propositions_values);
 164       int right_res =
 165           MC_automaton_evaluate_label(l->u.or_and.right_exp,
 166                                       atomic_propositions_values);
 167       return (left_res || right_res);
 168     }
 169   case 1:{
 170       int left_res =
 171           MC_automaton_evaluate_label(l->u.or_and.left_exp,
 172                                       atomic_propositions_values);
 173       int right_res =
 174           MC_automaton_evaluate_label(l->u.or_and.right_exp,
 175                                       atomic_propositions_values);
 176       return (left_res && right_res);
 177     }
 178   case 2:{
 179       int res =
 180           MC_automaton_evaluate_label(l->u.exp_not, atomic_propositions_values);
 181       return (!res);
 182     }
 183   case 3:{
 184       unsigned int cursor = 0;
 185       xbt_automaton_propositional_symbol_t p = NULL;
 186       xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor,
 187                         p) {
 188         if (strcmp(p->pred, l->u.predicat) == 0)
 189           return (int) xbt_dynar_get_as(atomic_propositions_values, cursor,
 190                                         int);
 191       }
 192       return -1;
 193     }
 194   case 4:{
 195       return 2;
 196     }
 197   default:
 198     return -1;
 199   }
 200 }
 201
 202 void MC_pre_modelcheck_liveness(void)
 203 {
 204
 205   initial_global_state->raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
 206
 207   mc_pair_t initial_pair = NULL;
 208   smx_process_t process;
 209
 210   MC_wait_for_requests();
 211
 212   MC_SET_MC_HEAP;
 213
 214   acceptance_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
 215   visited_pairs = xbt_dynar_new(sizeof(mc_visited_pair_t), NULL);
 216   successors = xbt_dynar_new(sizeof(mc_pair_t), NULL);
 217
 218   initial_global_state->snapshot = MC_take_snapshot(0);
 219   initial_global_state->prev_pair = 0;
 220
 221   MC_SET_STD_HEAP;
 222
 223   unsigned int cursor = 0;
 224   xbt_automaton_state_t automaton_state;
 225
 226   xbt_dynar_foreach(_mc_property_automaton->states, cursor, automaton_state) {
 227     if (automaton_state->type == -1) {  /* Initial automaton state */
 228
 229       MC_SET_MC_HEAP;
 230
 231       initial_pair = MC_pair_new();
 232       initial_pair->automaton_state = automaton_state;
 233       initial_pair->graph_state = MC_state_new();
 234       initial_pair->atomic_propositions = get_atomic_propositions_values();
 235
 236       /* Get enabled processes and insert them in the interleave set of the graph_state */
 237       xbt_swag_foreach(process, simix_global->process_list) {
 238         if (MC_process_is_enabled(process)) {
 239           MC_state_interleave_process(initial_pair->graph_state, process);
 240         }
 241       }
 242
 243       initial_pair->requests =
 244           MC_state_interleave_size(initial_pair->graph_state);
 245       initial_pair->search_cycle = 0;
 246
 247       xbt_fifo_unshift(mc_stack, initial_pair);
 248
 249       MC_SET_STD_HEAP;
 250
 251       MC_modelcheck_liveness();
 252
 253       if (cursor != 0) {
 254         MC_restore_snapshot(initial_global_state->snapshot);
 255         MC_SET_STD_HEAP;
 256       }
 257     }
 258   }
 259
 260   if (initial_global_state->raw_mem_set)
 261     MC_SET_MC_HEAP;
 262   else
 263     MC_SET_STD_HEAP;
 264 }
 265
 266
 267 void MC_modelcheck_liveness()
 268 {
 269   smx_process_t process;
 270   mc_pair_t current_pair = NULL;
 271
 272   if (xbt_fifo_size(mc_stack) == 0)
 273     return;
 274
 275   /* Get current pair */
 276   current_pair =
 277       (mc_pair_t) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
 278
 279   /* Update current state in buchi automaton */
 280   _mc_property_automaton->current_state = current_pair->automaton_state;
 281
 282   XBT_DEBUG
 283       ("********************* ( Depth = %d, search_cycle = %d, interleave size %d, pair_num %d)",
 284        xbt_fifo_size(mc_stack), current_pair->search_cycle,
 285        MC_state_interleave_size(current_pair->graph_state), current_pair->num);
 286
 287   mc_stats->visited_pairs++;
 288
 289   int value;
 290   smx_simcall_t req = NULL;
 291
 292   xbt_automaton_transition_t transition_succ;
 293   unsigned int cursor = 0;
 294   int res;
 295   int visited_num;
 296
 297   mc_pair_t next_pair = NULL;
 298   xbt_dynar_t prop_values = NULL;
 299   mc_visited_pair_t reached_pair = NULL;
 300   int counter_example_depth = 0;
 301
 302   if (xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
 303
 304     if (current_pair->requests > 0) {
 305
 306       if (current_pair->search_cycle) {
 307
 308         if ((current_pair->automaton_state->type == 1)
 309             || (current_pair->automaton_state->type == 2)) {
 310           if ((reached_pair =
 311                is_reached_acceptance_pair(current_pair->num,
 312                                           current_pair->automaton_state,
 313                                           current_pair->atomic_propositions)) ==
 314               NULL) {
 315
 316             counter_example_depth = xbt_fifo_size(mc_stack);
 317             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 318             XBT_INFO("|             ACCEPTANCE CYCLE            |");
 319             XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
 320             XBT_INFO("Counter-example that violates formula :");
 321             MC_show_stack_liveness(mc_stack);
 322             MC_dump_stack_liveness(mc_stack);
 323             MC_print_statistics(mc_stats);
 324             XBT_INFO("Counter-example depth : %d", counter_example_depth);
 325             xbt_abort();
 326
 327           }
 328         }
 329       }
 330
 331       if ((visited_num =
 332            is_visited_pair(reached_pair, current_pair->num,
 333                            current_pair->automaton_state,
 334                            current_pair->atomic_propositions)) != -1) {
 335
 336         MC_SET_MC_HEAP;
 337         if (dot_output != NULL)
 338           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 339                   initial_global_state->prev_pair, visited_num,
 340                   initial_global_state->prev_req);
 341         MC_SET_STD_HEAP;
 342
 343       } else {
 344
 345         while ((req =
 346                 MC_state_get_request(current_pair->graph_state,
 347                                      &value)) != NULL) {
 348
 349           MC_SET_MC_HEAP;
 350           if (dot_output != NULL) {
 351             if (initial_global_state->prev_pair != 0
 352                 && initial_global_state->prev_pair != current_pair->num) {
 353               fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 354                       initial_global_state->prev_pair, current_pair->num,
 355                       initial_global_state->prev_req);
 356               xbt_free(initial_global_state->prev_req);
 357             }
 358             initial_global_state->prev_pair = current_pair->num;
 359           }
 360           MC_SET_STD_HEAP;
 361
 362           MC_LOG_REQUEST(mc_liveness, req, value);
 363
 364           MC_SET_MC_HEAP;
 365           if (dot_output != NULL) {
 366             initial_global_state->prev_req =
 367                 MC_request_get_dot_output(req, value);
 368             if (current_pair->search_cycle)
 369               fprintf(dot_output, "%d [shape=doublecircle];\n",
 370                       current_pair->num);
 371           }
 372           MC_SET_STD_HEAP;
 373
 374           MC_state_set_executed_request(current_pair->graph_state, req, value);
 375           mc_stats->executed_transitions++;
 376
 377           /* Answer the request */
 378           SIMIX_simcall_handle(req, value);
 379
 380           /* Wait for requests (schedules processes) */
 381           MC_wait_for_requests();
 382
 383           MC_SET_MC_HEAP;
 384           prop_values = get_atomic_propositions_values();
 385           MC_SET_STD_HEAP;
 386
 387           int new_pair = 0;
 388
 389           /* Evaluate enabled transition according to atomic propositions values */
 390           cursor = 0;
 391           xbt_dynar_foreach(current_pair->automaton_state->out, cursor,
 392                             transition_succ) {
 393
 394             res =
 395                 MC_automaton_evaluate_label(transition_succ->label,
 396                                             prop_values);
 397
 398             if (res == 1) {     // enabled transition in automaton
 399
 400               if (new_pair)
 401                 MC_replay_liveness(mc_stack, 1);
 402
 403               MC_SET_MC_HEAP;
 404
 405               next_pair = MC_pair_new();
 406               next_pair->graph_state = MC_state_new();
 407               next_pair->automaton_state = transition_succ->dst;
 408               next_pair->atomic_propositions = get_atomic_propositions_values();
 409
 410               /* Get enabled processes and insert them in the interleave set of the next graph_state */
 411               xbt_swag_foreach(process, simix_global->process_list) {
 412                 if (MC_process_is_enabled(process)) {
 413                   MC_state_interleave_process(next_pair->graph_state, process);
 414                 }
 415               }
 416
 417               next_pair->requests =
 418                   MC_state_interleave_size(next_pair->graph_state);
 419
 420               if (next_pair->automaton_state->type == 1
 421                   || next_pair->automaton_state->type == 2
 422                   || current_pair->search_cycle)
 423                 next_pair->search_cycle = 1;
 424
 425               xbt_fifo_unshift(mc_stack, next_pair);
 426
 427               if (mc_stats->expanded_pairs % 1000000 == 0)
 428                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 429
 430               MC_SET_STD_HEAP;
 431
 432               new_pair = 1;
 433
 434               MC_modelcheck_liveness();
 435
 436             }
 437
 438           }
 439
 440           /* Then, evaluate true transitions (always true, whatever atomic propositions values) */
 441           cursor = 0;
 442           xbt_dynar_foreach(current_pair->automaton_state->out, cursor,
 443                             transition_succ) {
 444
 445             res =
 446                 MC_automaton_evaluate_label(transition_succ->label,
 447                                             prop_values);
 448
 449             if (res == 2) {     // true transition in automaton
 450
 451               if (new_pair)
 452                 MC_replay_liveness(mc_stack, 1);
 453
 454               MC_SET_MC_HEAP;
 455
 456               next_pair = MC_pair_new();
 457               next_pair->graph_state = MC_state_new();
 458               next_pair->automaton_state = transition_succ->dst;
 459               next_pair->atomic_propositions = get_atomic_propositions_values();
 460
 461               /* Get enabled process and insert it in the interleave set of the next graph_state */
 462               xbt_swag_foreach(process, simix_global->process_list) {
 463                 if (MC_process_is_enabled(process)) {
 464                   MC_state_interleave_process(next_pair->graph_state, process);
 465                 }
 466               }
 467
 468               next_pair->requests =
 469                   MC_state_interleave_size(next_pair->graph_state);
 470
 471               if (next_pair->automaton_state->type == 1
 472                   || next_pair->automaton_state->type == 2
 473                   || current_pair->search_cycle)
 474                 next_pair->search_cycle = 1;
 475
 476               xbt_fifo_unshift(mc_stack, next_pair);
 477
 478               if (mc_stats->expanded_pairs % 1000000 == 0)
 479                 XBT_INFO("Expanded pairs : %lu", mc_stats->expanded_pairs);
 480
 481               MC_SET_STD_HEAP;
 482
 483               new_pair = 1;
 484
 485               MC_modelcheck_liveness();
 486
 487             }
 488
 489           }
 490
 491           if (MC_state_interleave_size(current_pair->graph_state) > 0) {
 492             XBT_DEBUG("Backtracking to depth %d", xbt_fifo_size(mc_stack));
 493             MC_replay_liveness(mc_stack, 0);
 494           }
 495
 496         }
 497
 498       }
 499
 500     }
 501
 502   } else {
 503
 504     XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 505     if (MC_state_interleave_size(current_pair->graph_state) > 0) {
 506       XBT_WARN
 507           ("/!\\ But, there are still processes to interleave. Model-checker will not be able to ensure the soundness of the verification from now. /!\\ ");
 508       if (_sg_mc_max_depth == 1000)
 509         XBT_WARN
 510             ("Notice : the default value of max depth is 1000 but you can change it with cfg=model-check/max_depth:value.");
 511     }
 512
 513   }
 514
 515   if (xbt_fifo_size(mc_stack) == _sg_mc_max_depth) {
 516     XBT_DEBUG("Pair %d (depth = %d) shifted in stack, maximum depth reached",
 517               current_pair->num, xbt_fifo_size(mc_stack));
 518   } else {
 519     XBT_DEBUG("Pair %d (depth = %d) shifted in stack", current_pair->num,
 520               xbt_fifo_size(mc_stack));
 521   }
 522
 523
 524   MC_SET_MC_HEAP;
 525   xbt_dynar_free(&prop_values);
 526   current_pair = xbt_fifo_shift(mc_stack);
 527   if (xbt_fifo_size(mc_stack) != _sg_mc_max_depth - 1
 528       && current_pair->requests > 0 && current_pair->search_cycle) {
 529     remove_acceptance_pair(current_pair->num);
 530   }
 531   MC_pair_delete(current_pair);
 532
 533   MC_SET_STD_HEAP;
 534
 535 }