src/mc/api/ClockVector.hpp

   1 /* Copyright (c) 2016-2023. 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 #ifndef SIMGRID_MC_CLOCK_VECTOR_HPP
   7 #define SIMGRID_MC_CLOCK_VECTOR_HPP
   8
   9 #include "simgrid/forward.h"
  10
  11 #include <cstdint>
  12 #include <initializer_list>
  13 #include <optional>
  14 #include <unordered_map>
  15
  16 namespace simgrid::mc {
  17
  18 /**
  19  * @brief A multi-dimensional vector used to keep track of
  20  * happens-before relation between dependent events in an
  21  * execution of DPOR, SDPOR, or ODPOR
  22  */
  23 struct ClockVector final {
  24 private:
  25   std::unordered_map<aid_t, uint32_t> contents;
  26
  27 public:
  28   ClockVector()                              = default;
  29   ClockVector(const ClockVector&)            = default;
  30   ClockVector& operator=(ClockVector const&) = default;
  31   ClockVector(ClockVector&&)                 = default;
  32   ClockVector(std::initializer_list<std::pair<const aid_t, uint32_t>> init) : contents(std::move(init)) {}
  33
  34   /**
  35    * @brief The number of components in this
  36    * clock vector
  37    *
  38    * A `ClockVector` implicitly maps the id of an actor
  39    * it does not contain to a default value of `0`.
  40    * Thus, a `ClockVector` is "lazy" in the sense
  41    * that new actors are "automatically" mapped
  42    * without needing to be explicitly added the clock
  43    * vector when the actor is created. This means that
  44    * comparison between clock vectors is possible
  45    * even as actors become enabled and disabled
  46    *
  47    * @return uint32_t the number of elements in
  48    * the clock vector
  49    */
  50   size_t size() const { return this->contents.size(); }
  51
  52   uint32_t& operator[](aid_t aid)
  53   {
  54     // NOTE: The `operator[]` overload of
  55     // unordered_map will create a new key-value
  56     // pair if `tid` does not exist and will use
  57     // a _default_ value for the value (0 in this case)
  58     // which is precisely what we want here
  59     return this->contents[aid];
  60   }
  61
  62   /**
  63    * @brief Retrieves the value mapped to the given
  64    * actor if it is contained in this clock vector
  65    */
  66   std::optional<uint32_t> get(aid_t aid) const
  67   {
  68     if (const auto iter = this->contents.find(aid); iter != this->contents.end())
  69       return std::optional<uint32_t>{iter->second};
  70     return std::nullopt;
  71   }
  72
  73   /**
  74    * @brief Computes a clock vector whose components
  75    * are larger than the components of both of
  76    * the given clock vectors
  77    *
  78    * The maximum of two clock vectors is definied to
  79    * be the clock vector whose components are the maxmimum
  80    * of the corresponding components of the arguments.
  81    * Since the `ClockVector` class is "lazy", the two
  82    * clock vectors given as arguments may not be of the same size.
  83    * The resultant clock vector has components as follows:
  84    *
  85    * 1. For each actor that each clock vector maps, the
  86    * resulting clock vector maps that thread to the maxmimum
  87    * of the values mapped for the actor in each clock vector
  88    *
  89    * 2. For each actor that only a single clock vector maps,
  90    * the resulting clock vector maps that thread to the
  91    * value mapped by the lone clock vector
  92    *
  93    * The scheme is equivalent to assuming that an unmapped
  94    * thread by any one clock vector is implicitly mapped to zero
  95    *
  96    * @param cv1 the first clock vector
  97    * @param cv2  the second clock vector
  98    * @return a clock vector whose components are at
  99    * least as large as the corresponding components of each clock
 100    * vector and whose size is large enough to contain the union
 101    * of components of each clock vector
 102    */
 103   static ClockVector max(const ClockVector& cv1, const ClockVector& cv2);
 104 };
 105
 106 } // namespace simgrid::mc
 107
 108 #endif