inline a function, kill a file

diff --git a/MANIFEST.in b/MANIFEST.in
index 5be3136..cf536e2 100644 (file)
--- a/MANIFEST.in
+++ b/MANIFEST.in
@@ -2332,7 +2332,6 @@ include src/mc/mc_record.cpp
 include src/mc/mc_record.hpp
 include src/mc/mc_replay.hpp
 include src/mc/mc_safety.hpp
-include src/mc/mc_smx.cpp
 include src/mc/remote/AppSide.cpp
 include src/mc/remote/AppSide.hpp
 include src/mc/remote/Channel.cpp

diff --git a/src/mc/mc_smx.cpp b/src/mc/mc_smx.cpp
deleted file mode 100644 (file)
index 7593fc2..0000000
--- a/src/mc/mc_smx.cpp
+++ /dev/null
@@ -1,68 +0,0 @@
-/* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved.          */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#include "simgrid/s4u/Host.hpp"
-
-#include "src/mc/ModelChecker.hpp"
-#include "src/mc/remote/RemoteProcess.hpp"
-
-/** @file
- *  @brief (Cross-process, MCer/MCed) Access to SMX structures
- *
- *  We copy some C data structure from the MCed process in the MCer process.
- *  This is implemented by:
- *
- *   - `model_checker->process.smx_process_infos`
- *      (copy of `EngineImpl::actor_list_`);
- *
- *   - `model_checker->hostnames`.
- *
- * The process lists are currently refreshed each time MCed code is executed.
- * We don't try to give a persistent MCer address for a given MCed process.
- * For this reason, a MCer simgrid::mc::Process* is currently not reusable after
- * MCed code.
- */
-
-/** Load the remote list of processes into a vector
- *
- *  @param process      MCed process
- *  @param target       Local vector (to be filled with `simgrid::mc::ActorInformation`)
- *  @param remote_dynar Address of the process dynar in the remote list
- */
-static void MC_process_refresh_simix_actor_dynar(const simgrid::mc::RemoteProcess* process,
-                                                 std::vector<simgrid::mc::ActorInformation>& target,
-                                                 simgrid::mc::RemotePtr<s_xbt_dynar_t> remote_dynar)
-{
-  target.clear();
-
-  s_xbt_dynar_t dynar;
-  process->read_bytes(&dynar, sizeof(dynar), remote_dynar);
-
-  auto* data = static_cast<simgrid::kernel::actor::ActorImpl**>(::operator new(dynar.elmsize * dynar.used));
-  process->read_bytes(data, dynar.elmsize * dynar.used, simgrid::mc::RemotePtr<void>(dynar.data));
-
-  // Load each element of the vector from the MCed process:
-  for (unsigned int i = 0; i < dynar.used; ++i) {
-    simgrid::mc::ActorInformation info;
-
-    info.address  = simgrid::mc::RemotePtr<simgrid::kernel::actor::ActorImpl>(data[i]);
-    process->read_bytes(&info.copy, sizeof(info.copy), simgrid::mc::remote(data[i]));
-    target.push_back(std::move(info));
-  }
-  ::operator delete(data);
-}
-namespace simgrid::mc {
-
-void RemoteProcess::refresh_simix()
-{
-  if (this->cache_flags_ & RemoteProcess::cache_simix_processes)
-    return;
-
-  MC_process_refresh_simix_actor_dynar(this, this->smx_actors_infos, actors_addr_);
-
-  this->cache_flags_ |= RemoteProcess::cache_simix_processes;
-}
-
-} // namespace simgrid::mc

diff --git a/src/mc/remote/RemoteProcess.cpp b/src/mc/remote/RemoteProcess.cpp
index 654717d..4411375 100644 (file)
--- a/src/mc/remote/RemoteProcess.cpp
+++ b/src/mc/remote/RemoteProcess.cpp
@@ -410,9 +410,37 @@ void RemoteProcess::ignore_local_variable(const char* var_name, const char* fram
     info->remove_local_variable(var_name, frame_name);
 }
 
+/** Load the remote list of actors into the Checker process
+ *
+ * FIXME: This shall die alltogether and be reimplemented with a networked communication to not suppose anything about
+ * the memory layout of the checked App if avoidable.
+ *
+ * Liveness checking will always require to explore the memory of the App, but safety checking doesn't.
+ */
+
 std::vector<simgrid::mc::ActorInformation>& RemoteProcess::actors()
 {
-  this->refresh_simix();
+  if (not(this->cache_flags_ & RemoteProcess::cache_simix_processes)) {
+    smx_actors_infos.clear();
+
+    s_xbt_dynar_t dynar;
+    read_bytes(&dynar, sizeof(dynar), actors_addr_);
+
+    auto* data = static_cast<simgrid::kernel::actor::ActorImpl**>(::operator new(dynar.elmsize* dynar.used));
+    read_bytes(data, dynar.elmsize * dynar.used, simgrid::mc::RemotePtr<void>(dynar.data));
+
+    // Load each element of the vector from the MCed process:
+    for (unsigned int i = 0; i < dynar.used; ++i) {
+      simgrid::mc::ActorInformation info;
+
+      info.address = simgrid::mc::RemotePtr<simgrid::kernel::actor::ActorImpl>(data[i]);
+      read_bytes(&info.copy, sizeof(info.copy), simgrid::mc::remote(data[i]));
+      smx_actors_infos.push_back(std::move(info));
+    }
+    ::operator delete(data);
+
+    this->cache_flags_ |= RemoteProcess::cache_simix_processes;
+  }
   return smx_actors_infos;
 }
 

diff --git a/src/mc/remote/RemoteProcess.hpp b/src/mc/remote/RemoteProcess.hpp
index 47f6151..02c4fba 100644 (file)
--- a/src/mc/remote/RemoteProcess.hpp
+++ b/src/mc/remote/RemoteProcess.hpp
@@ -181,7 +181,6 @@ private:
   void init_memory_map_info();
   void refresh_heap();
   void refresh_malloc_info();
-  void refresh_simix();
 
   pid_t pid_    = -1;
   bool running_ = false;

diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index ae045ce..38a8e26 100644 (file)
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -653,7 +653,6 @@ set(MC_SRC
   src/mc/mc_private.hpp
   src/mc/mc_record.cpp
   src/mc/mc_safety.hpp
-  src/mc/mc_smx.cpp
   src/mc/udpor_global.cpp
   src/mc/udpor_global.hpp