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 #include <algorithm>
  12
  13 #include <xbt/automaton.h>
  14 #include <xbt/log.h>
  15 #include <xbt/sysdep.h>
  16 #include <xbt/dynar.h>
  17 #include <xbt/fifo.h>
  18
  19 #include "src/mc/mc_comm_pattern.h"
  20 #include "src/mc/mc_safety.h"
  21 #include "src/mc/mc_liveness.h"
  22 #include "src/mc/mc_private.h"
  23 #include "src/mc/Process.hpp"
  24 #include "src/mc/mc_smx.h"
  25
  26 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
  27                                 "Logging specific to state equaity detection mechanisms");
  28
  29 namespace simgrid {
  30 namespace mc {
  31
  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 static
 122 bool some_communications_are_not_finished()
 123 {
 124   for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
 125     xbt_dynar_t pattern = xbt_dynar_get_as(
 126       incomplete_communications_pattern, current_process, xbt_dynar_t);
 127     if (!xbt_dynar_is_empty(pattern)) {
 128       XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
 129       return true;
 130     }
 131   }
 132   return false;
 133 }
 134
 135 namespace simgrid {
 136 namespace mc {
 137
 138 /**
 139  * \brief Checks whether a given state has already been visited by the algorithm.
 140  */
 141 std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state)
 142 {
 143   if (_sg_mc_visited == 0)
 144     return nullptr;
 145
 146   /* If comm determinism verification, we cannot stop the exploration if some
 147      communications are not finished (at least, data are transfered). These communications
 148      are incomplete and they cannot be analyzed and compared with the initial pattern. */
 149   int partial_comm = (_sg_mc_comms_determinism || _sg_mc_send_determinism) &&
 150     some_communications_are_not_finished();
 151
 152   std::unique_ptr<simgrid::mc::VisitedState> new_state =
 153     std::unique_ptr<simgrid::mc::VisitedState>(new VisitedState());
 154   graph_state->system_state = new_state->system_state;
 155   graph_state->in_visited_states = 1;
 156   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
 157
 158   auto range = std::equal_range(visited_states.begin(), visited_states.end(),
 159     new_state.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
 160
 161       if (_sg_mc_safety || (!partial_comm
 162         && initial_global_state->initial_communications_pattern_done)) {
 163
 164         for (auto i = range.first; i != range.second; ++i) {
 165           auto& visited_state = *i;
 166           if (snapshot_compare(visited_state.get(), new_state.get()) == 0) {
 167             // The state has been visited:
 168
 169             std::unique_ptr<simgrid::mc::VisitedState> old_state =
 170               std::move(visited_state);
 171
 172             if (old_state->other_num == -1)
 173               new_state->other_num = old_state->num;
 174             else
 175               new_state->other_num = old_state->other_num;
 176
 177             if (dot_output == nullptr)
 178               XBT_DEBUG("State %d already visited ! (equal to state %d)",
 179                 new_state->num, old_state->num);
 180             else
 181               XBT_DEBUG(
 182                 "State %d already visited ! (equal to state %d (state %d in dot_output))",
 183                 new_state->num, old_state->num, new_state->other_num);
 184
 185             /* Replace the old state with the new one (with a bigger num)
 186                (when the max number of visited states is reached,  the oldest
 187                one is removed according to its number (= with the min number) */
 188             XBT_DEBUG("Replace visited state %d with the new visited state %d",
 189               old_state->num, new_state->num);
 190
 191             visited_state = std::move(new_state);
 192             return std::move(old_state);
 193           }
 194         }
 195       }
 196
 197   XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, (unsigned long) visited_states.size());
 198   visited_states.insert(range.first, std::move(new_state));
 199
 200   if (visited_states.size() <= (std::size_t) _sg_mc_visited)
 201     return nullptr;
 202
 203   // We have reached the maximum number of stored states;
 204
 205       XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
 206
 207       // Find the (index of the) older state (with the smallest num):
 208       int min2 = mc_stats->expanded_states;
 209       unsigned int index2 = 0;
 210
 211       for (std::size_t cursor2 = 0; cursor2 != visited_states.size(); ++cursor2)
 212         if (!mc_model_checker->is_important_snapshot(
 213               *visited_states[cursor2]->system_state)
 214             && visited_states[cursor2]->num < min2) {
 215           index2 = cursor2;
 216           min2 = visited_states[cursor2]->num;
 217         }
 218
 219       // and drop it:
 220       visited_states.erase(visited_states.begin() + index2);
 221       XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
 222
 223     return nullptr;
 224 }
 225
 226 }
 227 }