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. */
10 #include <xbt/automaton.h>
12 #include <xbt/sysdep.h>
13 #include <xbt/dynar.h>
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"
25 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
26 "Logging specific to state equaity detection mechanisms");
33 xbt_dynar_t visited_pairs;
34 xbt_dynar_t visited_states;
36 static int is_exploration_stack_state(simgrid::mc::VisitedState* state){
37 xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
39 if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
40 ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
43 item = xbt_fifo_get_next_item(item);
49 * \brief Save the current state
50 * \return Snapshot of the current state.
52 VisitedState::VisitedState()
54 simgrid::mc::Process* process = &(mc_model_checker->process());
55 this->heap_bytes_used = mmalloc_get_bytes_used_remote(
56 process->get_heap()->heaplimit,
57 process->get_malloc_info());
59 MC_process_smx_refresh(&mc_model_checker->process());
61 mc_model_checker->process().smx_process_infos.size();
63 this->num = mc_stats->expanded_states;
67 VisitedState::~VisitedState()
69 if(!is_exploration_stack_state(this))
70 delete this->system_state;
73 VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state)
75 simgrid::mc::Process* process = &(mc_model_checker->process());
77 this->graph_state = graph_state;
78 if(this->graph_state->system_state == nullptr)
79 this->graph_state->system_state = simgrid::mc::take_snapshot(pair_num);
80 this->heap_bytes_used = mmalloc_get_bytes_used_remote(
81 process->get_heap()->heaplimit,
82 process->get_malloc_info());
84 MC_process_smx_refresh(&mc_model_checker->process());
86 mc_model_checker->process().smx_process_infos.size();
88 this->automaton_state = automaton_state;
91 this->acceptance_removed = 0;
92 this->visited_removed = 0;
93 this->acceptance_pair = 0;
94 this->atomic_propositions = simgrid::xbt::unique_ptr<s_xbt_dynar_t>(
95 xbt_dynar_new(sizeof(int), nullptr));
97 unsigned int cursor = 0;
99 xbt_dynar_foreach(atomic_propositions, cursor, value)
100 xbt_dynar_push_as(this->atomic_propositions.get(), int, value);
103 static int is_exploration_stack_pair(simgrid::mc::VisitedPair* pair){
104 xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
106 if (((simgrid::mc::Pair*)xbt_fifo_get_item_content(item))->num == pair->num){
107 ((simgrid::mc::Pair*)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
110 item = xbt_fifo_get_next_item(item);
115 VisitedPair::~VisitedPair()
117 if( !is_exploration_stack_pair(this))
118 MC_state_delete(this->graph_state, 1);
125 * \brief Find a suitable subrange of candidate duplicates for a given state
126 * \param list dynamic array of states/pairs with candidate duplicates of the current state;
127 * \param ref current state/pair;
128 * \param min (output) index of the beginning of the the subrange
129 * \param max (output) index of the enf of the subrange
131 * Given a suitably ordered array of states/pairs, this function extracts a subrange
132 * (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
133 * This function uses only fast discriminating criterions and does not use the
134 * full state/pair comparison algorithms.
136 * The states/pairs in list MUST be ordered using a (given) weak order
137 * (based on nb_processes and heap_bytes_used).
138 * The subrange is the subrange of "equivalence" of the given state/pair.
140 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
142 int cursor = 0, previous_cursor;
143 int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
146 if (_sg_mc_liveness) {
147 nb_processes = ((simgrid::mc::VisitedPair*) ref)->nb_processes;
148 heap_bytes_used = ((simgrid::mc::VisitedPair*) ref)->heap_bytes_used;
150 nb_processes = ((simgrid::mc::VisitedState*) ref)->nb_processes;
151 heap_bytes_used = ((simgrid::mc::VisitedState*) ref)->heap_bytes_used;
155 int end = xbt_dynar_length(list) - 1;
157 while (start <= end) {
158 cursor = (start + end) / 2;
159 if (_sg_mc_liveness) {
160 ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, cursor, simgrid::mc::VisitedPair*);
161 nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes;
162 heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used;
164 ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, cursor, simgrid::mc::VisitedState*);
165 nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes;
166 heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used;
168 if (nb_processes_test < nb_processes)
170 else if (nb_processes_test > nb_processes)
172 else if (heap_bytes_used_test < heap_bytes_used)
174 else if (heap_bytes_used_test > heap_bytes_used)
177 *min = *max = cursor;
178 previous_cursor = cursor - 1;
179 while (previous_cursor >= 0) {
180 if (_sg_mc_liveness) {
181 ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, previous_cursor, simgrid::mc::VisitedPair*);
182 nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes;
183 heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used;
185 ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, previous_cursor, simgrid::mc::VisitedState*);
186 nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes;
187 heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used;
189 if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
191 *min = previous_cursor;
194 size_t next_cursor = cursor + 1;
195 while (next_cursor < xbt_dynar_length(list)) {
196 if (_sg_mc_liveness) {
197 ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, next_cursor, simgrid::mc::VisitedPair*);
198 nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes;
199 heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used;
201 ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, next_cursor, simgrid::mc::VisitedState*);
202 nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes;
203 heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used;
205 if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
218 simgrid::mc::VisitedState* state_test, simgrid::mc::VisitedState* new_state, int cursor)
220 if (state_test->other_num == -1)
221 new_state->other_num = state_test->num;
223 new_state->other_num = state_test->other_num;
225 if (dot_output == nullptr)
226 XBT_DEBUG("State %d already visited ! (equal to state %d)",
227 new_state->num, state_test->num);
230 "State %d already visited ! (equal to state %d (state %d in dot_output))",
231 new_state->num, state_test->num, new_state->other_num);
233 /* Replace the old state with the new one (with a bigger num)
234 (when the max number of visited states is reached, the oldest
235 one is removed according to its number (= with the min number) */
236 xbt_dynar_remove_at(simgrid::mc::visited_states, cursor, nullptr);
237 xbt_dynar_insert_at(simgrid::mc::visited_states, cursor, &new_state);
238 XBT_DEBUG("Replace visited state %d with the new visited state %d",
239 state_test->num, new_state->num);
243 bool some_communications_are_not_finished()
245 for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
246 xbt_dynar_t pattern = xbt_dynar_get_as(
247 incomplete_communications_pattern, current_process, xbt_dynar_t);
248 if (!xbt_dynar_is_empty(pattern)) {
249 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
260 * \brief Checks whether a given state has already been visited by the algorithm.
262 simgrid::mc::VisitedState* is_visited_state(mc_state_t graph_state)
264 if (_sg_mc_visited == 0)
267 /* If comm determinism verification, we cannot stop the exploration if some
268 communications are not finished (at least, data are transfered). These communications
269 are incomplete and they cannot be analyzed and compared with the initial pattern. */
270 int partial_comm = (_sg_mc_comms_determinism || _sg_mc_send_determinism) &&
271 some_communications_are_not_finished();
273 simgrid::mc::VisitedState* new_state = new VisitedState();
274 graph_state->system_state = new_state->system_state;
275 graph_state->in_visited_states = 1;
276 XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
278 if (xbt_dynar_is_empty(visited_states)) {
279 xbt_dynar_push(visited_states, &new_state);
283 int min = -1, max = -1, index;
285 index = get_search_interval(visited_states, new_state, &min, &max);
287 if (min != -1 && max != -1) {
289 if (_sg_mc_safety || (!partial_comm
290 && initial_global_state->initial_communications_pattern_done)) {
293 while (cursor <= max) {
294 simgrid::mc::VisitedState* state_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(visited_states, cursor, simgrid::mc::VisitedState*);
295 if (snapshot_compare(state_test, new_state) == 0) {
296 // The state has been visited:
298 replace_state(state_test, new_state, cursor);
305 xbt_dynar_insert_at(visited_states, min, &new_state);
306 XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
310 // The state has not been visited: insert the state in the dynamic array.
311 simgrid::mc::VisitedState* state_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(visited_states, index, simgrid::mc::VisitedState*);
312 if (state_test->nb_processes < new_state->nb_processes)
313 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
314 else if (state_test->heap_bytes_used < new_state->heap_bytes_used)
315 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
317 xbt_dynar_insert_at(visited_states, index, &new_state);
319 XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
323 if ((ssize_t) xbt_dynar_length(visited_states) <= _sg_mc_visited)
326 // We have reached the maximum number of stored states;
328 XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
330 // Find the (index of the) older state (with the smallest num):
331 int min2 = mc_stats->expanded_states;
332 unsigned int cursor2 = 0;
333 unsigned int index2 = 0;
335 simgrid::mc::VisitedState* state_test;
336 xbt_dynar_foreach(visited_states, cursor2, state_test)
337 if (!mc_model_checker->is_important_snapshot(*state_test->system_state)
338 && state_test->num < min2) {
340 min2 = state_test->num;
344 xbt_dynar_remove_at(visited_states, index2, nullptr);
345 XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
351 * \brief Checks whether a given pair has already been visited by the algorithm.
353 int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair) {
355 if (_sg_mc_visited == 0)
358 simgrid::mc::VisitedPair* new_visited_pair = nullptr;
359 if (visited_pair == nullptr)
360 new_visited_pair = new simgrid::mc::VisitedPair(
361 pair->num, pair->automaton_state, pair->atomic_propositions.get(),
364 new_visited_pair = visited_pair;
366 if (xbt_dynar_is_empty(visited_pairs)) {
367 xbt_dynar_push(visited_pairs, &new_visited_pair);
371 int min = -1, max = -1, index;
373 simgrid::mc::VisitedPair* pair_test;
376 index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
378 if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
380 while (cursor <= max) {
381 pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, cursor, simgrid::mc::VisitedPair*);
382 if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
383 if (xbt_automaton_propositional_symbols_compare_value(
384 pair_test->atomic_propositions.get(),
385 new_visited_pair->atomic_propositions.get()) == 0) {
386 if (snapshot_compare(pair_test, new_visited_pair) == 0) {
387 if (pair_test->other_num == -1)
388 new_visited_pair->other_num = pair_test->num;
390 new_visited_pair->other_num = pair_test->other_num;
391 if (dot_output == nullptr)
392 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
394 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);
395 xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
396 xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
397 pair_test->visited_removed = 1;
398 if (!pair_test->acceptance_pair
399 || pair_test->acceptance_removed == 1)
401 return new_visited_pair->other_num;
407 xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
409 pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, index, simgrid::mc::VisitedPair*);
410 if (pair_test->nb_processes < new_visited_pair->nb_processes)
411 xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
412 else if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
413 xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
415 xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
418 if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
419 int min2 = mc_stats->expanded_pairs;
420 unsigned int cursor2 = 0;
421 unsigned int index2 = 0;
422 xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
423 if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
424 && pair_test->num < min2) {
426 min2 = pair_test->num;
429 xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
430 pair_test->visited_removed = 1;
431 if (!pair_test->acceptance_pair || pair_test->acceptance_removed)