src/mc/mc_visited.cpp

   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 #include "mc_process.h"
  15 #include "mc_smx.h"
  16
  17 extern "C" {
  18
  19 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
  20                                 "Logging specific to state equaity detection mechanisms");
  21
  22 xbt_dynar_t visited_pairs;
  23 xbt_dynar_t visited_states;
  24
  25 static int is_exploration_stack_state(mc_visited_state_t state){
  26   xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
  27   while (item) {
  28     if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
  29       ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
  30       return 1;
  31     }
  32     item = xbt_fifo_get_next_item(item);
  33   }
  34   return 0;
  35 }
  36
  37 void visited_state_free(mc_visited_state_t state)
  38 {
  39   if (state) {
  40     if(!is_exploration_stack_state(state)){
  41       MC_free_snapshot(state->system_state);
  42     }
  43     xbt_free(state);
  44   }
  45 }
  46
  47 void visited_state_free_voidp(void *s)
  48 {
  49   visited_state_free((mc_visited_state_t) * (void **) s);
  50 }
  51
  52 /**
  53  * \brief Save the current state
  54  * \return Snapshot of the current state.
  55  */
  56 static mc_visited_state_t visited_state_new()
  57 {
  58   mc_process_t process = &(mc_model_checker->process());
  59   mc_visited_state_t new_state = xbt_new0(s_mc_visited_state_t, 1);
  60   new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
  61     MC_process_get_heap(process)->heaplimit,
  62     MC_process_get_malloc_info(process));
  63
  64   if (MC_process_is_self(&mc_model_checker->process())) {
  65     new_state->nb_processes = xbt_swag_size(simix_global->process_list);
  66   } else {
  67     MC_process_smx_refresh(&mc_model_checker->process());
  68     new_state->nb_processes = xbt_dynar_length(
  69       mc_model_checker->process().smx_process_infos);
  70   }
  71
  72   new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
  73   new_state->num = mc_stats->expanded_states;
  74   new_state->other_num = -1;
  75   return new_state;
  76 }
  77
  78 mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state)
  79 {
  80   mc_process_t process = &(mc_model_checker->process());
  81   mc_visited_pair_t pair = NULL;
  82   pair = xbt_new0(s_mc_visited_pair_t, 1);
  83   pair->graph_state = graph_state;
  84   if(pair->graph_state->system_state == NULL)
  85     pair->graph_state->system_state = MC_take_snapshot(pair_num);
  86   pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
  87     MC_process_get_heap(process)->heaplimit,
  88     MC_process_get_malloc_info(process));
  89   if (MC_process_is_self(&mc_model_checker->process())) {
  90     pair->nb_processes = xbt_swag_size(simix_global->process_list);
  91   } else {
  92     MC_process_smx_refresh(&mc_model_checker->process());
  93     pair->nb_processes = xbt_dynar_length(
  94       mc_model_checker->process().smx_process_infos);
  95   }
  96   pair->automaton_state = automaton_state;
  97   pair->num = pair_num;
  98   pair->other_num = -1;
  99   pair->acceptance_removed = 0;
 100   pair->visited_removed = 0;
 101   pair->acceptance_pair = 0;
 102   pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
 103   unsigned int cursor = 0;
 104   int value;
 105   xbt_dynar_foreach(atomic_propositions, cursor, value)
 106       xbt_dynar_push_as(pair->atomic_propositions, int, value);
 107   return pair;
 108 }
 109
 110 static int is_exploration_stack_pair(mc_visited_pair_t pair){
 111   xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
 112   while (item) {
 113     if (((mc_pair_t)xbt_fifo_get_item_content(item))->num == pair->num){
 114       ((mc_pair_t)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
 115       return 1;
 116     }
 117     item = xbt_fifo_get_next_item(item);
 118   }
 119   return 0;
 120 }
 121
 122 void MC_visited_pair_delete(mc_visited_pair_t p)
 123 {
 124   p->automaton_state = NULL;
 125   if( !is_exploration_stack_pair(p))
 126     MC_state_delete(p->graph_state, 1);
 127   xbt_dynar_free(&(p->atomic_propositions));
 128   xbt_free(p);
 129   p = NULL;
 130 }
 131
 132 /**
 133  *  \brief Find a suitable subrange of candidate duplicates for a given state
 134  *  \param list dynamic array of states/pairs with candidate duplicates of the current state;
 135  *  \param ref current state/pair;
 136  *  \param min (output) index of the beginning of the the subrange
 137  *  \param max (output) index of the enf of the subrange
 138  *
 139  *  Given a suitably ordered array of states/pairs, this function extracts a subrange
 140  *  (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
 141  *  This function uses only fast discriminating criterions and does not use the
 142  *  full state/pair comparison algorithms.
 143  *
 144  *  The states/pairs in list MUST be ordered using a (given) weak order
 145  *  (based on nb_processes and heap_bytes_used).
 146  *  The subrange is the subrange of "equivalence" of the given state/pair.
 147  */
 148 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
 149 {
 150   int cursor = 0, previous_cursor;
 151   int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
 152   void *ref_test;
 153
 154   if (_sg_mc_liveness) {
 155     nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
 156     heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
 157   } else {
 158     nb_processes = ((mc_visited_state_t) ref)->nb_processes;
 159     heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
 160   }
 161
 162   int start = 0;
 163   int end = xbt_dynar_length(list) - 1;
 164
 165   while (start <= end) {
 166     cursor = (start + end) / 2;
 167     if (_sg_mc_liveness) {
 168       ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
 169       nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 170       heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 171     } else {
 172       ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, cursor, mc_visited_state_t);
 173       nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 174       heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 175     }
 176     if (nb_processes_test < nb_processes) {
 177       start = cursor + 1;
 178     } else if (nb_processes_test > nb_processes) {
 179       end = cursor - 1;
 180     } else {
 181       if (heap_bytes_used_test < heap_bytes_used) {
 182         start = cursor + 1;
 183       } else if (heap_bytes_used_test > heap_bytes_used) {
 184         end = cursor - 1;
 185       } else {
 186         *min = *max = cursor;
 187         previous_cursor = cursor - 1;
 188         while (previous_cursor >= 0) {
 189           if (_sg_mc_liveness) {
 190             ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_pair_t);
 191             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 192             heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 193           } else {
 194             ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t);
 195             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 196             heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 197           }
 198           if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
 199             break;
 200           *min = previous_cursor;
 201           previous_cursor--;
 202         }
 203         size_t next_cursor = cursor + 1;
 204         while (next_cursor < xbt_dynar_length(list)) {
 205           if (_sg_mc_liveness) {
 206             ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
 207             nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
 208             heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
 209           } else {
 210             ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t);
 211             nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
 212             heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
 213           }
 214           if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
 215             break;
 216           *max = next_cursor;
 217           next_cursor++;
 218         }
 219         return -1;
 220       }
 221     }
 222   }
 223   return cursor;
 224 }
 225
 226
 227 /**
 228  * \brief Checks whether a given state has already been visited by the algorithm.
 229  */
 230
 231 mc_visited_state_t is_visited_state(mc_state_t graph_state)
 232 {
 233
 234   if (_sg_mc_visited == 0)
 235     return NULL;
 236
 237   int partial_comm = 0;
 238
 239   /* If comm determinism verification, we cannot stop the exploration if some
 240      communications are not finished (at least, data are transfered). These communications
 241      are incomplete and they cannot be analyzed and compared with the initial pattern. */
 242   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
 243     size_t current_process = 1;
 244     while (current_process < MC_smx_get_maxpid()) {
 245       if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
 246         XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
 247         partial_comm = 1;
 248         break;
 249       }
 250       current_process++;
 251     }
 252   }
 253
 254   mc_visited_state_t new_state = visited_state_new();
 255   graph_state->system_state = new_state->system_state;
 256   graph_state->in_visited_states = 1;
 257   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
 258
 259   if (xbt_dynar_is_empty(visited_states)) {
 260
 261     xbt_dynar_push(visited_states, &new_state);
 262     return NULL;
 263
 264   } else {
 265
 266     int min = -1, max = -1, index;
 267     //int res;
 268     mc_visited_state_t state_test;
 269     int cursor;
 270
 271     index = get_search_interval(visited_states, new_state, &min, &max);
 272
 273     if (min != -1 && max != -1) {
 274
 275       // Parallell implementation
 276       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
 277          if(res != -1){
 278          state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
 279          if(state_test->other_num == -1)
 280          new_state->other_num = state_test->num;
 281          else
 282          new_state->other_num = state_test->other_num;
 283          if(dot_output == NULL)
 284          XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 285          else
 286          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);
 287          xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
 288          xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
 289          return new_state->other_num;
 290          } */
 291
 292       if (_sg_mc_safety || (!partial_comm
 293         && initial_global_state->initial_communications_pattern_done)) {
 294
 295         cursor = min;
 296         while (cursor <= max) {
 297           state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
 298           if (snapshot_compare(state_test, new_state) == 0) {
 299             // The state has been visited:
 300
 301             if (state_test->other_num == -1)
 302               new_state->other_num = state_test->num;
 303             else
 304               new_state->other_num = state_test->other_num;
 305             if (dot_output == NULL)
 306               XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
 307             else
 308               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);
 309
 310             /* Replace the old state with the new one (with a bigger num)
 311                (when the max number of visited states is reached,  the oldest
 312                one is removed according to its number (= with the min number) */
 313             xbt_dynar_remove_at(visited_states, cursor, NULL);
 314             xbt_dynar_insert_at(visited_states, cursor, &new_state);
 315             XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
 316
 317             return state_test;
 318           }
 319           cursor++;
 320         }
 321       }
 322
 323       xbt_dynar_insert_at(visited_states, min, &new_state);
 324       XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
 325
 326     } else {
 327
 328       // The state has not been visited: insert the state in the dynamic array.
 329       state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
 330       if (state_test->nb_processes < new_state->nb_processes) {
 331         xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 332       } else {
 333         if (state_test->heap_bytes_used < new_state->heap_bytes_used)
 334           xbt_dynar_insert_at(visited_states, index + 1, &new_state);
 335         else
 336           xbt_dynar_insert_at(visited_states, index, &new_state);
 337       }
 338
 339        XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
 340
 341     }
 342
 343     // We have reached the maximum number of stored states;
 344     if ((ssize_t) xbt_dynar_length(visited_states) > _sg_mc_visited) {
 345
 346       XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
 347
 348       // Find the (index of the) older state (with the smallest num):
 349       int min2 = mc_stats->expanded_states;
 350       unsigned int cursor2 = 0;
 351       unsigned int index2 = 0;
 352       xbt_dynar_foreach(visited_states, cursor2, state_test){
 353         if (state_test->num < min2) {
 354           index2 = cursor2;
 355           min2 = state_test->num;
 356         }
 357       }
 358
 359       // and drop it:
 360       xbt_dynar_remove_at(visited_states, index2, NULL);
 361       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
 362     }
 363
 364     return NULL;
 365   }
 366 }
 367
 368 /**
 369  * \brief Checks whether a given pair has already been visited by the algorithm.
 370  */
 371 int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
 372
 373   if (_sg_mc_visited == 0)
 374     return -1;
 375
 376   mc_visited_pair_t new_visited_pair = NULL;
 377
 378   if (visited_pair == NULL) {
 379     new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
 380   } else {
 381     new_visited_pair = visited_pair;
 382   }
 383
 384   if (xbt_dynar_is_empty(visited_pairs)) {
 385
 386     xbt_dynar_push(visited_pairs, &new_visited_pair);
 387
 388   } else {
 389
 390     int min = -1, max = -1, index;
 391     //int res;
 392     mc_visited_pair_t pair_test;
 393     int cursor;
 394
 395     index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
 396
 397     if (min != -1 && max != -1) {       // Visited pair with same number of processes and same heap bytes used exists
 398       /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
 399          if(res != -1){
 400          pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
 401          if(pair_test->other_num == -1)
 402          pair->other_num = pair_test->num;
 403          else
 404          pair->other_num = pair_test->other_num;
 405          if(dot_output == NULL)
 406          XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
 407          else
 408          XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
 409          xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
 410          xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
 411          pair_test->visited_removed = 1;
 412          if(pair_test->stack_removed && pair_test->visited_removed){
 413          if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
 414          if(pair_test->acceptance_removed){
 415          MC_pair_delete(pair_test);
 416          }
 417          }else{
 418          MC_pair_delete(pair_test);
 419          }
 420          }
 421          return pair->other_num;
 422          } */
 423       cursor = min;
 424       while (cursor <= max) {
 425         pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
 426         if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
 427           if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
 428             if (snapshot_compare(pair_test, new_visited_pair) == 0) {
 429               if (pair_test->other_num == -1)
 430                 new_visited_pair->other_num = pair_test->num;
 431               else
 432                 new_visited_pair->other_num = pair_test->other_num;
 433               if (dot_output == NULL)
 434                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
 435               else
 436                 XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", new_visited_pair->num, pair_test->num, new_visited_pair->other_num);
 437               xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
 438               xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
 439               pair_test->visited_removed = 1;
 440               if (pair_test->acceptance_pair) {
 441                 if (pair_test->acceptance_removed == 1)
 442                   MC_visited_pair_delete(pair_test);
 443               } else {
 444                 MC_visited_pair_delete(pair_test);
 445               }
 446               return new_visited_pair->other_num;
 447             }
 448           }
 449         }
 450         cursor++;
 451       }
 452       xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
 453     } else {
 454       pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
 455       if (pair_test->nb_processes < new_visited_pair->nb_processes) {
 456         xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
 457       } else {
 458         if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
 459           xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
 460         else
 461           xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
 462       }
 463     }
 464
 465     if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
 466       int min2 = mc_stats->expanded_pairs;
 467       unsigned int cursor2 = 0;
 468       unsigned int index2 = 0;
 469       xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
 470         if (pair_test->num < min2) {
 471           index2 = cursor2;
 472           min2 = pair_test->num;
 473         }
 474       }
 475       xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
 476       pair_test->visited_removed = 1;
 477       if (pair_test->acceptance_pair) {
 478         if (pair_test->acceptance_removed)
 479           MC_visited_pair_delete(pair_test);
 480       } else {
 481         MC_visited_pair_delete(pair_test);
 482       }
 483     }
 484
 485   }
 486   return -1;
 487 }
 488
 489 }