make mc::State extendable so that CommDet does not polute it in any case

diff --git a/src/mc/api/State.cpp b/src/mc/api/State.cpp
index fb24019..e4772d9 100644 (file)
--- a/src/mc/api/State.cpp
+++ b/src/mc/api/State.cpp
@@ -29,10 +29,6 @@ State::State() : num_(++expended_states_)
   if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) {
     auto snapshot_ptr = api::get().take_snapshot(num_);
     system_state_     = std::shared_ptr<simgrid::mc::Snapshot>(snapshot_ptr);
   if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) {
     auto snapshot_ptr = api::get().take_snapshot(num_);
     system_state_     = std::shared_ptr<simgrid::mc::Snapshot>(snapshot_ptr);

-    if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
-      copy_incomplete_comm_pattern();
-      copy_index_comm_pattern();
-    }

   }
 }
 
   }
 }
 


@@ -90,25 +86,5 @@ void State::execute_next(int next)
   transition_.reset(mc_model_checker->handle_simcall(aid, times_considered, true));
   mc_model_checker->wait_for_requests();
 }
   transition_.reset(mc_model_checker->handle_simcall(aid, times_considered, true));
   mc_model_checker->wait_for_requests();
 }

-
-void State::copy_incomplete_comm_pattern()
-{
-  incomplete_comm_pattern_.clear();
-  const unsigned long maxpid = api::get().get_maxpid();
-  for (unsigned long i = 0; i < maxpid; i++) {
-    std::vector<simgrid::mc::PatternCommunication> res;
-    for (auto const& comm : incomplete_communications_pattern[i])
-      res.push_back(comm->dup());
-    incomplete_comm_pattern_.push_back(std::move(res));
-  }
-}
-
-void State::copy_index_comm_pattern()
-{
-  communication_indices_.clear();
-  for (auto const& list_process_comm : initial_communications_pattern)
-    this->communication_indices_.push_back(list_process_comm.index_comm);
-}
-

 } // namespace mc
 } // namespace simgrid
 } // namespace mc
 } // namespace simgrid

diff --git a/src/mc/api/State.hpp b/src/mc/api/State.hpp
index c01aa50..7d47e41 100644 (file)
--- a/src/mc/api/State.hpp
+++ b/src/mc/api/State.hpp
@@ -14,7 +14,7 @@ namespace simgrid {
 namespace mc {
 
 /* A node in the exploration graph (kind-of) */
 namespace mc {
 
 /* A node in the exploration graph (kind-of) */

-class XBT_PRIVATE State {
+class XBT_PRIVATE State : public xbt::Extendable<State> {

   static long expended_states_; /* Count total amount of states, for stats */
 
   /* Outgoing transition: what was the last transition that we took to leave this state? Useful for replay */
   static long expended_states_; /* Count total amount of states, for stats */
 
   /* Outgoing transition: what was the last transition that we took to leave this state? Useful for replay */


@@ -35,14 +35,10 @@ public:
   /** Snapshot of system state (if needed) */
   std::shared_ptr<simgrid::mc::Snapshot> system_state_;
 
   /** Snapshot of system state (if needed) */
   std::shared_ptr<simgrid::mc::Snapshot> system_state_;
 

-  // For CommunicationDeterminismChecker
-  std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern_;
-  std::vector<unsigned> communication_indices_;
-

   /* Returns a positive number if there is another transition to pick, or -1 if not */
   int next_transition() const;
 
   /* Returns a positive number if there is another transition to pick, or -1 if not */
   int next_transition() const;
 

-  /* Explore a new path */
+  /* Explore a new path; the parameter must be the result of a previous call to next_transition() */

   void execute_next(int next);
 
   std::size_t count_todo() const;
   void execute_next(int next);
 
   std::size_t count_todo() const;


@@ -52,10 +48,6 @@ public:
 
   /* Returns the total amount of states created so far (for statistics) */
   static long get_expanded_states() { return expended_states_; }
 
   /* Returns the total amount of states created so far (for statistics) */
   static long get_expanded_states() { return expended_states_; }

-
-private:
-  void copy_incomplete_comm_pattern();
-  void copy_index_comm_pattern();

 };
 } // namespace mc
 } // namespace simgrid
 };
 } // namespace mc
 } // namespace simgrid

diff --git a/src/mc/checker/CommunicationDeterminismChecker.cpp b/src/mc/checker/CommunicationDeterminismChecker.cpp
index 91f9f4a..8fc0415 100644 (file)
--- a/src/mc/checker/CommunicationDeterminismChecker.cpp
+++ b/src/mc/checker/CommunicationDeterminismChecker.cpp
@@ -23,6 +23,48 @@ std::vector<std::vector<simgrid::mc::PatternCommunication*>> incomplete_communic
 
 /********** Static functions ***********/
 
 
 /********** Static functions ***********/
 

