#include "src/mc/explo/odpor/Execution.hpp"
#include "src/mc/api/State.hpp"
+#include "src/mc/explo/odpor/ReversibleRaceCalculator.hpp"
#include "xbt/asserts.h"
+#include "xbt/string.hpp"
#include <algorithm>
#include <limits>
#include <vector>
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_execution, mc_dfs, "ODPOR exploration algorithm of the model-checker");
+
namespace simgrid::mc::odpor {
+std::vector<std::string> get_textual_trace(const PartialExecution& w)
+{
+ std::vector<std::string> trace;
+ for (const auto& t : w) {
+ auto a = xbt::string_printf("Actor %ld: %s", t->aid_, t->to_string(true).c_str());
+ trace.emplace_back(std::move(a));
+ }
+ return trace;
+}
+
+Execution::Execution(const PartialExecution& w)
+{
+ push_partial_execution(w);
+}
+
void Execution::push_transition(std::shared_ptr<Transition> t)
{
if (t == nullptr) {
contents_.push_back(Event({std::move(t), max_clock_vector}));
}
+void Execution::push_partial_execution(const PartialExecution& w)
+{
+ for (const auto& t : w) {
+ push_transition(t);
+ }
+}
+
+std::vector<std::string> Execution::get_textual_trace() const
+{
+ std::vector<std::string> trace;
+ for (const auto& t : this->contents_) {
+ auto a = xbt::string_printf("Actor %ld: %s", t.get_transition()->aid_, t.get_transition()->to_string(true).c_str());
+ trace.emplace_back(std::move(a));
+ }
+ return trace;
+}
+
std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
{
std::unordered_set<Execution::EventHandle> racing_events;
+ // This keep tracks of events that happens-before the target
std::unordered_set<Execution::EventHandle> disqualified_events;
// For each event of the execution
for (auto e_i = target; e_i != std::numeric_limits<Execution::EventHandle>::max(); e_i--) {
// We need `e_i -->_E target` as a necessary condition
if (not happens_before(e_i, target)) {
+ XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` discarded because `%u` --\\-->_E `%u`", target, e_i, e_i, target);
continue;
}
// Further, `proc(e_i) != proc(target)`
if (get_actor_with_handle(e_i) == get_actor_with_handle(target)) {
disqualified_events.insert(e_i);
+ XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` disqualified because proc(`%u`)=proc(`%u`)", target, e_i, e_i,
+ target);
continue;
}
// 2. disqualified_events.count(e_j) > 0
// then e_i --->_E target indirectly (either through
// e_j directly, or transitively through e_j)
- if (happens_before(e_i, e_j) and disqualified_events.count(e_j) > 0) {
+ if (disqualified_events.count(e_j) > 0 && happens_before(e_i, e_j)) {
+ XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` disqualified because `%u` happens-between `%u`-->`%u`-->`%u`)",
+ target, e_i, e_j, e_i, e_j, target);
disqualified_events.insert(e_i);
break;
}
// it (since this would transitively make it the event
// which "happens-between" `target` and `e`)
if (disqualified_events.count(e_i) == 0) {
+ XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` is a valid racing event", target, e_i);
racing_events.insert(e_i);
disqualified_events.insert(e_i);
}
return racing_events;
}
+std::unordered_set<Execution::EventHandle> Execution::get_reversible_races_of(EventHandle handle) const
+{
+ std::unordered_set<EventHandle> reversible_races;
+ for (EventHandle race : get_racing_events_of(handle)) {
+ if (ReversibleRaceCalculator::is_race_reversible(*this, race, handle)) {
+ reversible_races.insert(race);
+ }
+ }
+ return reversible_races;
+}
+
Execution Execution::get_prefix_before(Execution::EventHandle handle) const
{
return Execution(std::vector<Event>{contents_.begin(), contents_.begin() + handle});
}
-std::optional<aid_t> Execution::get_first_sdpor_initial_from(EventHandle e,
- std::unordered_set<aid_t> disqualified_actors) const
+std::unordered_set<aid_t>
+Execution::get_missing_source_set_actors_from(EventHandle e, const std::unordered_set<aid_t>& backtrack_set) const
{
// If this execution is empty, there are no initials
// relative to the last transition added to the execution
// since such a transition does not exist
if (empty()) {
- return std::nullopt;
+ return std::unordered_set<aid_t>{};
}
// To actually compute `I_[E'](v) ∩ backtrack(E')`, we must
// note of any events which occur after `e` but don't
// "happen-after" `e` by pushing them onto `E'`. Note that
// correctness is still preserved in computing `v` "on-the-fly"
- // to determine if an actor `q` is an initial for `E'` after `v`:
- // only those events that "occur-before" `v`
- // could happen-before `v` for any valid happens-before relation.
+ // to determine if an event `e` by actor `q` is an initial for `E'`
+ // after `v`: only those events that "occur-before" `e` in `v` could
+ // "happen-before" `ve for any valid "happens-before" relation
+ // (see property 1 in the ODPOR paper, viz. "is included in <_E")
// First, grab `E' := pre(e, E)` and determine what actor `p` is
const auto next_E_p = get_latest_event_handle().value();
+ xbt_assert(e != next_E_p,
+ "This method assumes that the event `e` (%u) and `next_[E](p)` (%u)"
+ "are in a reversible race, yet we claim to have such a race between the"
+ "same event. This indicates the the SDPOR pseudocode implementation is broken "
+ "as it supplies these values.",
+ e, next_E_p);
Execution E_prime_v = get_prefix_before(e);
std::vector<sdpor::Execution::EventHandle> v;
+ std::unordered_set<aid_t> I_E_prime_v;
+ std::unordered_set<aid_t> disqualified_actors;
// Note `e + 1` here: `notdep(e, E)` is defined as the
// set of events that *occur-after* but don't *happen-after* `e`
// happen after `e` is a member of `v`. In addition to marking
// the event in `v`, we also "simulate" running the action `v`
// from E'
- if (not happens_before(e, e_prime) or e_prime == next_E_p) {
+ if (not happens_before(e, e_prime) || e_prime == next_E_p) {
// First, push the transition onto the hypothetical execution
E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
// events relative to `E` (this execution) are different than those
// relative to `E'.v`. Thus e.g. event `7` in `E` may be event `4`
// in `E'.v`. Since we are asking about "happens-before"
- // `-->_[E'.v]` about `E'.v`, we must build `v` relative to `E'`
+ // `-->_[E'.v]` about `E'.v`, we must build `v` relative to `E'`.
+ //
+ // Note that we add `q` to v regardless of whether `q` itself has been
+ // disqualified since we've determined that `e_prime` "occurs-after" but
+ // does not "happen-after" `e`
v.push_back(e_prime_in_E_prime_v);
- // Note that we add `q` to v regardless of whether `q` itself has been
- // disqualified since `q` may itself disqualify other actors
- // (i.e. even if `q` is disqualified from being an initial, it
- // is still contained in the sequence `v`)
const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v);
- if (disqualified_actors.count(q) > 0) {
+ if (disqualified_actors.count(q) > 0) { // Did we already note that `q` is not an initial?
continue;
}
const bool is_initial = std::none_of(v.begin(), v.end(), [&](const auto& e_star) {
return E_prime_v.happens_before(e_star, e_prime_in_E_prime_v);
});
if (is_initial) {
- return q;
+ // If the backtrack set already contains `q`, we're done:
+ // they've made note to search for (or have already searched for)
+ // this initial
+ if (backtrack_set.count(q) > 0) {
+ return std::unordered_set<aid_t>{};
+ } else {
+ I_E_prime_v.insert(q);
+ }
} else {
// If `q` is disqualified as a candidate, clearly
// no event occurring after `e_prime` in `E` executed
}
}
}
- return std::nullopt;
+ xbt_assert(not I_E_prime_v.empty(),
+ "For any non-empty execution, we know that "
+ "at minimum one actor is an initial since "
+ "some execution is possible with respect to a "
+ "prefix before event `%u`, yet we didn't find anyone. "
+ "This implies the implementation of this function is broken.",
+ e);
+ return I_E_prime_v;
}
std::optional<PartialExecution> Execution::get_odpor_extension_from(EventHandle e, EventHandle e_prime,
}
PartialExecution v;
+ std::vector<Execution::EventHandle> v_handles;
+ std::unordered_set<aid_t> WI_E_prime_v;
+ std::unordered_set<aid_t> disqualified_actors;
Execution E_prime_v = get_prefix_before(e);
- std::unordered_set<aid_t> disqualified_actors = state_at_e.get_sleeping_actors();
- std::vector<sdpor::Execution::EventHandle> v_handles;
- bool located_actor_in_initial = false;
+ const std::unordered_set<aid_t> sleep_E_prime = state_at_e.get_sleeping_actors();
// Note `e + 1` here: `notdep(e, E)` is defined as the
// set of events that *occur-after* but don't *happen-after* `e`
// SUBTLE NOTE: Observe that any event that "happens-after" `e'`
// must necessarily "happen-after" `e` as well, since `e` and
// `e'` are presumed to be in a reversible race. Hence, we know that
- // all events `e_star` that `e` "happens-before" cannot affect
+ // all events `e_star` such that `e` "happens-before" `e_star` cannot affect
// the enabledness of `e'`; furthermore, `e'` cannot affect the enabledness
// of any event independent with `e` that "occurs-after" `e'`
for (auto e_star = e + 1; e_star <= get_latest_event_handle().value(); ++e_star) {
// `-->_[E'.v]` about `E'.v`, we must build `v` relative to `E'`
v_handles.push_back(e_star_in_E_prime_v);
- if (located_actor_in_initial) {
- // It suffices that we find one initial. If we've already found
- // one, we simply need to finish building `v`
- continue;
- }
-
// Note that we add `q` to v regardless of whether `q` itself has been
// disqualified since `q` may itself disqualify other actors
// (i.e. even if `q` is disqualified from being an initial, it
// is still contained in the sequence `v`)
const aid_t q = E_prime_v.get_actor_with_handle(e_star_in_E_prime_v);
- if (disqualified_actors.count(q) > 0) {
+ if (disqualified_actors.count(q) > 0) { // Did we already note that `q` is not an initial?
continue;
}
- const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_loc) {
- return E_prime_v.happens_before(e_loc, e_star_in_E_prime_v);
+ const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& handle) {
+ return E_prime_v.happens_before(handle, e_star_in_E_prime_v);
});
if (is_initial) {
- located_actor_in_initial = true;
+ // If the sleep set already contains `q`, we're done:
+ // we've found an initial contained in the sleep set and
+ // so the intersection is non-empty
+ if (sleep_E_prime.count(q) > 0) {
+ return std::nullopt;
+ } else {
+ WI_E_prime_v.insert(q);
+ }
} else {
// If `q` is disqualified as a candidate, clearly
// no event occurring after `e_prime` in `E` executed
}
// Now we add `e_prime := <q, i>` to `E'.v` and repeat the same work
- {
- v.push_back(get_event_with_handle(e_prime).get_transition());
-
- if (not located_actor_in_initial) {
- // It's possible `proc(e_prime)` is an initial
- E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
- const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
- v_handles.push_back(e_prime_in_E_prime_v);
-
- const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v);
- located_actor_in_initial = disqualified_actors.count(q) == 0 and
- std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_loc) {
- return E_prime_v.happens_before(e_loc, e_prime_in_E_prime_v);
- });
+ // It's possible `proc(e_prime)` is an initial
+ //
+ // Note the form of `v` in the pseudocode:
+ // `v := notdep(e, E).e'^
+ E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
+ v.push_back(get_event_with_handle(e_prime).get_transition());
+
+ const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
+ v_handles.push_back(e_prime_in_E_prime_v);
+
+ const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& handle) {
+ return E_prime_v.happens_before(handle, e_prime_in_E_prime_v);
+ });
+ if (is_initial) {
+ if (const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v); sleep_E_prime.count(q) > 0) {
+ return std::nullopt;
+ } else {
+ WI_E_prime_v.insert(q);
}
}
- /** Some actor `p` in `v` is an initial for `E' := pre(e, E)`*/
- if (located_actor_in_initial) {
- return v;
- }
-
const Execution pre_E_e = get_prefix_before(e);
const auto sleeping_actors = state_at_e.get_sleeping_actors();
- // Otherwise, for each enabled actor also not in the sleep set, check if
- // any of them are independent with this execution after `v`. This
- // completes the check for weak initials
+ // Check if any enabled actor that is independent with
+ // this execution after `v` is contained in the sleep set
for (const auto& [aid, astate] : state_at_e.get_actors_list()) {
- // TODO: We have to be able to react appropriately here when adding new
- // types of transitions (multiple choices can be made :( )
- if (sleeping_actors.count(aid) == 0 and pre_E_e.is_independent_with_execution(v, astate.get_transition(0))) {
- return v;
- }
+ const bool is_in_WI_E =
+ astate.is_enabled() and pre_E_e.is_independent_with_execution_of(v, astate.get_transition());
+ const bool is_in_sleep_set = sleeping_actors.count(aid) > 0;
+
+ // `action(aid)` is in `WI_[E](v)` but also is contained in the sleep set.
+ // This implies that the intersection between the two is non-empty
+ if (is_in_WI_E && is_in_sleep_set)
+ return std::nullopt;
}
- return std::nullopt;
+ return v;
}
-bool Execution::is_initial_after_execution(const PartialExecution& w, aid_t p) const
+bool Execution::is_initial_after_execution_of(const PartialExecution& w, aid_t p) const
{
auto E_w = *this;
std::vector<EventHandle> w_handles;
return false;
}
-bool Execution::is_independent_with_execution(const PartialExecution& w, std::shared_ptr<Transition> next_E_p) const
+bool Execution::is_independent_with_execution_of(const PartialExecution& w, std::shared_ptr<Transition> next_E_p) const
{
// INVARIANT: Here, we assume that for any process `p_i` of `w`,
// the events of this execution followed by the execution of all
auto w_now = w;
for (const auto& next_E_p : v) {
- const aid_t p = next_E_p->aid_;
-
// Is `p in `I_[E](w)`?
- if (E_v.is_initial_after_execution(w_now, p)) {
+ if (const aid_t p = next_E_p->aid_; E_v.is_initial_after_execution_of(w_now, p)) {
// Remove `p` from w and continue
- // TODO: If `p` occurs in `w`, it had better refer to the same
+ // INVARIANT: If `p` occurs in `w`, it had better refer to the same
// transition referenced by `v`. Unfortunately, we have two
// sources of truth here which can be manipulated at the same
// time as arguments to the function. If ODPOR works correctly,
w_now.erase(action_by_p_in_w);
}
// Is `E ⊢ p ◇ w`?
- else if (E_v.is_independent_with_execution(w, next_E_p)) {
+ else if (E_v.is_independent_with_execution_of(w_now, next_E_p)) {
// INVARIANT: Note that it is impossible for `p` to be
// excluded from the set `I_[E](w)` BUT ALSO be contained in
- // `w` itself if `E ⊢ p ◇ w`. We assert this is the case here
+ // `w` itself if `E ⊢ p ◇ w` (intuitively, the fact that `E ⊢ p ◇ w`
+ // means that are able to move `p` anywhere in `w` IF it occurred, so
+ // if it really does occur we know it must then be an initial).
+ // We assert this is the case here
const auto action_by_p_in_w =
std::find_if(w_now.begin(), w_now.end(), [=](const auto& action) { return action->aid_ == p; });
xbt_assert(action_by_p_in_w == w_now.end(),
return false;
}
-} // namespace simgrid::mc::odpor
\ No newline at end of file
+} // namespace simgrid::mc::odpor
