src/mc/mc_visited.cpp

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