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