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