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");
28 xbt_dynar_t visited_pairs;
29 xbt_dynar_t visited_states;
31 static int is_exploration_stack_state(mc_visited_state_t state){
32 xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
34 if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
35 ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
38 item = xbt_fifo_get_next_item(item);
43 void visited_state_free(mc_visited_state_t state)
47 if(!is_exploration_stack_state(state))
48 delete state->system_state;
52 void visited_state_free_voidp(void *s)
54 visited_state_free((mc_visited_state_t) * (void **) s);
58 * \brief Save the current state
59 * \return Snapshot of the current state.
61 static mc_visited_state_t visited_state_new()
63 simgrid::mc::Process* process = &(mc_model_checker->process());
64 mc_visited_state_t new_state = xbt_new0(s_mc_visited_state_t, 1);
65 new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
66 process->get_heap()->heaplimit,
67 process->get_malloc_info());
69 MC_process_smx_refresh(&mc_model_checker->process());
70 new_state->nb_processes =
71 mc_model_checker->process().smx_process_infos.size();
73 new_state->system_state = simgrid::mc::take_snapshot(mc_stats->expanded_states);
74 new_state->num = mc_stats->expanded_states;
75 new_state->other_num = -1;
79 mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state)
81 simgrid::mc::Process* process = &(mc_model_checker->process());
82 mc_visited_pair_t pair = nullptr;
83 pair = xbt_new0(s_mc_visited_pair_t, 1);
84 pair->graph_state = graph_state;
85 if(pair->graph_state->system_state == nullptr)
86 pair->graph_state->system_state = simgrid::mc::take_snapshot(pair_num);
87 pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
88 process->get_heap()->heaplimit,
89 process->get_malloc_info());
91 MC_process_smx_refresh(&mc_model_checker->process());
93 mc_model_checker->process().smx_process_infos.size();
95 pair->automaton_state = automaton_state;
98 pair->acceptance_removed = 0;
99 pair->visited_removed = 0;
100 pair->acceptance_pair = 0;
101 pair->atomic_propositions = xbt_dynar_new(sizeof(int), nullptr);
102 unsigned int cursor = 0;
104 xbt_dynar_foreach(atomic_propositions, cursor, value)
105 xbt_dynar_push_as(pair->atomic_propositions, int, value);
109 static int is_exploration_stack_pair(mc_visited_pair_t pair){
110 xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
112 if (((mc_pair_t)xbt_fifo_get_item_content(item))->num == pair->num){
113 ((mc_pair_t)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
116 item = xbt_fifo_get_next_item(item);
121 void MC_visited_pair_delete(mc_visited_pair_t p)
123 p->automaton_state = nullptr;
124 if( !is_exploration_stack_pair(p))
125 MC_state_delete(p->graph_state, 1);
126 xbt_dynar_free(&(p->atomic_propositions));
132 * \brief Find a suitable subrange of candidate duplicates for a given state
133 * \param list dynamic array of states/pairs with candidate duplicates of the current state;
134 * \param ref current state/pair;
135 * \param min (output) index of the beginning of the the subrange
136 * \param max (output) index of the enf of the subrange
138 * Given a suitably ordered array of states/pairs, this function extracts a subrange
139 * (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
140 * This function uses only fast discriminating criterions and does not use the
141 * full state/pair comparison algorithms.
143 * The states/pairs in list MUST be ordered using a (given) weak order
144 * (based on nb_processes and heap_bytes_used).
145 * The subrange is the subrange of "equivalence" of the given state/pair.
147 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
149 int cursor = 0, previous_cursor;
150 int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
153 if (_sg_mc_liveness) {
154 nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
155 heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
157 nb_processes = ((mc_visited_state_t) ref)->nb_processes;
158 heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
162 int end = xbt_dynar_length(list) - 1;
164 while (start <= end) {
165 cursor = (start + end) / 2;
166 if (_sg_mc_liveness) {
167 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
168 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
169 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
171 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, cursor, mc_visited_state_t);
172 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
173 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
175 if (nb_processes_test < nb_processes)
177 else if (nb_processes_test > nb_processes)
179 else if (heap_bytes_used_test < heap_bytes_used)
181 else if (heap_bytes_used_test > heap_bytes_used)
184 *min = *max = cursor;
185 previous_cursor = cursor - 1;
186 while (previous_cursor >= 0) {
187 if (_sg_mc_liveness) {
188 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_pair_t);
189 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
190 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
192 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t);
193 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
194 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
196 if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
198 *min = previous_cursor;
201 size_t next_cursor = cursor + 1;
202 while (next_cursor < xbt_dynar_length(list)) {
203 if (_sg_mc_liveness) {
204 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
205 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
206 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
208 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t);
209 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
210 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
212 if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
225 mc_visited_state_t state_test, mc_visited_state_t new_state, int cursor)
227 if (state_test->other_num == -1)
228 new_state->other_num = state_test->num;
230 new_state->other_num = state_test->other_num;
232 if (dot_output == nullptr)
233 XBT_DEBUG("State %d already visited ! (equal to state %d)",
234 new_state->num, state_test->num);
237 "State %d already visited ! (equal to state %d (state %d in dot_output))",
238 new_state->num, state_test->num, new_state->other_num);
240 /* Replace the old state with the new one (with a bigger num)
241 (when the max number of visited states is reached, the oldest
242 one is removed according to its number (= with the min number) */
243 xbt_dynar_remove_at(visited_states, cursor, nullptr);
244 xbt_dynar_insert_at(visited_states, cursor, &new_state);
245 XBT_DEBUG("Replace visited state %d with the new visited state %d",
246 state_test->num, new_state->num);
250 bool some_dommunications_are_not_finished()
252 for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
253 xbt_dynar_t pattern = xbt_dynar_get_as(
254 incomplete_communications_pattern, current_process, xbt_dynar_t);
255 if (!xbt_dynar_is_empty(pattern)) {
256 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
264 * \brief Checks whether a given state has already been visited by the algorithm.
267 mc_visited_state_t is_visited_state(mc_state_t graph_state)
269 if (_sg_mc_visited == 0)
272 /* If comm determinism verification, we cannot stop the exploration if some
273 communications are not finished (at least, data are transfered). These communications
274 are incomplete and they cannot be analyzed and compared with the initial pattern. */
275 int partial_comm = (_sg_mc_comms_determinism || _sg_mc_send_determinism) &&
276 some_dommunications_are_not_finished();
278 mc_visited_state_t new_state = visited_state_new();
279 graph_state->system_state = new_state->system_state;
280 graph_state->in_visited_states = 1;
281 XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
283 if (xbt_dynar_is_empty(visited_states)) {
284 xbt_dynar_push(visited_states, &new_state);
288 int min = -1, max = -1, index;
290 index = get_search_interval(visited_states, new_state, &min, &max);
292 if (min != -1 && max != -1) {
294 // Parallell implementation
295 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
297 mc_visited_state_t state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
298 if(state_test->other_num == -1)
299 new_state->other_num = state_test->num;
301 new_state->other_num = state_test->other_num;
302 if(dot_output == nullptr)
303 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
305 XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", new_state->num, state_test->num, new_state->other_num);
306 xbt_dynar_remove_at(visited_states, (min + res) - 1, nullptr);
307 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
308 return new_state->other_num;
311 if (_sg_mc_safety || (!partial_comm
312 && initial_global_state->initial_communications_pattern_done)) {
315 while (cursor <= max) {
316 mc_visited_state_t state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
317 if (snapshot_compare(state_test, new_state) == 0) {
318 // The state has been visited:
320 replace_state(state_test, new_state, cursor);
327 xbt_dynar_insert_at(visited_states, min, &new_state);
328 XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
332 // The state has not been visited: insert the state in the dynamic array.
333 mc_visited_state_t state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
334 if (state_test->nb_processes < new_state->nb_processes)
335 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
336 else if (state_test->heap_bytes_used < new_state->heap_bytes_used)
337 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
339 xbt_dynar_insert_at(visited_states, index, &new_state);
341 XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
345 if ((ssize_t) xbt_dynar_length(visited_states) <= _sg_mc_visited)
348 // We have reached the maximum number of stored states;
350 XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
352 // Find the (index of the) older state (with the smallest num):
353 int min2 = mc_stats->expanded_states;
354 unsigned int cursor2 = 0;
355 unsigned int index2 = 0;
357 mc_visited_state_t state_test;
358 xbt_dynar_foreach(visited_states, cursor2, state_test)
359 if (!mc_model_checker->is_important_snapshot(*state_test->system_state)
360 && state_test->num < min2) {
362 min2 = state_test->num;
366 xbt_dynar_remove_at(visited_states, index2, nullptr);
367 XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
373 * \brief Checks whether a given pair has already been visited by the algorithm.
375 int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
377 if (_sg_mc_visited == 0)
380 mc_visited_pair_t new_visited_pair = nullptr;
381 if (visited_pair == nullptr)
382 new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
384 new_visited_pair = visited_pair;
386 if (xbt_dynar_is_empty(visited_pairs)) {
387 xbt_dynar_push(visited_pairs, &new_visited_pair);
391 int min = -1, max = -1, index;
393 mc_visited_pair_t pair_test;
396 index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
398 if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
399 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
401 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
402 if(pair_test->other_num == -1)
403 pair->other_num = pair_test->num;
405 pair->other_num = pair_test->other_num;
406 if(dot_output == nullptr)
407 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
409 XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
410 xbt_dynar_remove_at(visited_pairs, (min + res) - 1, nullptr);
411 xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
412 pair_test->visited_removed = 1;
413 if(pair_test->stack_removed && pair_test->visited_removed){
414 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
415 if(pair_test->acceptance_removed){
416 MC_pair_delete(pair_test);
419 MC_pair_delete(pair_test);
422 return pair->other_num;
425 while (cursor <= max) {
426 pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
427 if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
428 if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
429 if (snapshot_compare(pair_test, new_visited_pair) == 0) {
430 if (pair_test->other_num == -1)
431 new_visited_pair->other_num = pair_test->num;
433 new_visited_pair->other_num = pair_test->other_num;
434 if (dot_output == nullptr)
435 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
437 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);
438 xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
439 xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
440 pair_test->visited_removed = 1;
441 if (!pair_test->acceptance_pair
442 || pair_test->acceptance_removed == 1)
443 MC_visited_pair_delete(pair_test);
444 return new_visited_pair->other_num;
450 xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
452 pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
453 if (pair_test->nb_processes < new_visited_pair->nb_processes)
454 xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
455 else if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
456 xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
458 xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
461 if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
462 int min2 = mc_stats->expanded_pairs;
463 unsigned int cursor2 = 0;
464 unsigned int index2 = 0;
465 xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
466 if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
467 && pair_test->num < min2) {
469 min2 = pair_test->num;
472 xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
473 pair_test->visited_removed = 1;
474 if (!pair_test->acceptance_pair || pair_test->acceptance_removed)
475 MC_visited_pair_delete(pair_test);