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_process_t process = &(mc_model_checker->process);
41 mc_visited_state_t new_state = NULL;
42 new_state = xbt_new0(s_mc_visited_state_t, 1);
43 new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
44 MC_process_get_heap(process)->heaplimit,
45 MC_process_get_malloc_info(process));
46 new_state->nb_processes = xbt_swag_size(simix_global->process_list);
47 new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
48 new_state->num = mc_stats->expanded_states;
49 new_state->other_num = -1;
54 mc_visited_pair_t MC_visited_pair_new(int pair_num,
55 xbt_automaton_state_t automaton_state,
56 xbt_dynar_t atomic_propositions)
58 mc_process_t process = &(mc_model_checker->process);
59 mc_visited_pair_t pair = NULL;
60 pair = xbt_new0(s_mc_visited_pair_t, 1);
61 pair->graph_state = MC_state_new();
62 pair->graph_state->system_state = MC_take_snapshot(pair_num);
63 pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
64 MC_process_get_heap(process)->heaplimit,
65 MC_process_get_malloc_info(process));
66 pair->nb_processes = xbt_swag_size(simix_global->process_list);
67 pair->automaton_state = automaton_state;
70 pair->acceptance_removed = 0;
71 pair->visited_removed = 0;
72 pair->acceptance_pair = 0;
73 pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
74 unsigned int cursor = 0;
76 xbt_dynar_foreach(atomic_propositions, cursor, value)
77 xbt_dynar_push_as(pair->atomic_propositions, int, value);
81 void MC_visited_pair_delete(mc_visited_pair_t p)
83 p->automaton_state = NULL;
84 MC_state_delete(p->graph_state);
85 xbt_dynar_free(&(p->atomic_propositions));
91 * \brief Find a suitable subrange of candidate duplicates for a given state
92 * \param list dynamic array of states/pairs with candidate duplicates of the current state;
93 * \param ref current state/pair;
94 * \param min (output) index of the beginning of the the subrange
95 * \param max (output) index of the enf of the subrange
97 * Given a suitably ordered array of states/pairs, this function extracts a subrange
98 * (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
99 * This function uses only fast discriminating criterions and does not use the
100 * full state/pair comparison algorithms.
102 * The states/pairs in list MUST be ordered using a (given) weak order
103 * (based on nb_processes and heap_bytes_used).
104 * The subrange is the subrange of "equivalence" of the given state/pair.
106 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
109 int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
113 int cursor = 0, previous_cursor, next_cursor;
114 int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
117 if (_sg_mc_liveness) {
118 nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
119 heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
121 nb_processes = ((mc_visited_state_t) ref)->nb_processes;
122 heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
126 int end = xbt_dynar_length(list) - 1;
128 while (start <= end) {
129 cursor = (start + end) / 2;
130 if (_sg_mc_liveness) {
132 (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
133 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
134 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
137 (mc_visited_state_t) xbt_dynar_get_as(list, cursor,
139 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
140 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
142 if (nb_processes_test < nb_processes) {
144 } else if (nb_processes_test > nb_processes) {
147 if (heap_bytes_used_test < heap_bytes_used) {
149 } else if (heap_bytes_used_test > heap_bytes_used) {
152 *min = *max = cursor;
153 previous_cursor = cursor - 1;
154 while (previous_cursor >= 0) {
155 if (_sg_mc_liveness) {
157 (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor,
159 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
160 heap_bytes_used_test =
161 ((mc_visited_pair_t) ref_test)->heap_bytes_used;
164 (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor,
166 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
167 heap_bytes_used_test =
168 ((mc_visited_state_t) ref_test)->heap_bytes_used;
170 if (nb_processes_test != nb_processes
171 || heap_bytes_used_test != heap_bytes_used)
173 *min = previous_cursor;
176 next_cursor = cursor + 1;
177 while (next_cursor < xbt_dynar_length(list)) {
178 if (_sg_mc_liveness) {
180 (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor,
182 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
183 heap_bytes_used_test =
184 ((mc_visited_pair_t) ref_test)->heap_bytes_used;
187 (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor,
189 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
190 heap_bytes_used_test =
191 ((mc_visited_state_t) ref_test)->heap_bytes_used;
193 if (nb_processes_test != nb_processes
194 || heap_bytes_used_test != heap_bytes_used)
214 * \brief Checks whether a given state has already been visited by the algorithm.
217 mc_visited_state_t is_visited_state()
220 if (_sg_mc_visited == 0)
223 /* If comm determinism verification, we cannot stop the exploration if some
224 communications are not finished (at least, data are transfered). These communications
225 are incomplete and they cannot be analyzed and compared with the initial pattern */
226 if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
227 int current_process = 1;
228 while (current_process < simix_process_maxpid) {
229 if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t)))
235 int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
239 mc_visited_state_t new_state = visited_state_new();
241 if (xbt_dynar_is_empty(visited_states)) {
243 xbt_dynar_push(visited_states, &new_state);
252 int min = -1, max = -1, index;
254 mc_visited_state_t state_test;
257 index = get_search_interval(visited_states, new_state, &min, &max);
259 if (min != -1 && max != -1) {
261 // Parallell implementation
262 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
264 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
265 if(state_test->other_num == -1)
266 new_state->other_num = state_test->num;
268 new_state->other_num = state_test->other_num;
269 if(dot_output == NULL)
270 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
272 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);
273 xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
274 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
277 return new_state->other_num;
281 while (cursor <= max) {
283 (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor,
285 if (snapshot_compare(state_test, new_state) == 0) {
286 // The state has been visited:
288 if (state_test->other_num == -1)
289 new_state->other_num = state_test->num;
291 new_state->other_num = state_test->other_num;
292 if (dot_output == NULL)
293 XBT_DEBUG("State %d already visited ! (equal to state %d)",
294 new_state->num, state_test->num);
297 ("State %d already visited ! (equal to state %d (state %d in dot_output))",
298 new_state->num, state_test->num, new_state->other_num);
300 /* Replace the old state with the new one (with a bigger num)
301 (when the max number of visited states is reached, the oldest
302 one is removed according to its number (= with the min number) */
303 xbt_dynar_remove_at(visited_states, cursor, NULL);
304 xbt_dynar_insert_at(visited_states, cursor, &new_state);
313 // The state has not been visited: insert the state in the dynamic array.
314 xbt_dynar_insert_at(visited_states, min, &new_state);
318 // The state has not been visited: insert the state in the dynamic array.
320 (mc_visited_state_t) xbt_dynar_get_as(visited_states, index,
322 if (state_test->nb_processes < new_state->nb_processes) {
323 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
325 if (state_test->heap_bytes_used < new_state->heap_bytes_used)
326 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
328 xbt_dynar_insert_at(visited_states, index, &new_state);
333 // We have reached the maximum number of stored states;
334 if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
336 // Find the (index of the) older state (with the smallest num):
337 int min2 = mc_stats->expanded_states;
338 unsigned int cursor2 = 0;
339 unsigned int index2 = 0;
340 xbt_dynar_foreach(visited_states, cursor2, state_test){
341 if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
343 min2 = state_test->num;
348 xbt_dynar_remove_at(visited_states, index2, NULL);
360 * \brief Checks whether a given pair has already been visited by the algorithm.
362 int is_visited_pair(mc_visited_pair_t pair, int pair_num,
363 xbt_automaton_state_t automaton_state,
364 xbt_dynar_t atomic_propositions)
367 if (_sg_mc_visited == 0)
370 int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
374 mc_visited_pair_t new_pair = NULL;
378 MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
383 if (xbt_dynar_is_empty(visited_pairs)) {
385 xbt_dynar_push(visited_pairs, &new_pair);
389 int min = -1, max = -1, index;
391 mc_visited_pair_t pair_test;
394 index = get_search_interval(visited_pairs, new_pair, &min, &max);
396 if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
397 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
399 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
400 if(pair_test->other_num == -1)
401 pair->other_num = pair_test->num;
403 pair->other_num = pair_test->other_num;
404 if(dot_output == NULL)
405 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
407 XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
408 xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
409 xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
410 pair_test->visited_removed = 1;
411 if(pair_test->stack_removed && pair_test->visited_removed){
412 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
413 if(pair_test->acceptance_removed){
414 MC_pair_delete(pair_test);
417 MC_pair_delete(pair_test);
422 return pair->other_num;
425 while (cursor <= max) {
427 (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor,
429 if (xbt_automaton_state_compare
430 (pair_test->automaton_state, new_pair->automaton_state) == 0) {
431 if (xbt_automaton_propositional_symbols_compare_value
432 (pair_test->atomic_propositions,
433 new_pair->atomic_propositions) == 0) {
434 if (snapshot_compare(pair_test, new_pair) == 0) {
435 if (pair_test->other_num == -1)
436 new_pair->other_num = pair_test->num;
438 new_pair->other_num = pair_test->other_num;
439 if (dot_output == NULL)
440 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
441 new_pair->num, pair_test->num);
444 ("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
445 new_pair->num, pair_test->num, new_pair->other_num);
446 xbt_dynar_remove_at(visited_pairs, cursor, NULL);
447 xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
448 pair_test->visited_removed = 1;
449 if (pair_test->acceptance_pair) {
450 if (pair_test->acceptance_removed == 1)
451 MC_visited_pair_delete(pair_test);
453 MC_visited_pair_delete(pair_test);
457 return new_pair->other_num;
463 xbt_dynar_insert_at(visited_pairs, min, &new_pair);
466 (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index,
468 if (pair_test->nb_processes < new_pair->nb_processes) {
469 xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
471 if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
472 xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
474 xbt_dynar_insert_at(visited_pairs, index, &new_pair);
478 if (xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
479 int min2 = mc_stats->expanded_pairs;
480 unsigned int cursor2 = 0;
481 unsigned int index2 = 0;
482 xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
483 if (!mc_important_snapshot(pair_test->graph_state->system_state) && 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);