Convert Api::get_maxpid() into RemoteApp::get_maxpid()

The patch is a bit complex because RemoteApp is not a singleton, and
because I converted some pointers to references on the way.

diff --git a/src/mc/api.cpp b/src/mc/api.cpp
index c57dd69..f670433 100644 (file)
--- a/src/mc/api.cpp
+++ b/src/mc/api.cpp
@@ -50,19 +50,19 @@ simgrid::mc::Exploration* Api::initialize(char** argv, const std::unordered_map<
   simgrid::mc::Exploration* explo;
   switch (algo) {
     case ExplorationAlgorithm::CommDeterminism:
-      explo = simgrid::mc::create_communication_determinism_checker(remote_app_.get());
+      explo = simgrid::mc::create_communication_determinism_checker(*(remote_app_.get()));
       break;
 
     case ExplorationAlgorithm::UDPOR:
-      explo = simgrid::mc::create_udpor_checker(remote_app_.get());
+      explo = simgrid::mc::create_udpor_checker(*(remote_app_.get()));
       break;
 
     case ExplorationAlgorithm::Safety:
-      explo = simgrid::mc::create_dfs_exploration(remote_app_.get());
+      explo = simgrid::mc::create_dfs_exploration(*(remote_app_.get()));
       break;
 
     case ExplorationAlgorithm::Liveness:
-      explo = simgrid::mc::create_liveness_checker(remote_app_.get());
+      explo = simgrid::mc::create_liveness_checker(*(remote_app_.get()));
       break;
 
     default:
@@ -73,10 +73,6 @@ simgrid::mc::Exploration* Api::initialize(char** argv, const std::unordered_map<
   return explo;
 }
 
-unsigned long Api::get_maxpid() const
-{
-  return mc_model_checker->get_remote_process().get_maxpid();
-}
 
 std::size_t Api::get_remote_heap_bytes() const
 {

diff --git a/src/mc/api.hpp b/src/mc/api.hpp
index 98baee7..3631479 100644 (file)
--- a/src/mc/api.hpp
+++ b/src/mc/api.hpp
@@ -56,9 +56,6 @@ public:
   simgrid::mc::Exploration* initialize(char** argv, const std::unordered_map<std::string, std::string>& env,
                                        simgrid::mc::ExplorationAlgorithm algo);
 
-  // ACTOR APIs
-  unsigned long get_maxpid() const;
-
   // REMOTE APIs
   std::size_t get_remote_heap_bytes() const;
 

diff --git a/src/mc/api/RemoteApp.cpp b/src/mc/api/RemoteApp.cpp
index 810f527..5edd18c 100644 (file)
--- a/src/mc/api/RemoteApp.cpp
+++ b/src/mc/api/RemoteApp.cpp
@@ -130,6 +130,11 @@ void RemoteApp::close()
   }
 }
 
+unsigned long RemoteApp::get_maxpid() const
+{
+  return model_checker_->get_remote_process().get_maxpid();
+}
+
 void RemoteApp::get_actors_status(std::map<aid_t, ActorState>& whereto)
 {
   s_mc_message_t msg;

diff --git a/src/mc/api/RemoteApp.hpp b/src/mc/api/RemoteApp.hpp
index 1b862bc..377b99f 100644 (file)
--- a/src/mc/api/RemoteApp.hpp
+++ b/src/mc/api/RemoteApp.hpp
@@ -52,6 +52,10 @@ public:
 
   void log_state() const;
 
+  /** Retrieve the max PID of the running actors */
+  unsigned long get_maxpid() const;
+
+  /* Get the list of actors that are ready to run at that step. Usually shorter than maxpid */
   void get_actors_status(std::map<aid_t, ActorState>& whereto);
 };
 } // namespace simgrid::mc

