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. */
7 #include "mc_private.h"
11 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
12 "Logging specific to state equaity detection mechanisms");
14 xbt_dynar_t visited_pairs;
15 xbt_dynar_t visited_states;
17 void visited_state_free(mc_visited_state_t state)
20 MC_free_snapshot(state->system_state);
25 void visited_state_free_voidp(void *s)
27 visited_state_free((mc_visited_state_t) * (void **) s);
31 * \brief Save the current state
32 * \return Snapshot of the current state.
34 static mc_visited_state_t visited_state_new()
36 mc_visited_state_t new_state = NULL;
37 new_state = xbt_new0(s_mc_visited_state_t, 1);
38 new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
39 new_state->nb_processes = xbt_swag_size(simix_global->process_list);
40 new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
41 new_state->num = mc_stats->expanded_states;
42 new_state->other_num = -1;
47 mc_visited_pair_t MC_visited_pair_new(int pair_num,
48 xbt_automaton_state_t automaton_state,
49 xbt_dynar_t atomic_propositions)
51 mc_visited_pair_t pair = NULL;
52 pair = xbt_new0(s_mc_visited_pair_t, 1);
53 pair->graph_state = MC_state_new();
54 pair->graph_state->system_state = MC_take_snapshot(pair_num);
55 pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
56 pair->nb_processes = xbt_swag_size(simix_global->process_list);
57 pair->automaton_state = automaton_state;
60 pair->acceptance_removed = 0;
61 pair->visited_removed = 0;
62 pair->acceptance_pair = 0;
63 pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
64 unsigned int cursor = 0;
66 xbt_dynar_foreach(atomic_propositions, cursor, value)
67 xbt_dynar_push_as(pair->atomic_propositions, int, value);
71 void MC_visited_pair_delete(mc_visited_pair_t p)
73 p->automaton_state = NULL;
74 MC_state_delete(p->graph_state);
75 xbt_dynar_free(&(p->atomic_propositions));
81 * \brief Find a suitable subrange of candidate duplicates for a given state
82 * \param list dynamic array of states/pairs with candidate duplicates of the current state;
83 * \param ref current state/pair;
84 * \param min (output) index of the beginning of the the subrange
85 * \param max (output) index of the enf of the subrange
87 * Given a suitably ordered array of states/pairs, this function extracts a subrange
88 * (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
89 * This function uses only fast discriminating criterions and does not use the
90 * full state/pair comparison algorithms.
92 * The states/pairs in list MUST be ordered using a (given) weak order
93 * (based on nb_processes and heap_bytes_used).
94 * The subrange is the subrange of "equivalence" of the given state/pair.
96 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
99 int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
103 int cursor = 0, previous_cursor, next_cursor;
104 int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
107 if (_sg_mc_liveness) {
108 nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
109 heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
111 nb_processes = ((mc_visited_state_t) ref)->nb_processes;
112 heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
116 int end = xbt_dynar_length(list) - 1;
118 while (start <= end) {
119 cursor = (start + end) / 2;
120 if (_sg_mc_liveness) {
122 (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
123 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
124 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
127 (mc_visited_state_t) xbt_dynar_get_as(list, cursor,
129 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
130 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
132 if (nb_processes_test < nb_processes) {
134 } else if (nb_processes_test > nb_processes) {
137 if (heap_bytes_used_test < heap_bytes_used) {
139 } else if (heap_bytes_used_test > heap_bytes_used) {
142 *min = *max = cursor;
143 previous_cursor = cursor - 1;
144 while (previous_cursor >= 0) {
145 if (_sg_mc_liveness) {
147 (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor,
149 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
150 heap_bytes_used_test =
151 ((mc_visited_pair_t) ref_test)->heap_bytes_used;
154 (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor,
156 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
157 heap_bytes_used_test =
158 ((mc_visited_state_t) ref_test)->heap_bytes_used;
160 if (nb_processes_test != nb_processes
161 || heap_bytes_used_test != heap_bytes_used)
163 *min = previous_cursor;
166 next_cursor = cursor + 1;
167 while (next_cursor < xbt_dynar_length(list)) {
168 if (_sg_mc_liveness) {
170 (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor,
172 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
173 heap_bytes_used_test =
174 ((mc_visited_pair_t) ref_test)->heap_bytes_used;
177 (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor,
179 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
180 heap_bytes_used_test =
181 ((mc_visited_state_t) ref_test)->heap_bytes_used;
183 if (nb_processes_test != nb_processes
184 || heap_bytes_used_test != heap_bytes_used)
204 * \brief Checks whether a given state has already been visited by the algorithm.
207 mc_visited_state_t is_visited_state()
210 if (_sg_mc_visited == 0)
213 /* If comm determinism verification, we cannot stop the exploration if some
214 communications are not finished (at least, data are transfered). These communications
215 are incomplete and they cannot be analyzed and compared with the initial pattern */
216 if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
217 int current_process = 1;
218 while (current_process < simix_process_maxpid) {
219 if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t)))
225 int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
229 mc_visited_state_t new_state = visited_state_new();
231 if (xbt_dynar_is_empty(visited_states)) {
233 xbt_dynar_push(visited_states, &new_state);
242 int min = -1, max = -1, index;
244 mc_visited_state_t state_test;
247 index = get_search_interval(visited_states, new_state, &min, &max);
249 if (min != -1 && max != -1) {
251 // Parallell implementation
252 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
254 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
255 if(state_test->other_num == -1)
256 new_state->other_num = state_test->num;
258 new_state->other_num = state_test->other_num;
259 if(dot_output == NULL)
260 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
262 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);
263 xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
264 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
267 return new_state->other_num;
271 while (cursor <= max) {
273 (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor,
275 if (snapshot_compare(state_test, new_state) == 0) {
276 // The state has been visited:
278 if (state_test->other_num == -1)
279 new_state->other_num = state_test->num;
281 new_state->other_num = state_test->other_num;
282 if (dot_output == NULL)
283 XBT_DEBUG("State %d already visited ! (equal to state %d)",
284 new_state->num, state_test->num);
287 ("State %d already visited ! (equal to state %d (state %d in dot_output))",
288 new_state->num, state_test->num, new_state->other_num);
290 /* Replace the old state with the new one (with a bigger num)
291 (when the max number of visited states is reached, the oldest
292 one is removed according to its number (= with the min number) */
293 xbt_dynar_remove_at(visited_states, cursor, NULL);
294 xbt_dynar_insert_at(visited_states, cursor, &new_state);
303 // The state has not been visited: insert the state in the dynamic array.
304 xbt_dynar_insert_at(visited_states, min, &new_state);
308 // The state has not been visited: insert the state in the dynamic array.
310 (mc_visited_state_t) xbt_dynar_get_as(visited_states, index,
312 if (state_test->nb_processes < new_state->nb_processes) {
313 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
315 if (state_test->heap_bytes_used < new_state->heap_bytes_used)
316 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
318 xbt_dynar_insert_at(visited_states, index, &new_state);
323 // We have reached the maximum number of stored states;
324 if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
326 // Find the (index of the) older state (with the smallest num):
327 int min2 = mc_stats->expanded_states;
328 unsigned int cursor2 = 0;
329 unsigned int index2 = 0;
330 xbt_dynar_foreach(visited_states, cursor2, state_test){
331 if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
333 min2 = state_test->num;
338 xbt_dynar_remove_at(visited_states, index2, NULL);
350 * \brief Checks whether a given pair has already been visited by the algorithm.
352 int is_visited_pair(mc_visited_pair_t pair, int pair_num,
353 xbt_automaton_state_t automaton_state,
354 xbt_dynar_t atomic_propositions)
357 if (_sg_mc_visited == 0)
360 int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
364 mc_visited_pair_t new_pair = NULL;
368 MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
373 if (xbt_dynar_is_empty(visited_pairs)) {
375 xbt_dynar_push(visited_pairs, &new_pair);
379 int min = -1, max = -1, index;
381 mc_visited_pair_t pair_test;
384 index = get_search_interval(visited_pairs, new_pair, &min, &max);
386 if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
387 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
389 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
390 if(pair_test->other_num == -1)
391 pair->other_num = pair_test->num;
393 pair->other_num = pair_test->other_num;
394 if(dot_output == NULL)
395 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
397 XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
398 xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
399 xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
400 pair_test->visited_removed = 1;
401 if(pair_test->stack_removed && pair_test->visited_removed){
402 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
403 if(pair_test->acceptance_removed){
404 MC_pair_delete(pair_test);
407 MC_pair_delete(pair_test);
412 return pair->other_num;
415 while (cursor <= max) {
417 (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor,
419 if (xbt_automaton_state_compare
420 (pair_test->automaton_state, new_pair->automaton_state) == 0) {
421 if (xbt_automaton_propositional_symbols_compare_value
422 (pair_test->atomic_propositions,
423 new_pair->atomic_propositions) == 0) {
424 if (snapshot_compare(pair_test, new_pair) == 0) {
425 if (pair_test->other_num == -1)
426 new_pair->other_num = pair_test->num;
428 new_pair->other_num = pair_test->other_num;
429 if (dot_output == NULL)
430 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
431 new_pair->num, pair_test->num);
434 ("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
435 new_pair->num, pair_test->num, new_pair->other_num);
436 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
437 xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
438 pair_test->visited_removed = 1;
439 if (pair_test->acceptance_pair) {
440 if (pair_test->acceptance_removed == 1)
441 MC_visited_pair_delete(pair_test);
443 MC_visited_pair_delete(pair_test);
447 return new_pair->other_num;
453 xbt_dynar_insert_at(visited_pairs, min, &new_pair);
456 (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index,
458 if (pair_test->nb_processes < new_pair->nb_processes) {
459 xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
461 if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
462 xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
464 xbt_dynar_insert_at(visited_pairs, index, &new_pair);
468 if (xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
469 int min2 = mc_stats->expanded_pairs;
470 unsigned int cursor2 = 0;
471 unsigned int index2 = 0;
472 xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
473 if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
475 min2 = pair_test->num;
478 xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
479 pair_test->visited_removed = 1;
480 if (pair_test->acceptance_pair) {
481 if (pair_test->acceptance_removed)
482 MC_visited_pair_delete(pair_test);
484 MC_visited_pair_delete(pair_test);