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