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 std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
  32
  33 static int is_exploration_stack_state(simgrid::mc::VisitedState* state){
  34   xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
  35   while (item) {
  36     if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
  37       ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
  38       return 1;
  39     }
  40     item = xbt_fifo_get_next_item(item);
  41   }
  42   return 0;
  43 }
  44
  45 /**
  46  * \brief Save the current state
  47  * \return Snapshot of the current state.
  48  */
  49 VisitedState::VisitedState()
  50 {
  51   simgrid::mc::Process* process = &(mc_model_checker->process());
  52   this->heap_bytes_used = mmalloc_get_bytes_used_remote(
  53     process->get_heap()->heaplimit,
  54     process->get_malloc_info());
  55
  56   this->nb_processes =
  57     mc_model_checker->process().simix_processes().size();
  58
  59   this->system_state = simgrid::mc::take_snapshot(mc_stats->expanded_states);
  60   this->num = mc_stats->expanded_states;
  61   this->other_num = -1;
  62 }
  63
  64 VisitedState::~VisitedState()
  65 {
  66   if(!is_exploration_stack_state(this))
  67     delete this->system_state;
  68 }
  69
  70 VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state)
  71 {
  72   simgrid::mc::Process* process = &(mc_model_checker->process());
  73
  74   this->graph_state = graph_state;
  75   if(this->graph_state->system_state == nullptr)
  76     this->graph_state->system_state = simgrid::mc::take_snapshot(pair_num);
  77   this->heap_bytes_used = mmalloc_get_bytes_used_remote(
  78     process->get_heap()->heaplimit,
  79     process->get_malloc_info());
  80
  81   this->nb_processes =
  82     mc_model_checker->process().simix_processes().size();
  83
  84   this->automaton_state = automaton_state;
  85   this->num = pair_num;
  86   this->other_num = -1;
  87   this->acceptance_removed = 0;
  88   this->visited_removed = 0;
  89   this->acceptance_pair = 0;
  90   this->atomic_propositions = simgrid::xbt::unique_ptr<s_xbt_dynar_t>(
  91     xbt_dynar_new(sizeof(int), nullptr));
  92
  93   unsigned int cursor = 0;
  94   int value;
  95   xbt_dynar_foreach(atomic_propositions, cursor, value)
  96       xbt_dynar_push_as(this->atomic_propositions.get(), int, value);
  97 }
  98
  99 static int is_exploration_stack_pair(simgrid::mc::VisitedPair* pair){
 100   xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
 101   while (item) {
 102     if (((simgrid::mc::Pair*)xbt_fifo_get_item_content(item))->num == pair->num){
 103       ((simgrid::mc::Pair*)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
 104       return 1;
 105     }
 106     item = xbt_fifo_get_next_item(item);
 107   }
 108   return 0;
 109 }
 110
 111 VisitedPair::~VisitedPair()
 112 {
 113   if( !is_exploration_stack_pair(this))
 114     MC_state_delete(this->graph_state, 1);
 115 }
 116
 117 }
 118 }
 119
 120 static
 121 bool some_communications_are_not_finished()
 122 {
 123   for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
 124     xbt_dynar_t pattern = xbt_dynar_get_as(
 125       incomplete_communications_pattern, current_process, xbt_dynar_t);
 126     if (!xbt_dynar_is_empty(pattern)) {
 127       XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
 128       return true;
 129     }
 130   }
 131   return false;
 132 }
 133
 134 namespace simgrid {
 135 namespace mc {
 136
 137 /**
 138  * \brief Checks whether a given state has already been visited by the algorithm.
 139  */
 140 std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state)
 141 {
 142   if (_sg_mc_visited == 0)
 143     return nullptr;
 144
 145   /* If comm determinism verification, we cannot stop the exploration if some
 146      communications are not finished (at least, data are transfered). These communications
 147      are incomplete and they cannot be analyzed and compared with the initial pattern. */
 148   int partial_comm = (_sg_mc_comms_determinism || _sg_mc_send_determinism) &&
 149     some_communications_are_not_finished();
 150
 151   std::unique_ptr<simgrid::mc::VisitedState> new_state =
 152     std::unique_ptr<simgrid::mc::VisitedState>(new VisitedState());
 153   graph_state->system_state = new_state->system_state;
 154   graph_state->in_visited_states = 1;
 155   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
 156
 157   if (visited_states.empty()) {
 158     visited_states.push_back(std::move(new_state));
 159     return nullptr;
 160   }
 161
 162     int min = -1, max = -1, index;
 163
 164     index = simgrid::mc::get_search_interval(
 165       visited_states.data(), visited_states.size(),
 166       new_state.get(), &min, &max);
 167
 168     if (min != -1 && max != -1) {
 169
 170       if (_sg_mc_safety || (!partial_comm
 171         && initial_global_state->initial_communications_pattern_done)) {
 172
 173         int cursor = min;
 174         while (cursor <= max) {
 175           if (snapshot_compare(visited_states[cursor].get(), new_state.get()) == 0) {
 176             // The state has been visited:
 177
 178             std::unique_ptr<simgrid::mc::VisitedState> old_state =
 179               std::move(visited_states[cursor]);
 180
 181             if (old_state->other_num == -1)
 182               new_state->other_num = old_state->num;
 183             else
 184               new_state->other_num = old_state->other_num;
 185
 186             if (dot_output == nullptr)
 187               XBT_DEBUG("State %d already visited ! (equal to state %d)",
 188                 new_state->num, old_state->num);
 189             else
 190               XBT_DEBUG(
 191                 "State %d already visited ! (equal to state %d (state %d in dot_output))",
 192                 new_state->num, old_state->num, new_state->other_num);
 193
 194             /* Replace the old state with the new one (with a bigger num)
 195                (when the max number of visited states is reached,  the oldest
 196                one is removed according to its number (= with the min number) */
 197             XBT_DEBUG("Replace visited state %d with the new visited state %d",
 198               old_state->num, new_state->num);
 199
 200             simgrid::mc::visited_states[cursor] = std::move(new_state);
 201             return std::move(old_state);
 202           }
 203           cursor++;
 204         }
 205       }
 206
 207       XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, (unsigned long) visited_states.size());
 208       visited_states.insert(visited_states.begin() + min, std::move(new_state));
 209
 210     } else {
 211
 212       // The state has not been visited: insert the state in the dynamic array.
 213       visited_states.insert(visited_states.begin() + index, std::move(new_state));
 214       XBT_DEBUG("Insert new visited state %d (total : %lu)",
 215         visited_states[index]->num,
 216         (unsigned long) visited_states.size());
 217
 218     }
 219
 220   if (visited_states.size() <= (std::size_t) _sg_mc_visited)
 221     return nullptr;
 222
 223   // We have reached the maximum number of stored states;
 224
 225       XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
 226
 227       // Find the (index of the) older state (with the smallest num):
 228       int min2 = mc_stats->expanded_states;
 229       unsigned int index2 = 0;
 230
 231       for (std::size_t cursor2 = 0; cursor2 != visited_states.size(); ++cursor2)
 232         if (!mc_model_checker->is_important_snapshot(
 233               *visited_states[cursor2]->system_state)
 234             && visited_states[cursor2]->num < min2) {
 235           index2 = cursor2;
 236           min2 = visited_states[cursor2]->num;
 237         }
 238
 239       // and drop it:
 240       visited_states.erase(visited_states.begin() + index2);
 241       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
 242
 243     return nullptr;
 244 }
 245
 246 }
 247 }