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