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 static int is_exploration_stack_state(mc_visited_state_t state){
22 xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
24 if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
25 ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
28 item = xbt_fifo_get_next_item(item);
33 void visited_state_free(mc_visited_state_t state)
36 if(!is_exploration_stack_state(state)){
37 MC_free_snapshot(state->system_state);
43 void visited_state_free_voidp(void *s)
45 visited_state_free((mc_visited_state_t) * (void **) s);
49 * \brief Save the current state
50 * \return Snapshot of the current state.
52 static mc_visited_state_t visited_state_new()
54 mc_process_t process = &(mc_model_checker->process);
55 mc_visited_state_t new_state = NULL;
56 new_state = xbt_new0(s_mc_visited_state_t, 1);
57 new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
58 MC_process_get_heap(process)->heaplimit,
59 MC_process_get_malloc_info(process));
60 new_state->nb_processes = xbt_swag_size(simix_global->process_list);
61 new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
62 new_state->num = mc_stats->expanded_states;
63 new_state->other_num = -1;
67 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)
69 mc_process_t process = &(mc_model_checker->process);
70 mc_visited_pair_t pair = NULL;
71 pair = xbt_new0(s_mc_visited_pair_t, 1);
72 pair->graph_state = graph_state;
73 if(pair->graph_state->system_state == NULL)
74 pair->graph_state->system_state = MC_take_snapshot(pair_num);
75 pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
76 MC_process_get_heap(process)->heaplimit,
77 MC_process_get_malloc_info(process));
78 pair->nb_processes = xbt_swag_size(simix_global->process_list);
79 pair->automaton_state = automaton_state;
82 pair->acceptance_removed = 0;
83 pair->visited_removed = 0;
84 pair->acceptance_pair = 0;
85 pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
86 unsigned int cursor = 0;
88 xbt_dynar_foreach(atomic_propositions, cursor, value)
89 xbt_dynar_push_as(pair->atomic_propositions, int, value);
93 static int is_exploration_stack_pair(mc_visited_pair_t pair){
94 xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
96 if (((mc_pair_t)xbt_fifo_get_item_content(item))->num == pair->num){
97 ((mc_pair_t)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
100 item = xbt_fifo_get_next_item(item);
105 void MC_visited_pair_delete(mc_visited_pair_t p)
107 p->automaton_state = NULL;
108 if( !is_exploration_stack_pair(p))
109 MC_state_delete(p->graph_state, 1);
110 xbt_dynar_free(&(p->atomic_propositions));
116 * \brief Find a suitable subrange of candidate duplicates for a given state
117 * \param list dynamic array of states/pairs with candidate duplicates of the current state;
118 * \param ref current state/pair;
119 * \param min (output) index of the beginning of the the subrange
120 * \param max (output) index of the enf of the subrange
122 * Given a suitably ordered array of states/pairs, this function extracts a subrange
123 * (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
124 * This function uses only fast discriminating criterions and does not use the
125 * full state/pair comparison algorithms.
127 * The states/pairs in list MUST be ordered using a (given) weak order
128 * (based on nb_processes and heap_bytes_used).
129 * The subrange is the subrange of "equivalence" of the given state/pair.
131 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
134 xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
136 int cursor = 0, previous_cursor, next_cursor;
137 int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
140 if (_sg_mc_liveness) {
141 nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
142 heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
144 nb_processes = ((mc_visited_state_t) ref)->nb_processes;
145 heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
149 int end = xbt_dynar_length(list) - 1;
151 while (start <= end) {
152 cursor = (start + end) / 2;
153 if (_sg_mc_liveness) {
154 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
155 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
156 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
158 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, cursor, mc_visited_state_t);
159 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
160 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
162 if (nb_processes_test < nb_processes) {
164 } else if (nb_processes_test > nb_processes) {
167 if (heap_bytes_used_test < heap_bytes_used) {
169 } else if (heap_bytes_used_test > heap_bytes_used) {
172 *min = *max = cursor;
173 previous_cursor = cursor - 1;
174 while (previous_cursor >= 0) {
175 if (_sg_mc_liveness) {
176 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_pair_t);
177 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
178 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
180 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t);
181 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
182 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
184 if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
186 *min = previous_cursor;
189 next_cursor = cursor + 1;
190 while (next_cursor < xbt_dynar_length(list)) {
191 if (_sg_mc_liveness) {
192 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
193 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
194 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
196 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t);
197 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
198 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
200 if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
205 mmalloc_set_current_heap(heap);
211 mmalloc_set_current_heap(heap);
217 * \brief Checks whether a given state has already been visited by the algorithm.
220 mc_visited_state_t is_visited_state(mc_state_t graph_state)
223 if (_sg_mc_visited == 0)
226 int partial_comm = 0;
228 /* If comm determinism verification, we cannot stop the exploration if some
229 communications are not finished (at least, data are transfered). These communications
230 are incomplete and they cannot be analyzed and compared with the initial pattern. */
231 if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
232 int current_process = 1;
233 while (current_process < MC_smx_get_maxpid()) {
234 if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
235 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
243 xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
245 mc_visited_state_t new_state = visited_state_new();
246 graph_state->system_state = new_state->system_state;
247 graph_state->in_visited_states = 1;
248 XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
250 if (xbt_dynar_is_empty(visited_states)) {
252 xbt_dynar_push(visited_states, &new_state);
253 mmalloc_set_current_heap(heap);
258 int min = -1, max = -1, index;
260 mc_visited_state_t state_test;
263 index = get_search_interval(visited_states, new_state, &min, &max);
265 if (min != -1 && max != -1) {
267 // Parallell implementation
268 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
270 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
271 if(state_test->other_num == -1)
272 new_state->other_num = state_test->num;
274 new_state->other_num = state_test->other_num;
275 if(dot_output == NULL)
276 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
278 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);
279 xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
280 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
283 return new_state->other_num;
286 if(!partial_comm && initial_global_state->initial_communications_pattern_done){
289 while (cursor <= max) {
290 state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
291 if (snapshot_compare(state_test, new_state) == 0) {
292 // The state has been visited:
294 if (state_test->other_num == -1)
295 new_state->other_num = state_test->num;
297 new_state->other_num = state_test->other_num;
298 if (dot_output == NULL)
299 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
301 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);
303 /* Replace the old state with the new one (with a bigger num)
304 (when the max number of visited states is reached, the oldest
305 one is removed according to its number (= with the min number) */
306 xbt_dynar_remove_at(visited_states, cursor, NULL);
307 xbt_dynar_insert_at(visited_states, cursor, &new_state);
308 XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
310 mmalloc_set_current_heap(heap);
317 xbt_dynar_insert_at(visited_states, min, &new_state);
318 XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
322 // The state has not been visited: insert the state in the dynamic array.
323 state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
324 if (state_test->nb_processes < new_state->nb_processes) {
325 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
327 if (state_test->heap_bytes_used < new_state->heap_bytes_used)
328 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
330 xbt_dynar_insert_at(visited_states, index, &new_state);
333 XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
337 // We have reached the maximum number of stored states;
338 if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
340 XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
342 // Find the (index of the) older state (with the smallest num):
343 int min2 = mc_stats->expanded_states;
344 unsigned int cursor2 = 0;
345 unsigned int index2 = 0;
346 xbt_dynar_foreach(visited_states, cursor2, state_test){
347 if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
349 min2 = state_test->num;
354 xbt_dynar_remove_at(visited_states, index2, NULL);
355 XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
358 mmalloc_set_current_heap(heap);
364 * \brief Checks whether a given pair has already been visited by the algorithm.
366 int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
368 if (_sg_mc_visited == 0)
371 xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
373 mc_visited_pair_t new_visited_pair = NULL;
375 if (visited_pair == NULL) {
376 new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
378 new_visited_pair = visited_pair;
381 if (xbt_dynar_is_empty(visited_pairs)) {
383 xbt_dynar_push(visited_pairs, &new_visited_pair);
387 int min = -1, max = -1, index;
389 mc_visited_pair_t pair_test;
392 index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
394 if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
395 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
397 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
398 if(pair_test->other_num == -1)
399 pair->other_num = pair_test->num;
401 pair->other_num = pair_test->other_num;
402 if(dot_output == NULL)
403 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
405 XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
406 xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
407 xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
408 pair_test->visited_removed = 1;
409 if(pair_test->stack_removed && pair_test->visited_removed){
410 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
411 if(pair_test->acceptance_removed){
412 MC_pair_delete(pair_test);
415 MC_pair_delete(pair_test);
420 return pair->other_num;
423 while (cursor <= max) {
424 pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
425 if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
426 if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
427 if (snapshot_compare(pair_test, new_visited_pair) == 0) {
428 if (pair_test->other_num == -1)
429 new_visited_pair->other_num = pair_test->num;
431 new_visited_pair->other_num = pair_test->other_num;
432 if (dot_output == NULL)
433 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
435 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);
436 xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
437 xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_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);
445 mmalloc_set_current_heap(heap);
446 return new_visited_pair->other_num;
452 xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
454 pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
455 if (pair_test->nb_processes < new_visited_pair->nb_processes) {
456 xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
458 if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
459 xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
461 xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
465 if (xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
466 int min2 = mc_stats->expanded_pairs;
467 unsigned int cursor2 = 0;
468 unsigned int index2 = 0;
469 xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
470 if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
472 min2 = pair_test->num;
475 xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
476 pair_test->visited_removed = 1;
477 if (pair_test->acceptance_pair) {
478 if (pair_test->acceptance_removed)
479 MC_visited_pair_delete(pair_test);
481 MC_visited_pair_delete(pair_test);
487 mmalloc_set_current_heap(heap);