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