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