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