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