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