MC: after all, checker does not need the list of dead actors

Also kill some other unused code in MC

diff --git a/src/kernel/EngineImpl.cpp b/src/kernel/EngineImpl.cpp
index 8e719a7..1e669cb 100644 (file)
--- a/src/kernel/EngineImpl.cpp
+++ b/src/kernel/EngineImpl.cpp
@@ -50,15 +50,6 @@ xbt_dynar_t get_actors_addr()
 #endif
 }
 
-xbt_dynar_t get_dead_actors_addr()
-{
-#if SIMGRID_HAVE_MC
-  return EngineImpl::get_instance()->get_dead_actors_vector();
-#else
-  xbt_die("This function is intended to be used when compiling with MC");
-#endif
-}
-
 constexpr std::initializer_list<std::pair<const char*, context::ContextFactoryInitializer>> context_factories = {
 #if HAVE_RAW_CONTEXTS
     {"raw", &context::raw_factory},
@@ -203,7 +194,6 @@ EngineImpl::~EngineImpl()
     /* Free the remaining data structures */
 #if SIMGRID_HAVE_MC
   xbt_dynar_free(&actors_vector_);
-  xbt_dynar_free(&dead_actors_vector_);
 #endif
   /* clear models before freeing handle, network models can use external callback defined in the handle */
   models_prio_.clear();
@@ -531,9 +521,6 @@ void EngineImpl::empty_trash()
     XBT_DEBUG("Getting rid of %s (refcount: %d)", actor->get_cname(), actor->get_refcount());
     intrusive_ptr_release(actor);
   }
-#if SIMGRID_HAVE_MC
-  xbt_dynar_reset(dead_actors_vector_);
-#endif
 }
 
 void EngineImpl::display_all_actor_status() const

diff --git a/src/kernel/EngineImpl.hpp b/src/kernel/EngineImpl.hpp
index b3259ce..e2a082c 100644 (file)
--- a/src/kernel/EngineImpl.hpp
+++ b/src/kernel/EngineImpl.hpp
@@ -33,7 +33,6 @@ namespace simgrid {
 namespace kernel {
 // In MC mode, the application sends these pointers to the MC
 xbt_dynar_t get_actors_addr();
-xbt_dynar_t get_dead_actors_addr();
 
 class EngineImpl {
   std::map<std::string, s4u::Host*, std::less<>> hosts_;
@@ -58,8 +57,7 @@ class EngineImpl {
                                                        &actor::ActorImpl::kernel_destroy_list_hook>>
       actors_to_destroy_;
 #if SIMGRID_HAVE_MC
-  /* MCer cannot read members actor_list_ and actors_to_destroy_ above in the remote process, so we copy the info it
-   * needs in a dynar.
+  /* MCer cannot read members actor_list_ above in the remote process, so we copy the info it needs in a dynar.
    * FIXME: This is supposed to be a temporary hack.
    * A better solution would be to change the split between MCer and MCed, where the responsibility
    *   to compute the list of the enabled transitions goes to the MCed.
@@ -67,7 +65,6 @@ class EngineImpl {
    * These info could be published by the MCed to the MCer in a way inspired of vd.so
    */
   xbt_dynar_t actors_vector_      = xbt_dynar_new(sizeof(actor::ActorImpl*), nullptr);
-  xbt_dynar_t dead_actors_vector_ = xbt_dynar_new(sizeof(actor::ActorImpl*), nullptr);
 #endif
 
   std::vector<xbt::Task<void()>> tasks;
@@ -157,13 +154,8 @@ public:
 
 #if SIMGRID_HAVE_MC
   xbt_dynar_t get_actors_vector() const { return actors_vector_; }
-  xbt_dynar_t get_dead_actors_vector() const { return dead_actors_vector_; }
   void reset_actor_dynar() { xbt_dynar_reset(actors_vector_); }
   void add_actor_to_dynar(actor::ActorImpl* actor) { xbt_dynar_push_as(actors_vector_, actor::ActorImpl*, actor); }
-  void add_dead_actor_to_dynar(actor::ActorImpl* actor)
-  {
-    xbt_dynar_push_as(dead_actors_vector_, actor::ActorImpl*, actor);
-  }
 #endif
 
   const std::map<aid_t, actor::ActorImpl*>& get_actor_list() const { return actor_list_; }

diff --git a/src/kernel/actor/ActorImpl.cpp b/src/kernel/actor/ActorImpl.cpp
index 817d2c1..4e12056 100644 (file)
--- a/src/kernel/actor/ActorImpl.cpp
+++ b/src/kernel/actor/ActorImpl.cpp
@@ -141,12 +141,8 @@ void ActorImpl::cleanup_from_simix()
   engine->remove_actor(pid_);
   if (host_ && host_actor_list_hook.is_linked())
     host_->get_impl()->remove_actor(this);
-  if (not kernel_destroy_list_hook.is_linked()) {
-#if SIMGRID_HAVE_MC
-    engine->add_dead_actor_to_dynar(this);
-#endif
+  if (not kernel_destroy_list_hook.is_linked())
     engine->add_actor_to_destroy_list(*this);
-  }
 }
 
 void ActorImpl::cleanup()

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index cb17269..4d7be7f 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -162,7 +162,7 @@ bool ModelChecker::handle_message(const char* buffer, ssize_t size)
       xbt_assert(size == sizeof(message), "Broken message. Got %d bytes instead of %d.", (int)size, (int)sizeof(message));
       memcpy(&message, buffer, sizeof(message));
 
-      get_remote_process().init(message.mmalloc_default_mdp, message.maxpid, message.actors, message.dead_actors);
+      get_remote_process().init(message.mmalloc_default_mdp, message.maxpid, message.actors);
       break;
     }
 

diff --git a/src/mc/mc_smx.cpp b/src/mc/mc_smx.cpp
index 82d03d4..ca37c21 100644 (file)
--- a/src/mc/mc_smx.cpp
+++ b/src/mc/mc_smx.cpp
@@ -66,7 +66,6 @@ void RemoteProcess::refresh_simix()
     return;
 
   MC_process_refresh_simix_actor_dynar(this, this->smx_actors_infos, actors_addr_);
-  MC_process_refresh_simix_actor_dynar(this, this->smx_dead_actors_infos, dead_actors_addr_);
 
   this->cache_flags_ |= RemoteProcess::cache_simix_processes;
 }

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index 910ec35..bf79dfc 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -75,8 +75,7 @@ AppSide* AppSide::initialize()
              strerror(errno));
 
   s_mc_message_initial_addresses_t message{MessageType::INITIAL_ADDRESSES, mmalloc_preinit(),
-                                           kernel::actor::get_maxpid_addr(), kernel::get_actors_addr(),
-                                           kernel::get_dead_actors_addr()};
+                                           kernel::actor::get_maxpid_addr(), kernel::get_actors_addr()};
   xbt_assert(instance_->channel_.send(message) == 0, "Could not send the initial message with addresses.");
 
   instance_->handle_messages();

