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"
23 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
24 "Logging specific to state equaity detection mechanisms");
29 xbt_dynar_t visited_pairs;
30 xbt_dynar_t visited_states;
32 static int is_exploration_stack_state(simgrid::mc::VisitedState* state){
33 xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
35 if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
36 ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
39 item = xbt_fifo_get_next_item(item);
45 * \brief Save the current state
46 * \return Snapshot of the current state.
48 VisitedState::VisitedState()
50 simgrid::mc::Process* process = &(mc_model_checker->process());
51 this->heap_bytes_used = mmalloc_get_bytes_used_remote(
52 process->get_heap()->heaplimit,
53 process->get_malloc_info());
56 mc_model_checker->process().simix_processes().size();
58 this->num = mc_stats->expanded_states;
62 VisitedState::~VisitedState()
64 if(!is_exploration_stack_state(this))
65 delete this->system_state;
68 VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state)
70 simgrid::mc::Process* process = &(mc_model_checker->process());
72 this->graph_state = graph_state;
73 if(this->graph_state->system_state == nullptr)
74 this->graph_state->system_state = simgrid::mc::take_snapshot(pair_num);
75 this->heap_bytes_used = mmalloc_get_bytes_used_remote(
76 process->get_heap()->heaplimit,
77 process->get_malloc_info());
80 mc_model_checker->process().simix_processes().size();
82 this->automaton_state = automaton_state;
85 this->acceptance_removed = 0;
86 this->visited_removed = 0;
87 this->acceptance_pair = 0;
88 this->atomic_propositions = simgrid::xbt::unique_ptr<s_xbt_dynar_t>(
89 xbt_dynar_new(sizeof(int), nullptr));
91 unsigned int cursor = 0;
93 xbt_dynar_foreach(atomic_propositions, cursor, value)
94 xbt_dynar_push_as(this->atomic_propositions.get(), int, value);
97 static int is_exploration_stack_pair(simgrid::mc::VisitedPair* pair){
98 xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
100 if (((simgrid::mc::Pair*)xbt_fifo_get_item_content(item))->num == pair->num){
101 ((simgrid::mc::Pair*)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
104 item = xbt_fifo_get_next_item(item);
109 VisitedPair::~VisitedPair()
111 if( !is_exploration_stack_pair(this))
112 MC_state_delete(this->graph_state, 1);
119 * \brief Find a suitable subrange of candidate duplicates for a given state
120 * \param list dynamic array of states/pairs with candidate duplicates of the current state;
121 * \param ref current state/pair;
122 * \param min (output) index of the beginning of the the subrange
123 * \param max (output) index of the enf of the subrange
125 * Given a suitably ordered array of states/pairs, this function extracts a subrange
126 * (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
127 * This function uses only fast discriminating criterions and does not use the
128 * full state/pair comparison algorithms.
130 * The states/pairs in list MUST be ordered using a (given) weak order
131 * (based on nb_processes and heap_bytes_used).
132 * The subrange is the subrange of "equivalence" of the given state/pair.
134 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
136 int cursor = 0, previous_cursor;
137 int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
140 if (_sg_mc_liveness) {
141 nb_processes = ((simgrid::mc::VisitedPair*) ref)->nb_processes;
142 heap_bytes_used = ((simgrid::mc::VisitedPair*) ref)->heap_bytes_used;
144 nb_processes = ((simgrid::mc::VisitedState*) ref)->nb_processes;
145 heap_bytes_used = ((simgrid::mc::VisitedState*) ref)->heap_bytes_used;
149 int end = xbt_dynar_length(list) - 1;
151 while (start <= end) {
152 cursor = (start + end) / 2;
153 if (_sg_mc_liveness) {
154 ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, cursor, simgrid::mc::VisitedPair*);
155 nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes;
156 heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used;
158 ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, cursor, simgrid::mc::VisitedState*);
159 nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes;
160 heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used;
162 if (nb_processes_test < nb_processes)
164 else if (nb_processes_test > nb_processes)
166 else if (heap_bytes_used_test < heap_bytes_used)
168 else if (heap_bytes_used_test > heap_bytes_used)
171 *min = *max = cursor;
172 previous_cursor = cursor - 1;
173 while (previous_cursor >= 0) {
174 if (_sg_mc_liveness) {
175 ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, previous_cursor, simgrid::mc::VisitedPair*);
176 nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes;
177 heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used;
179 ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, previous_cursor, simgrid::mc::VisitedState*);
180 nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes;
181 heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used;
183 if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
185 *min = previous_cursor;
188 size_t next_cursor = cursor + 1;
189 while (next_cursor < xbt_dynar_length(list)) {
190 if (_sg_mc_liveness) {
191 ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, next_cursor, simgrid::mc::VisitedPair*);
192 nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes;
193 heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used;
195 ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, next_cursor, simgrid::mc::VisitedState*);
196 nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes;
197 heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used;
199 if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
212 simgrid::mc::VisitedState* state_test, simgrid::mc::VisitedState* new_state, int cursor)
214 if (state_test->other_num == -1)
215 new_state->other_num = state_test->num;
217 new_state->other_num = state_test->other_num;
219 if (dot_output == nullptr)
220 XBT_DEBUG("State %d already visited ! (equal to state %d)",
221 new_state->num, state_test->num);
224 "State %d already visited ! (equal to state %d (state %d in dot_output))",
225 new_state->num, state_test->num, new_state->other_num);
227 /* Replace the old state with the new one (with a bigger num)
228 (when the max number of visited states is reached, the oldest
229 one is removed according to its number (= with the min number) */
230 xbt_dynar_remove_at(simgrid::mc::visited_states, cursor, nullptr);
231 xbt_dynar_insert_at(simgrid::mc::visited_states, cursor, &new_state);
232 XBT_DEBUG("Replace visited state %d with the new visited state %d",
233 state_test->num, new_state->num);
237 bool some_communications_are_not_finished()
239 for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
240 xbt_dynar_t pattern = xbt_dynar_get_as(
241 incomplete_communications_pattern, current_process, xbt_dynar_t);
242 if (!xbt_dynar_is_empty(pattern)) {
243 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
254 * \brief Checks whether a given state has already been visited by the algorithm.
256 simgrid::mc::VisitedState* is_visited_state(mc_state_t graph_state)
258 if (_sg_mc_visited == 0)
261 /* If comm determinism verification, we cannot stop the exploration if some
262 communications are not finished (at least, data are transfered). These communications
263 are incomplete and they cannot be analyzed and compared with the initial pattern. */
264 int partial_comm = (_sg_mc_comms_determinism || _sg_mc_send_determinism) &&
265 some_communications_are_not_finished();
267 simgrid::mc::VisitedState* new_state = new VisitedState();
268 graph_state->system_state = new_state->system_state;
269 graph_state->in_visited_states = 1;
270 XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
272 if (xbt_dynar_is_empty(visited_states)) {
273 xbt_dynar_push(visited_states, &new_state);
277 int min = -1, max = -1, index;
279 index = get_search_interval(visited_states, new_state, &min, &max);
281 if (min != -1 && max != -1) {
283 if (_sg_mc_safety || (!partial_comm
284 && initial_global_state->initial_communications_pattern_done)) {
287 while (cursor <= max) {
288 simgrid::mc::VisitedState* state_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(visited_states, cursor, simgrid::mc::VisitedState*);
289 if (snapshot_compare(state_test, new_state) == 0) {
290 // The state has been visited:
292 replace_state(state_test, new_state, cursor);
299 xbt_dynar_insert_at(visited_states, min, &new_state);
300 XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
304 // The state has not been visited: insert the state in the dynamic array.
305 simgrid::mc::VisitedState* state_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(visited_states, index, simgrid::mc::VisitedState*);
306 if (state_test->nb_processes < new_state->nb_processes)
307 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
308 else if (state_test->heap_bytes_used < new_state->heap_bytes_used)
309 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
311 xbt_dynar_insert_at(visited_states, index, &new_state);
313 XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
317 if ((ssize_t) xbt_dynar_length(visited_states) <= _sg_mc_visited)
320 // We have reached the maximum number of stored states;
322 XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
324 // Find the (index of the) older state (with the smallest num):
325 int min2 = mc_stats->expanded_states;
326 unsigned int cursor2 = 0;
327 unsigned int index2 = 0;
329 simgrid::mc::VisitedState* state_test;
330 xbt_dynar_foreach(visited_states, cursor2, state_test)
331 if (!mc_model_checker->is_important_snapshot(*state_test->system_state)
332 && state_test->num < min2) {
334 min2 = state_test->num;
338 xbt_dynar_remove_at(visited_states, index2, nullptr);
339 XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
345 * \brief Checks whether a given pair has already been visited by the algorithm.
347 int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair) {
349 if (_sg_mc_visited == 0)
352 simgrid::mc::VisitedPair* new_visited_pair = nullptr;
353 if (visited_pair == nullptr)
354 new_visited_pair = new simgrid::mc::VisitedPair(
355 pair->num, pair->automaton_state, pair->atomic_propositions.get(),
358 new_visited_pair = visited_pair;
360 if (xbt_dynar_is_empty(visited_pairs)) {
361 xbt_dynar_push(visited_pairs, &new_visited_pair);
365 int min = -1, max = -1, index;
367 simgrid::mc::VisitedPair* pair_test;
370 index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
372 if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
374 while (cursor <= max) {
375 pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, cursor, simgrid::mc::VisitedPair*);
376 if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
377 if (xbt_automaton_propositional_symbols_compare_value(
378 pair_test->atomic_propositions.get(),
379 new_visited_pair->atomic_propositions.get()) == 0) {
380 if (snapshot_compare(pair_test, new_visited_pair) == 0) {
381 if (pair_test->other_num == -1)
382 new_visited_pair->other_num = pair_test->num;
384 new_visited_pair->other_num = pair_test->other_num;
385 if (dot_output == nullptr)
386 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
388 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);
389 xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
390 xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
391 pair_test->visited_removed = 1;
392 if (!pair_test->acceptance_pair
393 || pair_test->acceptance_removed == 1)
395 return new_visited_pair->other_num;
401 xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
403 pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, index, simgrid::mc::VisitedPair*);
404 if (pair_test->nb_processes < new_visited_pair->nb_processes)
405 xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
406 else if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
407 xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
409 xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
412 if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
413 int min2 = mc_stats->expanded_pairs;
414 unsigned int cursor2 = 0;
415 unsigned int index2 = 0;
416 xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
417 if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
418 && pair_test->num < min2) {
420 min2 = pair_test->num;
423 xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
424 pair_test->visited_removed = 1;
425 if (!pair_test->acceptance_pair || pair_test->acceptance_removed)