diff --git a/src/mc/explo/CommunicationDeterminismChecker.cpp b/src/mc/explo/CommunicationDeterminismChecker.cpp
index 3212daa..1f3c1ed 100644 (file)
--- a/src/mc/explo/CommunicationDeterminismChecker.cpp
+++ b/src/mc/explo/CommunicationDeterminismChecker.cpp
@@ -72,14 +72,14 @@ struct CommDetExtension {
   std::string send_diff;
   std::string recv_diff;
 
-  void exploration_start()
+  void exploration_start(RemoteApp& remote_app)
   {
-    const unsigned long maxpid = Api::get().get_maxpid();
+    const unsigned long maxpid = remote_app.get_maxpid();
 
     initial_communications_pattern.resize(maxpid);
     incomplete_communications_pattern.resize(maxpid);
   }
-  void restore_communications_pattern(const simgrid::mc::State* state);
+  void restore_communications_pattern(const simgrid::mc::State* state, RemoteApp& remote_app);
   void enforce_deterministic_pattern(aid_t process, const PatternCommunication* comm);
   void get_comm_pattern(const Transition* transition);
   void complete_comm_pattern(const CommWaitTransition* transition);
@@ -94,17 +94,17 @@ public:
   std::vector<unsigned> communication_indices_;
 
   static simgrid::xbt::Extension<simgrid::mc::State, StateCommDet> EXTENSION_ID;
-  explicit StateCommDet(CommDetExtension* checker)
+  explicit StateCommDet(CommDetExtension& checker, RemoteApp& remote_app)
   {
-    const unsigned long maxpid = Api::get().get_maxpid();
+    const unsigned long maxpid = remote_app.get_maxpid();
     for (unsigned long i = 0; i < maxpid; i++) {
       std::vector<simgrid::mc::PatternCommunication> res;
-      for (auto const& comm : checker->incomplete_communications_pattern[i])
+      for (auto const& comm : checker.incomplete_communications_pattern[i])
         res.push_back(comm->dup());
       incomplete_comm_pattern_.push_back(std::move(res));
     }
 
-    for (auto const& list_process_comm : checker->initial_communications_pattern)
+    for (auto const& list_process_comm : checker.initial_communications_pattern)
       this->communication_indices_.push_back(list_process_comm.index_comm);
   }
 };
@@ -129,13 +129,13 @@ static simgrid::mc::CommPatternDifference compare_comm_pattern(const simgrid::mc
   return CommPatternDifference::NONE;
 }
 
