From: Gabriel Corona Date: Thu, 14 Apr 2016 13:13:45 +0000 (+0200) Subject: [mc] Move the remaining restoreState() into CommuinicationDeterminismChecker X-Git-Tag: v3_13~97^2~2^2~4 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/bdde4c97ef4a5c90e301b76c52da159005e43b55?hp=af53a6d1fbdda6d8d5523d1284927e8c72e24f91 [mc] Move the remaining restoreState() into CommuinicationDeterminismChecker --- diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index 3eb634d388..0288cfda09 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -400,6 +400,57 @@ bool all_communications_are_finished() return true; } +void CommunicationDeterminismChecker::restoreState() +{ + /* Intermediate backtracking */ + { + simgrid::mc::State* state = stack_.back().get(); + if (state->system_state) { + simgrid::mc::restore_snapshot(state->system_state); + MC_restore_communications_pattern(state); + return; + } + } + + /* Restore the initial state */ + simgrid::mc::session->restoreInitialState(); + + // int n = xbt_dynar_length(incomplete_communications_pattern); + unsigned n = MC_smx_get_maxpid(); + assert(n == xbt_dynar_length(incomplete_communications_pattern)); + assert(n == xbt_dynar_length(initial_communications_pattern)); + for (unsigned j=0; j < n ; j++) { + xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t)); + xbt_dynar_get_as(initial_communications_pattern, j, simgrid::mc::PatternCommunicationList*)->index_comm = 0; + } + + /* Traverse the stack from the state at position start and re-execute the transitions */ + for (std::unique_ptr const& state : stack_) { + if (state == stack_.back()) + break; + + int req_num = state->transition.argument; + smx_simcall_t saved_req = &state->executed_req; + xbt_assert(saved_req); + + /* because we got a copy of the executed request, we have to fetch the + real one, pointed by the request field of the issuer process */ + + const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); + smx_simcall_t req = &issuer->simcall; + + /* TODO : handle test and testany simcalls */ + e_mc_call_type_t call = MC_get_call_type(req); + mc_model_checker->handle_simcall(state->transition); + MC_handle_comm_pattern(call, req, req_num, nullptr, 1); + mc_model_checker->wait_for_requests(); + + /* Update statistics */ + mc_model_checker->visited_states++; + mc_model_checker->executed_transitions++; + } +} + int CommunicationDeterminismChecker::main(void) { std::unique_ptr visited_state = nullptr; @@ -517,7 +568,7 @@ int CommunicationDeterminismChecker::main(void) state->num, stack_.size() + 1); stack_.push_back(std::move(state)); - simgrid::mc::restoreState(stack_); + this->restoreState(); XBT_DEBUG("Back-tracking to state %d at depth %zi done", stack_.back()->num, stack_.size()); diff --git a/src/mc/CommunicationDeterminismChecker.hpp b/src/mc/CommunicationDeterminismChecker.hpp index b19fb12e4a..0680226e76 100644 --- a/src/mc/CommunicationDeterminismChecker.hpp +++ b/src/mc/CommunicationDeterminismChecker.hpp @@ -31,6 +31,7 @@ private: int main(); void logState() override; void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking); + void restoreState(); public: // These are used by functions which should be moved in CommunicationDeterminismChecker: void get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking); diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index 52dd48ca85..56fbbb3cb8 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -110,93 +110,6 @@ void MC_run() simgrid::mc::processes_time.clear(); } -namespace simgrid { -namespace mc { - -/** - * \brief Re-executes from the state at position start all the transitions indicated by - * a given model-checker stack. - * \param stack The stack with the transitions to execute. - * \param start Start index to begin the re-execution. - */ -void restoreState(std::list> const& stack) -{ - XBT_DEBUG("**** Begin Replay ****"); - - /* Intermediate backtracking */ - if(_sg_mc_checkpoint > 0 || _sg_mc_termination || _sg_mc_visited > 0) { - simgrid::mc::State* state = stack.back().get(); - if (state->system_state) { - simgrid::mc::restore_snapshot(state->system_state); - if(_sg_mc_comms_determinism || _sg_mc_send_determinism) - MC_restore_communications_pattern(state); - return; - } - } - - - /* Restore the initial state */ - simgrid::mc::session->restoreInitialState(); - - if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { - // int n = xbt_dynar_length(incomplete_communications_pattern); - unsigned n = MC_smx_get_maxpid(); - assert(n == xbt_dynar_length(incomplete_communications_pattern)); - assert(n == xbt_dynar_length(initial_communications_pattern)); - for (unsigned j=0; j < n ; j++) { - xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t)); - xbt_dynar_get_as(initial_communications_pattern, j, simgrid::mc::PatternCommunicationList*)->index_comm = 0; - } - } - - int count = 1; - - /* Traverse the stack from the state at position start and re-execute the transitions */ - for (std::unique_ptr const& state : stack) { - if (state == stack.back()) - break; - - int req_num = state->transition.argument; - smx_simcall_t saved_req = &state->executed_req; - - if (saved_req) { - /* because we got a copy of the executed request, we have to fetch the - real one, pointed by the request field of the issuer process */ - - const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); - smx_simcall_t req = &issuer->simcall; - - /* Debug information */ - XBT_DEBUG("Replay: %s (%p)", - simgrid::mc::request_to_string( - req, req_num, simgrid::mc::RequestType::simix).c_str(), - state.get()); - - /* TODO : handle test and testany simcalls */ - e_mc_call_type_t call = MC_CALL_TYPE_NONE; - if (_sg_mc_comms_determinism || _sg_mc_send_determinism) - call = MC_get_call_type(req); - - mc_model_checker->handle_simcall(state->transition); - if (_sg_mc_comms_determinism || _sg_mc_send_determinism) - MC_handle_comm_pattern(call, req, req_num, nullptr, 1); - mc_model_checker->wait_for_requests(); - - count++; - } - - /* Update statistics */ - mc_model_checker->visited_states++; - mc_model_checker->executed_transitions++; - - } - - XBT_DEBUG("**** End Replay ****"); -} - -} -} - void MC_show_deadlock(void) { XBT_INFO("**************************");