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)
46 if(!is_exploration_stack_state(state))
47 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 = xbt_dynar_length(
71 mc_model_checker->process().smx_process_infos);
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());
92 pair->nb_processes = xbt_dynar_length(
93 mc_model_checker->process().smx_process_infos);
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) {
180 if (heap_bytes_used_test < heap_bytes_used) {
182 } else if (heap_bytes_used_test > heap_bytes_used) {
185 *min = *max = cursor;
186 previous_cursor = cursor - 1;
187 while (previous_cursor >= 0) {
188 if (_sg_mc_liveness) {
189 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_pair_t);
190 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
191 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
193 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t);
194 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
195 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
197 if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
199 *min = previous_cursor;
202 size_t next_cursor = cursor + 1;
203 while (next_cursor < xbt_dynar_length(list)) {
204 if (_sg_mc_liveness) {
205 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
206 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
207 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
209 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t);
210 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
211 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
213 if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
227 mc_visited_state_t state_test, mc_visited_state_t new_state, int cursor)
229 if (state_test->other_num == -1)
230 new_state->other_num = state_test->num;
232 new_state->other_num = state_test->other_num;
234 if (dot_output == nullptr)
235 XBT_DEBUG("State %d already visited ! (equal to state %d)",
236 new_state->num, state_test->num);
239 "State %d already visited ! (equal to state %d (state %d in dot_output))",
240 new_state->num, state_test->num, new_state->other_num);
242 /* Replace the old state with the new one (with a bigger num)
243 (when the max number of visited states is reached, the oldest
244 one is removed according to its number (= with the min number) */
245 xbt_dynar_remove_at(visited_states, cursor, nullptr);
246 xbt_dynar_insert_at(visited_states, cursor, &new_state);
247 XBT_DEBUG("Replace visited state %d with the new visited state %d",
248 state_test->num, new_state->num);
252 bool some_dommunications_are_not_finished()
254 for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
255 xbt_dynar_t pattern = xbt_dynar_get_as(
256 incomplete_communications_pattern, current_process, xbt_dynar_t);
257 if (!xbt_dynar_is_empty(pattern)) {
258 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
266 * \brief Checks whether a given state has already been visited by the algorithm.
269 mc_visited_state_t is_visited_state(mc_state_t graph_state)
272 if (_sg_mc_visited == 0)
275 /* If comm determinism verification, we cannot stop the exploration if some
276 communications are not finished (at least, data are transfered). These communications
277 are incomplete and they cannot be analyzed and compared with the initial pattern. */
278 int partial_comm = (_sg_mc_comms_determinism || _sg_mc_send_determinism) &&
279 some_dommunications_are_not_finished();
281 mc_visited_state_t new_state = visited_state_new();
282 graph_state->system_state = new_state->system_state;
283 graph_state->in_visited_states = 1;
284 XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
286 if (xbt_dynar_is_empty(visited_states)) {
288 xbt_dynar_push(visited_states, &new_state);
293 int min = -1, max = -1, index;
295 index = get_search_interval(visited_states, new_state, &min, &max);
297 if (min != -1 && max != -1) {
299 // Parallell implementation
300 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
302 mc_visited_state_t state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
303 if(state_test->other_num == -1)
304 new_state->other_num = state_test->num;
306 new_state->other_num = state_test->other_num;
307 if(dot_output == nullptr)
308 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
310 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);
311 xbt_dynar_remove_at(visited_states, (min + res) - 1, nullptr);
312 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
313 return new_state->other_num;
316 if (_sg_mc_safety || (!partial_comm
317 && initial_global_state->initial_communications_pattern_done)) {
320 while (cursor <= max) {
321 mc_visited_state_t state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
322 if (snapshot_compare(state_test, new_state) == 0) {
323 // The state has been visited:
325 replace_state(state_test, new_state, cursor);
332 xbt_dynar_insert_at(visited_states, min, &new_state);
333 XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
337 // The state has not been visited: insert the state in the dynamic array.
338 mc_visited_state_t state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
339 if (state_test->nb_processes < new_state->nb_processes) {
340 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
342 if (state_test->heap_bytes_used < new_state->heap_bytes_used)
343 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
345 xbt_dynar_insert_at(visited_states, index, &new_state);
348 XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
352 // We have reached the maximum number of stored states;
353 if ((ssize_t) xbt_dynar_length(visited_states) > _sg_mc_visited) {
355 XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
357 // Find the (index of the) older state (with the smallest num):
358 int min2 = mc_stats->expanded_states;
359 unsigned int cursor2 = 0;
360 unsigned int index2 = 0;
362 mc_visited_state_t state_test;
363 xbt_dynar_foreach(visited_states, cursor2, state_test){
364 if (!mc_model_checker->is_important_snapshot(*state_test->system_state)
365 && state_test->num < min2) {
367 min2 = state_test->num;
372 xbt_dynar_remove_at(visited_states, index2, nullptr);
373 XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
381 * \brief Checks whether a given pair has already been visited by the algorithm.
383 int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
385 if (_sg_mc_visited == 0)
388 mc_visited_pair_t new_visited_pair = nullptr;
390 if (visited_pair == nullptr) {
391 new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
393 new_visited_pair = visited_pair;
396 if (xbt_dynar_is_empty(visited_pairs)) {
398 xbt_dynar_push(visited_pairs, &new_visited_pair);
402 int min = -1, max = -1, index;
404 mc_visited_pair_t pair_test;
407 index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
409 if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
410 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
412 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
413 if(pair_test->other_num == -1)
414 pair->other_num = pair_test->num;
416 pair->other_num = pair_test->other_num;
417 if(dot_output == nullptr)
418 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
420 XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
421 xbt_dynar_remove_at(visited_pairs, (min + res) - 1, nullptr);
422 xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
423 pair_test->visited_removed = 1;
424 if(pair_test->stack_removed && pair_test->visited_removed){
425 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
426 if(pair_test->acceptance_removed){
427 MC_pair_delete(pair_test);
430 MC_pair_delete(pair_test);
433 return pair->other_num;
436 while (cursor <= max) {
437 pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
438 if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
439 if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
440 if (snapshot_compare(pair_test, new_visited_pair) == 0) {
441 if (pair_test->other_num == -1)
442 new_visited_pair->other_num = pair_test->num;
444 new_visited_pair->other_num = pair_test->other_num;
445 if (dot_output == nullptr)
446 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
448 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);
449 xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
450 xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
451 pair_test->visited_removed = 1;
452 if (pair_test->acceptance_pair) {
453 if (pair_test->acceptance_removed == 1)
454 MC_visited_pair_delete(pair_test);
456 MC_visited_pair_delete(pair_test);
458 return new_visited_pair->other_num;
464 xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
466 pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
467 if (pair_test->nb_processes < new_visited_pair->nb_processes) {
468 xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
470 if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
471 xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
473 xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
477 if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
478 int min2 = mc_stats->expanded_pairs;
479 unsigned int cursor2 = 0;
480 unsigned int index2 = 0;
481 xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
482 if (!mc_model_checker->is_important_snapshot(*pair_test->graph_state->system_state)
483 && pair_test->num < min2) {
485 min2 = pair_test->num;
488 xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
489 pair_test->visited_removed = 1;
490 if (pair_test->acceptance_pair) {
491 if (pair_test->acceptance_removed)
492 MC_visited_pair_delete(pair_test);
494 MC_visited_pair_delete(pair_test);