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 std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
  13 {
  14   std::unordered_set<Execution::EventHandle> racing_events;
  15   std::unordered_set<Execution::EventHandle> disqualified_events;
  16
  17   // For each event of the execution
  18   for (auto e_i = target; e_i > 0 && e_i != std::numeric_limits<Execution::EventHandle>::max(); e_i--) {
  19     // We need `e_i -->_E target` as a necessary condition
  20     if (not happens_before(e_i, target)) {
  21       continue;
  22     }
  23
  24     // Further, `proc(e_i) != proc(target)`
  25     if (get_actor_with_handle(e_i) == get_actor_with_handle(target)) {
  26       disqualified_events.insert(e_i);
  27       continue;
  28     }
  29
  30     // There could an event that "happens-between" the two events which would discount `e_i` as a race
  31     for (auto e_j = e_i; e_j < target; e_j++) {
  32       // If both:
  33       // 1. e_i --->_E e_j; and
  34       // 2. disqualified_events.count(e_j) > 0
  35       // then e_i --->_E target indirectly (either through
  36       // e_j directly, or transitively through e_j)
  37       if (happens_before(e_i, e_j) and disqualified_events.count(e_j) > 0) {
  38         disqualified_events.insert(e_i);
  39         break;
  40       }
  41     }
  42
  43     // If `e_i` wasn't disqualified in the last round,
  44     // it's in a race with `target`. After marking it
  45     // as such, we ensure no other event `e` can happen-before
  46     // it (since this would transitively make it the event
  47     // which "happens-between" `target` and `e`)
  48     if (disqualified_events.count(e_i) == 0) {
  49       racing_events.insert(e_i);
  50       disqualified_events.insert(e_i);
  51     }
  52   }
  53
  54   return racing_events;
  55 }
  56
  57 bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::EventHandle e2_handle) const
  58 {
  59   // 1. "happens-before" is a subset of "occurs before"
  60   if (e1_handle > e2_handle) {
  61     return false;
  62   }
  63
  64   // Each execution maintains a stack of clock vectors which are updated
  65   // according to the procedure outlined in section 4 of the original DPOR paper
  66   const Event& e2     = get_event_with_handle(e2_handle);
  67   const aid_t proc_e1 = get_actor_with_handle(e1_handle);
  68   return e1_handle <= e2.get_clock_vector().get(proc_e1).value_or(0);
  69 }
  70
  71 Execution Execution::get_prefix_up_to(Execution::EventHandle handle)
  72 {
  73   if (handle == static_cast<Execution::EventHandle>(0)) {
  74     return Execution();
  75   }
  76   return Execution(std::vector<Event>{contents_.begin(), contents_.begin() + (handle - 1)});
  77 }
  78
  79 void Execution::push_transition(const Transition* t)
  80 {
  81   if (t == nullptr) {
  82     throw std::invalid_argument("Unexpectedly received `nullptr`");
  83   }
  84   ClockVector max_clock_vector;
  85   for (const Event& e : this->contents_) {
  86     if (e.get_transition()->depends(t)) {
  87       max_clock_vector = ClockVector::max(max_clock_vector, e.get_clock_vector());
  88     }
  89   }
  90   // The entry in the vector for `t->aid_` is the size
  91   // of the new stack, which will have a size one greater
  92   // than that before we insert the new events
  93   max_clock_vector[t->aid_] = this->size() + 1;
  94   contents_.push_back(Event({t, max_clock_vector}));
  95 }
  96
  97 void Execution::pop_latest()
  98 {
  99   contents_.pop_back();
 100 }
 101
 102 } // namespace simgrid::mc::odpor