From 0287507e7e5adf63caec82d4b34704652cb73739 Mon Sep 17 00:00:00 2001
From: Maxwell Pirtle <maxwellpirtle@gmail.com>
Date: Mon, 15 May 2023 09:37:22 +0200
Subject: [PATCH] Add more documentation to ClockVector/Execution

---
 src/mc/api/ClockVector.hpp       | 22 ++++++++++++++++++++++
 src/mc/explo/odpor/Execution.hpp | 17 ++++++++++++++---
 2 files changed, 36 insertions(+), 3 deletions(-)

diff --git a/src/mc/api/ClockVector.hpp b/src/mc/api/ClockVector.hpp
index 93900358c8..5e6318bf4e 100644
--- a/src/mc/api/ClockVector.hpp
+++ b/src/mc/api/ClockVector.hpp
@@ -19,6 +19,28 @@ 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
+ *
+ * Clock vectors permit actors in a distributed system
+ * to determine whether two events occurred one after the other
+ * but they may not have); i.e. they permit actors to keep track of "time".
+ * A clever observation made in the original DPOR paper is that a
+ * transition-based "happens-before" relation can be computed for
+ * any particular trace `S` using clock vectors, effectively
+ * treating dependency like the passing of a message (the context
+ * in which vector clocks are typically used).
+ *
+ * Support, however, needs to be added to clock vectors since
+ * Simgrid permits the *creation* of new actors during execution.
+ * Since we don't know this size before-hand, we have to allow
+ * clock vectors to behave as if they were "infinitely" large. To
+ * do so, all newly mapped elements, if not assigned a value, are
+ * defaulted to `0`. This corresponds to the value this actor would
+ * have had regardless had its creation been known to have evnetually
+ * occurred: no actions taken by that actor had occurred prior, so
+ * there's no way the clock vector would have been updated. In other
+ * words, when comparing clock vectors of different sizes, it's equivalent
+ * to imagine both of the same size with elements absent in one or
+ * the other implicitly mapped to zero.
  */
 struct ClockVector final {
 private:
diff --git a/src/mc/explo/odpor/Execution.hpp b/src/mc/explo/odpor/Execution.hpp
index 552f76b95a..6013d216eb 100644
--- a/src/mc/explo/odpor/Execution.hpp
+++ b/src/mc/explo/odpor/Execution.hpp
@@ -23,6 +23,10 @@ using Hypothetical      = ExecutionSequence;
 
 /**
  * @brief The occurrence of a transition in an execution
+ *
+ * An execution is set of *events*, where each element represents
+ * the occurrence or execution of the `i`th step of a particular
+ * actor `j`
  */
 class Event {
   std::pair<const Transition*, ClockVector> contents_;
@@ -32,7 +36,6 @@ public:
   Event(Event&&)                 = default;
   Event(const Event&)            = default;
   Event& operator=(const Event&) = default;
-
   explicit Event(std::pair<const Transition*, ClockVector> pair) : contents_(std::move(pair)) {}
 
   const Transition* get_transition() const { return std::get<0>(contents_); }
@@ -57,8 +60,16 @@ public:
  * In addition to representing an actual steps taken,
  * an execution keeps track of the "happens-before"
  * relation among the transitions in the execution
- * by following the procedure outlined in the
- * original DPOR paper with clock vectors
+ * by following the procedure outlined in section 4 of the
+ * original DPOR paper with clock vectors.
+ * As new transitions are added to the execution, clock vectors are
+ * computed as appropriate and associated with the corresponding position
+ * in the execution. This allows us to determine “happens-before” in
+ * constant-time between points in the execution (called events
+ * [which is unfortunately the same name used in UDPOR for a slightly
+ * different concept]), albeit for an up-front cost of traversing the
+ * execution stack. The happens-before relation is important in many
+ * places in SDPOR and ODPOR.
  *
  * @note: For more nuanced happens-before relations, clock
  * vectors may not always suffice. Clock vectors work
-- 
2.20.1