From 76673935f66c0e1606bb1cdc05f37be3c0a135b1 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Sat, 21 Jan 2017 09:52:16 +0100 Subject: [PATCH] try to make SafetyChecker a bit easier to read Mostly adding comments and renaming symbols, but not changing to the logic (yet) --- src/mc/VisitedState.cpp | 20 ++++++++-------- src/mc/VisitedState.hpp | 6 ++--- .../CommunicationDeterminismChecker.cpp | 7 +++--- src/mc/checker/SafetyChecker.cpp | 18 ++++++++------- src/mc/mc_base.cpp | 2 +- src/mc/mc_state.cpp | 23 +++++++++++++++---- src/mc/mc_state.h | 9 ++++---- 7 files changed, 50 insertions(+), 35 deletions(-) diff --git a/src/mc/VisitedState.cpp b/src/mc/VisitedState.cpp index 88bc0c2e44..c57bf9c056 100644 --- a/src/mc/VisitedState.cpp +++ b/src/mc/VisitedState.cpp @@ -51,7 +51,7 @@ VisitedState::VisitedState(unsigned long state_number) this->system_state = simgrid::mc::take_snapshot(state_number); this->num = state_number; - this->other_num = -1; + this->original_num = -1; } VisitedState::~VisitedState() @@ -73,8 +73,7 @@ void VisitedStates::prune() } } -/** - * \brief Checks whether a given state has already been visited by the algorithm. +/** \brief Checks whether a given state has already been visited by the algorithm. */ std::unique_ptr VisitedStates::addVisitedState( unsigned long state_number, simgrid::mc::State* graph_state, bool compare_snpashots) @@ -97,18 +96,17 @@ std::unique_ptr VisitedStates::addVisitedState( std::unique_ptr old_state = std::move(visited_state); - if (old_state->other_num == -1) - new_state->other_num = old_state->num; - else - new_state->other_num = old_state->other_num; + if (old_state->original_num == -1) // I'm the copy of an original process + new_state->original_num = old_state->num; + else // I'm the copy of a copy + new_state->original_num = old_state->original_num; if (dot_output == nullptr) XBT_DEBUG("State %d already visited ! (equal to state %d)", - new_state->num, old_state->num); + new_state->num, old_state->num); else - XBT_DEBUG( - "State %d already visited ! (equal to state %d (state %d in dot_output))", - new_state->num, old_state->num, new_state->other_num); + XBT_DEBUG("State %d already visited ! (equal to state %d (state %d in dot_output))", + new_state->num, old_state->num, new_state->original_num); /* Replace the old state with the new one (with a bigger num) (when the max number of visited states is reached, the oldest diff --git a/src/mc/VisitedState.hpp b/src/mc/VisitedState.hpp index eced3ecc0f..3ac5e7b15f 100644 --- a/src/mc/VisitedState.hpp +++ b/src/mc/VisitedState.hpp @@ -20,9 +20,9 @@ namespace mc { struct XBT_PRIVATE VisitedState { std::shared_ptr system_state = nullptr; std::size_t heap_bytes_used = 0; - int actors_count = 0; - int num = 0; - int other_num = 0; // dot_output for + int actors_count = 0; + int num = 0; // unique id of that state in the storage of all stored IDs + int original_num = 0; // num field of the VisitedState to which I was declared equal to (used for dot_output) VisitedState(unsigned long state_number); ~VisitedState(); diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp index 6c93733397..fa5ab40612 100644 --- a/src/mc/checker/CommunicationDeterminismChecker.cpp +++ b/src/mc/checker/CommunicationDeterminismChecker.cpp @@ -526,8 +526,8 @@ void CommunicationDeterminismChecker::main(void) state->num, next_state->num, req_str.c_str()); } else if (dot_output != nullptr) - fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str.c_str()); + fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, + visited_state->original_num == -1 ? visited_state->num : visited_state->original_num, req_str.c_str()); stack_.push_back(std::move(next_state)); @@ -536,7 +536,8 @@ void CommunicationDeterminismChecker::main(void) if (stack_.size() > (std::size_t) _sg_mc_max_depth) XBT_WARN("/!\\ Max depth reached ! /!\\ "); else if (visited_state != nullptr) - XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num); + XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", + visited_state->original_num == -1 ? visited_state->num : visited_state->original_num); else XBT_DEBUG("There are no more processes to interleave. (depth %zi)", stack_.size()); diff --git a/src/mc/checker/SafetyChecker.cpp b/src/mc/checker/SafetyChecker.cpp index 088841a3f5..52e1e70831 100644 --- a/src/mc/checker/SafetyChecker.cpp +++ b/src/mc/checker/SafetyChecker.cpp @@ -93,7 +93,7 @@ void SafetyChecker::run() { /* This function runs the DFS algorithm the state space. * We do so iteratively instead of recursively, dealing with the call stack manually. - * This allows to explore the call stack when we want to. */ + * This allows to explore the call stack at wish. */ while (!stack_.empty()) { @@ -116,7 +116,7 @@ void SafetyChecker::run() // Backtrack if we are revisiting a state we saw previously if (visitedState_ != nullptr) { XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", - visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num); + visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num); visitedState_ = nullptr; this->backtrack(); @@ -124,7 +124,10 @@ void SafetyChecker::run() } // Search an enabled transition in the current state; backtrack if the interleave set is empty + // get_request also sets state.transition to be the one corresponding to the returned req smx_simcall_t req = MC_state_get_request(state); + // req is now the transition of the process that was selected to be executed + if (req == nullptr) { XBT_DEBUG("There are no more processes to interleave. (depth %zi)", stack_.size() + 1); @@ -144,7 +147,7 @@ void SafetyChecker::run() mc_model_checker->executed_transitions++; - /* Answer the request */ + /* Actually answer the request: let the remote process do execute that request */ this->getSession().execute(state->transition); /* Create the new expanded state */ @@ -174,9 +177,9 @@ void SafetyChecker::run() state->num, next_state->num, req_str.c_str()); } else if (dot_output != nullptr) - std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", - state->num, - visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str()); + std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, + visitedState_->original_num == -1 ? visitedState_->num : visitedState_->original_num, + req_str.c_str()); stack_.push_back(std::move(next_state)); } @@ -258,8 +261,7 @@ void SafetyChecker::backtrack() if (state->interleaveSize() && stack_.size() < (std::size_t) _sg_mc_max_depth) { /* We found a back-tracking point, let's loop */ - XBT_DEBUG("Back-tracking to state %d at depth %zi", - state->num, stack_.size() + 1); + XBT_DEBUG("Back-tracking to state %d at depth %zi", state->num, stack_.size() + 1); stack_.push_back(std::move(state)); this->restoreState(); XBT_DEBUG("Back-tracking to state %d at depth %zi done", diff --git a/src/mc/mc_base.cpp b/src/mc/mc_base.cpp index 96fee34cff..f5530bd3ee 100644 --- a/src/mc/mc_base.cpp +++ b/src/mc/mc_base.cpp @@ -137,8 +137,8 @@ bool request_is_enabled(smx_simcall_t req) xbt_dynar_t comms; simgrid::kernel::activity::Comm *act = static_cast(simcall_comm_wait__get__comm(req)); -#if HAVE_MC +#if HAVE_MC s_xbt_dynar_t comms_buffer; size_t buffer_size = 0; if (mc_model_checker != nullptr) { diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index 3e211de54e..861e399698 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -58,12 +58,27 @@ Transition State::getTransition() const } } +/* Search an enabled transition for the given process. + * + * This can be seen as an iterator returning the next transition of the process. + * + * We only consider the processes that are both + * - marked "to be interleaved" in their ProcessState (controled by the checker algo). + * - which simcall can currently be executed (like a comm where the other partner is already known) + * Once we returned the last enabled transition of a process, it is marked done. + * + * Things can get muddled with the WAITANY and TESTANY simcalls, that are rewritten + * on the fly to a bunch of WAIT (resp TEST) transitions using the transition.argument + * field to remember what was the last returned sub-transition. + */ static inline smx_simcall_t MC_state_get_request_for_process( simgrid::mc::State* state, smx_actor_t process) { + /* reset the outgoing transition */ simgrid::mc::ProcessState* procstate = &state->processStates[process->pid]; - state->transition.pid = -1; - state->transition.argument = -1; + state->transition.pid = -1; + state->transition.argument = -1; + state->executed_req.call = SIMCALL_NONE; if (!procstate->isToInterleave()) return nullptr; @@ -215,8 +230,8 @@ static inline smx_simcall_t MC_state_get_request_for_process( smx_simcall_t MC_state_get_request(simgrid::mc::State* state) { - for (auto& p : mc_model_checker->process().actors()) { - smx_simcall_t res = MC_state_get_request_for_process(state, p.copy.getBuffer()); + for (auto& actor : mc_model_checker->process().actors()) { + smx_simcall_t res = MC_state_get_request_for_process(state, actor.copy.getBuffer()); if (res) return res; } diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h index 0dd64177ed..9ee934f4a1 100644 --- a/src/mc/mc_state.h +++ b/src/mc/mc_state.h @@ -125,13 +125,13 @@ struct XBT_PRIVATE State { Transition transition; - /** The simcall which was executed */ + /** The simcall which was executed, going out of that state */ s_smx_simcall_t executed_req; - /* Internal translation of the simcall + /* Internal translation of the executed_req simcall * * SIMCALL_COMM_TESTANY is translated to a SIMCALL_COMM_TEST - * and SIMCALL_COMM_WAITANY to a SIMCALL_COMM_WAIT. + * and SIMCALL_COMM_WAITANY to a SIMCALL_COMM_WAIT. */ s_smx_simcall_t internal_req; @@ -148,8 +148,7 @@ struct XBT_PRIVATE State { State(unsigned long state_number); std::size_t interleaveSize() const; - void interleave(smx_actor_t process) - { + void interleave(smx_actor_t process) { this->processStates[process->pid].interleave(); } Transition getTransition() const; -- 2.20.1