From: Gabriel Corona Date: Tue, 8 Mar 2016 13:07:14 +0000 (+0100) Subject: [mc] Move mc_safety code in simgrid::mc X-Git-Tag: v3_13~478 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/269fcd3a8b8e4ae311a99640e3993bdc30b98a5b [mc] Move mc_safety code in simgrid::mc --- diff --git a/include/xbt/dynar.hpp b/include/xbt/dynar.hpp index a1b49c7643..2129007223 100644 --- a/include/xbt/dynar.hpp +++ b/include/xbt/dynar.hpp @@ -32,6 +32,22 @@ DynarRange range(xbt_dynar_t dynar) (T*) ((char*) dynar->data + dynar->used * dynar->elmsize)); } +/** Dynar of `T*` which `delete` its values */ +template inline +xbt_dynar_t newDeleteDynar() +{ + return xbt_dynar_new(sizeof(T*), + [](void* p) { delete *(T**)p; }); +} + +/** Dynar of `T*` which `destroy()` its values */ +template inline +xbt_dynar_t newDestroyDynar() +{ + return xbt_dynar_new(sizeof(T*), + [](void* p) { simgrid::xbt::destroy(*(T**)p); }); +} + } } #endif diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp index 410510d9d4..f1119d2330 100644 --- a/src/mc/mc_comm_determinism.cpp +++ b/src/mc/mc_comm_determinism.cpp @@ -7,6 +7,7 @@ #include #include +#include #include #include #include @@ -304,7 +305,7 @@ static void MC_pre_modelcheck_comm_determinism(void) const int maxpid = MC_smx_get_maxpid(); if (_sg_mc_visited > 0) - visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); + simgrid::mc::visited_states = simgrid::xbt::newDeleteDynar(); // Create initial_communications_pattern elements: initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), MC_list_comm_pattern_free_voidp); @@ -342,7 +343,7 @@ static int MC_modelcheck_comm_determinism_main(void) char *req_str = nullptr; int value; - mc_visited_state_t visited_state = nullptr; + simgrid::mc::VisitedState* visited_state = nullptr; smx_simcall_t req = nullptr; mc_state_t state = nullptr, next_state = NULL; @@ -392,7 +393,7 @@ static int MC_modelcheck_comm_determinism_main(void) /* Create the new expanded state */ next_state = MC_state_new(); - if ((visited_state = is_visited_state(next_state)) == nullptr) { + if ((visited_state = simgrid::mc::is_visited_state(next_state)) == nullptr) { /* Get enabled processes and insert them in the interleave set of the next state */ for (auto& p : mc_model_checker->process().simix_processes()) @@ -462,7 +463,7 @@ static int MC_modelcheck_comm_determinism_main(void) int MC_modelcheck_comm_determinism(void) { XBT_INFO("Check communication determinism"); - mc_reduce_kind = e_mc_reduce_none; + simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none; mc_model_checker->wait_for_requests(); if (mc_mode == MC_MODE_CLIENT) diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp index 9b65001dcd..4afbc7951e 100644 --- a/src/mc/mc_compare.cpp +++ b/src/mc/mc_compare.cpp @@ -369,10 +369,10 @@ int snapshot_compare(void *state1, void *state2) num1 = ((mc_state_t) state1)->num; num2 = ((mc_state_t) state2)->num; } else { /* Safety or comm determinism MC */ - s1 = ((mc_visited_state_t) state1)->system_state; - s2 = ((mc_visited_state_t) state2)->system_state; - num1 = ((mc_visited_state_t) state1)->num; - num2 = ((mc_visited_state_t) state2)->num; + s1 = ((simgrid::mc::VisitedState*) state1)->system_state; + s2 = ((simgrid::mc::VisitedState*) state2)->system_state; + num1 = ((simgrid::mc::VisitedState*) state1)->num; + num2 = ((simgrid::mc::VisitedState*) state2)->num; } int errors = 0; diff --git a/src/mc/mc_config.cpp b/src/mc/mc_config.cpp index 244b4a0046..d7752f16f3 100644 --- a/src/mc/mc_config.cpp +++ b/src/mc/mc_config.cpp @@ -25,9 +25,15 @@ extern "C" { XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_config, mc, "Configuration of MC"); +} + #ifdef HAVE_MC +namespace simgrid { +namespace mc { /* Configuration support */ -e_mc_reduce_t mc_reduce_kind = e_mc_reduce_unset; +simgrid::mc::ReductionMode reduction_mode = simgrid::mc::ReductionMode::unset; +} +} #endif #ifndef HAVE_MC @@ -72,9 +78,9 @@ void _mc_cfg_cb_reduce(const char *name, int pos) char *val = xbt_cfg_get_string(_sg_cfg_set, name); if (!strcasecmp(val, "none")) - mc_reduce_kind = e_mc_reduce_none; + simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none; else if (!strcasecmp(val, "dpor")) - mc_reduce_kind = e_mc_reduce_dpor; + simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::dpor; else xbt_die("configuration option %s can only take 'none' or 'dpor' as a value", name); @@ -196,5 +202,3 @@ void _mc_cfg_cb_termination(const char *name, int pos) } #endif - -} diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp index b45c70c3ae..718fe43bb1 100644 --- a/src/mc/mc_liveness.cpp +++ b/src/mc/mc_liveness.cpp @@ -379,8 +379,8 @@ static int MC_modelcheck_liveness_main(void) int modelcheck_liveness(void) { - if (mc_reduce_kind == e_mc_reduce_unset) - mc_reduce_kind = e_mc_reduce_none; + if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::unset) + simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none; XBT_INFO("Check the liveness property %s", _sg_mc_property_file); MC_automaton_load(_sg_mc_property_file); mc_model_checker->wait_for_requests(); diff --git a/src/mc/mc_request.cpp b/src/mc/mc_request.cpp index 29d008efda..d6be4512d5 100644 --- a/src/mc/mc_request.cpp +++ b/src/mc/mc_request.cpp @@ -140,7 +140,7 @@ bool request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2) // Those are MC_state_get_internal_request(state) bool request_depend(smx_simcall_t r1, smx_simcall_t r2) { - if (mc_reduce_kind == e_mc_reduce_none) + if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::none) return true; if (r1->issuer == r2->issuer) diff --git a/src/mc/mc_safety.cpp b/src/mc/mc_safety.cpp index bd63a0ab69..74fde12485 100644 --- a/src/mc/mc_safety.cpp +++ b/src/mc/mc_safety.cpp @@ -10,6 +10,7 @@ #include #include +#include #include #include @@ -31,6 +32,9 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc, } +namespace simgrid { +namespace mc { + static int is_exploration_stack_state(mc_state_t current_state){ xbt_fifo_item_t item; @@ -45,15 +49,15 @@ static int is_exploration_stack_state(mc_state_t current_state){ return 0; } -static void MC_modelcheck_safety_init(void); +static void modelcheck_safety_init(void); /** * \brief Initialize the DPOR exploration algorithm */ -static void MC_pre_modelcheck_safety() +static void pre_modelcheck_safety() { if (_sg_mc_visited > 0) - visited_states = xbt_dynar_new(sizeof(mc_visited_state_t), visited_state_free_voidp); + simgrid::mc::visited_states = simgrid::xbt::newDeleteDynar(); mc_state_t initial_state = MC_state_new(); @@ -67,7 +71,7 @@ static void MC_pre_modelcheck_safety() for (auto& p : mc_model_checker->process().simix_processes()) if (simgrid::mc::process_is_enabled(&p.copy)) { MC_state_interleave_process(initial_state, &p.copy); - if (mc_reduce_kind != e_mc_reduce_none) + if (simgrid::mc::reduction_mode != simgrid::mc::ReductionMode::none) break; } @@ -78,16 +82,16 @@ static void MC_pre_modelcheck_safety() /** \brief Model-check the application using a DFS exploration * with DPOR (Dynamic Partial Order Reductions) */ -int MC_modelcheck_safety(void) +int modelcheck_safety(void) { - MC_modelcheck_safety_init(); + modelcheck_safety_init(); char *req_str = nullptr; int value; smx_simcall_t req = nullptr; mc_state_t state = nullptr, prev_state = NULL, next_state = NULL; xbt_fifo_item_t item = nullptr; - mc_visited_state_t visited_state = nullptr; + simgrid::mc::VisitedState* visited_state = nullptr; while (xbt_fifo_size(mc_stack) > 0) { @@ -133,13 +137,13 @@ int MC_modelcheck_safety(void) return SIMGRID_MC_EXIT_NON_TERMINATION; } - if ((visited_state = is_visited_state(next_state)) == nullptr) { + if ((visited_state = simgrid::mc::is_visited_state(next_state)) == nullptr) { /* Get an enabled process and insert it in the interleave set of the next state */ for (auto& p : mc_model_checker->process().simix_processes()) if (simgrid::mc::process_is_enabled(&p.copy)) { MC_state_interleave_process(next_state, &p.copy); - if (mc_reduce_kind != e_mc_reduce_none) + if (simgrid::mc::reduction_mode != simgrid::mc::ReductionMode::none) break; } @@ -193,7 +197,7 @@ int MC_modelcheck_safety(void) state that executed that previous request. */ while ((state = (mc_state_t) xbt_fifo_shift(mc_stack))) { - if (mc_reduce_kind == e_mc_reduce_dpor) { + if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::dpor) { req = MC_state_get_internal_request(state); if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK) xbt_die("Mutex is currently not supported with DPOR, " @@ -258,12 +262,12 @@ int MC_modelcheck_safety(void) return SIMGRID_MC_EXIT_SUCCESS; } -static void MC_modelcheck_safety_init(void) +static void modelcheck_safety_init(void) { if(_sg_mc_termination) - mc_reduce_kind = e_mc_reduce_none; - else if (mc_reduce_kind == e_mc_reduce_unset) - mc_reduce_kind = e_mc_reduce_dpor; + simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::none; + else if (simgrid::mc::reduction_mode == simgrid::mc::ReductionMode::unset) + simgrid::mc::reduction_mode = simgrid::mc::ReductionMode::dpor; _sg_mc_safety = 1; if (_sg_mc_termination) XBT_INFO("Check non progressive cycles"); @@ -278,9 +282,12 @@ static void MC_modelcheck_safety_init(void) /* Create exploration stack */ mc_stack = xbt_fifo_new(); - MC_pre_modelcheck_safety(); + pre_modelcheck_safety(); /* Save the initial state */ initial_global_state = xbt_new0(s_mc_global_t, 1); initial_global_state->snapshot = simgrid::mc::take_snapshot(0); } + +} +} diff --git a/src/mc/mc_safety.h b/src/mc/mc_safety.h index 46c5ec95dc..931584bb40 100644 --- a/src/mc/mc_safety.h +++ b/src/mc/mc_safety.h @@ -17,31 +17,34 @@ #include "src/mc/mc_forward.hpp" #include "src/mc/mc_state.h" -SG_BEGIN_DECL() +namespace simgrid { +namespace mc { -typedef enum { - e_mc_reduce_unset, - e_mc_reduce_none, - e_mc_reduce_dpor -} e_mc_reduce_t; +enum class ReductionMode { + unset, + none, + dpor, +}; -extern XBT_PRIVATE e_mc_reduce_t mc_reduce_kind; +extern XBT_PRIVATE simgrid::mc::ReductionMode reduction_mode; -int MC_modelcheck_safety(void); +int modelcheck_safety(void); -typedef struct XBT_PRIVATE s_mc_visited_state{ +struct XBT_PRIVATE VisitedState { mc_snapshot_t system_state; size_t heap_bytes_used; int nb_processes; int num; int other_num; // dot_output for -}s_mc_visited_state_t, *mc_visited_state_t; + + VisitedState(); + ~VisitedState(); +}; extern XBT_PRIVATE xbt_dynar_t visited_states; -XBT_PRIVATE mc_visited_state_t is_visited_state(mc_state_t graph_state); -XBT_PRIVATE void visited_state_free(mc_visited_state_t state); -XBT_PRIVATE void visited_state_free_voidp(void *s); +XBT_PRIVATE simgrid::mc::VisitedState* is_visited_state(mc_state_t graph_state); -SG_END_DECL() +} +} #endif diff --git a/src/mc/mc_visited.cpp b/src/mc/mc_visited.cpp index 80525901c7..8b084b5e8f 100644 --- a/src/mc/mc_visited.cpp +++ b/src/mc/mc_visited.cpp @@ -31,13 +31,9 @@ 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){ +static int is_exploration_stack_state(simgrid::mc::VisitedState* 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){ @@ -49,44 +45,30 @@ static int is_exploration_stack_state(mc_visited_state_t state){ return 0; } -void visited_state_free(mc_visited_state_t state) -{ - if (!state) - return; - if(!is_exploration_stack_state(state)) - delete state->system_state; - xbt_free(state); -} - -void visited_state_free_voidp(void *s) -{ - visited_state_free((mc_visited_state_t) * (void **) s); -} - /** * \brief Save the current state * \return Snapshot of the current state. */ -static mc_visited_state_t visited_state_new() +VisitedState::VisitedState() { simgrid::mc::Process* process = &(mc_model_checker->process()); - mc_visited_state_t new_state = xbt_new0(s_mc_visited_state_t, 1); - new_state->heap_bytes_used = mmalloc_get_bytes_used_remote( + this->heap_bytes_used = mmalloc_get_bytes_used_remote( process->get_heap()->heaplimit, process->get_malloc_info()); MC_process_smx_refresh(&mc_model_checker->process()); - new_state->nb_processes = + this->nb_processes = mc_model_checker->process().smx_process_infos.size(); - 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; + this->num = mc_stats->expanded_states; + this->other_num = -1; } -namespace simgrid { -namespace mc { +VisitedState::~VisitedState() +{ + if(!is_exploration_stack_state(this)) + delete this->system_state; +} VisitedPair::VisitedPair(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state) { @@ -165,8 +147,8 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) 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; + nb_processes = ((simgrid::mc::VisitedState*) ref)->nb_processes; + heap_bytes_used = ((simgrid::mc::VisitedState*) ref)->heap_bytes_used; } int start = 0; @@ -179,9 +161,9 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) 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; + ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, cursor, simgrid::mc::VisitedState*); + nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes; + heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used; } if (nb_processes_test < nb_processes) start = cursor + 1; @@ -200,9 +182,9 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) 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; - heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used; + ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, previous_cursor, simgrid::mc::VisitedState*); + nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes; + heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used; } if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used) break; @@ -216,9 +198,9 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) 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; - heap_bytes_used_test = ((mc_visited_state_t) ref_test)->heap_bytes_used; + ref_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(list, next_cursor, simgrid::mc::VisitedState*); + nb_processes_test = ((simgrid::mc::VisitedState*) ref_test)->nb_processes; + heap_bytes_used_test = ((simgrid::mc::VisitedState*) ref_test)->heap_bytes_used; } if (nb_processes_test != nb_processes || heap_bytes_used_test != heap_bytes_used) break; @@ -233,7 +215,7 @@ int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max) static void replace_state( - mc_visited_state_t state_test, mc_visited_state_t new_state, int cursor) + simgrid::mc::VisitedState* state_test, simgrid::mc::VisitedState* new_state, int cursor) { if (state_test->other_num == -1) new_state->other_num = state_test->num; @@ -251,8 +233,8 @@ 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, nullptr); - xbt_dynar_insert_at(visited_states, cursor, &new_state); + xbt_dynar_remove_at(simgrid::mc::visited_states, cursor, nullptr); + xbt_dynar_insert_at(simgrid::mc::visited_states, cursor, &new_state); XBT_DEBUG("Replace visited state %d with the new visited state %d", state_test->num, new_state->num); } @@ -271,11 +253,13 @@ bool some_dommunications_are_not_finished() return false; } +namespace simgrid { +namespace mc { + /** * \brief Checks whether a given state has already been visited by the algorithm. */ - -mc_visited_state_t is_visited_state(mc_state_t graph_state) +simgrid::mc::VisitedState* is_visited_state(mc_state_t graph_state) { if (_sg_mc_visited == 0) return nullptr; @@ -286,7 +270,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state) int partial_comm = (_sg_mc_comms_determinism || _sg_mc_send_determinism) && some_dommunications_are_not_finished(); - mc_visited_state_t new_state = visited_state_new(); + simgrid::mc::VisitedState* new_state = new VisitedState(); 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); @@ -307,7 +291,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state) int cursor = min; while (cursor <= max) { - mc_visited_state_t state_test = (mc_visited_state_t) xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t); + simgrid::mc::VisitedState* state_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(visited_states, cursor, simgrid::mc::VisitedState*); if (snapshot_compare(state_test, new_state) == 0) { // The state has been visited: @@ -324,7 +308,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state) } else { // 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); + simgrid::mc::VisitedState* state_test = (simgrid::mc::VisitedState*) xbt_dynar_get_as(visited_states, index, simgrid::mc::VisitedState*); 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) @@ -348,7 +332,7 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state) unsigned int cursor2 = 0; unsigned int index2 = 0; - mc_visited_state_t state_test; + simgrid::mc::VisitedState* 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) { @@ -363,9 +347,6 @@ mc_visited_state_t is_visited_state(mc_state_t graph_state) return nullptr; } -namespace simgrid { -namespace mc { - /** * \brief Checks whether a given pair has already been visited by the algorithm. */ diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp index 04112cac75..c05d0ae4ee 100644 --- a/src/mc/simgrid_mc.cpp +++ b/src/mc/simgrid_mc.cpp @@ -173,7 +173,7 @@ int main(int argc, char** argv) if (_sg_mc_comms_determinism || _sg_mc_send_determinism) res = MC_modelcheck_comm_determinism(); else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0') - res = MC_modelcheck_safety(); + res = simgrid::mc::modelcheck_safety(); else res = simgrid::mc::modelcheck_liveness(); mc_model_checker->shutdown();