src/mc/explo/sdpor/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 <unordered_set>
  13 #include <vector>
  14
  15 namespace simgrid::mc::odpor {
  16
  17 /**
  18  * @brief An ordered sequence of actions
  19  */
  20 class ExecutionSequence : public std::list<const Transition*> {};
  21 using Hypothetical = ExecutionSequence;
  22
  23 /**
  24  * @brief The occurrence of a transition in an execution
  25  */
  26 class Event {
  27   std::pair<const Transition*, ClockVector> contents_;
  28
  29 public:
  30   Event()                         = default;
  31   Event(Event&&)                  = default;
  32   Event(const Event&)             = default;
  33   Event& operator=(const Event&)  = default;
  34   Event& operator=(const Event&&) = default;
  35
  36   explicit Event(std::pair<const Transition*, ClockVector> pair) : contents_(std::move(pair)) {}
  37
  38   const Transition* get_transition() const { return contents_.get<0>(); }
  39   const ClockVector& get_clock_vector() const { return contents_.get<1>(); }
  40 }
  41
  42 /**
  43  * @brief An ordered sequence of transitions which describe
  44  * the evolution of a process undergoing model checking
  45  *
  46  * Executions are conceived based on the following papers:
  47  * 1. "Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction"
  48  * by Abdulla et al.
  49  *
  50  * In addition to representing an actual steps taken,
  51  * an execution keeps track of the "happens-before"
  52  * relation among the transitions in the execution
  53  * by following the procedure outlined in the
  54  * original DPOR paper with clock vectors
  55  *
  56  * @note: For more nuanced happens-before relations, clock
  57  * vectors may not always suffice. Clock vectors work
  58  * well with transition-based dependencies like that used in
  59  * SimGrid; but to have a more refined independence relation,
  60  * an event-based dependency approach is needed. See the section 2
  61  * in the ODPOR paper [1] concerning event-based dependencies and
  62  * how the happens-before relation can be refined in a
  63  * computation model much like that of SimGrid. In fact, the same issue
  64  * arrises with UDPOR with context-sensitive dependencies:
  65  * the two concepts are analogous if not identical
  66  */
  67 class Execution {
  68 private:
  69   /**
  70    * @brief The actual steps that are taken by the process
  71    * during exploration.
  72    */
  73   std::list<Event> contents_;
  74
  75 public:
  76   Execution()                            = default;
  77   Execution(const Execution&)            = default;
  78   Execution& operator=(Execution const&) = default;
  79   Execution(Execution&&)                 = default;
  80   explicit Execution(ExecutionSequence&& seq);
  81   explicit Execution(const ExecutionSequence& seq);
  82
  83   std::unordered_set<aid_t> get_initials_after(const Hypothetical& w) const;
  84   std::unordered_set<aid_t> get_weak_initials_after(const Hypothetical& w) const;
  85
  86   bool is_initial(aid_t p, const Hypothetical& w) const;
  87   bool is_weak_initial(aid_t p, const Hypothetical& w) const;
  88
  89   void take_action(const Transition*);
  90 };
  91
  92 } // namespace simgrid::mc::odpor
  93 #endif