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