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