src/mc/explo/odpor/Execution.cpp

   1 /* Copyright (c) 2008-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 #include "src/mc/explo/odpor/Execution.hpp"
   7 #include <exception>
   8 #include <limits>
   9
  10 namespace simgrid::mc::odpor {
  11
  12 void Execution::push_transition(const Transition* t)
  13 {
  14   if (t == nullptr) {
  15     throw std::invalid_argument("Unexpectedly received `nullptr`");
  16   }
  17   ClockVector max_clock_vector;
  18   for (const Event& e : this->contents_) {
  19     if (e.get_transition()->depends(t)) {
  20       max_clock_vector = ClockVector::max(max_clock_vector, e.get_clock_vector());
  21     }
  22   }
  23   // The entry in the vector for `t->aid_` is the size
  24   // of the stack
  25   max_clock_vector[t->aid_] = this->size();
  26   contents_.push_back(Event({t, max_clock_vector}));
  27 }
  28
  29 void Execution::pop_latest()
  30 {
  31   contents_.pop_back();
  32 }
  33
  34 std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
  35 {
  36   std::unordered_set<Execution::EventHandle> racing_events;
  37   std::unordered_set<Execution::EventHandle> disqualified_events;
  38
  39   // For each event of the execution
  40   for (auto e_i = target; e_i != std::numeric_limits<Execution::EventHandle>::max(); e_i--) {
  41     // We need `e_i -->_E target` as a necessary condition
  42     if (not happens_before(e_i, target)) {
  43       continue;
  44     }
  45
  46     // Further, `proc(e_i) != proc(target)`
  47     if (get_actor_with_handle(e_i) == get_actor_with_handle(target)) {
  48       disqualified_events.insert(e_i);
  49       continue;
  50     }
  51
  52     // There could an event that "happens-between" the two events which would discount `e_i` as a race
  53     for (auto e_j = e_i; e_j < target; e_j++) {
  54       // If both:
  55       // 1. e_i --->_E e_j; and
  56       // 2. disqualified_events.count(e_j) > 0
  57       // then e_i --->_E target indirectly (either through
  58       // e_j directly, or transitively through e_j)
  59       if (happens_before(e_i, e_j) and disqualified_events.count(e_j) > 0) {
  60         disqualified_events.insert(e_i);
  61         break;
  62       }
  63     }
  64
  65     // If `e_i` wasn't disqualified in the last round,
  66     // it's in a race with `target`. After marking it
  67     // as such, we ensure no other event `e` can happen-before
  68     // it (since this would transitively make it the event
  69     // which "happens-between" `target` and `e`)
  70     if (disqualified_events.count(e_i) == 0) {
  71       racing_events.insert(e_i);
  72       disqualified_events.insert(e_i);
  73     }
  74   }
  75
  76   return racing_events;
  77 }
  78
  79 Execution Execution::get_prefix_up_to(Execution::EventHandle handle) const
  80 {
  81   return Execution(std::vector<Event>{contents_.begin(), contents_.begin() + handle});
  82 }
  83
  84 std::optional<aid_t> Execution::get_first_ssdpor_initial_from(EventHandle e,
  85                                                               std::unordered_set<aid_t> disqualified_actors) const
  86 {
  87   // If this execution is empty, there are no initials
  88   // relative to the last transition added to the execution
  89   // since such a transition does not exist
  90   if (empty()) {
  91     return std::nullopt;
  92   }
  93
  94   // First, grab `E' := pre(e, E)` and determine what actor `p` is
  95   // TODO: Instead of copying around these big structs, it
  96   // would behoove us to incorporate some way to reference
  97   // portions of an execution. For simplicity and for a
  98   // "proof of concept" version, we opt to simply copy
  99   // the contents instead of making a view into the execution
 100   const auto next_E_p = get_latest_event_handle().value();
 101   Execution E_prime_v = get_prefix_up_to(e);
 102   std::vector<sdpor::Execution::EventHandle> v;
 103
 104   // Note `e + 1` here: `notdep(e, E)` is defined as the
 105   // set of events that *occur-after* but don't *happen-after* `e`
 106   for (auto e_prime = e + 1; e_prime <= next_E_p; ++e_prime) {
 107     // Any event `e*` which occurs after `e` but which does not
 108     // happen after `e` is a member of `v`. In addition to marking
 109     // the event in `v`, we also "simulate" running the action `v`
 110     // from E'
 111     if (not happens_before(e, e_prime) or e_prime == next_E_p) {
 112       v.push_back(e_prime);
 113       E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
 114     } else {
 115       continue;
 116     }
 117     const EventHandle e_prime_in_E_prime = E_prime_v.get_latest_event_handle().value();
 118     const aid_t q                        = E_prime_v.get_actor_with_handle(e_prime_in_E_prime);
 119     if (disqualified_actors.count(q) > 0) {
 120       continue;
 121     }
 122     const bool is_initial = std::none_of(
 123         v.begin(), v.end(), [&](const auto& e_star) { return E_prime_v.happens_before(e_star, e_prime_in_E_prime); });
 124     if (is_initial) {
 125       return q;
 126     } else {
 127       disqualified_actors.insert(q);
 128     }
 129   }
 130   return std::nullopt;
 131 }
 132
 133 std::unordered_set<aid_t> Execution::get_ssdpor_initials_from(EventHandle e,
 134                                                               std::unordered_set<aid_t> disqualified) const
 135 {
 136   return std::unordered_set<aid_t>();
 137 }
 138
 139 bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::EventHandle e2_handle) const
 140 {
 141   // 1. "happens-before" (-->_E) is a subset of "occurs before" (<_E)
 142   // and is an irreflexive relation
 143   if (e1_handle >= e2_handle) {
 144     return false;
 145   }
 146
 147   // Each execution maintains a stack of clock vectors which are updated
 148   // according to the procedure outlined in section 4 of the original DPOR paper
 149   const Event& e2     = get_event_with_handle(e2_handle);
 150   const aid_t proc_e1 = get_actor_with_handle(e1_handle);
 151
 152   if (const auto e1_in_e2_clock = e2.get_clock_vector().get(proc_e1); e1_in_e2_clock.has_value()) {
 153     return e1_handle <= e1_in_e2_clock.value();
 154   }
 155   // If `e1` does not appear in e2's clock vector, this implies
 156   // not only that the transitions associated with `e1` and `e2
 157   // are independent, but further that there are no transitive
 158   // dependencies between e1 and e2
 159   return false;
 160 }
 161
 162 } // namespace simgrid::mc::odpor