xbt_dynar_t visited_pairs;
xbt_dynar_t visited_states;
+static int is_exploration_stack_state(mc_visited_state_t state){
+ xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
+ while (item) {
+ if (((mc_state_t)xbt_fifo_get_item_content(item))->num == state->num){
+ ((mc_state_t)xbt_fifo_get_item_content(item))->in_visited_states = 0;
+ return 1;
+ }
+ item = xbt_fifo_get_next_item(item);
+ }
+ return 0;
+}
+
void visited_state_free(mc_visited_state_t state)
{
if (state) {
- MC_free_snapshot(state->system_state);
+ if(!is_exploration_stack_state(state)){
+ MC_free_snapshot(state->system_state);
+ }
xbt_free(state);
}
}
*/
static mc_visited_state_t visited_state_new()
{
+ mc_process_t process = &(mc_model_checker->process);
mc_visited_state_t new_state = NULL;
new_state = xbt_new0(s_mc_visited_state_t, 1);
- new_state->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
+ new_state->heap_bytes_used = mmalloc_get_bytes_used_remote(
+ MC_process_get_heap(process)->heaplimit,
+ MC_process_get_malloc_info(process));
new_state->nb_processes = xbt_swag_size(simix_global->process_list);
new_state->system_state = MC_take_snapshot(mc_stats->expanded_states);
new_state->num = mc_stats->expanded_states;
return new_state;
}
-
-mc_visited_pair_t MC_visited_pair_new(int pair_num,
- xbt_automaton_state_t automaton_state,
- xbt_dynar_t atomic_propositions)
+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)
{
+ mc_process_t process = &(mc_model_checker->process);
mc_visited_pair_t pair = NULL;
pair = xbt_new0(s_mc_visited_pair_t, 1);
- pair->graph_state = MC_state_new();
- pair->graph_state->system_state = MC_take_snapshot(pair_num);
- pair->heap_bytes_used = mmalloc_get_bytes_used(std_heap);
+ pair->graph_state = graph_state;
+ if(pair->graph_state->system_state == NULL)
+ pair->graph_state->system_state = MC_take_snapshot(pair_num);
+ pair->heap_bytes_used = mmalloc_get_bytes_used_remote(
+ MC_process_get_heap(process)->heaplimit,
+ MC_process_get_malloc_info(process));
pair->nb_processes = xbt_swag_size(simix_global->process_list);
pair->automaton_state = automaton_state;
pair->num = pair_num;
return pair;
}
+static int is_exploration_stack_pair(mc_visited_pair_t pair){
+ xbt_fifo_item_t item = xbt_fifo_get_first_item(mc_stack);
+ while (item) {
+ if (((mc_pair_t)xbt_fifo_get_item_content(item))->num == pair->num){
+ ((mc_pair_t)xbt_fifo_get_item_content(item))->visited_pair_removed = 1;
+ return 1;
+ }
+ item = xbt_fifo_get_next_item(item);
+ }
+ return 0;
+}
+
void MC_visited_pair_delete(mc_visited_pair_t p)
{
p->automaton_state = NULL;
- MC_state_delete(p->graph_state);
+ if( !is_exploration_stack_pair(p))
+ MC_state_delete(p->graph_state, 1);
xbt_dynar_free(&(p->atomic_propositions));
xbt_free(p);
p = NULL;
int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max)
{
- int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
int cursor = 0, previous_cursor, next_cursor;
int nb_processes, heap_bytes_used, nb_processes_test, heap_bytes_used_test;
while (start <= end) {
cursor = (start + end) / 2;
if (_sg_mc_liveness) {
- ref_test =
- (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
+ ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, cursor, mc_visited_pair_t);
nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
} else {
- ref_test =
- (mc_visited_state_t) xbt_dynar_get_as(list, cursor,
- mc_visited_state_t);
+ ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, cursor, mc_visited_state_t);
nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
}
previous_cursor = cursor - 1;
while (previous_cursor >= 0) {
if (_sg_mc_liveness) {
- ref_test =
- (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor,
- mc_visited_pair_t);
+ ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_pair_t);
nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
- heap_bytes_used_test =
- ((mc_visited_pair_t) ref_test)->heap_bytes_used;
+ heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
} else {
- ref_test =
- (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor,
- mc_visited_state_t);
+ ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, previous_cursor, mc_visited_state_t);
nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
- heap_bytes_used_test =
- ((mc_visited_state_t) ref_test)->heap_bytes_used;
+ heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
}
- if (nb_processes_test != nb_processes
- || heap_bytes_used_test != heap_bytes_used)
+ if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
break;
*min = previous_cursor;
previous_cursor--;
next_cursor = cursor + 1;
while (next_cursor < xbt_dynar_length(list)) {
if (_sg_mc_liveness) {
- ref_test =
- (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor,
- mc_visited_pair_t);
+ ref_test = (mc_visited_pair_t) xbt_dynar_get_as(list, next_cursor, mc_visited_pair_t);
nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes;
- heap_bytes_used_test =
- ((mc_visited_pair_t) ref_test)->heap_bytes_used;
+ heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used;
} else {
- ref_test =
- (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor,
- mc_visited_state_t);
+ ref_test = (mc_visited_state_t) xbt_dynar_get_as(list, next_cursor, mc_visited_state_t);
nb_processes_test = ((mc_visited_state_t) ref_test)->nb_processes;
- heap_bytes_used_test =
- ((mc_visited_state_t) ref_test)->heap_bytes_used;
+ heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used;
}
- if (nb_processes_test != nb_processes
- || heap_bytes_used_test != heap_bytes_used)
+ if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used)
break;
*max = next_cursor;
next_cursor++;
}
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
+ mmalloc_set_current_heap(heap);
return -1;
}
}
}
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
-
+ mmalloc_set_current_heap(heap);
return cursor;
}
* \brief Checks whether a given state has already been visited by the algorithm.
*/
-mc_visited_state_t is_visited_state()
+mc_visited_state_t is_visited_state(mc_state_t graph_state)
{
if (_sg_mc_visited == 0)
return NULL;
+ int partial_comm = 0;
+
/* If comm determinism verification, we cannot stop the exploration if some
communications are not finished (at least, data are transfered). These communications
- are incomplete and they cannot be analyzed and compared with the initial pattern */
+ are incomplete and they cannot be analyzed and compared with the initial pattern. */
if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
int current_process = 1;
- while (current_process < simix_process_maxpid) {
- if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t)))
- return NULL;
+ while (current_process < MC_smx_get_maxpid()) {
+ if (!xbt_dynar_is_empty((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, current_process, xbt_dynar_t))){
+ XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
+ partial_comm = 1;
+ break;
+ }
current_process++;
}
}
- int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
mc_visited_state_t new_state = visited_state_new();
+ graph_state->system_state = new_state->system_state;
+ graph_state->in_visited_states = 1;
+ XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)", new_state->system_state, new_state->num, graph_state->num);
if (xbt_dynar_is_empty(visited_states)) {
xbt_dynar_push(visited_states, &new_state);
-
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
-
+ mmalloc_set_current_heap(heap);
return NULL;
} else {
return new_state->other_num;
} */
- cursor = min;
- while (cursor <= max) {
- state_test =
- (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor,
- mc_visited_state_t);
- if (snapshot_compare(state_test, new_state) == 0) {
- // The state has been visited:
-
- if (state_test->other_num == -1)
- new_state->other_num = state_test->num;
- else
- new_state->other_num = state_test->other_num;
- if (dot_output == NULL)
- XBT_DEBUG("State %d already visited ! (equal to state %d)",
- new_state->num, state_test->num);
- else
- 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);
-
- /* Replace the old state with the new one (with a bigger num)
- (when the max number of visited states is reached, the oldest
- one is removed according to its number (= with the min number) */
- xbt_dynar_remove_at(visited_states, cursor, NULL);
- xbt_dynar_insert_at(visited_states, cursor, &new_state);
-
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
- return state_test;
+ if(!partial_comm && initial_global_state->initial_communications_pattern_done){
+
+ cursor = min;
+ while (cursor <= max) {
+ state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
+ if (snapshot_compare(state_test, new_state) == 0) {
+ // The state has been visited:
+
+ if (state_test->other_num == -1)
+ new_state->other_num = state_test->num;
+ else
+ new_state->other_num = state_test->other_num;
+ if (dot_output == NULL)
+ XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num);
+ else
+ 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);
+
+ /* Replace the old state with the new one (with a bigger num)
+ (when the max number of visited states is reached, the oldest
+ one is removed according to its number (= with the min number) */
+ xbt_dynar_remove_at(visited_states, cursor, NULL);
+ xbt_dynar_insert_at(visited_states, cursor, &new_state);
+ XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num);
+
+ mmalloc_set_current_heap(heap);
+ return state_test;
+ }
+ cursor++;
}
- cursor++;
}
-
- // The state has not been visited: insert the state in the dynamic array.
+
xbt_dynar_insert_at(visited_states, min, &new_state);
-
+ XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
+
} else {
// The state has not been visited: insert the state in the dynamic array.
- state_test =
- (mc_visited_state_t) xbt_dynar_get_as(visited_states, index,
- mc_visited_state_t);
+ state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, index, mc_visited_state_t);
if (state_test->nb_processes < new_state->nb_processes) {
xbt_dynar_insert_at(visited_states, index + 1, &new_state);
} else {
xbt_dynar_insert_at(visited_states, index, &new_state);
}
+ XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, xbt_dynar_length(visited_states));
+
}
// We have reached the maximum number of stored states;
if (xbt_dynar_length(visited_states) > _sg_mc_visited) {
+ XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
+
// Find the (index of the) older state (with the smallest num):
int min2 = mc_stats->expanded_states;
unsigned int cursor2 = 0;
// and drop it:
xbt_dynar_remove_at(visited_states, index2, NULL);
+ XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
}
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
-
+ mmalloc_set_current_heap(heap);
return NULL;
-
}
}
/**
* \brief Checks whether a given pair has already been visited by the algorithm.
*/
-int is_visited_pair(mc_visited_pair_t pair, int pair_num,
- xbt_automaton_state_t automaton_state,
- xbt_dynar_t atomic_propositions)
-{
+int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) {
if (_sg_mc_visited == 0)
return -1;
- int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
- MC_SET_MC_HEAP;
+ xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
- mc_visited_pair_t new_pair = NULL;
+ mc_visited_pair_t new_visited_pair = NULL;
- if (pair == NULL) {
- new_pair =
- MC_visited_pair_new(pair_num, automaton_state, atomic_propositions);
+ if (visited_pair == NULL) {
+ new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state);
} else {
- new_pair = pair;
+ new_visited_pair = visited_pair;
}
if (xbt_dynar_is_empty(visited_pairs)) {
- xbt_dynar_push(visited_pairs, &new_pair);
+ xbt_dynar_push(visited_pairs, &new_visited_pair);
} else {
mc_visited_pair_t pair_test;
int cursor;
- index = get_search_interval(visited_pairs, new_pair, &min, &max);
+ index = get_search_interval(visited_pairs, new_visited_pair, &min, &max);
if (min != -1 && max != -1) { // Visited pair with same number of processes and same heap bytes used exists
/*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_pairs, min), (max-min)+1, pair);
} */
cursor = min;
while (cursor <= max) {
- pair_test =
- (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor,
- mc_visited_pair_t);
- if (xbt_automaton_state_compare
- (pair_test->automaton_state, new_pair->automaton_state) == 0) {
- if (xbt_automaton_propositional_symbols_compare_value
- (pair_test->atomic_propositions,
- new_pair->atomic_propositions) == 0) {
- if (snapshot_compare(pair_test, new_pair) == 0) {
+ pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t);
+ if (xbt_automaton_state_compare(pair_test->automaton_state, new_visited_pair->automaton_state) == 0) {
+ if (xbt_automaton_propositional_symbols_compare_value(pair_test->atomic_propositions, new_visited_pair->atomic_propositions) == 0) {
+ if (snapshot_compare(pair_test, new_visited_pair) == 0) {
if (pair_test->other_num == -1)
- new_pair->other_num = pair_test->num;
+ new_visited_pair->other_num = pair_test->num;
else
- new_pair->other_num = pair_test->other_num;
+ new_visited_pair->other_num = pair_test->other_num;
if (dot_output == NULL)
- XBT_DEBUG("Pair %d already visited ! (equal to pair %d)",
- new_pair->num, pair_test->num);
+ XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", new_visited_pair->num, pair_test->num);
else
- XBT_DEBUG
- ("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))",
- new_pair->num, pair_test->num, new_pair->other_num);
- xbt_dynar_remove_at(visited_pairs, cursor, NULL);
- xbt_dynar_insert_at(visited_pairs, cursor, &new_pair);
+ 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);
+ xbt_dynar_remove_at(visited_pairs, cursor, &pair_test);
+ xbt_dynar_insert_at(visited_pairs, cursor, &new_visited_pair);
pair_test->visited_removed = 1;
if (pair_test->acceptance_pair) {
if (pair_test->acceptance_removed == 1)
} else {
MC_visited_pair_delete(pair_test);
}
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
- return new_pair->other_num;
+ mmalloc_set_current_heap(heap);
+ return new_visited_pair->other_num;
}
}
}
cursor++;
}
- xbt_dynar_insert_at(visited_pairs, min, &new_pair);
+ xbt_dynar_insert_at(visited_pairs, min, &new_visited_pair);
} else {
- pair_test =
- (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index,
- mc_visited_pair_t);
- if (pair_test->nb_processes < new_pair->nb_processes) {
- xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
+ pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, index, mc_visited_pair_t);
+ if (pair_test->nb_processes < new_visited_pair->nb_processes) {
+ xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
} else {
- if (pair_test->heap_bytes_used < new_pair->heap_bytes_used)
- xbt_dynar_insert_at(visited_pairs, index + 1, &new_pair);
+ if (pair_test->heap_bytes_used < new_visited_pair->heap_bytes_used)
+ xbt_dynar_insert_at(visited_pairs, index + 1, &new_visited_pair);
else
- xbt_dynar_insert_at(visited_pairs, index, &new_pair);
+ xbt_dynar_insert_at(visited_pairs, index, &new_visited_pair);
}
}
}
- if (!mc_mem_set)
- MC_SET_STD_HEAP;
-
+ mmalloc_set_current_heap(heap);
return -1;
}
