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   } else {
 114     xbt_die("Both liveness and safety are disabled.");
 115   }
 116
 117   int start = 0;
 118   int end = xbt_dynar_length(list) - 1;
 119
 120   while (start <= end) {
 121     cursor = (start + end) / 2;
 122     if (_sg_mc_safety) {
 123       ref_test =
 124           (mc_visited_state_t) xbt_dynar_get_as(list, cursor,
 125                                                 mc_visited_state_t);
 126       nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 127       heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 128     } else if (_sg_mc_liveness) {
 129       ref_test =
 130           (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
 131       nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 132       heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 133     } else {
 134       nb_processes_test = 0;
 135       heap_bytes_used_test = 0;
 136       xbt_die("Both liveness and safety are disabled.");
 137     }
 138     if (nb_processes_test < nb_processes) {
 139       start = cursor + 1;
 140     } else if (nb_processes_test > nb_processes) {
 141       end = cursor - 1;
 142     } else {
 143       if (heap_bytes_used_test < heap_bytes_used) {
 144         start = cursor + 1;
 145       } else if (heap_bytes_used_test > heap_bytes_used) {
 146         end = cursor - 1;
 147       } else {
 148         *min = *max = cursor;
 149         previous_cursor = cursor - 1;
 150         while (previous_cursor >= 0) {
 151           if (_sg_mc_safety) {
 152             ref_test =
 153                 (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor,
 154                                                       mc_visited_state_t);
 155             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 156             heap_bytes_used_test =
 157                 ((mc_visited_state_t) ref_test)->heap_bytes_used;
 158           } else if (_sg_mc_liveness) {
 159             ref_test =
 160                 (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor,
 161                                                      mc_visited_pair_t);
 162             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 163             heap_bytes_used_test =
 164                 ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 165           }
 166           if (nb_processes_test != nb_processes
 167               || heap_bytes_used_test != heap_bytes_used)
 168             break;
 169           *min = previous_cursor;
 170           previous_cursor--;
 171         }
 172         next_cursor = cursor + 1;
 173         while (next_cursor < xbt_dynar_length(list)) {
 174           if (_sg_mc_safety) {
 175             ref_test =
 176                 (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor,
 177                                                       mc_visited_state_t);
 178             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 179             heap_bytes_used_test =
 180                 ((mc_visited_state_t) ref_test)->heap_bytes_used;
 181           } else if (_sg_mc_liveness) {
 182             ref_test =
 183                 (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor,
 184                                                      mc_visited_pair_t);
 185             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 186             heap_bytes_used_test =
 187                 ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 188           }
 189           if (nb_processes_test != nb_processes
 190               || heap_bytes_used_test != heap_bytes_used)
 191             break;
 192           *max = next_cursor;
 193           next_cursor++;
 194         }
 195         if (!mc_mem_set)
 196           MC_SET_STD_HEAP;
 197         return -1;
 198       }
 199     }
 200   }
 201
 202   if (!mc_mem_set)
 203     MC_SET_STD_HEAP;
 204
 205   return cursor;
 206 }
 207
 208
 209 /**
 210  * \brief Checks whether a given state has already been visited by the algorithm.
 211  */
 212 int is_visited_state()
 213 {
 214
 215   if (_sg_mc_visited == 0)
 216     return -1;
 217
 218   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
 219
 220   MC_SET_MC_HEAP;
 221
 222   mc_visited_state_t new_state = visited_state_new();
 223
 224   if (xbt_dynar_is_empty(visited_states)) {
 225
 226     xbt_dynar_push(visited_states, &new_state);
 227
 228     if (!mc_mem_set)
 229       MC_SET_STD_HEAP;
 230
 231     return -1;
 232
 233   } else {
 234
 235     int min = -1, max = -1, index;
 236     //int res;
 237     mc_visited_state_t state_test;
 238     int cursor;
 239
 240     index = get_search_interval(visited_states, new_state, &min, &max);
 241
 242     if (min != -1 && max != -1) {
 243
 244       // Parallell implementation
 245       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
 246          if(res != -1){
 247          state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
 248          if(state_test->other_num == -1)
 249          new_state->other_num = state_test->num;
 250          else
 251          new_state->other_num = state_test->other_num;
 252          if(dot_output == NULL)
 253          XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 254          else
 255          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);
 256          xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
 257          xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
 258          if(!raw_mem_set)
 259          MC_SET_STD_HEAP;
 260          return new_state->other_num;
 261          } */
 262
 263       cursor = min;
 264       while (cursor <= max) {
 265         state_test =
 266             (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor,
 267                                                   mc_visited_state_t);
 268         if (snapshot_compare(state_test, new_state) == 0) {
 269           // The state has been visited:
 270
 271           if (state_test->other_num == -1)
 272             new_state->other_num = state_test->num;
 273           else
 274             new_state->other_num = state_test->other_num;
 275           if (dot_output == NULL)
 276             XBT_DEBUG("State %d already visited ! (equal to state %d)",
 277                       new_state->num, state_test->num);
 278           else
 279             XBT_DEBUG
 280                 ("State %d already visited ! (equal to state %d (state %d in dot_output))",
 281                  new_state->num, state_test->num, new_state->other_num);
 282
 283           // Replace the old state with the new one (why?):
 284           xbt_dynar_remove_at(visited_states, cursor, NULL);
 285           xbt_dynar_insert_at(visited_states, cursor, &new_state);
 286
 287           if (!mc_mem_set)
 288             MC_SET_STD_HEAP;
 289           return new_state->other_num;
 290         }
 291         cursor++;
 292       }
 293
 294       // The state has not been visited, add it to the list:
 295       xbt_dynar_insert_at(visited_states, min, &new_state);
 296
 297     } else {
 298
 299       // The state has not been visited: insert the state in the dynamic array.
 300       state_test =
 301           (mc_visited_state_t) xbt_dynar_get_as(visited_states, index,
 302                                                 mc_visited_state_t);
 303       if (state_test->nb_processes < new_state->nb_processes) {
 304         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 305       } else {
 306         if (state_test->heap_bytes_used < new_state->heap_bytes_used)
 307           xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 308         else
 309           xbt_dynar_insert_at(visited_states, index, &new_state);
 310       }
 311
 312     }
 313
 314     // We have reached the maximum number of stored states;
 315     if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
 316
 317       // Find the (index of the) older state:
 318       int min2 = mc_stats->expanded_states;
 319       unsigned int cursor2 = 0;
 320       unsigned int index2 = 0;
 321       xbt_dynar_foreach(visited_states, cursor2, state_test){
 322         if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
 323           index2 = cursor2;
 324           min2 = state_test->num;
 325         }
 326       }
 327
 328       // and drop it:
 329       xbt_dynar_remove_at(visited_states, index2, NULL);
 330     }
 331
 332     if (!mc_mem_set)
 333       MC_SET_STD_HEAP;
 334
 335     return -1;
 336
 337   }
 338 }
 339
 340 /**
 341  * \brief Checks whether a given pair has already been visited by the algorithm.
 342  */
 343 int is_visited_pair(mc_visited_pair_t pair, int pair_num,
 344                     xbt_automaton_state_t automaton_state,
 345                     xbt_dynar_t atomic_propositions)
 346 {
 347
 348   if (_sg_mc_visited == 0)
 349     return -1;
 350
 351   int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
 352
 353   MC_SET_MC_HEAP;
 354
 355   mc_visited_pair_t new_pair = NULL;
 356
 357   if (pair == NULL) {
 358     new_pair =
 359         MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
 360   } else {
 361     new_pair = pair;
 362   }
 363
 364   if (xbt_dynar_is_empty(visited_pairs)) {
 365
 366     xbt_dynar_push(visited_pairs, &new_pair);
 367
 368   } else {
 369
 370     int min = -1, max = -1, index;
 371     //int res;
 372     mc_visited_pair_t pair_test;
 373     int cursor;
 374
 375     index = get_search_interval(visited_pairs, new_pair, &min, &max);
 376
 377     if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
 378       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
 379          if(res != -1){
 380          pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
 381          if(pair_test->other_num == -1)
 382          pair->other_num = pair_test->num;
 383          else
 384          pair->other_num = pair_test->other_num;
 385          if(dot_output == NULL)
 386          XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
 387          else
 388          XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
 389          xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
 390          xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
 391          pair_test->visited_removed = 1;
 392          if(pair_test->stack_removed && pair_test->visited_removed){
 393          if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
 394          if(pair_test->acceptance_removed){
 395          MC_pair_delete(pair_test);
 396          }
 397          }else{
 398          MC_pair_delete(pair_test);
 399          }
 400          }
 401          if(!raw_mem_set)
 402          MC_SET_STD_HEAP;
 403          return pair->other_num;
 404          } */
 405       cursor = min;
 406       while (cursor <= max) {
 407         pair_test =
 408             (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor,
 409                                                  mc_visited_pair_t);
 410         //if(pair_test->acceptance_pair == 0){ /* Acceptance pair have been already checked before */
 411         if (xbt_automaton_state_compare
 412             (pair_test->automaton_state, new_pair->automaton_state) == 0) {
 413           if (xbt_automaton_propositional_symbols_compare_value
 414               (pair_test->atomic_propositions,
 415                new_pair->atomic_propositions) == 0) {
 416             if (snapshot_compare(pair_test, new_pair) == 0) {
 417               if (pair_test->other_num == -1)
 418                 new_pair->other_num = pair_test->num;
 419               else
 420                 new_pair->other_num = pair_test->other_num;
 421               if (dot_output == NULL)
 422                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
 423                           new_pair->num, pair_test->num);
 424               else
 425                 XBT_DEBUG
 426                     ("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
 427                      new_pair->num, pair_test->num, new_pair->other_num);
 428               xbt_dynar_remove_at(visited_pairs, cursor, NULL);
 429               xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
 430               pair_test->visited_removed = 1;
 431               if (pair_test->acceptance_pair) {
 432                 if (pair_test->acceptance_removed == 1)
 433                   MC_visited_pair_delete(pair_test);
 434               } else {
 435                 MC_visited_pair_delete(pair_test);
 436               }
 437               if (!mc_mem_set)
 438                 MC_SET_STD_HEAP;
 439               return new_pair->other_num;
 440             }
 441           }
 442           //}
 443         }
 444         cursor++;
 445       }
 446       xbt_dynar_insert_at(visited_pairs, min, &new_pair);
 447     } else {
 448       pair_test =
 449           (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index,
 450                                                mc_visited_pair_t);
 451       if (pair_test->nb_processes < new_pair->nb_processes) {
 452         xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
 453       } else {
 454         if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
 455           xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
 456         else
 457           xbt_dynar_insert_at(visited_pairs, index, &new_pair);
 458       }
 459     }
 460
 461     if (xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
 462       int min2 = mc_stats->expanded_pairs;
 463       unsigned int cursor2 = 0;
 464       unsigned int index2 = 0;
 465       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
 466         if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
 467           index2 = cursor2;
 468           min2 = pair_test->num;
 469         }
 470       }
 471       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
 472       pair_test->visited_removed = 1;
 473       if (pair_test->acceptance_pair) {
 474         if (pair_test->acceptance_removed)
 475           MC_visited_pair_delete(pair_test);
 476       } else {
 477         MC_visited_pair_delete(pair_test);
 478       }
 479     }
 480
 481   }
 482
 483   if (!mc_mem_set)
 484     MC_SET_STD_HEAP;
 485
 486   return -1;
 487 }