1 /* Copyright (c) 2011-2015. The SimGrid Team.
2 * All rights reserved. */
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. */
13 #include <xbt/automaton.h>
15 #include <xbt/sysdep.h>
16 #include <xbt/dynar.h>
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"
26 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
27 "Logging specific to state equaity detection mechanisms");
32 std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
34 static int is_exploration_stack_state(simgrid::mc::VisitedState* state){
35 xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
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;
41 item = xbt_fifo_get_next_item(item);
47 * \brief Save the current state
48 * \return Snapshot of the current state.
50 VisitedState::VisitedState()
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());
58 mc_model_checker->process().simix_processes().size();
60 this->system_state = simgrid::mc::take_snapshot(mc_stats->expanded_states);
61 this->num = mc_stats->expanded_states;
65 VisitedState::~VisitedState()
67 if(!is_exploration_stack_state(this))
68 delete this->system_state;
71 VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state)
73 simgrid::mc::Process* process = &(mc_model_checker->process());
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());
83 mc_model_checker->process().simix_processes().size();
85 this->automaton_state = automaton_state;
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));
94 unsigned int cursor = 0;
96 xbt_dynar_foreach(atomic_propositions, cursor, value)
97 xbt_dynar_push_as(this->atomic_propositions.get(), int, value);
100 static int is_exploration_stack_pair(simgrid::mc::VisitedPair* pair){
101 xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
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;
107 item = xbt_fifo_get_next_item(item);
112 VisitedPair::~VisitedPair()
114 if( !is_exploration_stack_pair(this))
115 MC_state_delete(this->graph_state, 1);
122 bool some_communications_are_not_finished()
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.");
139 * \brief Checks whether a given state has already been visited by the algorithm.
141 std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(mc_state_t graph_state)
143 if (_sg_mc_visited == 0)
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();
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);
158 auto range = std::equal_range(visited_states.begin(), visited_states.end(),
159 new_state.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
161 if (_sg_mc_safety || (!partial_comm
162 && initial_global_state->initial_communications_pattern_done)) {
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:
169 std::unique_ptr<simgrid::mc::VisitedState> old_state =
170 std::move(visited_state);
172 if (old_state->other_num == -1)
173 new_state->other_num = old_state->num;
175 new_state->other_num = old_state->other_num;
177 if (dot_output == nullptr)
178 XBT_DEBUG("State %d already visited ! (equal to state %d)",
179 new_state->num, old_state->num);
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);
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);
191 visited_state = std::move(new_state);
192 return std::move(old_state);
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));
200 if (visited_states.size() <= (std::size_t) _sg_mc_visited)
203 // We have reached the maximum number of stored states;
205 XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
207 // Find the (index of the) older state (with the smallest num):
208 int min2 = mc_stats->expanded_states;
209 unsigned int index2 = 0;
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) {
216 min2 = visited_states[cursor2]->num;
220 visited_states.erase(visited_states.begin() + index2);
221 XBT_DEBUG("Remove visited state (maximum number of stored states reached)");