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