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