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   RemotePtr<s_xbt_dynar_t> actor_vector;
  70   RemotePtr<s_xbt_dynar_t> dead_actor_vector;
  71   get_actor_vectors(actor_vector, dead_actor_vector);
  72
  73   MC_process_refresh_simix_actor_dynar(this, this->smx_actors_infos, actor_vector);
  74   MC_process_refresh_simix_actor_dynar(this, this->smx_dead_actors_infos, dead_actor_vector);
  75
  76   this->cache_flags_ |= RemoteProcess::cache_simix_processes;
  77 }
  78
  79 }
  80 }