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