src/mc/mc_smx.cpp

   1 /* Copyright (c) 2015-2021. The SimGrid Team. All rights reserved.          */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "simgrid/s4u/Host.hpp"
   7
   8 #include "src/mc/ModelChecker.hpp"
   9 #include "src/mc/remote/RemoteProcess.hpp"
  10
  11 using simgrid::mc::remote;
  12 /** @file
  13  *  @brief (Cross-process, MCer/MCed) Access to SMX structures
  14  *
  15  *  We copy some C data structure from the MCed process in the MCer process.
  16  *  This is implemented by:
  17  *
  18  *   - `model_checker->process.smx_process_infos`
  19  *      (copy of `simix_global->process_list`);
  20  *
  21  *   - `model_checker->process.smx_old_process_infos`
  22  *      (copy of `simix_global->actors_to_destroy`);
  23  *
  24  *   - `model_checker->hostnames`.
  25  *
  26  * The process lists are currently refreshed each time MCed code is executed.
  27  * We don't try to give a persistent MCer address for a given MCed process.
  28  * For this reason, a MCer simgrid::mc::Process* is currently not reusable after
  29  * MCed code.
  30  */
  31
  32 /** Load the remote list of processes into a vector
  33  *
  34  *  @param process      MCed process
  35  *  @param target       Local vector (to be filled with copies of `s_smx_actor_t`)
  36  *  @param remote_dynar Address of the process dynar in the remote list
  37  */
  38 static void MC_process_refresh_simix_actor_dynar(const simgrid::mc::RemoteProcess* process,
  39                                                  std::vector<simgrid::mc::ActorInformation>& target,
  40                                                  simgrid::mc::RemotePtr<s_xbt_dynar_t> remote_dynar)
  41 {
  42   target.clear();
  43
  44   s_xbt_dynar_t dynar;
  45   process->read_bytes(&dynar, sizeof(dynar), remote_dynar);
  46
  47   auto* data = static_cast<smx_actor_t*>(::operator new(dynar.elmsize * dynar.used));
  48   process->read_bytes(data, dynar.elmsize * dynar.used, simgrid::mc::RemotePtr<void>(dynar.data));
  49
  50   // Load each element of the vector from the MCed process:
  51   for (unsigned int i = 0; i < dynar.used; ++i) {
  52     simgrid::mc::ActorInformation info;
  53
  54     info.address  = simgrid::mc::RemotePtr<simgrid::kernel::actor::ActorImpl>(data[i]);
  55     info.hostname = nullptr;
  56     process->read_bytes(&info.copy, sizeof(info.copy), remote(data[i]));
  57     target.push_back(std::move(info));
  58   }
  59   ::operator delete(data);
  60 }
  61 namespace simgrid {
  62 namespace mc {
  63
  64 void RemoteProcess::refresh_simix()
  65 {
  66   if (this->cache_flags_ & RemoteProcess::cache_simix_processes)
  67     return;
  68
  69   // TODO, avoid to reload `&simix_global`, `simix_global`, `*simix_global`
  70
  71   static_assert(std::is_same<
  72       std::unique_ptr<simgrid::simix::Global>,
  73       decltype(simix_global)
  74     >::value, "Unexpected type for simix_global");
  75   static_assert(sizeof(simix_global) == sizeof(simgrid::simix::Global*),
  76     "Bad size for simix_global");
  77
  78   RemotePtr<simgrid::simix::Global> simix_global_p{this->read_variable<simgrid::simix::Global*>("simix_global")};
  79
  80   // simix_global = REMOTE(*simix_global)
  81   Remote<simgrid::simix::Global> simix_global =
  82     this->read<simgrid::simix::Global>(simix_global_p);
  83
  84   MC_process_refresh_simix_actor_dynar(this, this->smx_actors_infos, remote(simix_global.get_buffer()->actors_vector));
  85   MC_process_refresh_simix_actor_dynar(this, this->smx_dead_actors_infos,
  86                                        remote(simix_global.get_buffer()->dead_actors_vector));
  87
  88   this->cache_flags_ |= RemoteProcess::cache_simix_processes;
  89 }
  90
  91 }
  92 }