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