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