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_liveness) {
 108     nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
 109     heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
 110   } else {
 111     nb_processes = ((mc_visited_state_t) ref)->nb_processes;
 112     heap_bytes_used = ((mc_visited_state_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_liveness) {
 121       ref_test =
 122         (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
 123       nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 124       heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 125     } else {
 126       ref_test =
 127         (mc_visited_state_t) xbt_dynar_get_as(list, cursor,
 128                                               mc_visited_state_t);
 129       nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 130       heap_bytes_used_test = ((mc_visited_state_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_liveness) {
 146             ref_test =
 147               (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor,
 148                                                    mc_visited_pair_t);
 149             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 150             heap_bytes_used_test =
 151               ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 152           } else {
 153             ref_test =
 154                 (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor,
 155                                                       mc_visited_state_t);
 156             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 157             heap_bytes_used_test =
 158                 ((mc_visited_state_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_liveness) {
 169             ref_test =
 170                 (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor,
 171                                                      mc_visited_pair_t);
 172             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 173             heap_bytes_used_test =
 174                 ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 175           } else {
 176             ref_test =
 177               (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor,
 178                                                     mc_visited_state_t);
 179             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 180             heap_bytes_used_test =
 181               ((mc_visited_state_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
 207 mc_visited_state_t is_visited_state()
 208 {
 209
 210   if (_sg_mc_visited == 0)
 211     return NULL;
 212
 213   /* If comm determinism verification, we cannot stop the exploration if some
 214      communications are not finished (at least, data are transfered). These communications
 215      are incomplete and they cannot be analyzed and compared with the initial pattern */
 216   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
 217     int current_process = 1;
 218     while (current_process < simix_process_maxpid) {
 219       if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t)))
 220         return NULL;
 221       current_process++;
 222     }
 223   }
 224
 225   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
 226
 227   MC_SET_MC_HEAP;
 228
 229   mc_visited_state_t new_state = visited_state_new();
 230
 231   if (xbt_dynar_is_empty(visited_states)) {
 232
 233     xbt_dynar_push(visited_states, &new_state);
 234
 235     if (!mc_mem_set)
 236       MC_SET_STD_HEAP;
 237
 238     return NULL;
 239
 240   } else {
 241
 242     int min = -1, max = -1, index;
 243     //int res;
 244     mc_visited_state_t state_test;
 245     int cursor;
 246
 247     index = get_search_interval(visited_states, new_state, &min, &max);
 248
 249     if (min != -1 && max != -1) {
 250
 251       // Parallell implementation
 252       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
 253          if(res != -1){
 254          state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
 255          if(state_test->other_num == -1)
 256          new_state->other_num = state_test->num;
 257          else
 258          new_state->other_num = state_test->other_num;
 259          if(dot_output == NULL)
 260          XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 261          else
 262          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);
 263          xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
 264          xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
 265          if(!raw_mem_set)
 266          MC_SET_STD_HEAP;
 267          return new_state->other_num;
 268          } */
 269
 270       cursor = min;
 271       while (cursor <= max) {
 272         state_test =
 273             (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor,
 274                                                   mc_visited_state_t);
 275         if (snapshot_compare(state_test, new_state) == 0) {
 276           // The state has been visited:
 277
 278           if (state_test->other_num == -1)
 279             new_state->other_num = state_test->num;
 280           else
 281             new_state->other_num = state_test->other_num;
 282           if (dot_output == NULL)
 283             XBT_DEBUG("State %d already visited ! (equal to state %d)",
 284                       new_state->num, state_test->num);
 285           else
 286             XBT_DEBUG
 287                 ("State %d already visited ! (equal to state %d (state %d in dot_output))",
 288                  new_state->num, state_test->num, new_state->other_num);
 289
 290           /* Replace the old state with the new one (with a bigger num)
 291              (when the max number of visited states is reached,  the oldest
 292              one is removed according to its number (= with the min number) */
 293           xbt_dynar_remove_at(visited_states, cursor, NULL);
 294           xbt_dynar_insert_at(visited_states, cursor, &new_state);
 295
 296           if (!mc_mem_set)
 297             MC_SET_STD_HEAP;
 298           return state_test;
 299         }
 300         cursor++;
 301       }
 302
 303       // The state has not been visited: insert the state in the dynamic array.
 304       xbt_dynar_insert_at(visited_states, min, &new_state);
 305
 306     } else {
 307
 308       // The state has not been visited: insert the state in the dynamic array.
 309       state_test =
 310           (mc_visited_state_t) xbt_dynar_get_as(visited_states, index,
 311                                                 mc_visited_state_t);
 312       if (state_test->nb_processes < new_state->nb_processes) {
 313         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 314       } else {
 315         if (state_test->heap_bytes_used < new_state->heap_bytes_used)
 316           xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 317         else
 318           xbt_dynar_insert_at(visited_states, index, &new_state);
 319       }
 320
 321     }
 322
 323     // We have reached the maximum number of stored states;
 324     if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
 325
 326       // Find the (index of the) older state (with the smallest num):
 327       int min2 = mc_stats->expanded_states;
 328       unsigned int cursor2 = 0;
 329       unsigned int index2 = 0;
 330       xbt_dynar_foreach(visited_states, cursor2, state_test){
 331         if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
 332           index2 = cursor2;
 333           min2 = state_test->num;
 334         }
 335       }
 336
 337       // and drop it:
 338       xbt_dynar_remove_at(visited_states, index2, NULL);
 339     }
 340
 341     if (!mc_mem_set)
 342       MC_SET_STD_HEAP;
 343
 344     return NULL;
 345
 346   }
 347 }
 348
 349 /**
 350  * \brief Checks whether a given pair has already been visited by the algorithm.
 351  */
 352 int is_visited_pair(mc_visited_pair_t pair, int pair_num,
 353                     xbt_automaton_state_t automaton_state,
 354                     xbt_dynar_t atomic_propositions)
 355 {
 356
 357   if (_sg_mc_visited == 0)
 358     return -1;
 359
 360   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
 361
 362   MC_SET_MC_HEAP;
 363
 364   mc_visited_pair_t new_pair = NULL;
 365
 366   if (pair == NULL) {
 367     new_pair =
 368         MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
 369   } else {
 370     new_pair = pair;
 371   }
 372
 373   if (xbt_dynar_is_empty(visited_pairs)) {
 374
 375     xbt_dynar_push(visited_pairs, &new_pair);
 376
 377   } else {
 378
 379     int min = -1, max = -1, index;
 380     //int res;
 381     mc_visited_pair_t pair_test;
 382     int cursor;
 383
 384     index = get_search_interval(visited_pairs, new_pair, &min, &max);
 385
 386     if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
 387       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
 388          if(res != -1){
 389          pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
 390          if(pair_test->other_num == -1)
 391          pair->other_num = pair_test->num;
 392          else
 393          pair->other_num = pair_test->other_num;
 394          if(dot_output == NULL)
 395          XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
 396          else
 397          XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
 398          xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
 399          xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
 400          pair_test->visited_removed = 1;
 401          if(pair_test->stack_removed && pair_test->visited_removed){
 402          if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
 403          if(pair_test->acceptance_removed){
 404          MC_pair_delete(pair_test);
 405          }
 406          }else{
 407          MC_pair_delete(pair_test);
 408          }
 409          }
 410          if(!raw_mem_set)
 411          MC_SET_STD_HEAP;
 412          return pair->other_num;
 413          } */
 414       cursor = min;
 415       while (cursor <= max) {
 416         pair_test =
 417             (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor,
 418                                                  mc_visited_pair_t);
 419         if (xbt_automaton_state_compare
 420             (pair_test->automaton_state, new_pair->automaton_state) == 0) {
 421           if (xbt_automaton_propositional_symbols_compare_value
 422               (pair_test->atomic_propositions,
 423                new_pair->atomic_propositions) == 0) {
 424             if (snapshot_compare(pair_test, new_pair) == 0) {
 425               if (pair_test->other_num == -1)
 426                 new_pair->other_num = pair_test->num;
 427               else
 428                 new_pair->other_num = pair_test->other_num;
 429               if (dot_output == NULL)
 430                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
 431                           new_pair->num, pair_test->num);
 432               else
 433                 XBT_DEBUG
 434                     ("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
 435                      new_pair->num, pair_test->num, new_pair->other_num);
 436               xbt_dynar_remove_at(visited_pairs, cursor, NULL);
 437               xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
 438               pair_test->visited_removed = 1;
 439               if (pair_test->acceptance_pair) {
 440                 if (pair_test->acceptance_removed == 1)
 441                   MC_visited_pair_delete(pair_test);
 442               } else {
 443                 MC_visited_pair_delete(pair_test);
 444               }
 445               if (!mc_mem_set)
 446                 MC_SET_STD_HEAP;
 447               return new_pair->other_num;
 448             }
 449           }
 450         }
 451         cursor++;
 452       }
 453       xbt_dynar_insert_at(visited_pairs, min, &new_pair);
 454     } else {
 455       pair_test =
 456           (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index,
 457                                                mc_visited_pair_t);
 458       if (pair_test->nb_processes < new_pair->nb_processes) {
 459         xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
 460       } else {
 461         if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
 462           xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
 463         else
 464           xbt_dynar_insert_at(visited_pairs, index, &new_pair);
 465       }
 466     }
 467
 468     if (xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
 469       int min2 = mc_stats->expanded_pairs;
 470       unsigned int cursor2 = 0;
 471       unsigned int index2 = 0;
 472       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
 473         if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
 474           index2 = cursor2;
 475           min2 = pair_test->num;
 476         }
 477       }
 478       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
 479       pair_test->visited_removed = 1;
 480       if (pair_test->acceptance_pair) {
 481         if (pair_test->acceptance_removed)
 482           MC_visited_pair_delete(pair_test);
 483       } else {
 484         MC_visited_pair_delete(pair_test);
 485       }
 486     }
 487
 488   }
 489
 490   if (!mc_mem_set)
 491     MC_SET_STD_HEAP;
 492
 493   return -1;
 494 }