[mc] Move initial state into Session

We can get rid of s_mc_global_t in SafetyChecker.

diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp
index 0677f95..c6f1270 100644 (file)
--- 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");
 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<s_mc_global_t>(new s_mc_global_t());
 
   this->prepare();
 
   initial_global_state = std::unique_ptr<s_mc_global_t>(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;
   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 584337f..81b9833 100644 (file)
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -159,7 +159,6 @@ void LivenessChecker::removeAcceptancePair(int pair_num)
 
 void LivenessChecker::prepare(void)
 {
 
 void LivenessChecker::prepare(void)
 {

-  initial_global_state->snapshot = simgrid::mc::take_snapshot(0);

   initial_global_state->prev_pair = 0;
 
   std::shared_ptr<const std::vector<int>> propos = this->getPropositionValues();
   initial_global_state->prev_pair = 0;
 
   std::shared_ptr<const std::vector<int>> propos = this->getPropositionValues();


@@ -188,7 +187,7 @@ void LivenessChecker::replay()
   }
 
   /* Restore the initial state */
   }
 
   /* 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;
 
   /* 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);
 {
   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");
 
   XBT_DEBUG("Starting the liveness algorithm");

-
-  /* Create the initial state */

   simgrid::mc::initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
   simgrid::mc::initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());

-
+  simgrid::mc::session->initialize();

   this->prepare();
   this->prepare();

+

   int res = this->main();
   simgrid::mc::initial_global_state = nullptr;
 
   int res = this->main();
   simgrid::mc::initial_global_state = nullptr;
 

diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 5e106ad..4064b6a 100644 (file)
--- 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();
 
   XBT_INFO("No property violation found.");
   simgrid::mc::session->logState();

-  initial_global_state = nullptr;

   return SIMGRID_MC_EXIT_SUCCESS;
 }
 
   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");
     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");
 
 
   XBT_DEBUG("Starting the safety algorithm");
 


@@ -312,10 +311,6 @@ void SafetyChecker::init()
     }
 
   stack_.push_back(std::move(initial_state));
     }
 
   stack_.push_back(std::move(initial_state));

-
-  /* Save the initial state */
-  initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
-  initial_global_state->snapshot = simgrid::mc::take_snapshot(0);

 }
 
 SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 }
 
 SafetyChecker::SafetyChecker(Session& session) : Checker(session)

diff --git a/src/mc/Session.cpp b/src/mc/Session.cpp
index 1bb2878..9969665 100644 (file)
--- a/src/mc/Session.cpp
+++ b/src/mc/Session.cpp
@@ -99,12 +99,24 @@ Session::~Session()
   this->close();
 }
 
   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::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();
 void Session::logState()
 {
   mc_model_checker->getChecker()->logState();


@@ -162,6 +174,7 @@ Session* Session::spawnvp(const char *path, char *const argv[])
 
 void Session::close()
 {
 
 void Session::close()
 {

+  initialSnapshot_ = nullptr;

   if (modelChecker_) {
     modelChecker_->shutdown();
     modelChecker_ = nullptr;
   if (modelChecker_) {
     modelChecker_->shutdown();
     modelChecker_ = nullptr;

diff --git a/src/mc/Session.hpp b/src/mc/Session.hpp
index dd2e031..11afeda 100644 (file)
--- a/src/mc/Session.hpp
+++ b/src/mc/Session.hpp
@@ -37,6 +37,7 @@ namespace mc {
 class Session {
 private:
   std::unique_ptr<ModelChecker> modelChecker_;
 class Session {
 private:
   std::unique_ptr<ModelChecker> modelChecker_;

+  std::shared_ptr<simgrid::mc::Snapshot> initialSnapshot_;

 
 private:
   Session(pid_t pid, int socket);
 
 private:
   Session(pid_t pid, int socket);


@@ -50,9 +51,12 @@ public:
   void close();
 
 public:
   void close();
 
 public:

+  void initialize();

   void execute(Transition const& transition);
   void logState();
 
   void execute(Transition const& transition);
   void logState();
 

+  void restoreInitialState();
+

 public: // static constructors
 
   /** Create a new session by forking
 public: // static constructors
 
   /** Create a new session by forking

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 1b1afce..c1b88d1 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -137,7 +137,7 @@ void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack)
 
 
   /* Restore the initial state */
 
 
   /* 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);
 
   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 3817326..591acdd 100644 (file)
--- 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 {
 } s_mc_snapshot_stack_t, *mc_snapshot_stack_t;
 
 typedef struct s_mc_global_t {

-  std::shared_ptr<simgrid::mc::Snapshot> snapshot;

   int prev_pair = 0;
   std::string prev_req;
   int initial_communications_pattern_done = 0;
   int prev_pair = 0;
   std::string prev_req;
   int initial_communications_pattern_done = 0;