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  - @subpage inside
  10
  11 \section simgrid_uhood_async Asynchronous operations
  12
  13 \subsection simgrid_uhood_futures Futures
  14
  15 The `simgrid::kernel::Future` class has been added to SimGrid as an abstraction
  16 to represent asynchronous operations in the SimGrid maestro. Its API is based
  17 on `std::experimental::future` from the [C++ Extensions for Concurrency Technical
  18 Specification](http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2015/p0159r0.html):
  19
  20  - `simgrid::kernel::Future<T>` represents the result an asynchronous operations
  21     in the simulation inside the SimGrid maestro/kernel;
  22
  23  - `simgrid::kernel::Promise<T>` can be used to set the value of an assocaiated
  24    `simgrid::kernel::Future<T>`.
  25
  26 The expected way to work with `simgrid::kernel::Future<T>` is to add a
  27 completion handler/continuation:
  28
  29 ~~~
  30 // This code is executed in the maestro context, we cannot block for the result
  31 // to be ready:
  32 simgrid::kernel::Future<std::vector<char>> result = simgrid::kernel::readFile(file);
  33
  34 // Add a completion handler:
  35 result.then([file](simgrid::kernel::Future<std::vector<char>> result) {
  36   // At this point, the operation is complete and we can safely call .get():
  37   xbt_assert(result.is_ready());
  38   try {
  39     std::vector<char> data = result.get();
  40     XBT_DEBUG("Finished reading file %s: length %zu", file.c_str(), data.size());
  41   }
  42   // If the operation failed, .get() throws an exception:
  43   catch (std::runtime_error& e) {
  44     XBT_ERROR("Could not read file %s", file.c_str());
  45   }
  46 });
  47 ~~~
  48
  49 The SimGrid kernel cannot block so calling `.get()` or `.wait()` on a
  50 `simgrid::kernel::Future<T>` which is not ready will deadlock. In practice, the
  51 simulator detects this and aborts after reporting an error.
  52
  53 In order to generate your own future, you might need to use a
  54 `simgrid::kernel::Promise<T>`. The promise is a one-way channel which can be
  55 used to set the result of an associated `simgrid::kernel::Future<T>`
  56 (with either `.set_value()` or `.set_exception()`):
  57
  58 ~~~
  59 simgrid::kernel::Future<void> kernel_wait_until(double date)
  60 {
  61   auto promise = std::make_shared<simgrid::kernel::Promise<void>>();
  62   auto future = promise->get_future();
  63   SIMIX_timer_set(date, [promise] {
  64     promise->set_value();
  65   });
  66   return future;
  67 }
  68 ~~~
  69
  70 Like the experimental futures, we support chaining `.then()` methods with
  71 automatic future unwrapping.
  72 You might want to look at some [C++ tutorial on futures](https://www.youtube.com/watch?v=mPxIegd9J3w&list=PLHTh1InhhwT75gykhs7pqcR_uSiG601oh&index=43)
  73 for more details and examples. Some operations of the proposed experimental
  74 futures are currently not implemented in our futures however such as
  75 `.wait_for()`, `.wait_until()`, `shared_future`, `when_any()`.
  76
  77 \subsection simgrid_uhood_timer Timers
  78
  79 \section simgrid_uhood_mc Model Checker
  80
  81 The current implementation of the model-checker uses two distinct processes:
  82
  83  - the SimGrid model-checker (`simgrid-mc`) itself lives in the parent process;
  84
  85  - it spaws a child process for the SimGrid simulator/mastro and the simulated
  86    processes.
  87
  88 They communicate using a `AF_UNIX` `SOCK_DGRAM` socket and exchange messages
  89 defined in `mc_protocol.h`. The `SIMGRID_MC_SOCKET_FD` environment variable it
  90 set to the file descriptor of this socket in the child process.
  91
  92 The model-checker analyzes, saves and restores the state of the model-checked
  93 process using the following techniques:
  94
  95 * the model-checker reads and writes in the model-checked address space;
  96
  97 * the model-cheker `ptrace()`s the model-checked process and is thus able to
  98   know the state of the model-checked process if it crashes;
  99
 100 * DWARF debug informations are used to unwind the stack and identify local
 101   variables;
 102
 103 * a custom heap is enabled in the model-checked process which allows the model
 104   checker to know which chunks are allocated and which are freed.
 105
 106 \subsection simgrid_uhood_mc_address_space Address space
 107
 108 The `AddressSpace` is a base class used for both the model-checked process
 109 and its snapshots and has methods to read in the corresponding address space:
 110
 111  - the `Process` class is a subclass representing the model-checked process;
 112
 113  - the `Snapshot` class is a subclass representing a snapshot of the process.
 114
 115 Additional helper class include:
 116
 117  - `Remote<T>` is the result of reading a `T` in a remote AddressSpace. For
 118     trivial types (int, etc.), it is convertible t o `T`.
 119
 120  - `RemotePtr<T>` represents the address of an object of type `T` in some
 121     remote `AddressSpace` (it could be an alias to `Remote<T*>`).
 122
 123 \subsection simgrid_uhood_mc_address_elf_dwarf ELF and DWARF
 124
 125 ELF is a standard executable file and dynamic libraries file format.
 126 DWARF is a standard for debug informations. Both are used on GNU/Linux systems
 127 and exploited by the model-checker to understand the model-checked process:
 128
 129  - `ObjectInformation` represents the informations about a given ELF module
 130    (executable or shared-object);
 131
 132  - `Frame` represents a subprogram scope (either a subprogram or a scope within
 133     the subprogram);
 134
 135  - `Type` represents a type (`char*`, `int`, `std::string`) and is referenced
 136     by variables (global, variables, parameters), functions (return type),
 137     and other types (type of a `struct` field, etc.);
 138
 139  - `LocationList` and `DwarfExpression` are used to describe the location of
 140     variables.
 141
 142 */