src/mc/mc_visited.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 "mc_comm_pattern.h"
  11 #include "mc_safety.h"
  12 #include "mc_liveness.h"
  13 #include "mc_private.h"
  14
  15 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
  16                                 "Logging specific to state equaity detection mechanisms");
  17
  18 xbt_dynar_t visited_pairs;
  19 xbt_dynar_t visited_states;
  20
  21 void visited_state_free(mc_visited_state_t state)
  22 {
  23   if (state) {
  24     MC_free_snapshot(state->system_state);
  25     xbt_free(state);
  26   }
  27 }
  28
  29 void visited_state_free_voidp(void *s)
  30 {
  31   visited_state_free((mc_visited_state_t) * (void **) s);
  32 }
  33
  34 /**
  35  * \brief Save the current state
  36  * \return Snapshot of the current state.
  37  */
  38 static mc_visited_state_t visited_state_new()
  39 {
  40   mc_visited_state_t new_state = NULL;
  41   new_state = xbt_new0(s_mc_visited_state_t, 1);
  42   new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
  43   new_state->nb_processes = xbt_swag_size(simix_global->process_list);
  44   new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
  45   new_state->num = mc_stats->expanded_states;
  46   new_state->other_num = -1;
  47   return new_state;
  48 }
  49
  50
  51 mc_visited_pair_t MC_visited_pair_new(int pair_num,
  52                                       xbt_automaton_state_t automaton_state,
  53                                       xbt_dynar_t atomic_propositions)
  54 {
  55   mc_visited_pair_t pair = NULL;
  56   pair = xbt_new0(s_mc_visited_pair_t, 1);
  57   pair->graph_state = MC_state_new();
  58   pair->graph_state->system_state = MC_take_snapshot(pair_num);
  59   pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
  60   pair->nb_processes = xbt_swag_size(simix_global->process_list);
  61   pair->automaton_state = automaton_state;
  62   pair->num = pair_num;
  63   pair->other_num = -1;
  64   pair->acceptance_removed = 0;
  65   pair->visited_removed = 0;
  66   pair->acceptance_pair = 0;
  67   pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
  68   unsigned int cursor = 0;
  69   int value;
  70   xbt_dynar_foreach(atomic_propositions, cursor, value)
  71       xbt_dynar_push_as(pair->atomic_propositions, int, value);
  72   return pair;
  73 }
  74
  75 void MC_visited_pair_delete(mc_visited_pair_t p)
  76 {
  77   p->automaton_state = NULL;
  78   MC_state_delete(p->graph_state);
  79   xbt_dynar_free(&(p->atomic_propositions));
  80   xbt_free(p);
  81   p = NULL;
  82 }
  83
  84 /**
  85  *  \brief Find a suitable subrange of candidate duplicates for a given state
  86  *  \param list dynamic array of states/pairs with candidate duplicates of the current state;
  87  *  \param ref current state/pair;
  88  *  \param min (output) index of the beginning of the the subrange
  89  *  \param max (output) index of the enf of the subrange
  90  *
  91  *  Given a suitably ordered array of states/pairs, this function extracts a subrange
  92  *  (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
  93  *  This function uses only fast discriminating criterions and does not use the
  94  *  full state/pair comparison algorithms.
  95  *
  96  *  The states/pairs in list MUST be ordered using a (given) weak order
  97  *  (based on nb_processes and heap_bytes_used).
  98  *  The subrange is the subrange of "equivalence" of the given state/pair.
  99  */
 100 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
 101 {
 102
 103   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
 104
 105   MC_SET_MC_HEAP;
 106
 107   int cursor = 0, previous_cursor, next_cursor;
 108   int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
 109   void *ref_test;
 110
 111   if (_sg_mc_liveness) {
 112     nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
 113     heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
 114   } else {
 115     nb_processes = ((mc_visited_state_t) ref)->nb_processes;
 116     heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
 117   }
 118
 119   int start = 0;
 120   int end = xbt_dynar_length(list) - 1;
 121
 122   while (start <= end) {
 123     cursor = (start + end) / 2;
 124     if (_sg_mc_liveness) {
 125       ref_test =
 126         (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
 127       nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 128       heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 129     } else {
 130       ref_test =
 131         (mc_visited_state_t) xbt_dynar_get_as(list, cursor,
 132                                               mc_visited_state_t);
 133       nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 134       heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 135     }
 136     if (nb_processes_test < nb_processes) {
 137       start = cursor + 1;
 138     } else if (nb_processes_test > nb_processes) {
 139       end = cursor - 1;
 140     } else {
 141       if (heap_bytes_used_test < heap_bytes_used) {
 142         start = cursor + 1;
 143       } else if (heap_bytes_used_test > heap_bytes_used) {
 144         end = cursor - 1;
 145       } else {
 146         *min = *max = cursor;
 147         previous_cursor = cursor - 1;
 148         while (previous_cursor >= 0) {
 149           if (_sg_mc_liveness) {
 150             ref_test =
 151               (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor,
 152                                                    mc_visited_pair_t);
 153             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 154             heap_bytes_used_test =
 155               ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 156           } else {
 157             ref_test =
 158                 (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor,
 159                                                       mc_visited_state_t);
 160             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 161             heap_bytes_used_test =
 162                 ((mc_visited_state_t) ref_test)->heap_bytes_used;
 163           }
 164           if (nb_processes_test != nb_processes
 165               || heap_bytes_used_test != heap_bytes_used)
 166             break;
 167           *min = previous_cursor;
 168           previous_cursor--;
 169         }
 170         next_cursor = cursor + 1;
 171         while (next_cursor < xbt_dynar_length(list)) {
 172           if (_sg_mc_liveness) {
 173             ref_test =
 174                 (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor,
 175                                                      mc_visited_pair_t);
 176             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 177             heap_bytes_used_test =
 178                 ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 179           } else {
 180             ref_test =
 181               (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor,
 182                                                     mc_visited_state_t);
 183             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 184             heap_bytes_used_test =
 185               ((mc_visited_state_t) ref_test)->heap_bytes_used;
 186           }
 187           if (nb_processes_test != nb_processes
 188               || heap_bytes_used_test != heap_bytes_used)
 189             break;
 190           *max = next_cursor;
 191           next_cursor++;
 192         }
 193         if (!mc_mem_set)
 194           MC_SET_STD_HEAP;
 195         return -1;
 196       }
 197     }
 198   }
 199
 200   if (!mc_mem_set)
 201     MC_SET_STD_HEAP;
 202
 203   return cursor;
 204 }
 205
 206
 207 /**
 208  * \brief Checks whether a given state has already been visited by the algorithm.
 209  */
 210
 211 mc_visited_state_t is_visited_state(mc_state_t graph_state)
 212 {
 213
 214   if (_sg_mc_visited == 0)
 215     return NULL;
 216
 217   int partial_comm = 0;
 218
 219   /* If comm determinism verification, we cannot stop the exploration if some
 220      communications are not finished (at least, data are transfered). These communications
 221      are incomplete and they cannot be analyzed and compared with the initial pattern. */
 222   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
 223     int current_process = 1;
 224     while (current_process < simix_process_maxpid) {
 225       if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
 226         XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
 227         partial_comm = 1;
 228         break;
 229       }
 230       current_process++;
 231     }
 232   }
 233
 234   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
 235
 236   MC_SET_MC_HEAP;
 237
 238   mc_visited_state_t new_state = visited_state_new();
 239
 240   if (xbt_dynar_is_empty(visited_states)) {
 241
 242     xbt_dynar_push(visited_states, &new_state);
 243
 244     if (!mc_mem_set)
 245       MC_SET_STD_HEAP;
 246
 247     return NULL;
 248
 249   } else {
 250
 251     int min = -1, max = -1, index;
 252     //int res;
 253     mc_visited_state_t state_test;
 254     int cursor;
 255
 256     index = get_search_interval(visited_states, new_state, &min, &max);
 257
 258     if (min != -1 && max != -1) {
 259
 260       // Parallell implementation
 261       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
 262          if(res != -1){
 263          state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
 264          if(state_test->other_num == -1)
 265          new_state->other_num = state_test->num;
 266          else
 267          new_state->other_num = state_test->other_num;
 268          if(dot_output == NULL)
 269          XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 270          else
 271          XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
 272          xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
 273          xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
 274          if(!raw_mem_set)
 275          MC_SET_STD_HEAP;
 276          return new_state->other_num;
 277          } */
 278
 279       cursor = min;
 280       while (cursor <= max) {
 281         state_test =
 282             (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor,
 283                                                   mc_visited_state_t);
 284         if (snapshot_compare(state_test, new_state) == 0) {
 285           // The state has been visited:
 286
 287           if (state_test->other_num == -1)
 288             new_state->other_num = state_test->num;
 289           else
 290             new_state->other_num = state_test->other_num;
 291           if (dot_output == NULL)
 292             XBT_DEBUG("State %d already visited ! (equal to state %d)",
 293                       new_state->num, state_test->num);
 294           else
 295             XBT_DEBUG
 296                 ("State %d already visited ! (equal to state %d (state %d in dot_output))",
 297                  new_state->num, state_test->num, new_state->other_num);
 298
 299           /* Replace the old state with the new one (with a bigger num)
 300              (when the max number of visited states is reached,  the oldest
 301              one is removed according to its number (= with the min number) */
 302           xbt_dynar_remove_at(visited_states, cursor, NULL);
 303           xbt_dynar_insert_at(visited_states, cursor, &new_state);
 304
 305           if (!mc_mem_set)
 306             MC_SET_STD_HEAP;
 307           return state_test;
 308         }
 309         cursor++;
 310       }
 311
 312       // The state has not been visited: insert the state in the dynamic array.
 313       xbt_dynar_insert_at(visited_states, min, &new_state);
 314
 315     } else {
 316
 317       // The state has not been visited: insert the state in the dynamic array.
 318       state_test =
 319           (mc_visited_state_t) xbt_dynar_get_as(visited_states, index,
 320                                                 mc_visited_state_t);
 321       if (state_test->nb_processes < new_state->nb_processes) {
 322         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 323       } else {
 324         if (state_test->heap_bytes_used < new_state->heap_bytes_used)
 325           xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 326         else
 327           xbt_dynar_insert_at(visited_states, index, &new_state);
 328       }
 329
 330     }
 331
 332     // We have reached the maximum number of stored states;
 333     if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
 334
 335       // Find the (index of the) older state (with the smallest num):
 336       int min2 = mc_stats->expanded_states;
 337       unsigned int cursor2 = 0;
 338       unsigned int index2 = 0;
 339       xbt_dynar_foreach(visited_states, cursor2, state_test){
 340         if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
 341           index2 = cursor2;
 342           min2 = state_test->num;
 343         }
 344       }
 345
 346       // and drop it:
 347       xbt_dynar_remove_at(visited_states, index2, NULL);
 348     }
 349
 350     if (!mc_mem_set)
 351       MC_SET_STD_HEAP;
 352
 353     return NULL;
 354
 355   }
 356 }
 357
 358 /**
 359  * \brief Checks whether a given pair has already been visited by the algorithm.
 360  */
 361 int is_visited_pair(mc_visited_pair_t pair, int pair_num,
 362                     xbt_automaton_state_t automaton_state,
 363                     xbt_dynar_t atomic_propositions)
 364 {
 365
 366   if (_sg_mc_visited == 0)
 367     return -1;
 368
 369   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
 370
 371   MC_SET_MC_HEAP;
 372
 373   mc_visited_pair_t new_pair = NULL;
 374
 375   if (pair == NULL) {
 376     new_pair =
 377         MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
 378   } else {
 379     new_pair = pair;
 380   }
 381
 382   if (xbt_dynar_is_empty(visited_pairs)) {
 383
 384     xbt_dynar_push(visited_pairs, &new_pair);
 385
 386   } else {
 387
 388     int min = -1, max = -1, index;
 389     //int res;
 390     mc_visited_pair_t pair_test;
 391     int cursor;
 392
 393     index = get_search_interval(visited_pairs, new_pair, &min, &max);
 394
 395     if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
 396       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
 397          if(res != -1){
 398          pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
 399          if(pair_test->other_num == -1)
 400          pair->other_num = pair_test->num;
 401          else
 402          pair->other_num = pair_test->other_num;
 403          if(dot_output == NULL)
 404          XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
 405          else
 406          XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
 407          xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
 408          xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
 409          pair_test->visited_removed = 1;
 410          if(pair_test->stack_removed && pair_test->visited_removed){
 411          if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
 412          if(pair_test->acceptance_removed){
 413          MC_pair_delete(pair_test);
 414          }
 415          }else{
 416          MC_pair_delete(pair_test);
 417          }
 418          }
 419          if(!raw_mem_set)
 420          MC_SET_STD_HEAP;
 421          return pair->other_num;
 422          } */
 423       cursor = min;
 424       while (cursor <= max) {
 425         pair_test =
 426             (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor,
 427                                                  mc_visited_pair_t);
 428         if (xbt_automaton_state_compare
 429             (pair_test->automaton_state, new_pair->automaton_state) == 0) {
 430           if (xbt_automaton_propositional_symbols_compare_value
 431               (pair_test->atomic_propositions,
 432                new_pair->atomic_propositions) == 0) {
 433             if (snapshot_compare(pair_test, new_pair) == 0) {
 434               if (pair_test->other_num == -1)
 435                 new_pair->other_num = pair_test->num;
 436               else
 437                 new_pair->other_num = pair_test->other_num;
 438               if (dot_output == NULL)
 439                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
 440                           new_pair->num, pair_test->num);
 441               else
 442                 XBT_DEBUG
 443                     ("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
 444                      new_pair->num, pair_test->num, new_pair->other_num);
 445               xbt_dynar_remove_at(visited_pairs, cursor, NULL);
 446               xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
 447               pair_test->visited_removed = 1;
 448               if (pair_test->acceptance_pair) {
 449                 if (pair_test->acceptance_removed == 1)
 450                   MC_visited_pair_delete(pair_test);
 451               } else {
 452                 MC_visited_pair_delete(pair_test);
 453               }
 454               if (!mc_mem_set)
 455                 MC_SET_STD_HEAP;
 456               return new_pair->other_num;
 457             }
 458           }
 459         }
 460         cursor++;
 461       }
 462       xbt_dynar_insert_at(visited_pairs, min, &new_pair);
 463     } else {
 464       pair_test =
 465           (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index,
 466                                                mc_visited_pair_t);
 467       if (pair_test->nb_processes < new_pair->nb_processes) {
 468         xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
 469       } else {
 470         if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
 471           xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
 472         else
 473           xbt_dynar_insert_at(visited_pairs, index, &new_pair);
 474       }
 475     }
 476
 477     if (xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
 478       int min2 = mc_stats->expanded_pairs;
 479       unsigned int cursor2 = 0;
 480       unsigned int index2 = 0;
 481       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
 482         if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
 483           index2 = cursor2;
 484           min2 = pair_test->num;
 485         }
 486       }
 487       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
 488       pair_test->visited_removed = 1;
 489       if (pair_test->acceptance_pair) {
 490         if (pair_test->acceptance_removed)
 491           MC_visited_pair_delete(pair_test);
 492       } else {
 493         MC_visited_pair_delete(pair_test);
 494       }
 495     }
 496
 497   }
 498
 499   if (!mc_mem_set)
 500     MC_SET_STD_HEAP;
 501
 502   return -1;
 503 }