1 /* Copyright (c) 2011-2014. 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 "mc_comm_pattern.h"
11 #include "mc_safety.h"
12 #include "mc_liveness.h"
13 #include "mc_private.h"
15 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
16 "Logging specific to state equaity detection mechanisms");
18 xbt_dynar_t visited_pairs;
19 xbt_dynar_t visited_states;
21 void visited_state_free(mc_visited_state_t state)
24 MC_free_snapshot(state->system_state);
29 void visited_state_free_voidp(void *s)
31 visited_state_free((mc_visited_state_t) * (void **) s);
35 * \brief Save the current state
36 * \return Snapshot of the current state.
38 static mc_visited_state_t visited_state_new()
40 mc_visited_state_t new_state = NULL;
41 new_state = xbt_new0(s_mc_visited_state_t, 1);
42 new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
43 new_state->nb_processes = xbt_swag_size(simix_global->process_list);
44 new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
45 new_state->num = mc_stats->expanded_states;
46 new_state->other_num = -1;
51 mc_visited_pair_t MC_visited_pair_new(int pair_num,
52 xbt_automaton_state_t automaton_state,
53 xbt_dynar_t atomic_propositions)
55 mc_visited_pair_t pair = NULL;
56 pair = xbt_new0(s_mc_visited_pair_t, 1);
57 pair->graph_state = MC_state_new();
58 pair->graph_state->system_state = MC_take_snapshot(pair_num);
59 pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
60 pair->nb_processes = xbt_swag_size(simix_global->process_list);
61 pair->automaton_state = automaton_state;
64 pair->acceptance_removed = 0;
65 pair->visited_removed = 0;
66 pair->acceptance_pair = 0;
67 pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
68 unsigned int cursor = 0;
70 xbt_dynar_foreach(atomic_propositions, cursor, value)
71 xbt_dynar_push_as(pair->atomic_propositions, int, value);
75 void MC_visited_pair_delete(mc_visited_pair_t p)
77 p->automaton_state = NULL;
78 MC_state_delete(p->graph_state);
79 xbt_dynar_free(&(p->atomic_propositions));
85 * \brief Find a suitable subrange of candidate duplicates for a given state
86 * \param list dynamic array of states/pairs with candidate duplicates of the current state;
87 * \param ref current state/pair;
88 * \param min (output) index of the beginning of the the subrange
89 * \param max (output) index of the enf of the subrange
91 * Given a suitably ordered array of states/pairs, this function extracts a subrange
92 * (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
93 * This function uses only fast discriminating criterions and does not use the
94 * full state/pair comparison algorithms.
96 * The states/pairs in list MUST be ordered using a (given) weak order
97 * (based on nb_processes and heap_bytes_used).
98 * The subrange is the subrange of "equivalence" of the given state/pair.
100 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
103 int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
107 int cursor = 0, previous_cursor, next_cursor;
108 int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
111 if (_sg_mc_liveness) {
112 nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
113 heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
115 nb_processes = ((mc_visited_state_t) ref)->nb_processes;
116 heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
120 int end = xbt_dynar_length(list) - 1;
122 while (start <= end) {
123 cursor = (start + end) / 2;
124 if (_sg_mc_liveness) {
126 (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
127 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
128 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
131 (mc_visited_state_t) xbt_dynar_get_as(list, cursor,
133 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
134 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
136 if (nb_processes_test < nb_processes) {
138 } else if (nb_processes_test > nb_processes) {
141 if (heap_bytes_used_test < heap_bytes_used) {
143 } else if (heap_bytes_used_test > heap_bytes_used) {
146 *min = *max = cursor;
147 previous_cursor = cursor - 1;
148 while (previous_cursor >= 0) {
149 if (_sg_mc_liveness) {
151 (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor,
153 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
154 heap_bytes_used_test =
155 ((mc_visited_pair_t) ref_test)->heap_bytes_used;
158 (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor,
160 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
161 heap_bytes_used_test =
162 ((mc_visited_state_t) ref_test)->heap_bytes_used;
164 if (nb_processes_test != nb_processes
165 || heap_bytes_used_test != heap_bytes_used)
167 *min = previous_cursor;
170 next_cursor = cursor + 1;
171 while (next_cursor < xbt_dynar_length(list)) {
172 if (_sg_mc_liveness) {
174 (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor,
176 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
177 heap_bytes_used_test =
178 ((mc_visited_pair_t) ref_test)->heap_bytes_used;
181 (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor,
183 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
184 heap_bytes_used_test =
185 ((mc_visited_state_t) ref_test)->heap_bytes_used;
187 if (nb_processes_test != nb_processes
188 || heap_bytes_used_test != heap_bytes_used)
208 * \brief Checks whether a given state has already been visited by the algorithm.
211 mc_visited_state_t is_visited_state()
214 if (_sg_mc_visited == 0)
217 /* If comm determinism verification, we cannot stop the exploration if some
218 communications are not finished (at least, data are transfered). These communications
219 are incomplete and they cannot be analyzed and compared with the initial pattern */
220 if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
221 int current_process = 1;
222 while (current_process < simix_process_maxpid) {
223 if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t)))
229 int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
233 mc_visited_state_t new_state = visited_state_new();
235 if (xbt_dynar_is_empty(visited_states)) {
237 xbt_dynar_push(visited_states, &new_state);
246 int min = -1, max = -1, index;
248 mc_visited_state_t state_test;
251 index = get_search_interval(visited_states, new_state, &min, &max);
253 if (min != -1 && max != -1) {
255 // Parallell implementation
256 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
258 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
259 if(state_test->other_num == -1)
260 new_state->other_num = state_test->num;
262 new_state->other_num = state_test->other_num;
263 if(dot_output == NULL)
264 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
266 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);
267 xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
268 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
271 return new_state->other_num;
275 while (cursor <= max) {
277 (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor,
279 if (snapshot_compare(state_test, new_state) == 0) {
280 // The state has been visited:
282 if (state_test->other_num == -1)
283 new_state->other_num = state_test->num;
285 new_state->other_num = state_test->other_num;
286 if (dot_output == NULL)
287 XBT_DEBUG("State %d already visited ! (equal to state %d)",
288 new_state->num, state_test->num);
291 ("State %d already visited ! (equal to state %d (state %d in dot_output))",
292 new_state->num, state_test->num, new_state->other_num);
294 /* Replace the old state with the new one (with a bigger num)
295 (when the max number of visited states is reached, the oldest
296 one is removed according to its number (= with the min number) */
297 xbt_dynar_remove_at(visited_states, cursor, NULL);
298 xbt_dynar_insert_at(visited_states, cursor, &new_state);
307 // The state has not been visited: insert the state in the dynamic array.
308 xbt_dynar_insert_at(visited_states, min, &new_state);
312 // The state has not been visited: insert the state in the dynamic array.
314 (mc_visited_state_t) xbt_dynar_get_as(visited_states, index,
316 if (state_test->nb_processes < new_state->nb_processes) {
317 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
319 if (state_test->heap_bytes_used < new_state->heap_bytes_used)
320 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
322 xbt_dynar_insert_at(visited_states, index, &new_state);
327 // We have reached the maximum number of stored states;
328 if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
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;
334 xbt_dynar_foreach(visited_states, cursor2, state_test){
335 if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
337 min2 = state_test->num;
342 xbt_dynar_remove_at(visited_states, index2, NULL);
354 * \brief Checks whether a given pair has already been visited by the algorithm.
356 int is_visited_pair(mc_visited_pair_t pair, int pair_num,
357 xbt_automaton_state_t automaton_state,
358 xbt_dynar_t atomic_propositions)
361 if (_sg_mc_visited == 0)
364 int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
368 mc_visited_pair_t new_pair = NULL;
372 MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
377 if (xbt_dynar_is_empty(visited_pairs)) {
379 xbt_dynar_push(visited_pairs, &new_pair);
383 int min = -1, max = -1, index;
385 mc_visited_pair_t pair_test;
388 index = get_search_interval(visited_pairs, new_pair, &min, &max);
390 if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
391 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
393 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
394 if(pair_test->other_num == -1)
395 pair->other_num = pair_test->num;
397 pair->other_num = pair_test->other_num;
398 if(dot_output == NULL)
399 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
401 XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
402 xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
403 xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
404 pair_test->visited_removed = 1;
405 if(pair_test->stack_removed && pair_test->visited_removed){
406 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
407 if(pair_test->acceptance_removed){
408 MC_pair_delete(pair_test);
411 MC_pair_delete(pair_test);
416 return pair->other_num;
419 while (cursor <= max) {
421 (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor,
423 if (xbt_automaton_state_compare
424 (pair_test->automaton_state, new_pair->automaton_state) == 0) {
425 if (xbt_automaton_propositional_symbols_compare_value
426 (pair_test->atomic_propositions,
427 new_pair->atomic_propositions) == 0) {
428 if (snapshot_compare(pair_test, new_pair) == 0) {
429 if (pair_test->other_num == -1)
430 new_pair->other_num = pair_test->num;
432 new_pair->other_num = pair_test->other_num;
433 if (dot_output == NULL)
434 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
435 new_pair->num, pair_test->num);
438 ("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
439 new_pair->num, pair_test->num, new_pair->other_num);
440 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
441 xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
442 pair_test->visited_removed = 1;
443 if (pair_test->acceptance_pair) {
444 if (pair_test->acceptance_removed == 1)
445 MC_visited_pair_delete(pair_test);
447 MC_visited_pair_delete(pair_test);
451 return new_pair->other_num;
457 xbt_dynar_insert_at(visited_pairs, min, &new_pair);
460 (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index,
462 if (pair_test->nb_processes < new_pair->nb_processes) {
463 xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
465 if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
466 xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
468 xbt_dynar_insert_at(visited_pairs, index, &new_pair);
472 if (xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
473 int min2 = mc_stats->expanded_pairs;
474 unsigned int cursor2 = 0;
475 unsigned int index2 = 0;
476 xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
477 if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
479 min2 = pair_test->num;
482 xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
483 pair_test->visited_removed = 1;
484 if (pair_test->acceptance_pair) {
485 if (pair_test->acceptance_removed)
486 MC_visited_pair_delete(pair_test);
488 MC_visited_pair_delete(pair_test);