-void CommDetExtension::restore_communications_pattern(const simgrid::mc::State* state)
+void CommDetExtension::restore_communications_pattern(const simgrid::mc::State* state, RemoteApp& remote_app)
 {
   for (size_t i = 0; i < initial_communications_pattern.size(); i++)
     initial_communications_pattern[i].index_comm =
         state->extension<simgrid::mc::StateCommDet>()->communication_indices_[i];
 
-  const unsigned long maxpid = Api::get().get_maxpid();
+  const unsigned long maxpid = remote_app.get_maxpid();
   for (unsigned long i = 0; i < maxpid; i++) {
     incomplete_communications_pattern[i].clear();
     for (simgrid::mc::PatternCommunication const& comm :
@@ -314,7 +314,7 @@ void CommDetExtension::handle_comm_pattern(const Transition* transition)
       }
  */
 
-Exploration* create_communication_determinism_checker(RemoteApp* remote_app)
+Exploration* create_communication_determinism_checker(RemoteApp& remote_app)
 {
   CommDetExtension::EXTENSION_ID = simgrid::mc::Exploration::extension_create<CommDetExtension>();
   StateCommDet::EXTENSION_ID     = simgrid::mc::State::extension_create<StateCommDet>();
@@ -323,17 +323,19 @@ Exploration* create_communication_determinism_checker(RemoteApp* remote_app)
 
   auto extension = new CommDetExtension();
 
-  DFSExplorer::on_exploration_start([extension]() {
+  DFSExplorer::on_exploration_start([extension, &remote_app]() {
     XBT_INFO("Check communication determinism");
-    extension->exploration_start();
+    extension->exploration_start(remote_app);
   });
   DFSExplorer::on_backtracking([extension]() { extension->initial_communications_pattern_done = true; });
-  DFSExplorer::on_state_creation([extension](State* state) { state->extension_set(new StateCommDet(extension)); });
+  DFSExplorer::on_state_creation(
+      [extension, &remote_app](State* state) { state->extension_set(new StateCommDet(*extension, remote_app)); });
 
-  DFSExplorer::on_restore_system_state([extension](State* state) { extension->restore_communications_pattern(state); });
+  DFSExplorer::on_restore_system_state(
+      [extension, &remote_app](State* state) { extension->restore_communications_pattern(state, remote_app); });
 
-  DFSExplorer::on_restore_initial_state([extension]() {
-    const unsigned long maxpid = Api::get().get_maxpid();
+  DFSExplorer::on_restore_initial_state([extension, &remote_app]() {
+    const unsigned long maxpid = remote_app.get_maxpid();
     assert(maxpid == extension->incomplete_communications_pattern.size());
     assert(maxpid == extension->initial_communications_pattern.size());
     for (unsigned long j = 0; j < maxpid; j++) {

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index 22b4bda..9a61e12 100644 (file)
--- a/src/mc/explo/DFSExplorer.cpp
+++ b/src/mc/explo/DFSExplorer.cpp
@@ -266,7 +266,7 @@ void DFSExplorer::restore_state()
   }
 }
 
-DFSExplorer::DFSExplorer(RemoteApp* remote_app) : Exploration(remote_app)
+DFSExplorer::DFSExplorer(RemoteApp& remote_app) : Exploration(remote_app)
 {
   reductionMode_ = reduction_mode;
   if (_sg_mc_termination)
@@ -303,7 +303,7 @@ DFSExplorer::DFSExplorer(RemoteApp* remote_app) : Exploration(remote_app)
   stack_.push_back(std::move(initial_state));
 }
 
-Exploration* create_dfs_exploration(RemoteApp* remote_app)
+Exploration* create_dfs_exploration(RemoteApp& remote_app)
 {
   return new DFSExplorer(remote_app);
 }

diff --git a/src/mc/explo/DFSExplorer.hpp b/src/mc/explo/DFSExplorer.hpp
index ce5fa54..0eaac54 100644 (file)
--- a/src/mc/explo/DFSExplorer.hpp
+++ b/src/mc/explo/DFSExplorer.hpp
@@ -34,7 +34,7 @@ class XBT_PRIVATE DFSExplorer : public Exploration {
   static xbt::signal<void()> on_log_state_signal;
 
 public:
-  explicit DFSExplorer(RemoteApp* remote_app);
+  explicit DFSExplorer(RemoteApp& remote_app);
   void run() override;
   RecordTrace get_record_trace() override;
   std::vector<std::string> get_textual_trace() override;

diff --git a/src/mc/explo/Exploration.hpp b/src/mc/explo/Exploration.hpp
index 5b27bff..68f0f97 100644 (file)
--- a/src/mc/explo/Exploration.hpp
+++ b/src/mc/explo/Exploration.hpp
@@ -23,10 +23,10 @@ namespace simgrid::mc {
  * `RemoteApp` interface (that is currently not perfectly sufficient to that extend). */
 // abstract
 class Exploration : public xbt::Extendable<Exploration> {
-  RemoteApp* remote_app_;
+  RemoteApp& remote_app_;
 
 public:
-  explicit Exploration(RemoteApp* remote_app) : remote_app_(remote_app) {}
+  explicit Exploration(RemoteApp& remote_app) : remote_app_(remote_app) {}
 
   // No copy:
   Exploration(Exploration const&) = delete;
@@ -52,14 +52,14 @@ public:
   /** Log additional information about the state of the model-checker */
   virtual void log_state() = 0;
 
-  RemoteApp& get_remote_app() { return *remote_app_; }
+  RemoteApp& get_remote_app() { return remote_app_; }
 };
 
 // External constructors so that the types (and the types of their content) remain hidden
-XBT_PUBLIC Exploration* create_liveness_checker(RemoteApp* remote_app);
-XBT_PUBLIC Exploration* create_dfs_exploration(RemoteApp* remote_app);
-XBT_PUBLIC Exploration* create_communication_determinism_checker(RemoteApp* remote_app);
-XBT_PUBLIC Exploration* create_udpor_checker(RemoteApp* remote_app);
+XBT_PUBLIC Exploration* create_liveness_checker(RemoteApp& remote_app);
+XBT_PUBLIC Exploration* create_dfs_exploration(RemoteApp& remote_app);
+XBT_PUBLIC Exploration* create_communication_determinism_checker(RemoteApp& remote_app);
+XBT_PUBLIC Exploration* create_udpor_checker(RemoteApp& remote_app);
 
 } // namespace simgrid::mc
 

diff --git a/src/mc/explo/LivenessChecker.cpp b/src/mc/explo/LivenessChecker.cpp
index 3fc4fd2..455c23b 100644 (file)
--- a/src/mc/explo/LivenessChecker.cpp
+++ b/src/mc/explo/LivenessChecker.cpp
@@ -178,7 +178,7 @@ void LivenessChecker::purge_visited_pairs()
   }
 }
 
-LivenessChecker::LivenessChecker(RemoteApp* remote_app) : Exploration(remote_app) {}
+LivenessChecker::LivenessChecker(RemoteApp& remote_app) : Exploration(remote_app) {}
 
 RecordTrace LivenessChecker::get_record_trace() // override
 {
@@ -366,7 +366,7 @@ void LivenessChecker::run()
   log_state();
 }
 
-Exploration* create_liveness_checker(RemoteApp* remote_app)
+Exploration* create_liveness_checker(RemoteApp& remote_app)
 {
   return new LivenessChecker(remote_app);
 }

diff --git a/src/mc/explo/LivenessChecker.hpp b/src/mc/explo/LivenessChecker.hpp
index f47c4ec..45d3c18 100644 (file)
--- a/src/mc/explo/LivenessChecker.hpp
+++ b/src/mc/explo/LivenessChecker.hpp
@@ -50,7 +50,7 @@ public:
 
 class XBT_PRIVATE LivenessChecker : public Exploration {
 public:
-  explicit LivenessChecker(RemoteApp* remote_app);
+  explicit LivenessChecker(RemoteApp& remote_app);
   void run() override;
   RecordTrace get_record_trace() override;
   std::vector<std::string> get_textual_trace() override;

diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp
index b935dcc..5b4fb8b 100644 (file)
--- a/src/mc/explo/UdporChecker.cpp
+++ b/src/mc/explo/UdporChecker.cpp
@@ -10,7 +10,7 @@ XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_udpor, mc, "Logging specific to MC safety ver
 
 namespace simgrid::mc {
 
-UdporChecker::UdporChecker(RemoteApp* remote_app) : Exploration(remote_app) {}
+UdporChecker::UdporChecker(RemoteApp& remote_app) : Exploration(remote_app) {}
 
 void UdporChecker::run() {}
 
@@ -28,7 +28,7 @@ std::vector<std::string> UdporChecker::get_textual_trace()
 
 void UdporChecker::log_state() {}
 
-Exploration* create_udpor_checker(RemoteApp* remote_app)
+Exploration* create_udpor_checker(RemoteApp& remote_app)
 {
   return new UdporChecker(remote_app);
 }

diff --git a/src/mc/explo/UdporChecker.hpp b/src/mc/explo/UdporChecker.hpp
index e5e1097..71c5eff 100644 (file)
--- a/src/mc/explo/UdporChecker.hpp
+++ b/src/mc/explo/UdporChecker.hpp
@@ -14,7 +14,7 @@ namespace simgrid::mc {
 
 class XBT_PRIVATE UdporChecker : public Exploration {
 public:
-  explicit UdporChecker(RemoteApp* remote_app);
+  explicit UdporChecker(RemoteApp& remote_app);
   void run() override;
   RecordTrace get_record_trace() override;
   std::vector<std::string> get_textual_trace() override;