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 (with a bigger num)
 278              (when the max number of visited states is reached,  the oldest
 279              one is removed according to its number (= with the min number) */
 280           xbt_dynar_remove_at(visited_states, cursor, NULL);
 281           xbt_dynar_insert_at(visited_states, cursor, &new_state);
 282
 283           if (!mc_mem_set)
 284             MC_SET_STD_HEAP;
 285           return new_state->other_num;
 286         }
 287         cursor++;
 288       }
 289
 290       // The state has not been visited: insert the state in the dynamic array.
 291       xbt_dynar_insert_at(visited_states, min, &new_state);
 292
 293     } else {
 294
 295       // The state has not been visited: insert the state in the dynamic array.
 296       state_test =
 297           (mc_visited_state_t) xbt_dynar_get_as(visited_states, index,
 298                                                 mc_visited_state_t);
 299       if (state_test->nb_processes < new_state->nb_processes) {
 300         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 301       } else {
 302         if (state_test->heap_bytes_used < new_state->heap_bytes_used)
 303           xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 304         else
 305           xbt_dynar_insert_at(visited_states, index, &new_state);
 306       }
 307
 308     }
 309
 310     // We have reached the maximum number of stored states;
 311     if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
 312
 313       // Find the (index of the) older state (with the smallest num):
 314       int min2 = mc_stats->expanded_states;
 315       unsigned int cursor2 = 0;
 316       unsigned int index2 = 0;
 317       xbt_dynar_foreach(visited_states, cursor2, state_test) {
 318         if (state_test->num < min2) {
 319           index2 = cursor2;
 320           min2 = state_test->num;
 321         }
 322       }
 323
 324       // and drop it:
 325       xbt_dynar_remove_at(visited_states, index2, NULL);
 326     }
 327
 328     if (!mc_mem_set)
 329       MC_SET_STD_HEAP;
 330
 331     return -1;
 332
 333   }
 334 }
 335
 336 /**
 337  * \brief Checks whether a given pair has already been visited by the algorithm.
 338  */
 339 int is_visited_pair(mc_visited_pair_t pair, int pair_num,
 340                     xbt_automaton_state_t automaton_state,
 341                     xbt_dynar_t atomic_propositions)
 342 {
 343
 344   if (_sg_mc_visited == 0)
 345     return -1;
 346
 347   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
 348
 349   MC_SET_MC_HEAP;
 350
 351   mc_visited_pair_t new_pair = NULL;
 352
 353   if (pair == NULL) {
 354     new_pair =
 355         MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
 356   } else {
 357     new_pair = pair;
 358   }
 359
 360   if (xbt_dynar_is_empty(visited_pairs)) {
 361
 362     xbt_dynar_push(visited_pairs, &new_pair);
 363
 364   } else {
 365
 366     int min = -1, max = -1, index;
 367     //int res;
 368     mc_visited_pair_t pair_test;
 369     int cursor;
 370
 371     index = get_search_interval(visited_pairs, new_pair, &min, &max);
 372
 373     if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
 374       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
 375          if(res != -1){
 376          pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
 377          if(pair_test->other_num == -1)
 378          pair->other_num = pair_test->num;
 379          else
 380          pair->other_num = pair_test->other_num;
 381          if(dot_output == NULL)
 382          XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
 383          else
 384          XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
 385          xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
 386          xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
 387          pair_test->visited_removed = 1;
 388          if(pair_test->stack_removed && pair_test->visited_removed){
 389          if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
 390          if(pair_test->acceptance_removed){
 391          MC_pair_delete(pair_test);
 392          }
 393          }else{
 394          MC_pair_delete(pair_test);
 395          }
 396          }
 397          if(!raw_mem_set)
 398          MC_SET_STD_HEAP;
 399          return pair->other_num;
 400          } */
 401       cursor = min;
 402       while (cursor <= max) {
 403         pair_test =
 404             (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor,
 405                                                  mc_visited_pair_t);
 406         if (xbt_automaton_state_compare
 407             (pair_test->automaton_state, new_pair->automaton_state) == 0) {
 408           if (xbt_automaton_propositional_symbols_compare_value
 409               (pair_test->atomic_propositions,
 410                new_pair->atomic_propositions) == 0) {
 411             if (snapshot_compare(pair_test, new_pair) == 0) {
 412               if (pair_test->other_num == -1)
 413                 new_pair->other_num = pair_test->num;
 414               else
 415                 new_pair->other_num = pair_test->other_num;
 416               if (dot_output == NULL)
 417                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
 418                           new_pair->num, pair_test->num);
 419               else
 420                 XBT_DEBUG
 421                     ("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
 422                      new_pair->num, pair_test->num, new_pair->other_num);
 423               xbt_dynar_remove_at(visited_pairs, cursor, NULL);
 424               xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
 425               pair_test->visited_removed = 1;
 426               if (pair_test->acceptance_pair) {
 427                 if (pair_test->acceptance_removed == 1)
 428                   MC_visited_pair_delete(pair_test);
 429               } else {
 430                 MC_visited_pair_delete(pair_test);
 431               }
 432               if (!mc_mem_set)
 433                 MC_SET_STD_HEAP;
 434               return new_pair->other_num;
 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 (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 }