From: Gabriel Corona Date: Mon, 4 Apr 2016 15:14:08 +0000 (+0200) Subject: [mc] Use std::unique_ptr for States X-Git-Tag: v3_13~187^2~3 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/e91f4e50de913c126b42d09d227eb416bb320dae [mc] Use std::unique_ptr for States --- diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index 541a00135e..7075a2e498 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -316,9 +316,9 @@ CommunicationDeterminismChecker::~CommunicationDeterminismChecker() RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override { RecordTrace res; - for (simgrid::mc::State* state : stack_) { + for (auto const& state : stack_) { int value = 0; - smx_simcall_t saved_req = MC_state_get_executed_request(state, &value); + smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value); const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); const int pid = issuer->pid; res.push_back(RecordTraceElement(pid, value)); @@ -330,9 +330,9 @@ RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override std::vector CommunicationDeterminismChecker::getTextualTrace() // override { std::vector trace; - for (simgrid::mc::State* state : stack_) { + for (auto const& state : stack_) { int value; - smx_simcall_t req = MC_state_get_executed_request(state, &value); + smx_simcall_t req = MC_state_get_executed_request(state.get(), &value); if (req) { char* req_str = simgrid::mc::request_to_string( req, value, simgrid::mc::RequestType::executed); @@ -345,7 +345,7 @@ std::vector CommunicationDeterminismChecker::getTextualTrace() // o void CommunicationDeterminismChecker::prepare() { - simgrid::mc::State* initial_state = nullptr; + int i; const int maxpid = MC_smx_get_maxpid(); @@ -365,7 +365,8 @@ void CommunicationDeterminismChecker::prepare() xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern); } - initial_state = MC_state_new(); + std::unique_ptr initial_state = + std::unique_ptr(MC_state_new()); XBT_DEBUG("********* Start communication determinism verification *********"); @@ -375,9 +376,9 @@ void CommunicationDeterminismChecker::prepare() /* Get an enabled process and insert it in the interleave set of the initial state */ 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); + MC_state_interleave_process(initial_state.get(), &p.copy); - stack_.push_back(initial_state); + stack_.push_back(std::move(initial_state)); } static inline @@ -401,12 +402,11 @@ int CommunicationDeterminismChecker::main(void) int value; std::unique_ptr visited_state = nullptr; smx_simcall_t req = nullptr; - simgrid::mc::State* next_state = nullptr; while (!stack_.empty()) { /* Get current state */ - simgrid::mc::State* state = stack_.back(); + simgrid::mc::State* state = stack_.back().get(); XBT_DEBUG("**************************************************"); XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %d)", @@ -447,7 +447,8 @@ int CommunicationDeterminismChecker::main(void) mc_model_checker->wait_for_requests(); /* Create the new expanded state */ - next_state = MC_state_new(); + std::unique_ptr next_state = + std::unique_ptr(MC_state_new()); /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at least, data are transfered). @@ -456,12 +457,13 @@ int CommunicationDeterminismChecker::main(void) bool compare_snapshots = all_communications_are_finished() && initial_global_state->initial_communications_pattern_done; - if (_sg_mc_visited == 0 || (visited_state = visitedStates_.addVisitedState(next_state, compare_snapshots)) == nullptr) { + if (_sg_mc_visited == 0 + || (visited_state = visitedStates_.addVisitedState(next_state.get(), compare_snapshots)) == nullptr) { /* Get enabled processes and insert them 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); + MC_state_interleave_process(next_state.get(), &p.copy); if (dot_output != nullptr) fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str); @@ -470,7 +472,7 @@ int CommunicationDeterminismChecker::main(void) fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str); - stack_.push_back(next_state); + stack_.push_back(std::move(next_state)); if (dot_output != nullptr) xbt_free(req_str); @@ -489,10 +491,9 @@ int CommunicationDeterminismChecker::main(void) initial_global_state->initial_communications_pattern_done = 1; /* Trash the current state, no longer needed */ - stack_.pop_back(); - MC_state_delete(state, !state->in_visited_states ? 1 : 0); XBT_DEBUG("Delete state %d at depth %zi", - state->num, stack_.size() + 1); + state->num, stack_.size()); + stack_.pop_back(); visited_state = nullptr; @@ -503,25 +504,24 @@ int CommunicationDeterminismChecker::main(void) } while (!stack_.empty()) { - simgrid::mc::State* state = stack_.back(); + std::unique_ptr state = std::move(stack_.back()); stack_.pop_back(); - if (MC_state_interleave_size(state) + if (MC_state_interleave_size(state.get()) && stack_.size() < _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); - stack_.push_back(state); + stack_.push_back(std::move(state)); simgrid::mc::replay(stack_); XBT_DEBUG("Back-tracking to state %d at depth %zi done", - state->num, stack_.size()); + stack_.back()->num, stack_.size()); break; } else { XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size() + 1); - MC_state_delete(state, !state->in_visited_states ? 1 : 0); } } } diff --git a/src/mc/CommunicationDeterminismChecker.hpp b/src/mc/CommunicationDeterminismChecker.hpp index c345af7a64..a33c5ce8e8 100644 --- a/src/mc/CommunicationDeterminismChecker.hpp +++ b/src/mc/CommunicationDeterminismChecker.hpp @@ -28,7 +28,7 @@ private: int main(); private: /** Stack representing the position in the exploration graph */ - std::list stack_; + std::list> stack_; simgrid::mc::VisitedStates visitedStates_; }; diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index 58e9a1644e..4f527cbf39 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -57,7 +57,7 @@ static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* stat bool SafetyChecker::checkNonDeterminism(simgrid::mc::State* current_state) { for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) - if(snapshot_compare(*i, current_state) == 0){ + if (snapshot_compare(i->get(), current_state) == 0){ XBT_INFO("Non-progressive cycle : state %d -> state %d", (*i)->num, current_state->num); return true; @@ -68,9 +68,9 @@ bool SafetyChecker::checkNonDeterminism(simgrid::mc::State* current_state) RecordTrace SafetyChecker::getRecordTrace() // override { RecordTrace res; - for (simgrid::mc::State* state : stack_) { + for (auto const& state : stack_) { int value = 0; - smx_simcall_t saved_req = MC_state_get_executed_request(state, &value); + smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value); const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req); const int pid = issuer->pid; res.push_back(RecordTraceElement(pid, value)); @@ -81,9 +81,9 @@ RecordTrace SafetyChecker::getRecordTrace() // override std::vector SafetyChecker::getTextualTrace() // override { std::vector trace; - for (simgrid::mc::State* state : stack_) { + for (auto const& state : stack_) { int value; - smx_simcall_t req = MC_state_get_executed_request(state, &value); + smx_simcall_t req = MC_state_get_executed_request(state.get(), &value); if (req) { char* req_str = simgrid::mc::request_to_string( req, value, simgrid::mc::RequestType::executed); @@ -102,14 +102,13 @@ int SafetyChecker::run() int value; smx_simcall_t req = nullptr; simgrid::mc::State* prev_state = nullptr; - simgrid::mc::State* next_state = nullptr; xbt_fifo_item_t item = nullptr; std::unique_ptr visited_state = nullptr; while (!stack_.empty()) { /* Get current state */ - simgrid::mc::State* state = stack_.back(); + simgrid::mc::State* state = stack_.back().get(); XBT_DEBUG("**************************************************"); XBT_DEBUG( @@ -143,20 +142,21 @@ int SafetyChecker::run() mc_model_checker->wait_for_requests(); /* Create the new expanded state */ - next_state = MC_state_new(); + std::unique_ptr next_state = + std::unique_ptr(MC_state_new()); - if (_sg_mc_termination && this->checkNonDeterminism(next_state)){ + if (_sg_mc_termination && this->checkNonDeterminism(next_state.get())){ MC_show_non_termination(); return SIMGRID_MC_EXIT_NON_TERMINATION; } if (_sg_mc_visited == 0 - || (visited_state = visitedStates_.addVisitedState(next_state, true)) == nullptr) { + || (visited_state = visitedStates_.addVisitedState(next_state.get(), true)) == 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); + MC_state_interleave_process(next_state.get(), &p.copy); if (reductionMode_ != simgrid::mc::ReductionMode::none) break; } @@ -167,7 +167,7 @@ int SafetyChecker::run() } else if (dot_output != nullptr) std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str); - stack_.push_back(next_state); + stack_.push_back(std::move(next_state)); if (dot_output != nullptr) xbt_free(req_str); @@ -192,9 +192,8 @@ int SafetyChecker::run() stack_.size() + 1); /* Trash the current state, no longer needed */ + XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size()); stack_.pop_back(); - XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size() + 1); - MC_state_delete(state, !state->in_visited_states ? 1 : 0); visited_state = nullptr; @@ -212,16 +211,16 @@ int SafetyChecker::run() state that executed that previous request. */ while (!stack_.empty()) { - state = stack_.back(); + std::unique_ptr state = std::move(stack_.back()); stack_.pop_back(); if (reductionMode_ == simgrid::mc::ReductionMode::dpor) { - req = MC_state_get_internal_request(state); + req = MC_state_get_internal_request(state.get()); if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK) xbt_die("Mutex is currently not supported with DPOR, " "use --cfg=model-check/reduction:none"); const smx_process_t issuer = MC_smx_simcall_get_issuer(req); for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) { - simgrid::mc::State* prev_state = *i; + simgrid::mc::State* prev_state = i->get(); if (reductionMode_ != simgrid::mc::ReductionMode::none && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) { if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { @@ -230,7 +229,7 @@ int SafetyChecker::run() req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal); XBT_DEBUG("%s (state=%d)", req_str, prev_state->num); xbt_free(req_str); - prev_req = MC_state_get_executed_request(state, &value); + prev_req = MC_state_get_executed_request(state.get(), &value); req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed); XBT_DEBUG("%s (state=%d)", req_str, state->num); xbt_free(req_str); @@ -261,20 +260,19 @@ int SafetyChecker::run() } } - if (MC_state_interleave_size(state) + if (MC_state_interleave_size(state.get()) && stack_.size() < _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); - stack_.push_back(state); + stack_.push_back(std::move(state)); simgrid::mc::replay(stack_); XBT_DEBUG("Back-tracking to state %d at depth %zi done", - state->num, stack_.size()); + stack_.back()->num, stack_.size()); break; } else { XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size() + 1); - MC_state_delete(state, !state->in_visited_states ? 1 : 0); } } } @@ -302,7 +300,8 @@ void SafetyChecker::init() XBT_DEBUG("Starting the safety algorithm"); - simgrid::mc::State* initial_state = MC_state_new(); + std::unique_ptr initial_state = + std::unique_ptr(MC_state_new()); XBT_DEBUG("**************************************************"); XBT_DEBUG("Initial state"); @@ -313,12 +312,12 @@ void SafetyChecker::init() /* Get an enabled process and insert it in the interleave set of the initial state */ 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); + MC_state_interleave_process(initial_state.get(), &p.copy); if (reductionMode_ != simgrid::mc::ReductionMode::none) break; } - stack_.push_back(initial_state); + stack_.push_back(std::move(initial_state)); /* Save the initial state */ initial_global_state = std::unique_ptr(new s_mc_global_t()); diff --git a/src/mc/SafetyChecker.hpp b/src/mc/SafetyChecker.hpp index 143518277e..4f60b792ec 100644 --- a/src/mc/SafetyChecker.hpp +++ b/src/mc/SafetyChecker.hpp @@ -8,6 +8,7 @@ #define SIMGRID_MC_SAFETY_CHECKER_HPP #include +#include #include "src/mc/mc_forward.hpp" #include "src/mc/Checker.hpp" @@ -30,7 +31,7 @@ private: bool checkNonDeterminism(simgrid::mc::State* current_state); private: /** Stack representing the position in the exploration graph */ - std::list stack_; + std::list> stack_; simgrid::mc::VisitedStates visitedStates_; }; diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index 9d7073caa7..cf23f62827 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -118,13 +118,13 @@ namespace mc { * \param stack The stack with the transitions to execute. * \param start Start index to begin the re-execution. */ -void replay(std::list const& stack) +void replay(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(); + 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) @@ -153,12 +153,12 @@ void replay(std::list const& stack) int count = 1; /* Traverse the stack from the state at position start and re-execute the transitions */ - for (simgrid::mc::State* state : stack) { + for (std::unique_ptr const& state : stack) { if (state == stack.back()) break; int value; - smx_simcall_t saved_req = MC_state_get_executed_request(state, &value); + smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value); if (saved_req) { /* because we got a copy of the executed request, we have to fetch the @@ -170,7 +170,7 @@ void replay(std::list const& stack) /* Debug information */ if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) { char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix); - XBT_DEBUG("Replay: %s (%p)", req_str, state); + XBT_DEBUG("Replay: %s (%p)", req_str, state.get()); xbt_free(req_str); } diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h index 68acc459e6..94c72013d6 100644 --- a/src/mc/mc_state.h +++ b/src/mc/mc_state.h @@ -62,7 +62,7 @@ struct XBT_PRIVATE State { ~State(); }; -XBT_PRIVATE void replay(std::list const& stack); +XBT_PRIVATE void replay(std::list> const& stack); } }