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