diff --git a/src/mc/remote/RemoteProcess.cpp b/src/mc/remote/RemoteProcess.cpp
index 1bbd05a..dda2716 100644 (file)
--- a/src/mc/remote/RemoteProcess.cpp
+++ b/src/mc/remote/RemoteProcess.cpp
@@ -108,13 +108,11 @@ int open_vm(pid_t pid, int flags)
 
 RemoteProcess::RemoteProcess(pid_t pid) : AddressSpace(this), pid_(pid), running_(true) {}
 
-void RemoteProcess::init(xbt_mheap_t mmalloc_default_mdp, unsigned long* maxpid, xbt_dynar_t actors,
-                         xbt_dynar_t dead_actors)
+void RemoteProcess::init(xbt_mheap_t mmalloc_default_mdp, unsigned long* maxpid, xbt_dynar_t actors)
 {
   this->heap_address      = remote(mmalloc_default_mdp);
   this->maxpid_addr_      = remote(maxpid);
   this->actors_addr_      = remote(actors);
-  this->dead_actors_addr_ = remote(dead_actors);
 
   this->memory_map_ = simgrid::xbt::get_memory_map(this->pid_);
   this->init_memory_map_info();
@@ -124,7 +122,6 @@ void RemoteProcess::init(xbt_mheap_t mmalloc_default_mdp, unsigned long* maxpid,
   this->memory_file = fd;
 
   this->smx_actors_infos.clear();
-  this->smx_dead_actors_infos.clear();
   this->unw_addr_space            = simgrid::mc::UnwindContext::createUnwindAddressSpace();
   this->unw_underlying_addr_space = simgrid::unw::create_addr_space();
   this->unw_underlying_context    = simgrid::unw::create_context(this->unw_underlying_addr_space, this->pid_);
@@ -423,12 +420,6 @@ std::vector<simgrid::mc::ActorInformation>& RemoteProcess::actors()
   return smx_actors_infos;
 }
 
-std::vector<simgrid::mc::ActorInformation>& RemoteProcess::dead_actors()
-{
-  this->refresh_simix();
-  return smx_dead_actors_infos;
-}
-
 void RemoteProcess::dump_stack() const
 {
   unw_addr_space_t as = unw_create_addr_space(&_UPT_accessors, BYTE_ORDER);

diff --git a/src/mc/remote/RemoteProcess.hpp b/src/mc/remote/RemoteProcess.hpp
index 138cd82..1eec7fa 100644 (file)
--- a/src/mc/remote/RemoteProcess.hpp
+++ b/src/mc/remote/RemoteProcess.hpp
@@ -77,7 +77,7 @@ private:
 public:
   explicit RemoteProcess(pid_t pid);
   ~RemoteProcess() override;
-  void init(xbt_mheap_t mmalloc_default_mdp, unsigned long* maxpid, xbt_dynar_t actors, xbt_dynar_t dead_actors);
+  void init(xbt_mheap_t mmalloc_default_mdp, unsigned long* maxpid, xbt_dynar_t actors);
 
   RemoteProcess(RemoteProcess const&) = delete;
   RemoteProcess(RemoteProcess&&)      = delete;
@@ -170,37 +170,9 @@ private:
   // Cache the address of the variables we read directly in the memory of remote
   RemotePtr<unsigned long> maxpid_addr_;
   RemotePtr<s_xbt_dynar_t> actors_addr_;
-  RemotePtr<s_xbt_dynar_t> dead_actors_addr_;
 
 public:
   std::vector<ActorInformation>& actors();
-  std::vector<ActorInformation>& dead_actors();
-
-  /** Get a local description of a remote SIMIX actor */
-  ActorInformation* resolve_actor_info(RemotePtr<kernel::actor::ActorImpl> actor)
-  {
-    xbt_assert(mc_model_checker != nullptr);
-    if (not actor)
-      return nullptr;
-    this->refresh_simix();
-    for (auto& actor_info : this->smx_actors_infos)
-      if (actor_info.address == actor)
-        return &actor_info;
-    for (auto& actor_info : this->smx_dead_actors_infos)
-      if (actor_info.address == actor)
-        return &actor_info;
-    return nullptr;
-  }
-
-  /** Get a local copy of the SIMIX actor structure */
-  kernel::actor::ActorImpl* resolve_actor(RemotePtr<kernel::actor::ActorImpl> process)
-  {
-    ActorInformation* actor_info = this->resolve_actor_info(process);
-    if (actor_info)
-      return actor_info->copy.get_buffer();
-    else
-      return nullptr;
-  }
 
   unsigned long get_maxpid() const { return this->read(maxpid_addr_); }
 
@@ -229,12 +201,6 @@ private:
    */
   std::vector<ActorInformation> smx_actors_infos;
 
-  /** Copy of `EngineImpl::actors_to_destroy_`
-   *
-   *  See mc_smx.cpp.
-   */
-  std::vector<ActorInformation> smx_dead_actors_infos;
-
   /** State of the cache (which variables are up to date) */
   int cache_flags_ = RemoteProcess::cache_none;
 

diff --git a/src/mc/remote/mc_protocol.h b/src/mc/remote/mc_protocol.h
index 7a3dbac..67716eb 100644 (file)
--- a/src/mc/remote/mc_protocol.h
+++ b/src/mc/remote/mc_protocol.h
@@ -66,7 +66,6 @@ struct s_mc_message_initial_addresses_t {
   xbt_mheap_t mmalloc_default_mdp;
   unsigned long* maxpid;
   xbt_dynar_t actors;
-  xbt_dynar_t dead_actors;
 };
 
 struct s_mc_message_ignore_heap_t {

diff --git a/src/mc/sosp/Snapshot_test.cpp b/src/mc/sosp/Snapshot_test.cpp
index 84834a2..3d9bb72 100644 (file)
--- a/src/mc/sosp/Snapshot_test.cpp
+++ b/src/mc/sosp/Snapshot_test.cpp
@@ -58,7 +58,7 @@ void snap_test_helper::Init()
   REQUIRE(1 << xbt_pagebits == xbt_pagesize);
 
   process = std::make_unique<simgrid::mc::RemoteProcess>(getpid());
-  process->init(nullptr, nullptr, nullptr, nullptr);
+  process->init(nullptr, nullptr, nullptr);
   mc_model_checker = new ::simgrid::mc::ModelChecker(std::move(process), -1);
 }
 

diff --git a/teshsuite/mc/dwarf-expression/dwarf-expression.cpp b/teshsuite/mc/dwarf-expression/dwarf-expression.cpp
index a317517..8ed3273 100644 (file)
--- a/teshsuite/mc/dwarf-expression/dwarf-expression.cpp
+++ b/teshsuite/mc/dwarf-expression/dwarf-expression.cpp
@@ -149,7 +149,7 @@ static void test_deref(simgrid::dwarf::ExpressionContext const& state)
 int main()
 {
   auto* process = new simgrid::mc::RemoteProcess(getpid());
-  process->init(nullptr, nullptr, nullptr, nullptr);
+  process->init(nullptr, nullptr, nullptr);
 
   simgrid::dwarf::ExpressionContext state;
   state.address_space = (simgrid::mc::AddressSpace*) process;

diff --git a/teshsuite/mc/dwarf/dwarf.cpp b/teshsuite/mc/dwarf/dwarf.cpp
index 06332d9..1e3f57e 100644 (file)
--- a/teshsuite/mc/dwarf/dwarf.cpp
+++ b/teshsuite/mc/dwarf/dwarf.cpp
@@ -123,7 +123,7 @@ int main(int argc, char** argv)
   simgrid::mc::Type* type;
 
   simgrid::mc::RemoteProcess process(getpid());
-  process.init(nullptr, nullptr, nullptr, nullptr);
+  process.init(nullptr, nullptr, nullptr);
 
   test_global_variable(process, process.binary_info.get(), "some_local_variable", &some_local_variable, sizeof(int));