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"
14 #include "mc_process.h"
17 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
18 "Logging specific to state equaity detection mechanisms");
20 xbt_dynar_t visited_pairs;
21 xbt_dynar_t visited_states;
23 static int is_exploration_stack_state(mc_visited_state_t state){
24 xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
26 if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
27 ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
30 item = xbt_fifo_get_next_item(item);
35 void visited_state_free(mc_visited_state_t state)
38 if(!is_exploration_stack_state(state)){
39 MC_free_snapshot(state->system_state);
45 void visited_state_free_voidp(void *s)
47 visited_state_free((mc_visited_state_t) * (void **) s);
51 * \brief Save the current state
52 * \return Snapshot of the current state.
54 static mc_visited_state_t visited_state_new()
56 mc_process_t process = &(mc_model_checker->process);
57 mc_visited_state_t new_state = NULL;
58 new_state = xbt_new0(s_mc_visited_state_t, 1);
59 new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
60 MC_process_get_heap(process)->heaplimit,
61 MC_process_get_malloc_info(process));
63 if (MC_process_is_self(&mc_model_checker->process)) {
64 new_state->nb_processes = xbt_swag_size(simix_global->process_list);
66 MC_process_smx_refresh(&mc_model_checker->process);
67 new_state->nb_processes = xbt_dynar_length(mc_model_checker->process.smx_process_infos);
70 new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
71 new_state->num = mc_stats->expanded_states;
72 new_state->other_num = -1;
76 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)
78 mc_process_t process = &(mc_model_checker->process);
79 mc_visited_pair_t pair = NULL;
80 pair = xbt_new0(s_mc_visited_pair_t, 1);
81 pair->graph_state = graph_state;
82 if(pair->graph_state->system_state == NULL)
83 pair->graph_state->system_state = MC_take_snapshot(pair_num);
84 pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
85 MC_process_get_heap(process)->heaplimit,
86 MC_process_get_malloc_info(process));
87 pair->nb_processes = xbt_swag_size(simix_global->process_list);
88 pair->automaton_state = automaton_state;
91 pair->acceptance_removed = 0;
92 pair->visited_removed = 0;
93 pair->acceptance_pair = 0;
94 pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL);
95 unsigned int cursor = 0;
97 xbt_dynar_foreach(atomic_propositions, cursor, value)
98 xbt_dynar_push_as(pair->atomic_propositions, int, value);
102 static int is_exploration_stack_pair(mc_visited_pair_t pair){
103 xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
105 if (((mc_pair_t)xbt_fifo_get_item_content(item))->num == pair->num){
106 ((mc_pair_t)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
109 item = xbt_fifo_get_next_item(item);
114 void MC_visited_pair_delete(mc_visited_pair_t p)
116 p->automaton_state = NULL;
117 if( !is_exploration_stack_pair(p))
118 MC_state_delete(p->graph_state, 1);
119 xbt_dynar_free(&(p->atomic_propositions));
125 * \brief Find a suitable subrange of candidate duplicates for a given state
126 * \param list dynamic array of states/pairs with candidate duplicates of the current state;
127 * \param ref current state/pair;
128 * \param min (output) index of the beginning of the the subrange
129 * \param max (output) index of the enf of the subrange
131 * Given a suitably ordered array of states/pairs, this function extracts a subrange
132 * (with index *min <= i <= *max) with candidate duplicates of the given state/pair.
133 * This function uses only fast discriminating criterions and does not use the
134 * full state/pair comparison algorithms.
136 * The states/pairs in list MUST be ordered using a (given) weak order
137 * (based on nb_processes and heap_bytes_used).
138 * The subrange is the subrange of "equivalence" of the given state/pair.
140 int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
143 xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
145 int cursor = 0, previous_cursor, next_cursor;
146 int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
149 if (_sg_mc_liveness) {
150 nb_processes = ((mc_visited_pair_t) ref)->nb_processes;
151 heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used;
153 nb_processes = ((mc_visited_state_t) ref)->nb_processes;
154 heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used;
158 int end = xbt_dynar_length(list) - 1;
160 while (start <= end) {
161 cursor = (start + end) / 2;
162 if (_sg_mc_liveness) {
163 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
164 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
165 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
167 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, cursor, mc_visited_state_t);
168 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
169 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
171 if (nb_processes_test < nb_processes) {
173 } else if (nb_processes_test > nb_processes) {
176 if (heap_bytes_used_test < heap_bytes_used) {
178 } else if (heap_bytes_used_test > heap_bytes_used) {
181 *min = *max = cursor;
182 previous_cursor = cursor - 1;
183 while (previous_cursor >= 0) {
184 if (_sg_mc_liveness) {
185 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_pair_t);
186 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
187 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
189 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t);
190 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
191 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
193 if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
195 *min = previous_cursor;
198 next_cursor = cursor + 1;
199 while (next_cursor < xbt_dynar_length(list)) {
200 if (_sg_mc_liveness) {
201 ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
202 nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
203 heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
205 ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t);
206 nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
207 heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
209 if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
214 mmalloc_set_current_heap(heap);
220 mmalloc_set_current_heap(heap);
226 * \brief Checks whether a given state has already been visited by the algorithm.
229 mc_visited_state_t is_visited_state(mc_state_t graph_state)
232 if (_sg_mc_visited == 0)
235 int partial_comm = 0;
237 /* If comm determinism verification, we cannot stop the exploration if some
238 communications are not finished (at least, data are transfered). These communications
239 are incomplete and they cannot be analyzed and compared with the initial pattern. */
240 if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
241 int current_process = 1;
242 while (current_process < MC_smx_get_maxpid()) {
243 if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
244 XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
252 xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
254 mc_visited_state_t new_state = visited_state_new();
255 graph_state->system_state = new_state->system_state;
256 graph_state->in_visited_states = 1;
257 XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
259 if (xbt_dynar_is_empty(visited_states)) {
261 xbt_dynar_push(visited_states, &new_state);
262 mmalloc_set_current_heap(heap);
267 int min = -1, max = -1, index;
269 mc_visited_state_t state_test;
272 index = get_search_interval(visited_states, new_state, &min, &max);
274 if (min != -1 && max != -1) {
276 // Parallell implementation
277 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state);
279 state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t);
280 if(state_test->other_num == -1)
281 new_state->other_num = state_test->num;
283 new_state->other_num = state_test->other_num;
284 if(dot_output == NULL)
285 XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
287 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);
288 xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL);
289 xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state);
292 return new_state->other_num;
295 if(!partial_comm && initial_global_state->initial_communications_pattern_done){
298 while (cursor <= max) {
299 state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
300 if (snapshot_compare(state_test, new_state) == 0) {
301 // The state has been visited:
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 == NULL)
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);
312 /* Replace the old state with the new one (with a bigger num)
313 (when the max number of visited states is reached, the oldest
314 one is removed according to its number (= with the min number) */
315 xbt_dynar_remove_at(visited_states, cursor, NULL);
316 xbt_dynar_insert_at(visited_states, cursor, &new_state);
317 XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
319 mmalloc_set_current_heap(heap);
326 xbt_dynar_insert_at(visited_states, min, &new_state);
327 XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
331 // The state has not been visited: insert the state in the dynamic array.
332 state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
333 if (state_test->nb_processes < new_state->nb_processes) {
334 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
336 if (state_test->heap_bytes_used < new_state->heap_bytes_used)
337 xbt_dynar_insert_at(visited_states, index + 1, &new_state);
339 xbt_dynar_insert_at(visited_states, index, &new_state);
342 XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
346 // We have reached the maximum number of stored states;
347 if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
349 XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
351 // Find the (index of the) older state (with the smallest num):
352 int min2 = mc_stats->expanded_states;
353 unsigned int cursor2 = 0;
354 unsigned int index2 = 0;
355 xbt_dynar_foreach(visited_states, cursor2, state_test){
356 if (!mc_important_snapshot(state_test->system_state) && state_test->num < min2) {
358 min2 = state_test->num;
363 xbt_dynar_remove_at(visited_states, index2, NULL);
364 XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
367 mmalloc_set_current_heap(heap);
373 * \brief Checks whether a given pair has already been visited by the algorithm.
375 int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
377 if (_sg_mc_visited == 0)
380 xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
382 mc_visited_pair_t new_visited_pair = NULL;
384 if (visited_pair == NULL) {
385 new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
387 new_visited_pair = visited_pair;
390 if (xbt_dynar_is_empty(visited_pairs)) {
392 xbt_dynar_push(visited_pairs, &new_visited_pair);
396 int min = -1, max = -1, index;
398 mc_visited_pair_t pair_test;
401 index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
403 if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
404 /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
406 pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t);
407 if(pair_test->other_num == -1)
408 pair->other_num = pair_test->num;
410 pair->other_num = pair_test->other_num;
411 if(dot_output == NULL)
412 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num);
414 XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num);
415 xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL);
416 xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair);
417 pair_test->visited_removed = 1;
418 if(pair_test->stack_removed && pair_test->visited_removed){
419 if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){
420 if(pair_test->acceptance_removed){
421 MC_pair_delete(pair_test);
424 MC_pair_delete(pair_test);
429 return pair->other_num;
432 while (cursor <= max) {
433 pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
434 if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
435 if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
436 if (snapshot_compare(pair_test, new_visited_pair) == 0) {
437 if (pair_test->other_num == -1)
438 new_visited_pair->other_num = pair_test->num;
440 new_visited_pair->other_num = pair_test->other_num;
441 if (dot_output == NULL)
442 XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
444 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);
445 xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
446 xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
447 pair_test->visited_removed = 1;
448 if (pair_test->acceptance_pair) {
449 if (pair_test->acceptance_removed == 1)
450 MC_visited_pair_delete(pair_test);
452 MC_visited_pair_delete(pair_test);
454 mmalloc_set_current_heap(heap);
455 return new_visited_pair->other_num;
461 xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
463 pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
464 if (pair_test->nb_processes < new_visited_pair->nb_processes) {
465 xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
467 if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
468 xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
470 xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
474 if (xbt_dynar_length(visited_pairs) > _sg_mc_visited) {
475 int min2 = mc_stats->expanded_pairs;
476 unsigned int cursor2 = 0;
477 unsigned int index2 = 0;
478 xbt_dynar_foreach(visited_pairs, cursor2, pair_test) {
479 if (!mc_important_snapshot(pair_test->graph_state->system_state) && pair_test->num < min2) {
481 min2 = pair_test->num;
484 xbt_dynar_remove_at(visited_pairs, index2, &pair_test);
485 pair_test->visited_removed = 1;
486 if (pair_test->acceptance_pair) {
487 if (pair_test->acceptance_removed)
488 MC_visited_pair_delete(pair_test);
490 MC_visited_pair_delete(pair_test);
496 mmalloc_set_current_heap(heap);