From 9d23bfe5e8febe2b55c45e7fcd72d50644fac6ca Mon Sep 17 00:00:00 2001 From: Maxwell Pirtle Date: Mon, 24 Apr 2023 14:55:12 +0200 Subject: [PATCH] Add class for eventual "happens-before" computations Computing the "happens-before" relation over a sequence of executions is an important step in determining whether or not DPOR (and SDPOR alike) needs to add a backtracking point. This commit introduces the "ClockVector" class which acts effectively as a light wrapping around an `unordered_map` mapping actor ids to integer values. The essential component of the ClockVector class is that its contents are "implicit" in the sense that actors for which no value is explicitly contained in the map are assigned to the value `0` by default. This allows clock vectors to be flexible enough to support the creation of new actors and the enabling/disabling of old actors as they come and go. --- MANIFEST.in | 2 + src/mc/api/ClockVector.cpp | 23 +++++++ src/mc/api/ClockVector.hpp | 106 +++++++++++++++++++++++++++++++ tools/cmake/DefinePackages.cmake | 2 + 4 files changed, 133 insertions(+) create mode 100644 src/mc/api/ClockVector.cpp create mode 100644 src/mc/api/ClockVector.hpp diff --git a/MANIFEST.in b/MANIFEST.in index 3a5d39ce5e..74943c16d7 100644 --- a/MANIFEST.in +++ b/MANIFEST.in @@ -2171,6 +2171,8 @@ include src/mc/AddressSpace.hpp include src/mc/VisitedState.cpp include src/mc/VisitedState.hpp include src/mc/api/ActorState.hpp +include src/mc/api/ClockVector.cpp +include src/mc/api/ClockVector.hpp include src/mc/api/RemoteApp.cpp include src/mc/api/RemoteApp.hpp include src/mc/api/State.cpp diff --git a/src/mc/api/ClockVector.cpp b/src/mc/api/ClockVector.cpp new file mode 100644 index 0000000000..b411bba06a --- /dev/null +++ b/src/mc/api/ClockVector.cpp @@ -0,0 +1,23 @@ +/* Copyright (c) 2015-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#include "src/mc/api/ClockVector.hpp" + +namespace simgrid::mc { + +ClockVector ClockVector::max(const ClockVector& cv1, const ClockVector& cv2) +{ + auto max_vector = ClockVector(); + + for (const auto& [aid, value] : cv1.contents) + max_vector[aid] = std::max(value, cv2.get(aid).value_or(0)); + + for (const auto& [aid, value] : cv2.contents) + max_vector[aid] = std::max(value, cv1.get(aid).value_or(0)); + + return max_vector; +} + +} // namespace simgrid::mc \ No newline at end of file diff --git a/src/mc/api/ClockVector.hpp b/src/mc/api/ClockVector.hpp new file mode 100644 index 0000000000..d4dfa377cd --- /dev/null +++ b/src/mc/api/ClockVector.hpp @@ -0,0 +1,106 @@ +/* Copyright (c) 2016-2023. The SimGrid Team. All rights reserved. */ + +/* This program is free software; you can redistribute it and/or modify it + * under the terms of the license (GNU LGPL) which comes with this package. */ + +#ifndef SIMGRID_MC_CLOCK_VECTOR_HPP +#define SIMGRID_MC_CLOCK_VECTOR_HPP + +#include "simgrid/forward.h" + +#include +#include +#include + +namespace simgrid::mc { + +/** + * @brief A multi-dimensional vector used to keep track of + * happens-before relation between dependent events in an + * execution of DPOR, SDPOR, or ODPOR + */ +struct ClockVector final { +private: + std::unordered_map contents; + +public: + ClockVector() = default; + ClockVector(const ClockVector&) = default; + ClockVector& operator=(ClockVector const&) = default; + ClockVector(ClockVector&&) = default; + + /** + * @brief The number of components in this + * clock vector + * + * A `ClockVector` implicitly maps the id of an actor + * it does not contain to a default value of `0`. + * Thus, a `ClockVector` is "lazy" in the sense + * that new actors are "automatically" mapped + * without needing to be explicitly added the clock + * vector when the actor is created. This means that + * comparison between clock vectors is possible + * even as actors become enabled and disabled + * + * @return uint32_t the number of elements in + * the clock vector + */ + size_t size() const { return this->contents.size(); } + + uint32_t& operator[](aid_t aid) + { + // NOTE: The `operator[]` overload of + // unordered_map will create a new key-value + // pair if `tid` does not exist and will use + // a _default_ value for the value (0 in this case) + // which is precisely what we want here + return this->contents[aid]; + } + + /** + * @brief Retrieves the value mapped to the given + * actor if it is contained in this clock vector + */ + std::optional get(aid_t aid) const + { + if (const auto iter = this->contents.find(aid); iter != this->contents.end()) + return std::optional{iter->second}; + return std::nullopt; + } + + /** + * @brief Computes a clock vector whose components + * are larger than the components of both of + * the given clock vectors + * + * The maximum of two clock vectors is definied to + * be the clock vector whose components are the maxmimum + * of the corresponding components of the arguments. + * Since the `ClockVector` class is "lazy", the two + * clock vectors given as arguments may not be of the same size. + * The resultant clock vector has components as follows: + * + * 1. For each actor that each clock vector maps, the + * resulting clock vector maps that thread to the maxmimum + * of the values mapped for the actor in each clock vector + * + * 2. For each actor that only a single clock vector maps, + * the resulting clock vector maps that thread to the + * value mapped by the lone clock vector + * + * The scheme is equivalent to assuming that an unmapped + * thread by any one clock vector is implicitly mapped to zero + * + * @param cv1 the first clock vector + * @param cv2 the second clock vector + * @return a clock vector whose components are at + * least as large as the corresponding components of each clock + * vector and whose size is large enough to contain the union + * of components of each clock vector + */ + static ClockVector max(const ClockVector& cv1, const ClockVector& cv2); +}; + +} // namespace simgrid::mc + +#endif diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake index c7e01f71a6..d1a6d6738c 100644 --- a/tools/cmake/DefinePackages.cmake +++ b/tools/cmake/DefinePackages.cmake @@ -523,6 +523,8 @@ set(MC_SRC_BASE set(MC_SRC_STATELESS src/mc/api/ActorState.hpp + src/mc/api/ClockVector.cpp + src/mc/api/ClockVector.hpp src/mc/api/State.cpp src/mc/api/State.hpp src/mc/api/RemoteApp.cpp -- 2.20.1