doc/doxygen/uhood.doc

   1 /*! @page uhood Under the Hood
   2
   3 @tableofcontents
   4
   5 TBD
   6
   7  - Simulation Loop, LMM, sharing -> papers
   8  - Context Switching, privatization -> papers
   9
  10 @section simgrid_uhood_s4u S4U
  11
  12 S4U classes are designed to be user process interfaces to Maestro resources.
  13 We provide an uniform interface to them:
  14
  15 - automatic reference count with intrusive smart pointers `simgrid::s4u::FooPtr`
  16  (also called `simgrid::s4u::Foo::Ptr`);
  17
  18 - manual reference count with `intrusive_ptr_add_ref(p)`,
  19   `intrusive_ptr_release(p)` (which is the interface used by
  20   [`boost::intrusive_ptr`](http://www.boost.org/doc/libs/1_61_0/libs/smart_ptr/intrusive_ptr.html));
  21
  22 - delegation of the operations to an opaque `pimpl` (which is the Maestro object);
  23
  24 - the Maestro object and the corresponding S4U object have the same lifetime
  25   (and share the same reference count).
  26
  27 The ability to manipulate the objects through pointers and have the ability
  28 to use explicit reference count management is useful for creating C wrappers
  29 to the S4U and should play nicely with other language bindings (such as
  30 SWIG-based ones).
  31
  32 Some objects currently live for the whole duration of the simulation and do
  33 not have reference counts. We still provide dummy `intrusive_ptr_add_ref(p)`,
  34 `intrusive_ptr_release(p)` and `FooPtr` for consistency.
  35
  36 In many cases, we try to have an API which is consistent with the API or
  37 corresponding C++ standard classes. For example, the methods of
  38 `simgrid::s4u::Mutex` are based on [`std::mutex`](http://en.cppreference.com/w/cpp/thread/mutex).
  39 This has several benefits:
  40
  41  - we use a proven interface with a well defined and documented semantic;
  42
  43  - the interface is easy to understand and remember for people used to the C++
  44    standard interface;
  45
  46  -  we can use some standard C++ algorithms and helper classes with our types
  47    (`simgrid::s4u::Mutex` can be used with
  48    [`std::lock`](http://en.cppreference.com/w/cpp/thread/lock),
  49    [`std::unique_lock`](http://en.cppreference.com/w/cpp/thread/unique_lock),
  50    etc.).
  51
  52 Example of `simgrid::s4u::Actor`:
  53
  54 ~~~
  55 class Actor {
  56   // This is the corresponding maestro object:
  57   friend simgrid::simix::Process;
  58   simgrid::simix::Process* pimpl_ = nullptr;
  59 public:
  60
  61   Actor(simgrid::simix::Process* pimpl) : pimpl_(pimpl) {}
  62   Actor(Actor const&) = delete;
  63   Actor& operator=(Actor const&) = delete;
  64
  65   // Reference count is delegated to the S4u object:
  66   friend void intrusive_ptr_add_ref(Actor* actor)
  67   {
  68     xbt_assert(actor != nullptr);
  69     SIMIX_process_ref(actor->pimpl_);
  70   }
  71   friend void intrusive_ptr_release(Actor* actor)
  72   {
  73     xbt_assert(actor != nullptr);
  74     SIMIX_process_unref(actor->pimpl_);
  75   }
  76   using Ptr = boost::intrusive_ptr<Actor>;
  77
  78   // Create processes:
  79   static Ptr createActor(const char* name, s4u::Host *host, double killTime, std::function<void()> code);
  80
  81   // [...]
  82 };
  83
  84 using ActorPtr = Actor::Ptr;
  85 ~~~
  86
  87 It uses the `simgrid::simix::Process` as an opaque pimple:
  88
  89
  90 @section simgrid_uhood_mc Model Checker
  91
  92 The current implementation of the model-checker uses two distinct processes:
  93
  94  - the SimGrid model-checker (`simgrid-mc`) itself lives in the parent process;
  95
  96  - it spawns a child process for the SimGrid simulator/maestro and the simulated
  97    processes.
  98
  99 They communicate using a `AF_UNIX` `SOCK_SEQPACKET` socket and exchange messages
 100 defined in `mc_protocol.h`. The `SIMGRID_MC_SOCKET_FD` environment variable it
 101 set to the file descriptor of this socket in the child process.
 102
 103 The model-checker analyzes, saves and restores the state of the model-checked
 104 process using the following techniques:
 105
 106 - the model-checker reads and writes in the model-checked address space;
 107
 108 - the model-cheker `ptrace()`s the model-checked process and is thus able to
 109   know the state of the model-checked process if it crashes;
 110
 111 - DWARF debug information are used to unwind the stack and identify local
 112   variables;
 113
 114 - a custom heap is enabled in the model-checked process which allows the model
 115   checker to know which chunks are allocated and which are freed.
 116
 117 @subsection simgrid_uhood_mc_address_space Address space
 118
 119 The `AddressSpace` is a base class used for both the model-checked process
 120 and its snapshots and has methods to read in the corresponding address space:
 121
 122  - the `Process` class is a subclass representing the model-checked process;
 123
 124  - the `Snapshot` class is a subclass representing a snapshot of the process.
 125
 126 Additional helper class include:
 127
 128  - `Remote<T>` is the result of reading a `T` in a remote AddressSpace. For
 129     trivial types (int, etc.), it is convertible t o `T`;
 130
 131  - `RemotePtr<T>` represents the address of an object of type `T` in some
 132     remote `AddressSpace` (it could be an alias to `Remote<T*>`).
 133
 134 @subsection simgrid_uhood_mc_address_elf_dwarf ELF and DWARF
 135
 136 [ELF](http://refspecs.linuxbase.org/elf/elf.pdf) is a standard executable file
 137 and dynamic libraries file format.
 138 [DWARF](http://dwarfstd.org/) is a standard for debug information.
 139 Both are used on GNU/Linux systems and exploited by the model-checker to
 140 understand the model-checked process:
 141
 142  - `ObjectInformation` represents the information about a given ELF module
 143    (executable or shared-object);
 144
 145  - `Frame` represents a subprogram scope (either a subprogram or a scope within
 146     the subprogram);
 147
 148  - `Type` represents a type (eg. `char*`, `int`, `std::string`) and is referenced
 149     by variables (global, variables, parameters), functions (return type),
 150     and other types (type of a `struct` field, etc.);
 151
 152  - `LocationList` and `DwarfExpression` are used to describe the location of
 153     variables.
 154
 155 */