From 0a82e90d4cfdd7e27e1b946d22aff74a5abdda99 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Thu, 14 Apr 2016 10:34:17 +0200 Subject: [PATCH] [mc] Move initial state into Session We can get rid of s_mc_global_t in SafetyChecker. --- src/mc/CommunicationDeterminismChecker.cpp | 3 +-- src/mc/LivenessChecker.cpp | 9 +++------ src/mc/SafetyChecker.cpp | 7 +------ src/mc/Session.cpp | 13 +++++++++++++ src/mc/Session.hpp | 4 ++++ src/mc/mc_global.cpp | 2 +- src/mc/mc_snapshot.h | 1 - 7 files changed, 23 insertions(+), 16 deletions(-) diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp index 0677f95aff..c6f1270ba2 100644 --- a/src/mc/CommunicationDeterminismChecker.cpp +++ b/src/mc/CommunicationDeterminismChecker.cpp @@ -540,12 +540,11 @@ int CommunicationDeterminismChecker::main(void) int CommunicationDeterminismChecker::run() { XBT_INFO("Check communication determinism"); - mc_model_checker->wait_for_requests(); + simgrid::mc::session->initialize(); this->prepare(); initial_global_state = std::unique_ptr(new s_mc_global_t()); - initial_global_state->snapshot = simgrid::mc::take_snapshot(0); initial_global_state->initial_communications_pattern_done = 0; initial_global_state->recv_deterministic = 1; initial_global_state->send_deterministic = 1; diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp index 584337f5b5..81b9833447 100644 --- a/src/mc/LivenessChecker.cpp +++ b/src/mc/LivenessChecker.cpp @@ -159,7 +159,6 @@ void LivenessChecker::removeAcceptancePair(int pair_num) void LivenessChecker::prepare(void) { - initial_global_state->snapshot = simgrid::mc::take_snapshot(0); initial_global_state->prev_pair = 0; std::shared_ptr> propos = this->getPropositionValues(); @@ -188,7 +187,7 @@ void LivenessChecker::replay() } /* Restore the initial state */ - simgrid::mc::restore_snapshot(initial_global_state->snapshot); + simgrid::mc::session->restoreInitialState(); /* Traverse the stack from the initial state and re-execute the transitions */ int depth = 1; @@ -484,14 +483,12 @@ int LivenessChecker::run() { XBT_INFO("Check the liveness property %s", _sg_mc_property_file); MC_automaton_load(_sg_mc_property_file); - mc_model_checker->wait_for_requests(); XBT_DEBUG("Starting the liveness algorithm"); - - /* Create the initial state */ simgrid::mc::initial_global_state = std::unique_ptr(new s_mc_global_t()); - + simgrid::mc::session->initialize(); this->prepare(); + int res = this->main(); simgrid::mc::initial_global_state = nullptr; diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp index 5e106adb04..4064b6aaf4 100644 --- a/src/mc/SafetyChecker.cpp +++ b/src/mc/SafetyChecker.cpp @@ -174,7 +174,6 @@ int SafetyChecker::run() XBT_INFO("No property violation found."); simgrid::mc::session->logState(); - initial_global_state = nullptr; return SIMGRID_MC_EXIT_SUCCESS; } @@ -293,7 +292,7 @@ void SafetyChecker::init() XBT_INFO("Check non progressive cycles"); else XBT_INFO("Check a safety property"); - mc_model_checker->wait_for_requests(); + simgrid::mc::session->initialize(); XBT_DEBUG("Starting the safety algorithm"); @@ -312,10 +311,6 @@ void SafetyChecker::init() } stack_.push_back(std::move(initial_state)); - - /* Save the initial state */ - initial_global_state = std::unique_ptr(new s_mc_global_t()); - initial_global_state->snapshot = simgrid::mc::take_snapshot(0); } SafetyChecker::SafetyChecker(Session& session) : Checker(session) diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp index 1bb2878b62..99696652ab 100644 --- a/src/mc/Session.cpp +++ b/src/mc/Session.cpp @@ -99,12 +99,24 @@ Session::~Session() this->close(); } +void Session::initialize() +{ + xbt_assert(initialSnapshot_ == nullptr); + mc_model_checker->wait_for_requests(); + initialSnapshot_ = simgrid::mc::take_snapshot(0); +} + void Session::execute(Transition const& transition) { modelChecker_->handle_simcall(transition); modelChecker_->wait_for_requests(); } +void Session::restoreInitialState() +{ + simgrid::mc::restore_snapshot(this->initialSnapshot_); +} + void Session::logState() { mc_model_checker->getChecker()->logState(); @@ -162,6 +174,7 @@ Session* Session::spawnvp(const char *path, char *const argv[]) void Session::close() { + initialSnapshot_ = nullptr; if (modelChecker_) { modelChecker_->shutdown(); modelChecker_ = nullptr; diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp index dd2e031b99..11afedaf22 100644 --- a/src/mc/Session.hpp +++ b/src/mc/Session.hpp @@ -37,6 +37,7 @@ namespace mc { class Session { private: std::unique_ptr modelChecker_; + std::shared_ptr initialSnapshot_; private: Session(pid_t pid, int socket); @@ -50,9 +51,12 @@ public: void close(); public: + void initialize(); void execute(Transition const& transition); void logState(); + void restoreInitialState(); + public: // static constructors /** Create a new session by forking diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp index 1b1afcee21..c1b88d16f1 100644 --- a/src/mc/mc_global.cpp +++ b/src/mc/mc_global.cpp @@ -137,7 +137,7 @@ void replay(std::list> const& stack) /* Restore the initial state */ - simgrid::mc::restore_snapshot(simgrid::mc::initial_global_state->snapshot); + simgrid::mc::session->restoreInitialState(); if (_sg_mc_comms_determinism || _sg_mc_send_determinism) { // int n = xbt_dynar_length(incomplete_communications_pattern); diff --git a/src/mc/mc_snapshot.h b/src/mc/mc_snapshot.h index 38173265fa..591acdd7bd 100644 --- a/src/mc/mc_snapshot.h +++ b/src/mc/mc_snapshot.h @@ -129,7 +129,6 @@ typedef struct XBT_PRIVATE s_mc_snapshot_stack { } s_mc_snapshot_stack_t, *mc_snapshot_stack_t; typedef struct s_mc_global_t { - std::shared_ptr snapshot; int prev_pair = 0; std::string prev_req; int initial_communications_pattern_done = 0; -- 2.20.1