+namespace simgrid {
+namespace mc {
+
+class StateCommDet {
+  // State* state_;
+
+public:
+  std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern_;
+  std::vector<unsigned> communication_indices_;
+
+  static simgrid::xbt::Extension<simgrid::mc::State, StateCommDet> EXTENSION_ID;
+  explicit StateCommDet(State* /* ptr*/) //: state_(ptr)
+  {
+    copy_incomplete_comm_pattern();
+    copy_index_comm_pattern();
+  }
+
+  void copy_incomplete_comm_pattern()
+  {
+    incomplete_comm_pattern_.clear();
+    const unsigned long maxpid = api::get().get_maxpid();
+    for (unsigned long i = 0; i < maxpid; i++) {
+      std::vector<simgrid::mc::PatternCommunication> res;
+      for (auto const& comm : incomplete_communications_pattern[i])
+        res.push_back(comm->dup());
+      incomplete_comm_pattern_.push_back(std::move(res));
+    }
+  }
+
+  void copy_index_comm_pattern()
+  {
+    communication_indices_.clear();
+    for (auto const& list_process_comm : initial_communications_pattern)
+      this->communication_indices_.push_back(list_process_comm.index_comm);
+  }
+};
+
+simgrid::xbt::Extension<simgrid::mc::State, StateCommDet> StateCommDet::EXTENSION_ID;
+
+} // namespace mc
+} // namespace simgrid
+

 static simgrid::mc::CommPatternDifference compare_comm_pattern(const simgrid::mc::PatternCommunication* comm1,
                                                                const simgrid::mc::PatternCommunication* comm2)
 {
 static simgrid::mc::CommPatternDifference compare_comm_pattern(const simgrid::mc::PatternCommunication* comm1,
                                                                const simgrid::mc::PatternCommunication* comm2)
 {


@@ -57,11 +99,13 @@ static void patterns_copy(std::vector<simgrid::mc::PatternCommunication*>& dest,
 static void restore_communications_pattern(simgrid::mc::State* state)
 {
   for (size_t i = 0; i < initial_communications_pattern.size(); i++)
 static void restore_communications_pattern(simgrid::mc::State* state)
 {
   for (size_t i = 0; i < initial_communications_pattern.size(); i++)

-    initial_communications_pattern[i].index_comm = state->communication_indices_[i];
+    initial_communications_pattern[i].index_comm =
+        state->extension<simgrid::mc::StateCommDet>()->communication_indices_[i];

 
   const unsigned long maxpid = api::get().get_maxpid();
   for (unsigned long i = 0; i < maxpid; i++)
 
   const unsigned long maxpid = api::get().get_maxpid();
   for (unsigned long i = 0; i < maxpid; i++)

-    patterns_copy(incomplete_communications_pattern[i], state->incomplete_comm_pattern_[i]);
+    patterns_copy(incomplete_communications_pattern[i],
+                  state->extension<simgrid::mc::StateCommDet>()->incomplete_comm_pattern_[i]);

 }
 
 static char* print_determinism_result(simgrid::mc::CommPatternDifference diff, aid_t process,
 }
 
 static char* print_determinism_result(simgrid::mc::CommPatternDifference diff, aid_t process,


@@ -250,7 +294,10 @@ void CommunicationDeterminismChecker::complete_comm_pattern(RemotePtr<kernel::ac
   }
 }
 
   }
 }
 

-CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session* session) : Checker(session) {}
+CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session* session) : Checker(session)
+{
+  StateCommDet::EXTENSION_ID = simgrid::mc::State::extension_create<StateCommDet>();
+}

 
 CommunicationDeterminismChecker::~CommunicationDeterminismChecker() = default;
 
 
 CommunicationDeterminismChecker::~CommunicationDeterminismChecker() = default;
 


@@ -302,6 +349,7 @@ void CommunicationDeterminismChecker::prepare()
   incomplete_communications_pattern.resize(maxpid);
 
   auto initial_state = std::make_unique<State>();
   incomplete_communications_pattern.resize(maxpid);
 
   auto initial_state = std::make_unique<State>();

+  initial_state->extension_set(new StateCommDet(initial_state.get()));

 
   XBT_DEBUG("********* Start communication determinism verification *********");
 
 
   XBT_DEBUG("********* Start communication determinism verification *********");
 


@@ -438,6 +486,7 @@ void CommunicationDeterminismChecker::real_run()
 
       /* Create the new expanded state */
       auto next_state = std::make_unique<State>();
 
       /* Create the new expanded state */
       auto next_state = std::make_unique<State>();

+      next_state->extension_set(new StateCommDet(next_state.get()));

 
       /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at
        * least, data are transferred). These communications  are incomplete and they cannot be analyzed and compared
 
       /* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at
        * least, data are transferred). These communications  are incomplete and they cannot be analyzed and compared