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_process_t process = &(mc_model_checker->process);
  41   mc_visited_state_t new_state = NULL;
  42   new_state = xbt_new0(s_mc_visited_state_t, 1);
  43   new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
  44     MC_process_get_heap(process)->heaplimit,
  45     MC_process_get_malloc_info(process));
  46   new_state->nb_processes = xbt_swag_size(simix_global->process_list);
  47   new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
  48   new_state->num = mc_stats->expanded_states;
  49   new_state->other_num = -1;
  50   return new_state;
  51 }
  52
  53
  54 mc_visited_pair_t MC_visited_pair_new(int pair_num,
  55                                       xbt_automaton_state_t automaton_state,
  56                                       xbt_dynar_t atomic_propositions)
  57 {
  58   mc_process_t process = &(mc_model_checker->process);
  59   mc_visited_pair_t pair = NULL;
  60   pair = xbt_new0(s_mc_visited_pair_t, 1);
  61   pair->graph_state = MC_state_new();
  62   pair->graph_state->system_state = MC_take_snapshot(pair_num);
  63   pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
  64     MC_process_get_heap(process)->heaplimit,
  65     MC_process_get_malloc_info(process));
  66   pair->nb_processes = xbt_swag_size(simix_global->process_list);
  67   pair->automaton_state = automaton_state;
  68   pair->num = pair_num;
  69   pair->other_num = -1;
  70   pair->acceptance_removed = 0;
  71   pair->visited_removed = 0;
  72   pair->acceptance_pair = 0;
  73   pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
  74   unsigned int cursor = 0;
  75   int value;
  76   xbt_dynar_foreach(atomic_propositions, cursor, value)
  77       xbt_dynar_push_as(pair->atomic_propositions, int, value);
  78   return pair;
  79 }
  80
  81 void MC_visited_pair_delete(mc_visited_pair_t p)
  82 {
  83   p->automaton_state = NULL;
  84   MC_state_delete(p->graph_state);
  85   xbt_dynar_free(&(p->atomic_propositions));
  86   xbt_free(p);
  87   p = NULL;
  88 }
  89
  90 /**
  91  *  \brief Find a suitable subrange of candidate duplicates for a given state
  92  *  \param list dynamic array of states/pairs with candidate duplicates of the current state;
  93  *  \param ref current state/pair;
  94  *  \param min (output) index of the beginning of the the subrange
  95  *  \param max (output) index of the enf of the subrange
  96  *
  97  *  Given a suitably ordered array of states/pairs, this function extracts a subrange
  98  *  (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
  99  *  This function uses only fast discriminating criterions and does not use the
 100  *  full state/pair comparison algorithms.
 101  *
 102  *  The states/pairs in list MUST be ordered using a (given) weak order
 103  *  (based on nb_processes and heap_bytes_used).
 104  *  The subrange is the subrange of "equivalence" of the given state/pair.
 105  */
 106 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
 107 {
 108
 109   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 110
 111   int cursor = 0, previous_cursor, next_cursor;
 112   int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
 113   void *ref_test;
 114
 115   if (_sg_mc_liveness) {
 116     nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
 117     heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
 118   } else {
 119     nb_processes = ((mc_visited_state_t) ref)->nb_processes;
 120     heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
 121   }
 122
 123   int start = 0;
 124   int end = xbt_dynar_length(list) - 1;
 125
 126   while (start <= end) {
 127     cursor = (start + end) / 2;
 128     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       ref_test =
 135         (mc_visited_state_t) xbt_dynar_get_as(list, cursor,
 136                                               mc_visited_state_t);
 137       nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 138       heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 139     }
 140     if (nb_processes_test < nb_processes) {
 141       start = cursor + 1;
 142     } else if (nb_processes_test > nb_processes) {
 143       end = cursor - 1;
 144     } else {
 145       if (heap_bytes_used_test < heap_bytes_used) {
 146         start = cursor + 1;
 147       } else if (heap_bytes_used_test > heap_bytes_used) {
 148         end = cursor - 1;
 149       } else {
 150         *min = *max = cursor;
 151         previous_cursor = cursor - 1;
 152         while (previous_cursor >= 0) {
 153           if (_sg_mc_liveness) {
 154             ref_test =
 155               (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor,
 156                                                    mc_visited_pair_t);
 157             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 158             heap_bytes_used_test =
 159               ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 160           } else {
 161             ref_test =
 162                 (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor,
 163                                                       mc_visited_state_t);
 164             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 165             heap_bytes_used_test =
 166                 ((mc_visited_state_t) ref_test)->heap_bytes_used;
 167           }
 168           if (nb_processes_test != nb_processes
 169               || heap_bytes_used_test != heap_bytes_used)
 170             break;
 171           *min = previous_cursor;
 172           previous_cursor--;
 173         }
 174         next_cursor = cursor + 1;
 175         while (next_cursor < xbt_dynar_length(list)) {
 176           if (_sg_mc_liveness) {
 177             ref_test =
 178                 (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor,
 179                                                      mc_visited_pair_t);
 180             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 181             heap_bytes_used_test =
 182                 ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 183           } else {
 184             ref_test =
 185               (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor,
 186                                                     mc_visited_state_t);
 187             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 188             heap_bytes_used_test =
 189               ((mc_visited_state_t) ref_test)->heap_bytes_used;
 190           }
 191           if (nb_processes_test != nb_processes
 192               || heap_bytes_used_test != heap_bytes_used)
 193             break;
 194           *max = next_cursor;
 195           next_cursor++;
 196         }
 197         mmalloc_set_current_heap(heap);
 198         return -1;
 199       }
 200     }
 201   }
 202
 203   mmalloc_set_current_heap(heap);
 204   return cursor;
 205 }
 206
 207
 208 /**
 209  * \brief Checks whether a given state has already been visited by the algorithm.
 210  */
 211
 212 mc_visited_state_t is_visited_state()
 213 {
 214
 215   if (_sg_mc_visited == 0)
 216     return NULL;
 217
 218   /* If comm determinism verification, we cannot stop the exploration if some
 219      communications are not finished (at least, data are transfered). These communications
 220      are incomplete and they cannot be analyzed and compared with the initial pattern */
 221   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
 222     int current_process = 1;
 223     while (current_process < simix_process_maxpid) {
 224       if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t)))
 225         return NULL;
 226       current_process++;
 227     }
 228   }
 229
 230   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 231
 232   mc_visited_state_t new_state = visited_state_new();
 233
 234   if (xbt_dynar_is_empty(visited_states)) {
 235
 236     xbt_dynar_push(visited_states, &new_state);
 237     mmalloc_set_current_heap(heap);
 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           mmalloc_set_current_heap(heap);
 297           return state_test;
 298         }
 299         cursor++;
 300       }
 301
 302       // The state has not been visited: insert the state in the dynamic array.
 303       xbt_dynar_insert_at(visited_states, min, &new_state);
 304
 305     } else {
 306
 307       // The state has not been visited: insert the state in the dynamic array.
 308       state_test =
 309           (mc_visited_state_t) xbt_dynar_get_as(visited_states, index,
 310                                                 mc_visited_state_t);
 311       if (state_test->nb_processes < new_state->nb_processes) {
 312         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 313       } else {
 314         if (state_test->heap_bytes_used < new_state->heap_bytes_used)
 315           xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 316         else
 317           xbt_dynar_insert_at(visited_states, index, &new_state);
 318       }
 319
 320     }
 321
 322     // We have reached the maximum number of stored states;
 323     if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
 324
 325       // Find the (index of the) older state (with the smallest num):
 326       int min2 = mc_stats->expanded_states;
 327       unsigned int cursor2 = 0;
 328       unsigned int index2 = 0;
 329       xbt_dynar_foreach(visited_states, cursor2, state_test){
 330         if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
 331           index2 = cursor2;
 332           min2 = state_test->num;
 333         }
 334       }
 335
 336       // and drop it:
 337       xbt_dynar_remove_at(visited_states, index2, NULL);
 338     }
 339
 340     mmalloc_set_current_heap(heap);
 341     return NULL;
 342   }
 343 }
 344
 345 /**
 346  * \brief Checks whether a given pair has already been visited by the algorithm.
 347  */
 348 int is_visited_pair(mc_visited_pair_t pair, int pair_num,
 349                     xbt_automaton_state_t automaton_state,
 350                     xbt_dynar_t atomic_propositions)
 351 {
 352
 353   if (_sg_mc_visited == 0)
 354     return -1;
 355
 356   xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
 357
 358   mc_visited_pair_t new_pair = NULL;
 359
 360   if (pair == NULL) {
 361     new_pair =
 362         MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
 363   } else {
 364     new_pair = pair;
 365   }
 366
 367   if (xbt_dynar_is_empty(visited_pairs)) {
 368
 369     xbt_dynar_push(visited_pairs, &new_pair);
 370
 371   } else {
 372
 373     int min = -1, max = -1, index;
 374     //int res;
 375     mc_visited_pair_t pair_test;
 376     int cursor;
 377
 378     index = get_search_interval(visited_pairs, new_pair, &min, &max);
 379
 380     if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
 381       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
 382          if(res != -1){
 383          pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
 384          if(pair_test->other_num == -1)
 385          pair->other_num = pair_test->num;
 386          else
 387          pair->other_num = pair_test->other_num;
 388          if(dot_output == NULL)
 389          XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
 390          else
 391          XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
 392          xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
 393          xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
 394          pair_test->visited_removed = 1;
 395          if(pair_test->stack_removed && pair_test->visited_removed){
 396          if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
 397          if(pair_test->acceptance_removed){
 398          MC_pair_delete(pair_test);
 399          }
 400          }else{
 401          MC_pair_delete(pair_test);
 402          }
 403          }
 404          if(!raw_mem_set)
 405          MC_SET_STD_HEAP;
 406          return pair->other_num;
 407          } */
 408       cursor = min;
 409       while (cursor <= max) {
 410         pair_test =
 411             (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor,
 412                                                  mc_visited_pair_t);
 413         if (xbt_automaton_state_compare
 414             (pair_test->automaton_state, new_pair->automaton_state) == 0) {
 415           if (xbt_automaton_propositional_symbols_compare_value
 416               (pair_test->atomic_propositions,
 417                new_pair->atomic_propositions) == 0) {
 418             if (snapshot_compare(pair_test, new_pair) == 0) {
 419               if (pair_test->other_num == -1)
 420                 new_pair->other_num = pair_test->num;
 421               else
 422                 new_pair->other_num = pair_test->other_num;
 423               if (dot_output == NULL)
 424                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
 425                           new_pair->num, pair_test->num);
 426               else
 427                 XBT_DEBUG
 428                     ("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
 429                      new_pair->num, pair_test->num, new_pair->other_num);
 430               xbt_dynar_remove_at(visited_pairs, cursor, NULL);
 431               xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
 432               pair_test->visited_removed = 1;
 433               if (pair_test->acceptance_pair) {
 434                 if (pair_test->acceptance_removed == 1)
 435                   MC_visited_pair_delete(pair_test);
 436               } else {
 437                 MC_visited_pair_delete(pair_test);
 438               }
 439               mmalloc_set_current_heap(heap);
 440               return new_pair->other_num;
 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   mmalloc_set_current_heap(heap);
 484   return -1;
 485 }