src/mc/explo/odpor/Execution.hpp

   1 /* Copyright (c) 2007-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_ODPOR_EXECUTION_HPP
   7 #define SIMGRID_MC_ODPOR_EXECUTION_HPP
   8
   9 #include "src/mc/api/ClockVector.hpp"
  10 #include "src/mc/transition/Transition.hpp"
  11
  12 #include <optonal>
  13 #include <unordered_set>
  14 #include <vector>
  15
  16 namespace simgrid::mc::odpor {
  17
  18 using ProcessSequence   = std::list<aid_t>;
  19 using ExecutionSequence = std::list<const State*>;
  20 using Hypothetical      = ExecutionSequence;
  21
  22 /**
  23  * @brief The occurrence of a transition in an execution
  24  */
  25 class Event {
  26   std::pair<const Transition*, ClockVector> contents_;
  27
  28 public:
  29   Event()                         = default;
  30   Event(Event&&)                  = default;
  31   Event(const Event&)             = default;
  32   Event& operator=(const Event&)  = default;
  33   Event& operator=(const Event&&) = default;
  34
  35   explicit Event(std::pair<const Transition*, ClockVector> pair) : contents_(std::move(pair)) {}
  36
  37   const Transition* get_transition() const { return contents_.get<0>(); }
  38   const ClockVector& get_clock_vector() const { return contents_.get<1>(); }
  39 }
  40
  41 /**
  42  * @brief An ordered sequence of transitions which describe
  43  * the evolution of a process undergoing model checking
  44  *
  45  * An execution conceptually is just a string of actors
  46  * ids (e.g. "1.2.3.1.2.2.1.1"), where the `i`th occurrence
  47  * of actor id `j` corresponds to the `i`th action executed
  48  * by the actor with id `j` (viz. the `i`th step of actor `j`).
  49  * Executions can stand alone on their own or can extend
  50  * the execution of other sequences
  51  *
  52  * Executions are conceived based on the following papers:
  53  * 1. "Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction"
  54  * by Abdulla et al.
  55  *
  56  * In addition to representing an actual steps taken,
  57  * an execution keeps track of the "happens-before"
  58  * relation among the transitions in the execution
  59  * by following the procedure outlined in the
  60  * original DPOR paper with clock vectors
  61  *
  62  * @note: For more nuanced happens-before relations, clock
  63  * vectors may not always suffice. Clock vectors work
  64  * well with transition-based dependencies like that used in
  65  * SimGrid; but to have a more refined independence relation,
  66  * an event-based dependency approach is needed. See the section 2
  67  * in the ODPOR paper [1] concerning event-based dependencies and
  68  * how the happens-before relation can be refined in a
  69  * computation model much like that of SimGrid. In fact, the same issue
  70  * arrises with UDPOR with context-sensitive dependencies:
  71  * the two concepts are analogous if not identical
  72  */
  73 class Execution {
  74 public:
  75   using Handle = decltype(contents_)::const_iterator;
  76
  77   Execution()                            = default;
  78   Execution(const Execution&)            = default;
  79   Execution& operator=(Execution const&) = default;
  80   Execution(Execution&&)                 = default;
  81
  82   Execution(ExecutionSequence&& seq, std::optional<Handle> base = {});
  83   Execution(const ExecutionSequence& seq, std::optional<Handle> base = {});
  84
  85   std::unordered_set<aid_t> get_initials_after(const Hypothetical& w) const;
  86   std::unordered_set<aid_t> get_weak_initials_after(const Hypothetical& w) const;
  87
  88   bool is_initial(aid_t p, const Hypothetical& w) const;
  89   bool is_weak_initial(aid_t p, const Hypothetical& w) const;
  90
  91   /**
  92    * @brief Removes the last event of the execution,
  93    * if such an event exists
  94    *
  95    * @note: When you remove events from an execution, any views
  96    * of the execution referring to those removed events
  97    * become invalidated
  98    */
  99   void pop_latest();
 100
 101   /**
 102    * @brief Extends the execution by one more step
 103    *
 104    * Intutively, pushing a transition `t` onto execution `E`
 105    * is equivalent to making the execution become (using the
 106    * notation of [1]) `E.proc(t)` where `proc(t)` is the
 107    * actor which executed transition `t`.
 108    */
 109   void push_transition(const Transition*);
 110
 111   size_t size() const { return this->contents_.size(); }
 112   size_t size() const { return this->contents_.size(); }
 113
 114 private:
 115   /**
 116    * @brief A pointer into the execution off of which this
 117    * execution extends computation
 118    *
 119    * Conceptually, the `prior`
 120    */
 121   std::optional<Handle> prior;
 122
 123   /**
 124    * @brief The actual steps that are taken by the process
 125    * during exploration, relative to the
 126    */
 127   std::list<Event> contents_;
 128 };
 129
 130 } // namespace simgrid::mc::odpor
 131 #endif