X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/91c01af98e14d7aa23b1b95199d00aa684434fc6..e18b130366eaef03cef5a1eea2d588d43703981d:/src/mc/mc_visited.cpp diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp index 40db5aad8a..d9f93a2808 100644 --- a/src/mc/mc_visited.cpp +++ b/src/mc/mc_visited.cpp @@ -7,19 +7,34 @@ #include #include -#include "mc_comm_pattern.h" -#include "mc_safety.h" -#include "mc_liveness.h" -#include "mc_private.h" -#include "mc/Process.hpp" -#include "mc_smx.h" +#include +#include +#include +#include +#include + +#include "src/mc/mc_comm_pattern.h" +#include "src/mc/mc_safety.h" +#include "src/mc/mc_liveness.h" +#include "src/mc/mc_private.h" +#include "src/mc/Process.hpp" +#include "src/mc/mc_smx.h" extern "C" { XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc, "Logging specific to state equaity detection mechanisms"); +} + +namespace simgrid { +namespace mc { + xbt_dynar_t visited_pairs; + +} +} + xbt_dynar_t visited_states; static int is_exploration_stack_state(mc_visited_state_t state){ @@ -36,11 +51,11 @@ static int is_exploration_stack_state(mc_visited_state_t state){ void visited_state_free(mc_visited_state_t state) { - if (state) { - if(!is_exploration_stack_state(state)) - delete state->system_state; - xbt_free(state); - } + if (!state) + return; + if(!is_exploration_stack_state(state)) + delete state->system_state; + xbt_free(state); } void visited_state_free_voidp(void *s) @@ -61,30 +76,33 @@ static mc_visited_state_t visited_state_new() process->get_malloc_info()); MC_process_smx_refresh(&mc_model_checker->process()); - new_state->nb_processes = xbt_dynar_length( - mc_model_checker->process().smx_process_infos); + new_state->nb_processes = + mc_model_checker->process().smx_process_infos.size(); - new_state->system_state = MC_take_snapshot(mc_stats->expanded_states); + new_state->system_state = simgrid::mc::take_snapshot(mc_stats->expanded_states); new_state->num = mc_stats->expanded_states; new_state->other_num = -1; 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_state_t graph_state) +namespace simgrid { +namespace mc { + +simgrid::mc::VisitedPair* visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state) { simgrid::mc::Process* process = &(mc_model_checker->process()); - mc_visited_pair_t pair = NULL; - pair = xbt_new0(s_mc_visited_pair_t, 1); + simgrid::mc::VisitedPair* pair = nullptr; + pair = xbt_new0(simgrid::mc::VisitedPair, 1); pair->graph_state = graph_state; - if(pair->graph_state->system_state == NULL) - pair->graph_state->system_state = MC_take_snapshot(pair_num); + if(pair->graph_state->system_state == nullptr) + pair->graph_state->system_state = simgrid::mc::take_snapshot(pair_num); pair->heap_bytes_used = mmalloc_get_bytes_used_remote( process->get_heap()->heaplimit, process->get_malloc_info()); MC_process_smx_refresh(&mc_model_checker->process()); - pair->nb_processes = xbt_dynar_length( - mc_model_checker->process().smx_process_infos); + pair->nb_processes = + mc_model_checker->process().smx_process_infos.size(); pair->automaton_state = automaton_state; pair->num = pair_num; @@ -92,7 +110,7 @@ mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automa pair->acceptance_removed = 0; pair->visited_removed = 0; pair->acceptance_pair = 0; - pair->atomic_propositions = xbt_dynar_new(sizeof(int), NULL); + pair->atomic_propositions = xbt_dynar_new(sizeof(int), nullptr); unsigned int cursor = 0; int value; xbt_dynar_foreach(atomic_propositions, cursor, value) @@ -100,11 +118,11 @@ mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automa return pair; } -static int is_exploration_stack_pair(mc_visited_pair_t pair){ +static int is_exploration_stack_pair(simgrid::mc::VisitedPair* 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; + if (((simgrid::mc::Pair*)xbt_fifo_get_item_content(item))->num == pair->num){ + ((simgrid::mc::Pair*)xbt_fifo_get_item_content(item))->visited_pair_removed = 1; return 1; } item = xbt_fifo_get_next_item(item); @@ -112,14 +130,17 @@ static int is_exploration_stack_pair(mc_visited_pair_t pair){ return 0; } -void MC_visited_pair_delete(mc_visited_pair_t p) +void visited_pair_delete(simgrid::mc::VisitedPair* p) { - p->automaton_state = NULL; + p->automaton_state = nullptr; if( !is_exploration_stack_pair(p)) MC_state_delete(p->graph_state, 1); xbt_dynar_free(&(p->atomic_propositions)); xbt_free(p); - p = NULL; + p = nullptr; +} + +} } /** @@ -145,8 +166,8 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) void *ref_test; if (_sg_mc_liveness) { - nb_processes = ((mc_visited_pair_t) ref)->nb_processes; - heap_bytes_used = ((mc_visited_pair_t) ref)->heap_bytes_used; + nb_processes = ((simgrid::mc::VisitedPair*) ref)->nb_processes; + heap_bytes_used = ((simgrid::mc::VisitedPair*) ref)->heap_bytes_used; } else { nb_processes = ((mc_visited_state_t) ref)->nb_processes; heap_bytes_used = ((mc_visited_state_t) ref)->heap_bytes_used; @@ -158,31 +179,30 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) 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); - nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes; - heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used; + ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, cursor, simgrid::mc::VisitedPair*); + nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes; + heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used; } else { 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; } - if (nb_processes_test < nb_processes) { + if (nb_processes_test < nb_processes) start = cursor + 1; - } else if (nb_processes_test > nb_processes) { + else if (nb_processes_test > nb_processes) end = cursor - 1; - } else { - if (heap_bytes_used_test < heap_bytes_used) { - start = cursor + 1; - } else if (heap_bytes_used_test > heap_bytes_used) { - end = cursor - 1; - } else { + else if (heap_bytes_used_test < heap_bytes_used) + start = cursor + 1; + else if (heap_bytes_used_test > heap_bytes_used) + end = cursor - 1; + else { *min = *max = cursor; 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); - nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes; - heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used; + ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, previous_cursor, simgrid::mc::VisitedPair*); + nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes; + heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used; } else { 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; @@ -196,9 +216,9 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) size_t 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); - nb_processes_test = ((mc_visited_pair_t) ref_test)->nb_processes; - heap_bytes_used_test = ((mc_visited_pair_t) ref_test)->heap_bytes_used; + ref_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(list, next_cursor, simgrid::mc::VisitedPair*); + nb_processes_test = ((simgrid::mc::VisitedPair*) ref_test)->nb_processes; + heap_bytes_used_test = ((simgrid::mc::VisitedPair*) ref_test)->heap_bytes_used; } else { 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; @@ -210,7 +230,6 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) next_cursor++; } return -1; - } } } return cursor; @@ -225,7 +244,7 @@ void replace_state( else new_state->other_num = state_test->other_num; - if (dot_output == NULL) + if (dot_output == nullptr) XBT_DEBUG("State %d already visited ! (equal to state %d)", new_state->num, state_test->num); else @@ -236,7 +255,7 @@ void replace_state( /* 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_remove_at(visited_states, cursor, nullptr); 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); @@ -262,9 +281,8 @@ bool some_dommunications_are_not_finished() mc_visited_state_t is_visited_state(mc_state_t graph_state) { - if (_sg_mc_visited == 0) - return NULL; + return nullptr; /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at least, data are transfered). These communications @@ -278,11 +296,9 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state) 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); - return NULL; - - } else { + return nullptr; + } int min = -1, max = -1, index; @@ -290,23 +306,6 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state) if (min != -1 && max != -1) { - // Parallell implementation - /*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(visited_states, min), (max-min)+1, new_state); - if(res != -1){ - mc_visited_state_t state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, (min+res)-1, mc_visited_state_t); - 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); - xbt_dynar_remove_at(visited_states, (min + res) - 1, NULL); - xbt_dynar_insert_at(visited_states, (min+res) - 1, &new_state); - return new_state->other_num; - } */ - if (_sg_mc_safety || (!partial_comm && initial_global_state->initial_communications_pattern_done)) { @@ -330,21 +329,21 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state) // The state has not been visited: insert the state in the dynamic array. 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) { + if (state_test->nb_processes < new_state->nb_processes) xbt_dynar_insert_at(visited_states, index + 1, &new_state); - } else { - if (state_test->heap_bytes_used < new_state->heap_bytes_used) - xbt_dynar_insert_at(visited_states, index + 1, &new_state); - else - xbt_dynar_insert_at(visited_states, index, &new_state); - } + else if (state_test->heap_bytes_used < new_state->heap_bytes_used) + 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 ((ssize_t) xbt_dynar_length(visited_states) > _sg_mc_visited) { + if ((ssize_t) xbt_dynar_length(visited_states) <= _sg_mc_visited) + return nullptr; + + // We have reached the maximum number of stored states; XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)"); @@ -354,81 +353,55 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state) unsigned int index2 = 0; mc_visited_state_t state_test; - xbt_dynar_foreach(visited_states, cursor2, state_test){ + xbt_dynar_foreach(visited_states, cursor2, state_test) if (!mc_model_checker->is_important_snapshot(*state_test->system_state) && state_test->num < min2) { index2 = cursor2; min2 = state_test->num; } - } // and drop it: - xbt_dynar_remove_at(visited_states, index2, NULL); + xbt_dynar_remove_at(visited_states, index2, nullptr); XBT_DEBUG("Remove visited state (maximum number of stored states reached)"); - } - return NULL; - } + return nullptr; } +namespace simgrid { +namespace mc { + /** * \brief Checks whether a given pair has already been visited by the algorithm. */ -int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) { +int is_visited_pair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair) { if (_sg_mc_visited == 0) return -1; - mc_visited_pair_t new_visited_pair = NULL; - - if (visited_pair == NULL) { - new_visited_pair = MC_visited_pair_new(pair->num, pair->automaton_state, pair->atomic_propositions, pair->graph_state); - } else { + simgrid::mc::VisitedPair* new_visited_pair = nullptr; + if (visited_pair == nullptr) + new_visited_pair = simgrid::mc::visited_pair_new( + pair->num, pair->automaton_state, pair->atomic_propositions, + pair->graph_state); + else new_visited_pair = visited_pair; - } if (xbt_dynar_is_empty(visited_pairs)) { - xbt_dynar_push(visited_pairs, &new_visited_pair); - - } else { + return -1; + } int min = -1, max = -1, index; //int res; - mc_visited_pair_t pair_test; + simgrid::mc::VisitedPair* pair_test; int cursor; 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); - if(res != -1){ - pair_test = (mc_pair_t)xbt_dynar_get_as(visited_pairs, (min+res)-1, mc_pair_t); - if(pair_test->other_num == -1) - pair->other_num = pair_test->num; - else - pair->other_num = pair_test->other_num; - if(dot_output == NULL) - XBT_DEBUG("Pair %d already visited ! (equal to pair %d)", pair->num, pair_test->num); - else - XBT_DEBUG("Pair %d already visited ! (equal to pair %d (pair %d in dot_output))", pair->num, pair_test->num, pair->other_num); - xbt_dynar_remove_at(visited_pairs, (min + res) - 1, NULL); - xbt_dynar_insert_at(visited_pairs, (min+res) - 1, &pair); - pair_test->visited_removed = 1; - if(pair_test->stack_removed && pair_test->visited_removed){ - if((pair_test->automaton_state->type == 1) || (pair_test->automaton_state->type == 2)){ - if(pair_test->acceptance_removed){ - MC_pair_delete(pair_test); - } - }else{ - MC_pair_delete(pair_test); - } - } - return pair->other_num; - } */ cursor = min; while (cursor <= max) { - pair_test = (mc_visited_pair_t) xbt_dynar_get_as(visited_pairs, cursor, mc_visited_pair_t); + pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, cursor, simgrid::mc::VisitedPair*); 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) { @@ -436,19 +409,16 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) { new_visited_pair->other_num = pair_test->num; else new_visited_pair->other_num = pair_test->other_num; - if (dot_output == NULL) + if (dot_output == nullptr) 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_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) - MC_visited_pair_delete(pair_test); - } else { - MC_visited_pair_delete(pair_test); - } + if (!pair_test->acceptance_pair + || pair_test->acceptance_removed == 1) + simgrid::mc::visited_pair_delete(pair_test); return new_visited_pair->other_num; } } @@ -457,15 +427,13 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t 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_visited_pair->nb_processes) { + pair_test = (simgrid::mc::VisitedPair*) xbt_dynar_get_as(visited_pairs, index, simgrid::mc::VisitedPair*); + 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_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_visited_pair); - } + else 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_visited_pair); } if ((ssize_t) xbt_dynar_length(visited_pairs) > _sg_mc_visited) { @@ -481,16 +449,11 @@ int is_visited_pair(mc_visited_pair_t visited_pair, mc_pair_t pair) { } xbt_dynar_remove_at(visited_pairs, index2, &pair_test); pair_test->visited_removed = 1; - if (pair_test->acceptance_pair) { - if (pair_test->acceptance_removed) - MC_visited_pair_delete(pair_test); - } else { - MC_visited_pair_delete(pair_test); - } + if (!pair_test->acceptance_pair || pair_test->acceptance_removed) + simgrid::mc::visited_pair_delete(pair_test); } - - } return -1; } } +} \ No newline at end of file