include src/mc/VisitedState.cpp
include src/mc/VisitedState.hpp
include src/mc/api/ActorState.hpp
+include src/mc/api/ClockVector.cpp
+include src/mc/api/ClockVector.hpp
include src/mc/api/RemoteApp.cpp
include src/mc/api/RemoteApp.hpp
include src/mc/api/State.cpp
include src/mc/explo/LivenessChecker.hpp
include src/mc/explo/UdporChecker.cpp
include src/mc/explo/UdporChecker.hpp
+include src/mc/explo/odpor/ClockVector_test.cpp
+include src/mc/explo/odpor/Execution.cpp
+include src/mc/explo/odpor/Execution.hpp
+include src/mc/explo/odpor/Execution_test.cpp
+include src/mc/explo/odpor/ReversibleRaceCalculator.cpp
+include src/mc/explo/odpor/ReversibleRaceCalculator.hpp
+include src/mc/explo/odpor/WakeupTree.cpp
+include src/mc/explo/odpor/WakeupTree.hpp
+include src/mc/explo/odpor/WakeupTreeIterator.cpp
+include src/mc/explo/odpor/WakeupTreeIterator.hpp
+include src/mc/explo/odpor/WakeupTree_test.cpp
+include src/mc/explo/odpor/odpor_forward.hpp
+include src/mc/explo/odpor/odpor_tests_private.hpp
include src/mc/explo/simgrid_mc.cpp
include src/mc/explo/udpor/Comb.hpp
include src/mc/explo/udpor/Configuration.cpp
> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;3;3;1'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 551 unique states visited; 137 backtracks (2239 transition replays, 1551 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1070 unique states visited; 252 backtracks (4082 transition replays, 2760 states visited overall)
! expect return 1
! timeout 20
> [0.000000] [mc_explo/INFO] *** PROPERTY NOT VALID ***
> [0.000000] [mc_explo/INFO] **************************
> [0.000000] [mc_explo/INFO] Counter-example execution trace:
-> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
+> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] 1: iRecv(mbox=0)
> [0.000000] [mc_explo/INFO] 3: WaitComm(from 3 to 1, mbox=0, no timeout)
> [0.000000] [mc_explo/INFO] 3: iSend(mbox=0)
> [0.000000] [mc_explo/INFO] 1: WaitComm(from 3 to 1, mbox=0, no timeout)
-> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'3;1;1;1;3;3;1'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1161 unique states visited; 282 backtracks (4556 transition replays, 3113 states visited overall)
+> [0.000000] [mc_explo/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1;3;1;1;3;3;1'
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 995 unique states visited; 253 backtracks (4006 transition replays, 2758 states visited overall)
+
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/sleep-set' to 'true'
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'actors' to '2'
> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 130 unique states visited; 27 backtracks (209 transition replays, 52 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 66 unique states visited; 11 backtracks (97 transition replays, 20 states visited overall)
p The stats without checkpoints is: 130 unique states visited; 27 backtracks (308 transition replays, 151 states visited overall)
p But it runs much faster (0.6 sec vs. 1.6 sec), damn slow checkpointing code.
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/sleep-set' to 'true'
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'actors' to '2'
> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 130 unique states visited; 27 backtracks (308 transition replays, 151 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 66 unique states visited; 11 backtracks (126 transition replays, 49 states visited overall)
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:nb_wait -- ${bindir:=.}/s4u-synchro-mutex --cfg=actors:3 --log=s4u_test.thres:critical
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/sleep-set' to 'true'
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/strategy' to 'nb_wait'
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'actors' to '3'
> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 3492 unique states visited; 743 backtracks (12498 transition replays, 8263 states visited overall)
\ No newline at end of file
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 296 unique states visited; 52 backtracks (765 transition replays, 417 states visited overall)
\ No newline at end of file
> The thread 0 is terminating.
> The thread 1 is terminating.
> User's main is terminating.
-> The thread 1 is terminating.
> The thread 0 is terminating.
+> The thread 1 is terminating.
> User's main is terminating.
-> The thread 0 is terminating.
> The thread 1 is terminating.
+> The thread 0 is terminating.
> User's main is terminating.
> [0.000000] [mc_dfs/INFO] DFS exploration ended. 23 unique states visited; 2 backtracks (27 transition replays, 2 states visited overall)
\ No newline at end of file
> The thread 0 is terminating.
> The thread 1 is terminating.
> User's main is terminating.
+> The thread 0 is terminating.
+> The thread 1 is terminating.
+> User's main is terminating.
> [0.000000] [mc_global/INFO] **************************
> [0.000000] [mc_global/INFO] *** DEADLOCK DETECTED ***
> [0.000000] [mc_global/INFO] **************************
> [0.000000] [mc_global/INFO] 3: MUTEX_WAIT(mutex: 1, owner: 3)
> [0.000000] [mc_global/INFO] 3: MUTEX_ASYNC_LOCK(mutex: 0, owner: 2)
> [0.000000] [mc_Session/INFO] You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'2;2;3;2;3;3'
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 19 unique states visited; 1 backtracks (22 transition replays, 2 states visited overall)
\ No newline at end of file
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 28 unique states visited; 2 backtracks (37 transition replays, 7 states visited overall)
\ No newline at end of file
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/sleep-set' to 'true'
> [0.000000] [sthread/INFO] Starting the simulation.
> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1101 unique states visited; 136 backtracks (2950 transition replays, 1713 states visited overall)
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 106 unique states visited; 17 backtracks (295 transition replays, 172 states visited overall)
$ $VALGRIND_NO_TRACE_CHILDREN ${bindir:=.}/../../bin/simgrid-mc --cfg=model-check/sleep-set:true --cfg=model-check/strategy:nb_wait --cfg=model-check/setenv:LD_PRELOAD=${libdir:=.}/libsgmalloc.so:${libdir:=.}/libsthread.so ${bindir:=.}/pthread-producer-consumer -q -c 2 -C 1 -p 2 -P 1
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/sleep-set' to 'true'
> [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/strategy' to 'nb_wait'
> [0.000000] [sthread/INFO] Starting the simulation.
> [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: dpor.
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1101 unique states visited; 136 backtracks (2950 transition replays, 1713 states visited overall)
\ No newline at end of file
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 107 unique states visited; 18 backtracks (300 transition replays, 175 states visited overall)
\ No newline at end of file
#include "src/kernel/activity/CommImpl.hpp"
#include "src/mc/remote/RemotePtr.hpp"
+#include <algorithm>
#include <exception>
#include <vector>
mark_done();
return times_considered_++;
}
+ unsigned int get_max_considered() const { return max_consider_; }
unsigned int get_times_considered() const { return times_considered_; }
unsigned int get_times_not_considered() const { return max_consider_ - times_considered_; }
+ bool has_more_to_consider() const { return get_times_not_considered() > 0; }
aid_t get_aid() const { return aid_; }
/* returns whether the actor is marked as enabled in the application side */
}
void mark_done() { this->state_ = InterleavingType::done; }
- inline Transition* get_transition(unsigned times_considered) const
+ /**
+ * @brief Retrieves the transition that we should consider for execution by
+ * this actor from the State instance with respect to which this ActorState object
+ * is considered
+ */
+ std::shared_ptr<Transition> get_transition() const
+ {
+ // The rationale for this selection is as follows:
+ //
+ // 1. For transitions with only one possibility of execution,
+ // we always wish to select action `0` even if we've
+ // marked the transition already as considered (which
+ // we'll do if we explore a trace following that transition).
+ //
+ // 2. For transitions that can be considered multiple
+ // times, we want to be sure to select the most up-to-date
+ // action. In general, this means selecting that which is
+ // now being considered at this state. If, however, we've
+ // executed the
+ //
+ // The formula satisfies both of the above conditions:
+ //
+ // > std::clamp(times_considered_, 0u, max_consider_ - 1)
+ return get_transition(std::clamp(times_considered_, 0u, max_consider_ - 1));
+ }
+
+ std::shared_ptr<Transition> get_transition(unsigned times_considered) const
{
xbt_assert(times_considered < this->pending_transitions_.size(),
"Actor %ld does not have a state available transition with `times_considered = %u`,\n"
"yet one was asked for",
aid_, times_considered);
- return this->pending_transitions_[times_considered].get();
+ return this->pending_transitions_[times_considered];
}
- inline void set_transition(std::shared_ptr<Transition> t, unsigned times_considered)
+ void set_transition(std::shared_ptr<Transition> t, unsigned times_considered)
{
xbt_assert(times_considered < this->pending_transitions_.size(),
"Actor %ld does not have a state available transition with `times_considered = %u`, "
--- /dev/null
+/* Copyright (c) 2015-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/api/ClockVector.hpp"
+
+namespace simgrid::mc {
+
+ClockVector ClockVector::max(const ClockVector& cv1, const ClockVector& cv2)
+{
+ auto max_vector = ClockVector();
+
+ for (const auto& [aid, value] : cv1.contents)
+ max_vector[aid] = std::max(value, cv2.get(aid).value_or(0));
+
+ for (const auto& [aid, value] : cv2.contents)
+ max_vector[aid] = std::max(value, cv1.get(aid).value_or(0));
+
+ return max_vector;
+}
+
+} // namespace simgrid::mc
\ No newline at end of file
--- /dev/null
+/* Copyright (c) 2016-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_CLOCK_VECTOR_HPP
+#define SIMGRID_MC_CLOCK_VECTOR_HPP
+
+#include "simgrid/forward.h"
+
+#include <cstdint>
+#include <initializer_list>
+#include <optional>
+#include <unordered_map>
+
+namespace simgrid::mc {
+
+/**
+ * @brief A multi-dimensional vector used to keep track of
+ * happens-before relation between dependent events in an
+ * execution of DPOR, SDPOR, or ODPOR
+ *
+ * Clock vectors permit actors in a distributed system
+ * to determine whether two events occurred one after the other
+ * but they may not have); i.e. they permit actors to keep track of "time".
+ * A clever observation made in the original DPOR paper is that a
+ * transition-based "happens-before" relation can be computed for
+ * any particular trace `S` using clock vectors, effectively
+ * treating dependency like the passing of a message (the context
+ * in which vector clocks are typically used).
+ *
+ * Support, however, needs to be added to clock vectors since
+ * Simgrid permits the *creation* of new actors during execution.
+ * Since we don't know this size before-hand, we have to allow
+ * clock vectors to behave as if they were "infinitely" large. To
+ * do so, all newly mapped elements, if not assigned a value, are
+ * defaulted to `0`. This corresponds to the value this actor would
+ * have had regardless had its creation been known to have evnetually
+ * occurred: no actions taken by that actor had occurred prior, so
+ * there's no way the clock vector would have been updated. In other
+ * words, when comparing clock vectors of different sizes, it's equivalent
+ * to imagine both of the same size with elements absent in one or
+ * the other implicitly mapped to zero.
+ */
+struct ClockVector final {
+private:
+ std::unordered_map<aid_t, uint32_t> contents;
+
+public:
+ ClockVector() = default;
+ ClockVector(const ClockVector&) = default;
+ ClockVector& operator=(ClockVector const&) = default;
+ ClockVector(ClockVector&&) = default;
+ ClockVector(std::initializer_list<std::pair<const aid_t, uint32_t>> init) : contents(std::move(init)) {}
+
+ /**
+ * @brief The number of components in this
+ * clock vector
+ *
+ * A `ClockVector` implicitly maps the id of an actor
+ * it does not contain to a default value of `0`.
+ * Thus, a `ClockVector` is "lazy" in the sense
+ * that new actors are "automatically" mapped
+ * without needing to be explicitly added the clock
+ * vector when the actor is created. This means that
+ * comparison between clock vectors is possible
+ * even as actors become enabled and disabled
+ *
+ * @return uint32_t the number of elements in
+ * the clock vector
+ */
+ size_t size() const { return this->contents.size(); }
+
+ uint32_t& operator[](aid_t aid)
+ {
+ // NOTE: The `operator[]` overload of
+ // unordered_map will create a new key-value
+ // pair if `tid` does not exist and will use
+ // a _default_ value for the value (0 in this case)
+ // which is precisely what we want here
+ return this->contents[aid];
+ }
+
+ /**
+ * @brief Retrieves the value mapped to the given
+ * actor if it is contained in this clock vector
+ */
+ std::optional<uint32_t> get(aid_t aid) const
+ {
+ if (const auto iter = this->contents.find(aid); iter != this->contents.end())
+ return std::optional<uint32_t>{iter->second};
+ return std::nullopt;
+ }
+
+ /**
+ * @brief Computes a clock vector whose components
+ * are larger than the components of both of
+ * the given clock vectors
+ *
+ * The maximum of two clock vectors is definied to
+ * be the clock vector whose components are the maxmimum
+ * of the corresponding components of the arguments.
+ * Since the `ClockVector` class is "lazy", the two
+ * clock vectors given as arguments may not be of the same size.
+ * The resultant clock vector has components as follows:
+ *
+ * 1. For each actor that each clock vector maps, the
+ * resulting clock vector maps that thread to the maxmimum
+ * of the values mapped for the actor in each clock vector
+ *
+ * 2. For each actor that only a single clock vector maps,
+ * the resulting clock vector maps that thread to the
+ * value mapped by the lone clock vector
+ *
+ * The scheme is equivalent to assuming that an unmapped
+ * thread by any one clock vector is implicitly mapped to zero
+ *
+ * @param cv1 the first clock vector
+ * @param cv2 the second clock vector
+ * @return a clock vector whose components are at
+ * least as large as the corresponding components of each clock
+ * vector and whose size is large enough to contain the union
+ * of components of each clock vector
+ */
+ static ClockVector max(const ClockVector& cv1, const ClockVector& cv2);
+};
+
+} // namespace simgrid::mc
+
+#endif
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/mc_config.hpp"
+#include <algorithm>
#include <boost/range/algorithm.hpp>
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_state, mc, "Logging specific to MC states");
* And if we kept it and the actor is enabled in this state, mark the actor as already done, so that
* it is not explored*/
for (auto& [aid, transition] : parent_state_->get_sleep_set()) {
- if (not incoming_transition_->depends(&transition)) {
+ if (not incoming_transition_->depends(transition.get())) {
sleep_set_.try_emplace(aid, transition);
if (strategy_->actors_to_run_.count(aid) != 0) {
XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid);
-
strategy_->actors_to_run_.at(aid).mark_done();
}
} else
XBT_DEBUG("Transition >>%s<< removed from the sleep set because it was dependent with incoming >>%s<<",
- transition.to_string().c_str(), incoming_transition_->to_string().c_str());
+ transition->to_string().c_str(), incoming_transition_->to_string().c_str());
}
}
}
return strategy_->next_transition();
}
+aid_t State::next_odpor_transition() const
+{
+ return wakeup_tree_.get_min_single_process_actor().value_or(-1);
+}
+
// This should be done in GuidedState, or at least interact with it
std::shared_ptr<Transition> State::execute_next(aid_t next, RemoteApp& app)
{
// when simcall_handle will be called on it
auto& actor_state = strategy_->actors_to_run_.at(next);
const unsigned times_considered = actor_state.do_consider();
- const auto* expected_executed_transition = actor_state.get_transition(times_considered);
+ const auto* expected_executed_transition = actor_state.get_transition(times_considered).get();
xbt_assert(expected_executed_transition != nullptr,
"Expected a transition with %u times considered to be noted in actor %ld", times_considered, next);
return outgoing_transition_;
}
+
+std::unordered_set<aid_t> State::get_backtrack_set() const
+{
+ std::unordered_set<aid_t> actors;
+ for (const auto& [aid, state] : get_actors_list()) {
+ if (state.is_todo() or state.is_done()) {
+ actors.insert(aid);
+ }
+ }
+ return actors;
+}
+
+std::unordered_set<aid_t> State::get_sleeping_actors() const
+{
+ std::unordered_set<aid_t> actors;
+ for (const auto& [aid, _] : get_sleep_set()) {
+ actors.insert(aid);
+ }
+ return actors;
+}
+
+std::unordered_set<aid_t> State::get_enabled_actors() const
+{
+ std::unordered_set<aid_t> actors;
+ for (const auto& [aid, state] : get_actors_list()) {
+ if (state.is_enabled()) {
+ actors.insert(aid);
+ }
+ }
+ return actors;
+}
+
+void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior)
+{
+ // TODO: It would be better not to have such a flag.
+ if (has_initialized_wakeup_tree) {
+ return;
+ }
+ // TODO: Note that the next action taken by the actor may be updated
+ // after it executes. But we will have already inserted it into the
+ // tree and decided upon "happens-before" at that point for different
+ // executions :(
+ if (wakeup_tree_.empty()) {
+ // Find an enabled transition to pick
+ for (const auto& [_, actor] : get_actors_list()) {
+ if (actor.is_enabled()) {
+ // For each variant of the transition, we want
+ // to insert the action into the tree. This ensures
+ // that all variants are searched
+ for (unsigned times = 0; times < actor.get_max_considered(); ++times) {
+ wakeup_tree_.insert(prior, odpor::PartialExecution{actor.get_transition(times)});
+ }
+ break; // Only one actor gets inserted (see pseudocode)
+ }
+ }
+ }
+ has_initialized_wakeup_tree = true;
+}
+
+void State::sprout_tree_from_parent_state()
+{
+ xbt_assert(parent_state_ != nullptr, "Attempting to construct a wakeup tree for the root state "
+ "(or what appears to be, rather for state without a parent defined)");
+ const auto min_process_node = parent_state_->wakeup_tree_.get_min_single_process_node();
+ xbt_assert(min_process_node.has_value(), "Attempting to construct a subtree for a substate from a "
+ "parent with an empty wakeup tree. This indicates either that ODPOR "
+ "actor selection in State.cpp is incorrect, or that the code "
+ "deciding when to make subtrees in ODPOR is incorrect");
+ xbt_assert((get_transition_in()->aid_ == min_process_node.value()->get_actor()) &&
+ (get_transition_in()->type_ == min_process_node.value()->get_action()->type_),
+ "We tried to make a subtree from a parent state who claimed to have executed `%s` "
+ "but whose wakeup tree indicates it should have executed `%s`. This indicates "
+ "that exploration is not following ODPOR. Are you sure you're choosing actors "
+ "to schedule from the wakeup tree?",
+ get_transition_in()->to_string(false).c_str(),
+ min_process_node.value()->get_action()->to_string(false).c_str());
+ this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(min_process_node.value());
+}
+
+void State::remove_subtree_using_current_out_transition()
+{
+ if (auto out_transition = get_transition_out(); out_transition != nullptr) {
+ if (const auto min_process_node = wakeup_tree_.get_min_single_process_node(); min_process_node.has_value()) {
+ xbt_assert((out_transition->aid_ == min_process_node.value()->get_actor()) &&
+ (out_transition->type_ == min_process_node.value()->get_action()->type_),
+ "We tried to make a subtree from a parent state who claimed to have executed `%s` "
+ "but whose wakeup tree indicates it should have executed `%s`. This indicates "
+ "that exploration is not following ODPOR. Are you sure you're choosing actors "
+ "to schedule from the wakeup tree?",
+ out_transition->to_string(false).c_str(),
+ min_process_node.value()->get_action()->to_string(false).c_str());
+ }
+ }
+ wakeup_tree_.remove_min_single_process_subtree();
+}
+
+odpor::WakeupTree::InsertionResult State::insert_into_wakeup_tree(const odpor::PartialExecution& pe,
+ const odpor::Execution& E)
+{
+ return this->wakeup_tree_.insert(E, pe);
+}
+
+void State::do_odpor_unwind()
+{
+ if (auto out_transition = get_transition_out(); out_transition != nullptr) {
+ remove_subtree_using_current_out_transition();
+
+ // Only when we've exhausted all variants of the transition which
+ // can be chosen from this state do we finally add the actor to the
+ // sleep set. This ensures that the current logic handling sleep sets
+ // works with ODPOR in the way we intend it to work. There is not a
+ // good way to perform transition equality in SimGrid; instead, we
+ // effectively simply check for the presence of an actor in the sleep set.
+ if (!get_actors_list().at(out_transition->aid_).has_more_to_consider())
+ add_sleep_set(std::move(out_transition));
+ }
+}
+
} // namespace simgrid::mc
#define SIMGRID_MC_STATE_HPP
#include "src/mc/api/ActorState.hpp"
+#include "src/mc/api/ClockVector.hpp"
#include "src/mc/api/RemoteApp.hpp"
#include "src/mc/api/strategy/Strategy.hpp"
+#include "src/mc/explo/odpor/WakeupTree.hpp"
#include "src/mc/transition/Transition.hpp"
#if SIMGRID_HAVE_STATEFUL_MC
/* Sleep sets are composed of the actor and the corresponding transition that made it being added to the sleep
* set. With this information, it is check whether it should be removed from it or not when exploring a new
* transition */
- std::map<aid_t, Transition> sleep_set_;
+ std::map<aid_t, std::shared_ptr<Transition>> sleep_set_;
+
+ /**
+ * The wakeup tree with respect to the execution represented
+ * by the totality of all states before and including this one
+ * and with respect to this state's sleep set
+ */
+ odpor::WakeupTree wakeup_tree_;
+ bool has_initialized_wakeup_tree = false;
public:
explicit State(RemoteApp& remote_app);
/* Returns a positive number if there is another transition to pick, or -1 if not */
aid_t next_transition() const; // this function should disapear as it is redundant with the next one
- /* Same as next_transition, but choice is now guided, and an integer corresponding to the
+ /* Same as next_transition(), but choice is now guided, and an integer corresponding to the
internal cost of the transition is returned */
std::pair<aid_t, int> next_transition_guided() const;
+ /**
+ * Same as next_transition(), but the choice is not based off the ODPOR
+ * wakeup tree associated with this state
+ */
+ aid_t next_odpor_transition() const;
+
/**
* @brief Explore a new path on the remote app; the parameter 'next' must be the result of a previous call to
* next_transition()
/* Marking as TODO some actor in this state:
* + consider_one mark aid actor (and assert it is possible)
- * + consider_best ensure one actor is marked by eventually marking the best regarding its guiding methode
- * + conside_all mark all enabled actor that are not done yet */
+ * + consider_best ensure one actor is marked by eventually marking the best regarding its guiding method
+ * + consider_all mark all enabled actor that are not done yet */
void consider_one(aid_t aid) const { strategy_->consider_one(aid); }
void consider_best() const { strategy_->consider_best(); }
unsigned long consider_all() const { return strategy_->consider_all(); }
Snapshot* get_system_state() const { return system_state_.get(); }
void set_system_state(std::shared_ptr<Snapshot> state) { system_state_ = std::move(state); }
- std::map<aid_t, Transition> const& get_sleep_set() const { return sleep_set_; }
- void add_sleep_set(std::shared_ptr<Transition> t)
+ /**
+ * @brief Computes the backtrack set for this state
+ * according to its definition in Simgrid.
+ *
+ * The backtrack set as it appears in DPOR, SDPOR, and ODPOR
+ * in SimGrid consists of those actors marked as `todo`
+ * (i.e. those that have yet to be explored) as well as those
+ * marked `done` (i.e. those that have already been explored)
+ * since the pseudocode in none of the above algorithms explicitly
+ * removes elements from the backtrack set. DPOR makes use
+ * explicitly of the `done` set, but we again note that the
+ * backtrack set still contains processes added to the done set.
+ */
+ std::unordered_set<aid_t> get_backtrack_set() const;
+ std::unordered_set<aid_t> get_sleeping_actors() const;
+ std::unordered_set<aid_t> get_enabled_actors() const;
+ std::map<aid_t, std::shared_ptr<Transition>> const& get_sleep_set() const { return sleep_set_; }
+ void add_sleep_set(std::shared_ptr<Transition> t) { sleep_set_.insert_or_assign(t->aid_, std::move(t)); }
+ bool is_actor_sleeping(aid_t actor) const
{
- sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_));
+ return std::find_if(sleep_set_.begin(), sleep_set_.end(), [=](const auto& pair) { return pair.first == actor; }) !=
+ sleep_set_.end();
}
+ /**
+ * @brief Inserts an arbitrary enabled actor into the wakeup tree
+ * associated with this state, if such an actor exists and if
+ * the wakeup tree is already not empty
+ *
+ * @param prior The sequence of steps leading up to this state
+ * with respec to which the tree associated with this state should be
+ * a wakeup tree (wakeup trees are defined relative to an execution)
+ *
+ * @invariant: You should not manipulate a wakeup tree with respect
+ * to more than one execution; doing so will almost certainly lead to
+ * unexpected results as wakeup trees are defined relative to a single
+ * execution
+ */
+ void seed_wakeup_tree_if_needed(const odpor::Execution& prior);
+
+ /**
+ * @brief Initializes the wakeup_tree_ instance by taking the subtree rooted at the
+ * single-process node `N` running actor `p := "actor taken by parent to form this state"`
+ * of the *parent's* wakeup tree
+ */
+ void sprout_tree_from_parent_state();
+
+ /**
+ * @brief Removes the subtree rooted at the single-process node
+ * `N` running actor `p` of this state's wakeup tree
+ */
+ void remove_subtree_using_current_out_transition();
+ bool has_empty_tree() const { return this->wakeup_tree_.empty(); }
+
+ /**
+ * @brief
+ */
+ odpor::WakeupTree::InsertionResult insert_into_wakeup_tree(const odpor::PartialExecution&, const odpor::Execution&);
+
+ /** @brief Prepares the state for re-exploration following
+ * another after having followed ODPOR from this state with
+ * the current out transition
+ *
+ * After ODPOR has completed searching a maximal trace, it
+ * finds the first point in the execution with a nonempty wakeup
+ * tree. This method corresponds to lines 20 and 21 in the ODPOR
+ * pseudocode
+ */
+ void do_odpor_unwind();
+
/* Returns the total amount of states created so far (for statistics) */
static long get_expanded_states() { return expended_states_; }
};
}
*/
-Exploration* create_communication_determinism_checker(const std::vector<char*>& args, bool with_dpor)
+Exploration* create_communication_determinism_checker(const std::vector<char*>& args, ReductionMode mode)
{
CommDetExtension::EXTENSION_ID = simgrid::mc::Exploration::extension_create<CommDetExtension>();
StateCommDet::EXTENSION_ID = simgrid::mc::State::extension_create<StateCommDet>();
XBT_DEBUG("********* Start communication determinism verification *********");
- auto base = new DFSExplorer(args, with_dpor, true);
+ auto base = new DFSExplorer(args, mode, true);
auto extension = new CommDetExtension(*base);
DFSExplorer::on_exploration_start([extension](RemoteApp const&) {
#include <cassert>
#include <cstdio>
+#include <algorithm>
#include <memory>
#include <string>
+#include <unordered_set>
#include <vector>
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_dfs, mc, "DFS exploration algorithm of the model-checker");
void DFSExplorer::restore_stack(std::shared_ptr<State> state)
{
stack_.clear();
+ execution_seq_ = odpor::Execution();
auto current_state = state;
stack_.emplace_front(current_state);
// condition corresponds to reaching initial state
stack_.emplace_front(current_state);
}
XBT_DEBUG("Replaced stack by %s", get_record_trace().to_string().c_str());
+ if (reduction_mode_ == ReductionMode::sdpor || reduction_mode_ == ReductionMode::odpor) {
+ // NOTE: The outgoing transition for the top-most
+ // state of the stack refers to that which was taken
+ // as part of the last trace explored by the algorithm.
+ // Thus, only the sequence of transitions leading up to,
+ // but not including, the last state must be included
+ // when reconstructing the Exploration for SDPOR.
+ for (auto iter = std::next(stack_.begin()); iter != stack_.end(); ++iter) {
+ execution_seq_.push_transition((*iter)->get_transition_in());
+ }
+ XBT_DEBUG("Replaced SDPOR/ODPOR execution to reflect the new stack");
+ }
}
void DFSExplorer::log_state() // override
XBT_ERROR("/!\\ Max depth of %d reached! THIS WILL PROBABLY BREAK the dpor reduction /!\\",
_sg_mc_max_depth.get());
XBT_ERROR("/!\\ If bad things happen, disable dpor with --cfg=model-check/reduction:none /!\\");
- } else
+ } else if (reduction_mode_ == ReductionMode::sdpor || reduction_mode_ == ReductionMode::odpor) {
+ XBT_ERROR("/!\\ Max depth of %d reached! THIS **WILL** BREAK the reduction, which is not sound "
+ "when stopping at a fixed depth /!\\",
+ _sg_mc_max_depth.get());
+ XBT_ERROR("/!\\ If bad things happen, disable the reduction with --cfg=model-check/reduction:none /!\\");
+ } else {
XBT_WARN("/!\\ Max depth reached ! /!\\ ");
+ }
this->backtrack();
continue;
}
}
#endif
+ if (reduction_mode_ == ReductionMode::odpor) {
+ // In the case of ODPOR, the wakeup tree for this
+ // state may be empty if we're exploring new territory
+ // (rather than following the partial execution of a
+ // wakeup tree). This corresponds to lines 9 to 13 of
+ // the ODPOR pseudocode
+ //
+ // INVARIANT: The execution sequence should be consistent
+ // with the state when seeding the tree. If the sequence
+ // gets out of sync with the state, selection will not
+ // work as we intend
+ state->seed_wakeup_tree_if_needed(execution_seq_);
+ }
+
// Search for the next transition
- // next_transition returns a pair<aid_t, int> in case we want to consider multiple state (eg. during backtrack)
- auto [next, _] = state->next_transition_guided();
+ // next_transition returns a pair<aid_t, int>
+ // in case we want to consider multiple states (eg. during backtrack)
+ const aid_t next = reduction_mode_ == ReductionMode::odpor ? state->next_odpor_transition()
+ : std::get<0>(state->next_transition_guided());
if (next < 0) { // If there is no more transition in the current state, backtrack.
XBT_VERB("%lu actors remain, but none of them need to be interleaved (depth %zu).", state->get_actor_count(),
if (_sg_mc_sleep_set && XBT_LOG_ISENABLED(mc_dfs, xbt_log_priority_verbose)) {
XBT_VERB("Sleep set actually containing:");
for (auto& [aid, transition] : state->get_sleep_set())
- XBT_VERB(" <%ld,%s>", aid, transition.to_string().c_str());
+ XBT_VERB(" <%ld,%s>", aid, transition->to_string().c_str());
}
/* Actually answer the request: let's execute the selected request (MCed does one step) */
- state->execute_next(next, get_remote_app());
+ const auto executed_transition = state->execute_next(next, get_remote_app());
on_transition_execute_signal(state->get_transition_out().get(), get_remote_app());
// If there are processes to interleave and the maximum depth has not been
auto next_state = std::make_shared<State>(get_remote_app(), state);
on_state_creation_signal(next_state.get(), get_remote_app());
- /* Sleep set procedure:
- * adding the taken transition to the sleep set of the original state.
- * <!> Since the parent sleep set is used to compute the child sleep set, this need to be
- * done after next_state creation */
- XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set",
- state->get_transition_out()->to_string().c_str(), state->get_transition_out()->aid_);
- state->add_sleep_set(state->get_transition_out()); // Actors are marked done when they are considerd in ActorState
+ if (reduction_mode_ == ReductionMode::odpor) {
+ // With ODPOR, after taking a step forward, we must
+ // assign a copy of that subtree to the next state.
+ //
+ // NOTE: We only add actions to the sleep set AFTER
+ // we've regenerated states. We must perform the search
+ // fully down a single path before we consider adding
+ // any elements to the sleep set according to the pseudocode
+ next_state->sprout_tree_from_parent_state();
+ } else {
+ /* Sleep set procedure:
+ * adding the taken transition to the sleep set of the original state.
+ * <!> Since the parent sleep set is used to compute the child sleep set, this need to be
+ * done after next_state creation */
+ XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set",
+ state->get_transition_out()->to_string().c_str(), state->get_transition_out()->aid_);
+ state->add_sleep_set(
+ state->get_transition_out()); // Actors are marked done when they are considered in ActorState
+ }
/* DPOR persistent set procedure:
* for each new transition considered, check if it depends on any other previous transition executed before it
}
tmp_stack.pop_back();
}
+ } else if (reduction_mode_ == ReductionMode::sdpor) {
+ /**
+ * SDPOR Source Set Procedure:
+ *
+ * Find "reversible races" in the current execution `E` with respect
+ * to the latest action `p`. For each such race, determine one thread
+ * not contained in the backtrack set at the "race point" `r` which
+ * "represents" the trace formed by first executing everything after
+ * `r` that doesn't depend on it (`v := notdep(r, E)`) and then `p` to
+ * flip the race.
+ *
+ * The intuition is that some subsequence of `v` may enable `p`, so
+ * we want to be sure that search "in that direction"
+ */
+ execution_seq_.push_transition(std::move(executed_transition));
+ xbt_assert(execution_seq_.get_latest_event_handle().has_value(), "No events are contained in the SDPOR execution "
+ "even though one was just added");
+
+ const auto next_E_p = execution_seq_.get_latest_event_handle().value();
+ for (const auto e_race : execution_seq_.get_reversible_races_of(next_E_p)) {
+ State* prev_state = stack_[e_race].get();
+ const auto choices = execution_seq_.get_missing_source_set_actors_from(e_race, prev_state->get_backtrack_set());
+ if (!choices.empty()) {
+ // NOTE: To incorporate the idea of attempting to select the "best"
+ // backtrack point into SDPOR, instead of selecting the `first` initial,
+ // we should instead compute all choices and decide which is best
+ //
+ // Here, we choose the actor with the lowest ID to ensure
+ // we get deterministic results
+ const auto q =
+ std::min_element(choices.begin(), choices.end(), [](const aid_t a1, const aid_t a2) { return a1 < a2; });
+ prev_state->consider_one(*q);
+ opened_states_.emplace_back(std::move(prev_state));
+ }
+ }
+ } else if (reduction_mode_ == ReductionMode::odpor) {
+ // In the case of ODPOR, we simply observe the transition that was executed
+ // until we've reached a maximal trace
+ execution_seq_.push_transition(std::move(executed_transition));
}
// Before leaving that state, if the transition we just took can be taken multiple times, we
this->check_non_termination(next_state.get());
#if SIMGRID_HAVE_STATEFUL_MC
- /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction) */
+ /* Check whether we already explored next_state in the past (but only if interested in state-equality reduction)
+ */
if (_sg_mc_max_visited_states > 0)
visited_state_ = visited_states_.addVisitedState(next_state->get_num(), next_state.get(), get_remote_app());
#endif
return best_state;
}
+std::shared_ptr<State> DFSExplorer::next_odpor_state()
+{
+ for (auto iter = stack_.rbegin(); iter != stack_.rend(); ++iter) {
+ const auto& state = *iter;
+ state->do_odpor_unwind();
+ XBT_DEBUG("\tPerformed ODPOR 'clean-up'. Sleep set has:");
+ for (auto& [aid, transition] : state->get_sleep_set())
+ XBT_DEBUG("\t <%ld,%s>", aid, transition->to_string().c_str());
+ if (!state->has_empty_tree()) {
+ return state;
+ }
+ }
+ return nullptr;
+}
+
void DFSExplorer::backtrack()
{
+ if (const auto last_event = execution_seq_.get_latest_event_handle();
+ reduction_mode_ == ReductionMode::odpor and last_event.has_value()) {
+ /**
+ * ODPOR Race Detection Procedure:
+ *
+ * For each reversible race in the current execution, we
+ * note if there are any continuations `C` equivalent to that which
+ * would reverse the race that have already either a) been searched by ODPOR or
+ * b) been *noted* to be searched by the wakeup tree at the
+ * appropriate reversal point, either as `C` directly or
+ * an as equivalent to `C` ("eventually looks like C", viz. the `~_E`
+ * relation)
+ */
+ for (auto e_prime = static_cast<odpor::Execution::EventHandle>(0); e_prime <= last_event.value(); ++e_prime) {
+ for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) {
+ XBT_DEBUG("ODPOR: Reversible race detected between events `%u` and `%u`", e, e_prime);
+ State& prev_state = *stack_[e];
+ if (const auto v = execution_seq_.get_odpor_extension_from(e, e_prime, prev_state); v.has_value()) {
+ const auto result = prev_state.insert_into_wakeup_tree(v.value(), execution_seq_.get_prefix_before(e));
+ switch (result) {
+ case odpor::WakeupTree::InsertionResult::root: {
+ XBT_DEBUG("ODPOR: Reversible race with `%u` unaccounted for in the wakeup tree for "
+ "the execution prior to event `%u`:",
+ e_prime, e);
+ break;
+ }
+ case odpor::WakeupTree::InsertionResult::interior_node: {
+ XBT_DEBUG("ODPOR: Reversible race with `%u` partially accounted for in the wakeup tree for "
+ "the execution prior to event `%u`:",
+ e_prime, e);
+ break;
+ }
+ case odpor::WakeupTree::InsertionResult::leaf: {
+ XBT_DEBUG("ODPOR: Reversible race with `%u` accounted for in the wakeup tree for "
+ "the execution prior to event `%u`:",
+ e_prime, e);
+ break;
+ }
+ }
+ for (const auto& seq : simgrid::mc::odpor::get_textual_trace(v.value())) {
+ XBT_DEBUG(" %s", seq.c_str());
+ }
+ } else {
+ XBT_DEBUG("ODPOR: Ignoring race: `sleep(E')` intersects `WI_[E'](v := notdep(%u, E))`", e);
+ XBT_DEBUG("Sleep set contains:");
+ for (auto& [aid, transition] : prev_state.get_sleep_set())
+ XBT_DEBUG(" <%ld,%s>", aid, transition->to_string().c_str());
+ }
+ }
+ }
+ }
+
XBT_VERB("Backtracking from %s", get_record_trace().to_string().c_str());
XBT_DEBUG("%lu alternatives are yet to be explored:", opened_states_.size());
get_remote_app().check_deadlock();
// Take the point with smallest distance
- auto backtracking_point = best_opened_state();
+ auto backtracking_point = reduction_mode_ == ReductionMode::odpor ? next_odpor_state() : best_opened_state();
// if no backtracking point, then set the stack_ to empty so we can end the exploration
if (not backtracking_point) {
this->restore_stack(backtracking_point);
}
-DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor, bool need_memory_info)
+DFSExplorer::DFSExplorer(const std::vector<char*>& args, ReductionMode mode, bool need_memory_info)
: Exploration(args, need_memory_info || _sg_mc_termination
#if SIMGRID_HAVE_STATEFUL_MC
|| _sg_mc_checkpoint > 0
#endif
- )
+ )
+ , reduction_mode_(mode)
{
- if (with_dpor)
- reduction_mode_ = ReductionMode::dpor;
- else
- reduction_mode_ = ReductionMode::none;
-
if (_sg_mc_termination) {
- if (with_dpor) {
+ if (mode != ReductionMode::none) {
XBT_INFO("Check non progressive cycles (turning DPOR off)");
reduction_mode_ = ReductionMode::none;
} else {
}
if (stack_.back()->count_todo_multiples() > 1)
opened_states_.emplace_back(stack_.back());
+
+ if (mode == ReductionMode::odpor && !_sg_mc_sleep_set) {
+ // ODPOR requires the use of sleep sets; SDPOR
+ // "likes" using sleep sets but it is not strictly
+ // required
+ XBT_INFO("Forcing the use of sleep sets for use with ODPOR");
+ _sg_mc_sleep_set = true;
+ }
}
-Exploration* create_dfs_exploration(const std::vector<char*>& args, bool with_dpor)
+Exploration* create_dfs_exploration(const std::vector<char*>& args, ReductionMode mode)
{
- return new DFSExplorer(args, with_dpor);
+ return new DFSExplorer(args, mode);
}
} // namespace simgrid::mc
#ifndef SIMGRID_MC_SAFETY_CHECKER_HPP
#define SIMGRID_MC_SAFETY_CHECKER_HPP
+#include "src/mc/api/ClockVector.hpp"
#include "src/mc/api/State.hpp"
#include "src/mc/explo/Exploration.hpp"
+#include "src/mc/explo/odpor/Execution.hpp"
+#include "src/mc/mc_config.hpp"
#if SIMGRID_HAVE_STATEFUL_MC
#include "src/mc/VisitedState.hpp"
#endif
+#include <deque>
#include <list>
#include <memory>
#include <set>
#include <string>
+#include <unordered_map>
#include <vector>
namespace simgrid::mc {
-using stack_t = std::list<std::shared_ptr<State>>;
+using stack_t = std::deque<std::shared_ptr<State>>;
class XBT_PRIVATE DFSExplorer : public Exploration {
- XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor);
-
+private:
ReductionMode reduction_mode_;
unsigned long backtrack_count_ = 0; // for statistics
unsigned long visited_states_count_ = 0; // for statistics
static xbt::signal<void(RemoteApp&)> on_log_state_signal;
public:
- explicit DFSExplorer(const std::vector<char*>& args, bool with_dpor, bool need_memory_info = false);
+ explicit DFSExplorer(const std::vector<char*>& args, ReductionMode mode, bool need_memory_info = false);
void run() override;
RecordTrace get_record_trace() override;
void log_state() override;
/** Stack representing the position in the exploration graph */
stack_t stack_;
+
+ /**
+ * Provides additional metadata about the position in the exploration graph
+ * which is used by SDPOR and ODPOR
+ */
+ odpor::Execution execution_seq_;
+
+ /** Per-actor clock vectors used to compute the "happens-before" relation */
+ std::unordered_map<aid_t, ClockVector> per_actor_clocks_;
+
#if SIMGRID_HAVE_STATEFUL_MC
VisitedStates visited_states_;
std::unique_ptr<VisitedState> visited_state_;
std::vector<std::shared_ptr<State>> opened_states_;
std::shared_ptr<State> best_opened_state();
+ /** If we're running ODPOR, picks the corresponding state in the stack
+ * (opened_states_ are ignored)
+ */
+ std::shared_ptr<State> next_odpor_state();
+
/** Change current stack_ value to correspond to the one we would have
* had if we executed transition to get to state. This is required when
* backtracking, and achieved thanks to the fact states save their parent.*/
#include "simgrid/forward.h"
#include "src/mc/api/RemoteApp.hpp"
+#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_record.hpp"
#include <xbt/Extendable.hpp>
static Exploration* get_instance() { return instance_; }
// No copy:
- Exploration(Exploration const&) = delete;
+ Exploration(Exploration const&) = delete;
Exploration& operator=(Exploration const&) = delete;
/** Main function of this algorithm */
// External constructors so that the types (and the types of their content) remain hidden
XBT_PUBLIC Exploration* create_liveness_checker(const std::vector<char*>& args);
-XBT_PUBLIC Exploration* create_dfs_exploration(const std::vector<char*>& args, bool with_dpor);
-XBT_PUBLIC Exploration* create_communication_determinism_checker(const std::vector<char*>& args, bool with_dpor);
+XBT_PUBLIC Exploration* create_dfs_exploration(const std::vector<char*>& args, ReductionMode mode);
+XBT_PUBLIC Exploration* create_communication_determinism_checker(const std::vector<char*>& args, ReductionMode mode);
XBT_PUBLIC Exploration* create_udpor_checker(const std::vector<char*>& args);
} // namespace simgrid::mc
--- /dev/null
+/* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/3rd-party/catch.hpp"
+#include "src/mc/api/ClockVector.hpp"
+
+using namespace simgrid::mc;
+
+TEST_CASE("simgrid::mc::ClockVector: Constructing Vectors")
+{
+ SECTION("Without values")
+ {
+ ClockVector cv;
+ REQUIRE(cv.size() == 0);
+
+ // Verify `cv` doesn't map any values
+ REQUIRE_FALSE(cv.get(0).has_value());
+ REQUIRE_FALSE(cv.get(1).has_value());
+ REQUIRE_FALSE(cv.get(2).has_value());
+ REQUIRE_FALSE(cv.get(3).has_value());
+ }
+
+ SECTION("With initial values")
+ {
+ ClockVector cv{
+ {1, 5}, {3, 1}, {7, 10}, {6, 5}, {8, 1}, {10, 10},
+ };
+ REQUIRE(cv.size() == 6);
+
+ // Verify `cv` maps each value
+ REQUIRE(cv.get(1).has_value());
+ REQUIRE(cv.get(1).value() == 5);
+ REQUIRE(cv[1] == 5);
+ REQUIRE(cv.get(3).has_value());
+ REQUIRE(cv.get(3).value() == 1);
+ REQUIRE(cv[3] == 1);
+ REQUIRE(cv.get(7).has_value());
+ REQUIRE(cv.get(7).value() == 10);
+ REQUIRE(cv[7] == 10);
+ REQUIRE(cv.get(6).has_value());
+ REQUIRE(cv.get(6).value() == 5);
+ REQUIRE(cv[6] == 5);
+ REQUIRE(cv.get(8).has_value());
+ REQUIRE(cv.get(8).value() == 1);
+ REQUIRE(cv[8] == 1);
+ REQUIRE(cv.get(10).has_value());
+ REQUIRE(cv.get(10).value() == 10);
+ REQUIRE(cv[10] == 10);
+ }
+}
+
+TEST_CASE("simgrid::mc::ClockVector: Testing operator[]")
+{
+ ClockVector cv;
+ cv[0] = 1;
+ REQUIRE(cv.size() == 1);
+
+ REQUIRE(cv.get(0).has_value());
+ REQUIRE(cv.get(0).value() == 1);
+
+ // Verify `cv` doesn't map other values
+ REQUIRE_FALSE(cv.get(2).has_value());
+ REQUIRE_FALSE(cv.get(3).has_value());
+
+ cv[10] = 31;
+ REQUIRE(cv.size() == 2);
+
+ // Old values are still mapped
+ REQUIRE(cv.get(0).has_value());
+ REQUIRE(cv.get(0).value() == 1);
+ REQUIRE(cv[0] == 1);
+ REQUIRE(cv.get(10).has_value());
+ REQUIRE(cv.get(10).value() == 31);
+ REQUIRE(cv[10] == 31);
+
+ // Verify `cv` doesn't map other values
+ REQUIRE_FALSE(cv.get(2).has_value());
+ REQUIRE_FALSE(cv.get(3).has_value());
+}
+
+TEST_CASE("simgrid::mc::ClockVector: Testing Maximal Clock Vectors")
+{
+ SECTION("Max with zero clock vector yields self")
+ {
+ ClockVector cv1{
+ {1, 2},
+ {2, 10},
+ {3, 5},
+ };
+ ClockVector cv2;
+ ClockVector maxCV = ClockVector::max(cv1, cv2);
+
+ REQUIRE(maxCV.size() == 3);
+ REQUIRE(maxCV.get(1).has_value());
+ REQUIRE(maxCV.get(1).value() == 2);
+ REQUIRE(maxCV[1] == 2);
+
+ REQUIRE(maxCV.get(2).has_value());
+ REQUIRE(maxCV.get(2).value() == 10);
+ REQUIRE(maxCV[2] == 10);
+
+ REQUIRE(maxCV.get(3).has_value());
+ REQUIRE(maxCV.get(3).value() == 5);
+ REQUIRE(maxCV[3] == 5);
+ }
+
+ SECTION("Max with self clock vector yields self")
+ {
+ ClockVector cv1{
+ {1, 2},
+ {2, 10},
+ {3, 5},
+ };
+ ClockVector maxCV = ClockVector::max(cv1, cv1);
+
+ REQUIRE(maxCV.size() == 3);
+ REQUIRE(maxCV.get(1).has_value());
+ REQUIRE(maxCV.get(1).value() == 2);
+ REQUIRE(maxCV[1] == 2);
+
+ REQUIRE(maxCV.get(2).has_value());
+ REQUIRE(maxCV.get(2).value() == 10);
+ REQUIRE(maxCV[2] == 10);
+
+ REQUIRE(maxCV.get(3).has_value());
+ REQUIRE(maxCV.get(3).value() == 5);
+ REQUIRE(maxCV[3] == 5);
+ }
+
+ SECTION("Testing with partial overlaps")
+ {
+ SECTION("Example 1")
+ {
+ ClockVector cv1{
+ {1, 2},
+ {2, 10},
+ {3, 5},
+ };
+ ClockVector cv2{
+ {1, 5},
+ {3, 1},
+ {7, 10},
+ };
+ ClockVector maxCV = ClockVector::max(cv1, cv2);
+
+ REQUIRE(maxCV.size() == 4);
+ REQUIRE(maxCV.get(1).has_value());
+ REQUIRE(maxCV.get(1).value() == 5);
+ REQUIRE(maxCV[1] == 5);
+
+ REQUIRE(maxCV.get(2).has_value());
+ REQUIRE(maxCV.get(2).value() == 10);
+ REQUIRE(maxCV[2] == 10);
+
+ REQUIRE(maxCV.get(3).has_value());
+ REQUIRE(maxCV.get(3).value() == 5);
+ REQUIRE(maxCV[3] == 5);
+
+ REQUIRE(maxCV.get(7).has_value());
+ REQUIRE(maxCV.get(7).value() == 10);
+ REQUIRE(maxCV[7] == 10);
+ }
+
+ SECTION("Example 2")
+ {
+ ClockVector cv1{
+ {1, 2}, {2, 10}, {3, 5}, {4, 40}, {11, 3}, {12, 8},
+ };
+ ClockVector cv2{
+ {1, 18}, {2, 4}, {4, 41}, {10, 3}, {12, 8},
+ };
+ ClockVector maxCV = ClockVector::max(cv1, cv2);
+
+ REQUIRE(maxCV.size() == 7);
+ REQUIRE(maxCV.get(1).has_value());
+ REQUIRE(maxCV.get(1).value() == 18);
+ REQUIRE(maxCV[1] == 18);
+
+ REQUIRE(maxCV.get(2).has_value());
+ REQUIRE(maxCV.get(2).value() == 10);
+ REQUIRE(maxCV[2] == 10);
+
+ REQUIRE(maxCV.get(3).has_value());
+ REQUIRE(maxCV.get(3).value() == 5);
+ REQUIRE(maxCV[3] == 5);
+
+ REQUIRE(maxCV.get(4).has_value());
+ REQUIRE(maxCV.get(4).value() == 41);
+ REQUIRE(maxCV[4] == 41);
+
+ REQUIRE(maxCV.get(10).has_value());
+ REQUIRE(maxCV.get(10).value() == 3);
+ REQUIRE(maxCV[10] == 3);
+
+ REQUIRE(maxCV.get(11).has_value());
+ REQUIRE(maxCV.get(11).value() == 3);
+ REQUIRE(maxCV[11] == 3);
+
+ REQUIRE(maxCV.get(12).has_value());
+ REQUIRE(maxCV.get(12).value() == 8);
+ REQUIRE(maxCV[12] == 8);
+ }
+
+ SECTION("Example 3")
+ {
+ ClockVector cv1{{1, 2}, {4, 41}, {12, 0}, {100, 5}};
+ ClockVector cv2{{2, 4}, {4, 10}, {10, 3}, {12, 8}, {19, 0}, {21, 6}, {22, 0}};
+ ClockVector cv3{{21, 60}, {22, 6}, {100, 3}};
+ ClockVector maxCV = ClockVector::max(cv1, cv2);
+ maxCV = ClockVector::max(maxCV, cv3);
+
+ REQUIRE(maxCV.size() == 9);
+ REQUIRE(maxCV.get(1).has_value());
+ REQUIRE(maxCV.get(1).value() == 2);
+ REQUIRE(maxCV[1] == 2);
+
+ REQUIRE(maxCV.get(2).has_value());
+ REQUIRE(maxCV.get(2).value() == 4);
+ REQUIRE(maxCV[2] == 4);
+
+ REQUIRE(maxCV.get(4).has_value());
+ REQUIRE(maxCV.get(4).value() == 41);
+ REQUIRE(maxCV[4] == 41);
+
+ REQUIRE(maxCV.get(10).has_value());
+ REQUIRE(maxCV.get(10).value() == 3);
+ REQUIRE(maxCV[10] == 3);
+
+ REQUIRE(maxCV.get(12).has_value());
+ REQUIRE(maxCV.get(12).value() == 8);
+ REQUIRE(maxCV[12] == 8);
+
+ REQUIRE(maxCV.get(19).has_value());
+ REQUIRE(maxCV.get(19).value() == 0);
+ REQUIRE(maxCV[19] == 0);
+
+ REQUIRE(maxCV.get(21).has_value());
+ REQUIRE(maxCV.get(21).value() == 60);
+ REQUIRE(maxCV[21] == 60);
+
+ REQUIRE(maxCV.get(22).has_value());
+ REQUIRE(maxCV.get(22).value() == 6);
+ REQUIRE(maxCV[22] == 6);
+
+ REQUIRE(maxCV.get(100).has_value());
+ REQUIRE(maxCV.get(100).value() == 5);
+ REQUIRE(maxCV[100] == 5);
+ }
+ }
+
+ SECTION("Testing without overlaps")
+ {
+ SECTION("Example 1")
+ {
+ ClockVector cv1{{1, 2}};
+ ClockVector cv2{
+ {2, 4},
+ {4, 41},
+ {10, 3},
+ {12, 8},
+ };
+ ClockVector maxCV = ClockVector::max(cv1, cv2);
+
+ REQUIRE(maxCV.size() == 5);
+ REQUIRE(maxCV.get(1).has_value());
+ REQUIRE(maxCV.get(1).value() == 2);
+ REQUIRE(maxCV[1] == 2);
+
+ REQUIRE(maxCV.get(2).has_value());
+ REQUIRE(maxCV.get(2).value() == 4);
+ REQUIRE(maxCV[2] == 4);
+
+ REQUIRE(maxCV.get(4).has_value());
+ REQUIRE(maxCV.get(4).value() == 41);
+ REQUIRE(maxCV[4] == 41);
+
+ REQUIRE(maxCV.get(10).has_value());
+ REQUIRE(maxCV.get(10).value() == 3);
+ REQUIRE(maxCV[10] == 3);
+
+ REQUIRE(maxCV.get(12).has_value());
+ REQUIRE(maxCV.get(12).value() == 8);
+ REQUIRE(maxCV[12] == 8);
+ }
+
+ SECTION("Example 2")
+ {
+ ClockVector cv1{{1, 2}, {4, 41}};
+ ClockVector cv2{
+ {2, 4},
+ {10, 3},
+ {12, 8},
+ };
+ ClockVector maxCV = ClockVector::max(cv1, cv2);
+
+ REQUIRE(maxCV.size() == 5);
+ REQUIRE(maxCV.get(1).has_value());
+ REQUIRE(maxCV.get(1).value() == 2);
+ REQUIRE(maxCV[1] == 2);
+
+ REQUIRE(maxCV.get(2).has_value());
+ REQUIRE(maxCV.get(2).value() == 4);
+ REQUIRE(maxCV[2] == 4);
+
+ REQUIRE(maxCV.get(4).has_value());
+ REQUIRE(maxCV.get(4).value() == 41);
+ REQUIRE(maxCV[4] == 41);
+
+ REQUIRE(maxCV.get(10).has_value());
+ REQUIRE(maxCV.get(10).value() == 3);
+ REQUIRE(maxCV[10] == 3);
+
+ REQUIRE(maxCV.get(12).has_value());
+ REQUIRE(maxCV.get(12).value() == 8);
+ REQUIRE(maxCV[12] == 8);
+ }
+
+ SECTION("Example 3")
+ {
+ ClockVector cv1{{1, 2}, {4, 41}};
+ ClockVector cv2{{2, 4}, {10, 3}, {12, 8}, {19, 0}, {21, 6}};
+ ClockVector cv3{{22, 6}, {100, 3}};
+ ClockVector maxCV = ClockVector::max(cv1, cv2);
+ maxCV = ClockVector::max(maxCV, cv3);
+
+ REQUIRE(maxCV.size() == 9);
+ REQUIRE(maxCV.get(1).has_value());
+ REQUIRE(maxCV.get(1).value() == 2);
+ REQUIRE(maxCV[1] == 2);
+
+ REQUIRE(maxCV.get(2).has_value());
+ REQUIRE(maxCV.get(2).value() == 4);
+ REQUIRE(maxCV[2] == 4);
+
+ REQUIRE(maxCV.get(4).has_value());
+ REQUIRE(maxCV.get(4).value() == 41);
+ REQUIRE(maxCV[4] == 41);
+
+ REQUIRE(maxCV.get(10).has_value());
+ REQUIRE(maxCV.get(10).value() == 3);
+ REQUIRE(maxCV[10] == 3);
+
+ REQUIRE(maxCV.get(12).has_value());
+ REQUIRE(maxCV.get(12).value() == 8);
+ REQUIRE(maxCV[12] == 8);
+
+ REQUIRE(maxCV.get(19).has_value());
+ REQUIRE(maxCV.get(19).value() == 0);
+ REQUIRE(maxCV[19] == 0);
+
+ REQUIRE(maxCV.get(21).has_value());
+ REQUIRE(maxCV.get(21).value() == 6);
+ REQUIRE(maxCV[21] == 6);
+
+ REQUIRE(maxCV.get(22).has_value());
+ REQUIRE(maxCV.get(22).value() == 6);
+ REQUIRE(maxCV[22] == 6);
+
+ REQUIRE(maxCV.get(100).has_value());
+ REQUIRE(maxCV.get(100).value() == 3);
+ REQUIRE(maxCV[100] == 3);
+ }
+ }
+}
\ No newline at end of file
--- /dev/null
+/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#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>
+
+namespace simgrid::mc::odpor {
+
+std::vector<std::string> get_textual_trace(const PartialExecution& w)
+{
+ std::vector<std::string> trace;
+ for (const auto& t : w) {
+ const auto a = xbt::string_printf("Actor %ld: %s", t->aid_, t->to_string(true).c_str());
+ trace.push_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) {
+ throw std::invalid_argument("Unexpectedly received `nullptr`");
+ }
+ ClockVector max_clock_vector;
+ for (const Event& e : this->contents_) {
+ if (e.get_transition()->depends(t.get())) {
+ max_clock_vector = ClockVector::max(max_clock_vector, e.get_clock_vector());
+ }
+ }
+ max_clock_vector[t->aid_] = this->size();
+ 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_) {
+ const auto a =
+ xbt::string_printf("Actor %ld: %s", t.get_transition()->aid_, t.get_transition()->to_string(true).c_str());
+ trace.push_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;
+ 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)) {
+ continue;
+ }
+
+ // Further, `proc(e_i) != proc(target)`
+ if (get_actor_with_handle(e_i) == get_actor_with_handle(target)) {
+ disqualified_events.insert(e_i);
+ continue;
+ }
+
+ // There could an event that "happens-between" the two events which would discount `e_i` as a race
+ for (auto e_j = e_i; e_j < target; e_j++) {
+ // If both:
+ // 1. e_i --->_E e_j; and
+ // 2. disqualified_events.count(e_j) > 0
+ // then e_i --->_E target indirectly (either through
+ // e_j directly, or transitively through e_j)
+ if (disqualified_events.count(e_j) > 0 and happens_before(e_i, e_j)) {
+ disqualified_events.insert(e_i);
+ break;
+ }
+ }
+
+ // If `e_i` wasn't disqualified in the last round,
+ // it's in a race with `target`. After marking it
+ // as such, we ensure no other event `e` can happen-before
+ // it (since this would transitively make it the event
+ // which "happens-between" `target` and `e`)
+ if (disqualified_events.count(e_i) == 0) {
+ 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::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::unordered_set<aid_t>{};
+ }
+
+ // To actually compute `I_[E'](v) ∩ backtrack(E')`, we must
+ // first compute `E'` and "move" in the direction of `v`.
+ // We perform a scan over `E` (this execution) and make
+ // 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 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`
+ for (auto e_prime = e + 1; e_prime <= next_E_p; ++e_prime) {
+ // Any event `e*` which occurs after `e` but which does not
+ // 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) {
+ // 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();
+
+ // When checking whether any event in `dom_[E'](v)` happens before
+ // `next_[E'](q)` below for thread `q`, we must consider that the
+ // 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'`.
+ //
+ // 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);
+
+ const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v);
+ 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) {
+ // 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
+ // by actor `q` will qualify since any (valid) happens-before
+ // relation orders actions taken by each actor
+ disqualified_actors.insert(q);
+ }
+ }
+ }
+ xbt_assert(!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,
+ const State& state_at_e) const
+{
+ // `e` is assumed to be in a reversible race with `e_prime`.
+ // If `e > e_prime`, then `e` occurs-after `e_prime` which means
+ // `e` could not race with if
+ if (e > e_prime) {
+ throw std::invalid_argument("ODPOR extensions can only be computed for "
+ "events in a reversible race, which is claimed, "
+ "yet the racing event 'occurs-after' the target");
+ }
+
+ if (empty()) {
+ return std::nullopt;
+ }
+
+ 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);
+ 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: ODPOR requires us to compute `notdep(e, E)` EVEN THOUGH
+ // the race is between `e` and `e'`; that is, events occurring in `E`
+ // that "occur-after" `e'` may end up in the partial execution `v`.
+ //
+ // Observe that `notdep(e, E).proc(e')` will contain all transitions
+ // that don't happen-after `e` in the order they appear FOLLOWED BY
+ // THE **TRANSITION** ASSOCIATED WITH **`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` 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) {
+ // Any event `e*` which occurs after `e` but which does not
+ // 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'
+ // to be able to compute `--->[E'.v]`
+ if (not happens_before(e, e_star)) {
+ xbt_assert(e_star != e_prime,
+ "Invariant Violation: We claimed events %u and %u were in a reversible race, yet we also "
+ "claim that they do not happen-before one another. This is impossible: "
+ "are you sure that the two events are in a reversible race?",
+ e, e_prime);
+ E_prime_v.push_transition(get_event_with_handle(e_star).get_transition());
+ v.push_back(get_event_with_handle(e_star).get_transition());
+
+ const EventHandle e_star_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
+
+ // When checking whether any event in `dom_[E'](v)` happens before
+ // `next_[E'](q)` below for thread `q`, we must consider that the
+ // 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'`
+ v_handles.push_back(e_star_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_star_in_E_prime_v);
+ 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_star) {
+ return E_prime_v.happens_before(e_star, e_star_in_E_prime_v);
+ });
+ if (is_initial) {
+ // 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
+ // by actor `q` will qualify since any (valid) happens-before
+ // relation orders actions taken by each actor
+ disqualified_actors.insert(q);
+ }
+ }
+ }
+
+ // Now we add `e_prime := <q, i>` to `E'.v` and repeat the same work
+ // 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& e_star) {
+ return E_prime_v.happens_before(e_star, 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);
+ }
+ }
+ }
+ {
+ const Execution pre_E_e = get_prefix_before(e);
+ const auto sleeping_actors = state_at_e.get_sleeping_actors();
+
+ // 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()) {
+ 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 v;
+}
+
+bool Execution::is_initial_after_execution_of(const PartialExecution& w, aid_t p) const
+{
+ auto E_w = *this;
+ std::vector<EventHandle> w_handles;
+ for (const auto& w_i : w) {
+ // Take one step in the direction of `w`
+ E_w.push_transition(w_i);
+
+ // If that step happened to be executed by `p`,
+ // great: we know that `p` is contained in `w`.
+ // We now need to verify that it doens't "happen-after"
+ // any events which occur before it
+ if (w_i->aid_ == p) {
+ const auto p_handle = E_w.get_latest_event_handle().value();
+ return std::none_of(w_handles.begin(), w_handles.end(),
+ [&](const auto handle) { return E_w.happens_before(handle, p_handle); });
+ } else {
+ w_handles.push_back(E_w.get_latest_event_handle().value());
+ }
+ }
+ return false;
+}
+
+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
+ // actors occurring before `p_i` in `v` (`p_j`, `0 <= j < i`)
+ // are sufficient to enable `p_i`. This is fortunately the case
+ // with what ODPOR requires of us, viz. to ask the question about
+ // `v := notdep(e, E)` for some execution `E` and event `e` of
+ // that execution.
+ auto E_p_w = *this;
+ E_p_w.push_transition(std::move(next_E_p));
+ const auto p_handle = E_p_w.get_latest_event_handle().value();
+
+ // As we add events to `w`, verify that none
+ // of them "happen-after" the event associated with
+ // the step `next_E_p` (viz. p_handle)
+ for (const auto& w_i : w) {
+ E_p_w.push_transition(w_i);
+ const auto w_i_handle = E_p_w.get_latest_event_handle().value();
+ if (E_p_w.happens_before(p_handle, w_i_handle)) {
+ return false;
+ }
+ }
+ return true;
+}
+
+std::optional<PartialExecution> Execution::get_shortest_odpor_sq_subset_insertion(const PartialExecution& v,
+ const PartialExecution& w) const
+{
+ // See section 4 of Abdulla. et al.'s 2017 ODPOR paper for details (specifically
+ // where the [iterative] computation of `v ~_[E] w` is described)
+ auto E_v = *this;
+ 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_of(w_now, p)) {
+ // Remove `p` from w and continue
+
+ // 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,
+ // they should always refer to the same value; but as a sanity check,
+ // we have an assert that tests that at least the types are the same.
+ 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(), "Invariant violated: actor `p` "
+ "is claimed to be an initial after `w` but is "
+ "not actually contained in `w`. This indicates that there "
+ "is a bug computing initials");
+ const auto& w_action = *action_by_p_in_w;
+ xbt_assert(w_action->type_ == next_E_p->type_,
+ "Invariant violated: `v` claims that actor `%ld` executes '%s' while "
+ "`w` claims that it executes '%s'. These two partial executions both "
+ "refer to `next_[E](p)`, which should be the same",
+ p, next_E_p->to_string(false).c_str(), w_action->to_string(false).c_str());
+ w_now.erase(action_by_p_in_w);
+ }
+ // Is `E ⊢ p ◇ w`?
+ 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` (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(),
+ "Invariant violated: We claimed that actor `%ld` is not an initial "
+ "after `w`, yet it's independent with all actions of `w` AND occurs in `w`."
+ "This indicates that there is a bug computing initials",
+ p);
+ } else {
+ // Neither of the two above conditions hold, so the relation fails
+ return std::nullopt;
+ }
+
+ // Move one step forward in the direction of `v` and repeat
+ E_v.push_transition(next_E_p);
+ }
+ return std::optional<PartialExecution>{std::move(w_now)};
+}
+
+bool Execution::happens_before(Execution::EventHandle e1_handle, Execution::EventHandle e2_handle) const
+{
+ // 1. "happens-before" (-->_E) is a subset of "occurs before" (<_E)
+ // and is an irreflexive relation
+ if (e1_handle >= e2_handle) {
+ return false;
+ }
+
+ // Each execution maintains a stack of clock vectors which are updated
+ // according to the procedure outlined in section 4 of the original DPOR paper
+ const Event& e2 = get_event_with_handle(e2_handle);
+ const aid_t proc_e1 = get_actor_with_handle(e1_handle);
+
+ if (const auto e1_in_e2_clock = e2.get_clock_vector().get(proc_e1); e1_in_e2_clock.has_value()) {
+ return e1_handle <= e1_in_e2_clock.value();
+ }
+ // If `e1` does not appear in e2's clock vector, this implies
+ // not only that the transitions associated with `e1` and `e2
+ // are independent, but further that there are no transitive
+ // dependencies between e1 and e2
+ return false;
+}
+
+} // namespace simgrid::mc::odpor
\ No newline at end of file
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_ODPOR_EXECUTION_HPP
+#define SIMGRID_MC_ODPOR_EXECUTION_HPP
+
+#include "src/mc/api/ClockVector.hpp"
+#include "src/mc/explo/odpor/odpor_forward.hpp"
+#include "src/mc/mc_forward.hpp"
+#include "src/mc/mc_record.hpp"
+#include "src/mc/transition/Transition.hpp"
+
+#include <list>
+#include <optional>
+#include <unordered_set>
+#include <vector>
+
+namespace simgrid::mc::odpor {
+
+std::vector<std::string> get_textual_trace(const PartialExecution& w);
+
+/**
+ * @brief The occurrence of a transition in an execution
+ *
+ * An execution is set of *events*, where each element represents
+ * the occurrence or execution of the `i`th step of a particular
+ * actor `j`
+ */
+class Event {
+ std::pair<std::shared_ptr<Transition>, ClockVector> contents_;
+
+public:
+ Event() = default;
+ Event(Event&&) = default;
+ Event(const Event&) = default;
+ Event& operator=(const Event&) = default;
+ explicit Event(std::pair<std::shared_ptr<Transition>, ClockVector> pair) : contents_(std::move(pair)) {}
+
+ std::shared_ptr<Transition> get_transition() const { return std::get<0>(contents_); }
+ const ClockVector& get_clock_vector() const { return std::get<1>(contents_); }
+};
+
+/**
+ * @brief An ordered sequence of transitions which describe
+ * the evolution of a process undergoing model checking
+ *
+ * An execution conceptually is just a string of actors
+ * ids (e.g. "1.2.3.1.2.2.1.1"), where the `i`th occurrence
+ * of actor id `j` corresponds to the `i`th action executed
+ * by the actor with id `j` (viz. the `i`th step of actor `j`).
+ * Executions can stand alone on their own or can extend
+ * the execution of other sequences
+ *
+ * Executions are conceived based on the following papers:
+ * 1. "Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction"
+ * by Abdulla et al.
+ *
+ * In addition to representing an actual steps taken,
+ * an execution keeps track of the "happens-before"
+ * relation among the transitions in the execution
+ * by following the procedure outlined in section 4 of the
+ * original DPOR paper with clock vectors.
+ * As new transitions are added to the execution, clock vectors are
+ * computed as appropriate and associated with the corresponding position
+ * in the execution. This allows us to determine “happens-before” in
+ * constant-time between points in the execution (called events
+ * [which is unfortunately the same name used in UDPOR for a slightly
+ * different concept]), albeit for an up-front cost of traversing the
+ * execution stack. The happens-before relation is important in many
+ * places in SDPOR and ODPOR.
+ *
+ * @note: For more nuanced happens-before relations, clock
+ * vectors may not always suffice. Clock vectors work
+ * well with transition-based dependencies like that used in
+ * SimGrid; but to have a more refined independence relation,
+ * an event-based dependency approach is needed. See the section 2
+ * in the ODPOR paper [1] concerning event-based dependencies and
+ * how the happens-before relation can be refined in a
+ * computation model much like that of SimGrid. In fact, the same issue
+ * arrises with UDPOR with context-sensitive dependencies:
+ * the two concepts are analogous if not identical
+ */
+class Execution {
+private:
+ std::vector<Event> contents_;
+ Execution(std::vector<Event>&& contents) : contents_(std::move(contents)) {}
+
+public:
+ using EventHandle = uint32_t;
+
+ Execution() = default;
+ Execution(const Execution&) = default;
+ Execution& operator=(Execution const&) = default;
+ Execution(Execution&&) = default;
+ Execution(const PartialExecution&);
+
+ std::vector<std::string> get_textual_trace() const;
+
+ size_t size() const { return this->contents_.size(); }
+ bool empty() const { return this->contents_.empty(); }
+ auto begin() const { return this->contents_.begin(); }
+ auto end() const { return this->contents_.end(); }
+
+ /**
+ * @brief Computes the "core" portion the SDPOR algorithm,
+ * viz. the intersection of the backtracking set and the
+ * set of initials with respect to the *last* event added
+ * to the execution
+ *
+ * The "core" portion of the SDPOR algorithm is found on
+ * lines 6-9 of the pseudocode:
+ *
+ * 6 | let E' := pre(E, e)
+ * 7 | let v := notdep(e, E).p
+ * 8 | if I_[E'](v) ∩ backtrack(E') = empty then
+ * 9 | --> add some q in I_[E'](v) to backtrack(E')
+ *
+ * This method computes all of the lines simultaneously,
+ * returning some actor `q` if it passes line 8 and exists.
+ * The event `e` and the set `backtrack(E')` are the provided
+ * arguments to the method.
+ *
+ * @param e the event with respect to which to determine
+ * whether a backtrack point needs to be added for the
+ * prefix corresponding to the execution prior to `e`
+ *
+ * @param backtrack_set The set of actors which should
+ * not be considered for selection as an SDPOR initial.
+ * While this set need not necessarily correspond to the
+ * backtrack set `backtrack(E')`, doing so provides what
+ * is expected for SDPOR
+ *
+ * See the SDPOR algorithm pseudocode in [1] for more
+ * details for the context of the function.
+ *
+ * @invariant: This method assumes that events `e` and
+ * `e' := get_latest_event_handle()` are in a *reversible* race
+ * as is explicitly the case in SDPOR
+ *
+ * @returns an actor not contained in `disqualified` which
+ * can serve as an initial to reverse the race between `e`
+ * and `e'`
+ */
+ std::unordered_set<aid_t> get_missing_source_set_actors_from(EventHandle e,
+ const std::unordered_set<aid_t>& backtrack_set) const;
+
+ /**
+ * @brief Computes the analogous lines from the SDPOR algorithm
+ * in the ODPOR algorithm, viz. the intersection of the slee set
+ * and the set of weak initials with respect to the given pair
+ * of racing events
+ *
+ * This method computes lines 4-6 of the ODPOR pseudocode, viz.:
+ *
+ * 4 | let E' := pre(E, e)
+ * 5 | let v := notdep(e, E).e'^
+ * 6 | if sleep(E') ∩ WI_[E'](v) = empty then ...
+ *
+ * The sequence `v` is computed and returned as needed, based on whether
+ * the check on line 6 passes.
+ *
+ * @invariant: This method assumes that events `e` and
+ * `e_prime` are in a *reversible* race as is the case
+ * in ODPOR
+ */
+ std::optional<PartialExecution> get_odpor_extension_from(EventHandle e, EventHandle e_prime,
+ const State& state_at_e) const;
+
+ /**
+ * @brief For a given sequence of actors `v` and a sequence of transitions `w`,
+ * computes the sequence, if any, that should be inserted as a child in wakeup tree for
+ * this execution
+ *
+ * Recall that the procedure for implementing the insertion
+ * is outlined in section 6.2 of Abdulla et al. 2017 as follows:
+ *
+ * | Let `v` be the smallest (w.r.t to "<") sequence in [the tree] B
+ * | such that `v ~_[E] w`. If `v` is a leaf node, the tree can be left
+ * | unmodified.
+ * |
+ * | Otherwise let `w'` be the shortest sequence such that `w [=_[E] v.w'`
+ * | and add `v.w'` as a new leaf, ordered after all already existing nodes
+ * | of the form `v.w''`
+ *
+ * This method computes the result `v.w'` as needed (viz. only if `v ~_[E] w`
+ * with respect to this execution `E`)
+ *
+ * The procedure for determining `v ~_[E] w` is given as Lemma 4.6 of
+ * Abdulla et al. 2017:
+ *
+ * | The relation `v ~_[E] w` holds if either
+ * | (1) v = <>, or
+ * | (2) v := p.v' and either
+ * | (a) p in I_[E](w) and `v' ~_[E.p] (w \ p)`
+ * | (b) E ⊢ p ◊ w and `v' ~_[E.p] w`
+ *
+ * @invariant: This method assumes that `E.v` is a valid execution, viz.
+ * that the events of `E` are sufficient to enabled `v_0` and that
+ * `v_0, ..., v_{i - 1}` are sufficient to enable `v_i`. This is the
+ * case when e.g. `v := notdep(e, E).p` for example in ODPOR
+ *
+ * @returns a partial execution `w'` that should be inserted
+ * as a child of a wakeup tree node with the associated sequence `v`.
+ */
+ std::optional<PartialExecution> get_shortest_odpor_sq_subset_insertion(const PartialExecution& v,
+ const PartialExecution& w) const;
+
+ /**
+ * @brief For a given sequence `w`, determines whether p in I_[E](w)
+ *
+ * @note: You may notice that some of the other methods compute this
+ * value as well. What we notice, though, in those cases is that
+ * we are repeatedly asking about initials with respect to an execution.
+ * It is better, then, to bunch the work together in those cases to
+ * get asymptotically better results (e.g. instead of calling with all
+ * `N` actors, we can process them "in-parallel" as is done with the
+ * computation of SDPOR initials)
+ */
+ bool is_initial_after_execution_of(const PartialExecution& w, aid_t p) const;
+
+ /**
+ * @brief Determines whether `E ⊢ p ◊ w` given the next action taken by `p`
+ */
+ bool is_independent_with_execution_of(const PartialExecution& w, std::shared_ptr<Transition> next_E_p) const;
+
+ /**
+ * @brief Determines the event associated with
+ * the given handle `handle`
+ */
+ const Event& get_event_with_handle(EventHandle handle) const { return contents_[handle]; }
+
+ /**
+ * @brief Determines the actor associated with
+ * the given event handle `handle`
+ */
+ aid_t get_actor_with_handle(EventHandle handle) const { return get_event_with_handle(handle).get_transition()->aid_; }
+
+ /**
+ * @brief Determines the transition associated with the given handle `handle`
+ */
+ const Transition* get_transition_for_handle(EventHandle handle) const
+ {
+ return get_event_with_handle(handle).get_transition().get();
+ }
+
+ /**
+ * @brief Returns a handle to the newest event of the execution,
+ * if such an event exists
+ */
+ std::optional<EventHandle> get_latest_event_handle() const
+ {
+ return contents_.empty() ? std::nullopt : std::optional<EventHandle>{static_cast<EventHandle>(size() - 1)};
+ }
+
+ /**
+ * @brief Returns a set of events which are in
+ * "immediate conflict" (according to the definition given
+ * in the ODPOR paper) with the given event
+ *
+ * Two events `e` and `e'` in an execution `E` are said to
+ * race iff
+ *
+ * 1. `proc(e) != proc(e')`; that is, the events correspond to
+ * the execution of different actors
+ * 2. `e -->_E e'` and there is no `e''` in `E` such that
+ * `e -->_E e''` and `e'' -->_E e'`; that is, the two events
+ * "happen-before" one another in `E` and no other event in
+ * `E` "happens-between" `e` and `e'`
+ *
+ * @param handle the event with respect to which races are
+ * computed
+ * @returns a set of event handles from which race with `handle`
+ */
+ std::unordered_set<EventHandle> get_racing_events_of(EventHandle handle) const;
+
+ /**
+ * @brief Returns a set of events which are in a reversible
+ * race with the given event handle `handle`
+ *
+ * Two events `e` and `e'` in an execution `E` are said to
+ * be in a reversible race iff
+ *
+ * 1. `e` and `e'` race
+ * 2. In any equivalent execution sequence `E'` to `E`
+ * where `e` occurs immediately before `e'`, the actor
+ * running `e'` was enabled in the state prior to `e`
+ *
+ * @param handle the event with respect to which
+ * reversible races are computed
+ * @returns a set of event handles from which are in a reversible
+ * race with `handle`
+ */
+ std::unordered_set<EventHandle> get_reversible_races_of(EventHandle handle) const;
+
+ /**
+ * @brief Computes `pre(e, E)` as described in ODPOR [1]
+ *
+ * The execution `pre(e, E)` for an event `e` in an
+ * execution `E` is the contiguous prefix of events
+ * `E' <= E` up to by excluding the event `e` itself.
+ * The prefix intuitively represents the "history" of
+ * causes that permitted event `e` to exist (roughly
+ * speaking)
+ */
+ Execution get_prefix_before(EventHandle) const;
+
+ /**
+ * @brief Whether the event represented by `e1`
+ * "happens-before" the event represented by
+ * `e2` in the context of this execution
+ *
+ * In the terminology of the ODPOR paper,
+ * this function computes
+ *
+ * `e1 --->_E e2`
+ *
+ * where `E` is this execution
+ *
+ * @note: The happens-before relation computed by this
+ * execution is "coarse" in the sense that context-sensitive
+ * independence is not exploited. To include such context-sensitive
+ * dependencies requires a new method of keeping track of
+ * the happens-before procedure, which is nontrivial...
+ */
+ bool happens_before(EventHandle e1, EventHandle e2) const;
+
+ /**
+ * @brief Extends the execution by one more step
+ *
+ * Intutively, pushing a transition `t` onto execution `E`
+ * is equivalent to making the execution become (using the
+ * notation of [1]) `E.proc(t)` where `proc(t)` is the
+ * actor which executed transition `t`.
+ */
+ void push_transition(std::shared_ptr<Transition>);
+
+ /**
+ * @brief Extends the execution by a sequence of steps
+ */
+ void push_partial_execution(const PartialExecution&);
+};
+
+} // namespace simgrid::mc::odpor
+#endif
--- /dev/null
+/* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/3rd-party/catch.hpp"
+#include "src/mc/explo/odpor/Execution.hpp"
+#include "src/mc/explo/odpor/odpor_tests_private.hpp"
+#include "src/mc/transition/TransitionComm.hpp"
+
+using namespace simgrid::mc;
+using namespace simgrid::mc::odpor;
+using namespace simgrid::mc::udpor;
+
+TEST_CASE("simgrid::mc::odpor::Execution: Constructing Executions")
+{
+ Execution execution;
+ REQUIRE(execution.empty());
+ REQUIRE(execution.size() == 0);
+ REQUIRE_FALSE(execution.get_latest_event_handle().has_value());
+}
+
+TEST_CASE("simgrid::mc::odpor::Execution: Testing Happens-Before")
+{
+ SECTION("Example 1")
+ {
+ // We check each permutation for happens before
+ // among the given actions added to the execution
+ const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 4);
+
+ Execution execution;
+ execution.push_transition(a1);
+ execution.push_transition(a2);
+ execution.push_transition(a3);
+ execution.push_transition(a4);
+
+ SECTION("Happens-before is irreflexive")
+ {
+ REQUIRE_FALSE(execution.happens_before(0, 0));
+ REQUIRE_FALSE(execution.happens_before(1, 1));
+ REQUIRE_FALSE(execution.happens_before(2, 2));
+ REQUIRE_FALSE(execution.happens_before(3, 3));
+ }
+
+ SECTION("Happens-before values for each pair of events")
+ {
+ REQUIRE_FALSE(execution.happens_before(0, 1));
+ REQUIRE_FALSE(execution.happens_before(0, 2));
+ REQUIRE(execution.happens_before(0, 3));
+ REQUIRE_FALSE(execution.happens_before(1, 2));
+ REQUIRE_FALSE(execution.happens_before(1, 3));
+ REQUIRE_FALSE(execution.happens_before(2, 3));
+ }
+
+ SECTION("Happens-before is a subset of 'occurs-before' ")
+ {
+ REQUIRE_FALSE(execution.happens_before(1, 0));
+ REQUIRE_FALSE(execution.happens_before(2, 0));
+ REQUIRE_FALSE(execution.happens_before(3, 0));
+ REQUIRE_FALSE(execution.happens_before(2, 1));
+ REQUIRE_FALSE(execution.happens_before(3, 1));
+ REQUIRE_FALSE(execution.happens_before(3, 2));
+ }
+ }
+
+ SECTION("Example 2")
+ {
+ const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+
+ // Notice that `a5` and `a6` are executed by the same actor; thus, although
+ // the actor is executing independent actions, each still "happen-before"
+ // the another
+
+ Execution execution;
+ execution.push_transition(a1);
+ execution.push_transition(a2);
+ execution.push_transition(a3);
+ execution.push_transition(a4);
+
+ SECTION("Happens-before is irreflexive")
+ {
+ REQUIRE_FALSE(execution.happens_before(0, 0));
+ REQUIRE_FALSE(execution.happens_before(1, 1));
+ REQUIRE_FALSE(execution.happens_before(2, 2));
+ REQUIRE_FALSE(execution.happens_before(3, 3));
+ }
+
+ SECTION("Happens-before values for each pair of events")
+ {
+ REQUIRE_FALSE(execution.happens_before(0, 1));
+ REQUIRE_FALSE(execution.happens_before(0, 2));
+ REQUIRE_FALSE(execution.happens_before(0, 3));
+ REQUIRE(execution.happens_before(1, 2));
+ REQUIRE(execution.happens_before(1, 3));
+ REQUIRE(execution.happens_before(2, 3));
+ }
+
+ SECTION("Happens-before is a subset of 'occurs-before'")
+ {
+ REQUIRE_FALSE(execution.happens_before(1, 0));
+ REQUIRE_FALSE(execution.happens_before(2, 0));
+ REQUIRE_FALSE(execution.happens_before(3, 0));
+ REQUIRE_FALSE(execution.happens_before(2, 1));
+ REQUIRE_FALSE(execution.happens_before(3, 1));
+ REQUIRE_FALSE(execution.happens_before(3, 2));
+ }
+ }
+
+ SECTION("Happens-before is transitively-closed")
+ {
+ SECTION("Example 1")
+ {
+ // Given a reversible race between events `e1` and `e3` in a simulation,
+ // we assert that `e5` would be eliminated from being contained in
+ // the sequence `notdep(e1, E)`
+ const auto e0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto e3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+
+ Execution execution;
+ execution.push_partial_execution(PartialExecution{e0, e1, e2, e3, e4});
+ REQUIRE(execution.happens_before(0, 2));
+ REQUIRE(execution.happens_before(2, 4));
+ REQUIRE(execution.happens_before(0, 4));
+ }
+
+ SECTION("Stress testing transitivity of the happens-before relation")
+ {
+ // This test verifies that for each triple of events
+ // in the execution, for a modestly intersting one,
+ // that transitivity holds
+ const auto e0 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e3 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 2, -10);
+ const auto e4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto e5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0);
+ const auto e6 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 2, -5);
+ const auto e7 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e8 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0);
+ const auto e9 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 2, -10);
+ const auto e10 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+
+ Execution execution;
+ execution.push_partial_execution(PartialExecution{e0, e1, e2, e3, e4, e5, e6, e7, e8, e9, e10});
+
+ const auto max_handle = execution.get_latest_event_handle();
+ for (Execution::EventHandle e_i = 0; e_i < max_handle; ++e_i) {
+ for (Execution::EventHandle e_j = 0; e_j < max_handle; ++e_j) {
+ for (Execution::EventHandle e_k = 0; e_k < max_handle; ++e_k) {
+ const bool e_i_before_e_j = execution.happens_before(e_i, e_j);
+ const bool e_j_before_e_k = execution.happens_before(e_j, e_k);
+ const bool e_i_before_e_k = execution.happens_before(e_i, e_k);
+ // Logical equivalent of `e_i_before_e_j ^ e_j_before_e_k --> e_i_before_e_k`
+ REQUIRE((!(e_i_before_e_j and e_j_before_e_k) or e_i_before_e_k));
+ }
+ }
+ }
+ }
+ }
+}
+
+TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials")
+{
+ SECTION("Example 1")
+ {
+ const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a3 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a4 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+
+ Execution execution;
+ execution.push_transition(a1);
+ execution.push_transition(a2);
+ execution.push_transition(a3);
+ execution.push_transition(a4);
+ execution.push_transition(a5);
+
+ // Nothing comes before event 0
+ REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
+
+ // Events 0 and 1 are independent
+ REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
+
+ // 2 and 1 are executed by different actors and happen right after each other
+ REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{1});
+
+ // Although a3 and a4 are dependent, they are executed by the same actor
+ REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{});
+
+ // Event 4 is in a race with neither event 0 nor event 2 since those events
+ // "happen-before" event 3 with which event 4 races
+ //
+ // Furthermore, event 1 is run by the same actor and thus also is not in a race.
+ // Hence, only event 3 races with event 4
+ REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{3});
+ }
+
+ SECTION("Example 2: Events with multiple races")
+ {
+ const auto a1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+
+ Execution execution;
+ execution.push_transition(a1);
+ execution.push_transition(a2);
+ execution.push_transition(a3);
+ execution.push_transition(a4);
+
+ // Nothing comes before event 0
+ REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
+
+ // Events 0 and 1 are independent
+ REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
+
+ // Event 2 is independent with event 1 and run by the same actor as event 0
+ REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{});
+
+ // All events are dependent with event 3, but event 0 "happens-before" event 2
+ REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{1, 2});
+
+ SECTION("Check initials with respect to event 1")
+ {
+ // First, note that v := notdep(1, execution).p == {e2}.{e3} == {e2, e3}
+ // Since e2 -->_E e3, actor 3 is not an initial for E' := pre(1, execution)
+ // with respect to `v`. e2, however, has nothing happening before it in dom_E(v),
+ // so it is an initial of E' wrt. `v`
+ const auto initial_wrt_event1 = execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{});
+ REQUIRE(initial_wrt_event1 == std::unordered_set<aid_t>{1});
+ }
+
+ SECTION("Check initials with respect to event 2")
+ {
+ // First, note that v := notdep(1, execution).p == {}.{e3} == {e3}
+ // e3 has nothing happening before it in dom_E(v), so it is an initial
+ // of E' wrt. `v`
+ const auto initial_wrt_event2 = execution.get_missing_source_set_actors_from(2, std::unordered_set<aid_t>{});
+ REQUIRE(initial_wrt_event2 == std::unordered_set<aid_t>{3});
+ }
+ }
+
+ SECTION("Example 3: Testing 'Lock' Example")
+ {
+ // In this example, `e0` and `e1` are lock actions that
+ // are in a race. We assert that
+ const auto e0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+
+ Execution execution;
+ execution.push_transition(e0);
+ execution.push_transition(e1);
+ execution.push_transition(e2);
+ execution.push_transition(e3);
+ execution.push_transition(e4);
+ REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{0});
+ }
+
+ SECTION("Example 4: Indirect Races")
+ {
+ const auto e0 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 6);
+ const auto e5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e6 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto e7 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto e8 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto e9 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
+
+ Execution execution(PartialExecution{e0, e1, e2, e3, e4, e5, e6, e7, e8, e9});
+
+ // Nothing comes before event 0
+ REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
+
+ // Events 0 and 1 are independent
+ REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
+
+ // Events 1 and 2 are independent
+ REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{});
+
+ // Events 1 and 3 are independent; the rest are executed by the same actor
+ REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{});
+
+ // 1. Events 3 and 4 race
+ // 2. Events 2 and 4 do NOT race since 2 --> 3 --> 4
+ // 3. Events 1 and 4 do NOT race since 1 is independent of 4
+ // 4. Events 0 and 4 do NOT race since 0 --> 2 --> 4
+ REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{3});
+
+ // Events 4 and 5 race; and because everyone before 4 (including 3) either
+ // a) happens-before, b) races, or c) does not race with 4, 4 is the race
+ REQUIRE(execution.get_racing_events_of(5) == std::unordered_set<Execution::EventHandle>{4});
+
+ // The same logic that applied to event 5 applies to event 6
+ REQUIRE(execution.get_racing_events_of(6) == std::unordered_set<Execution::EventHandle>{5});
+
+ // The same logic applies, except that this time since events 6 and 7 are run
+ // by the same actor, they don'tt actually race with one another
+ REQUIRE(execution.get_racing_events_of(7) == std::unordered_set<Execution::EventHandle>{});
+
+ // Event 8 is independent with everything
+ REQUIRE(execution.get_racing_events_of(8) == std::unordered_set<Execution::EventHandle>{});
+
+ // Event 9 is independent with events 7 and 8; event 6, however, is in race with 9.
+ // The same logic above eliminates events before 6
+ REQUIRE(execution.get_racing_events_of(9) == std::unordered_set<Execution::EventHandle>{6});
+ }
+
+ SECTION("Example 5: Stress testing race detection")
+ {
+ const auto e0 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e3 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 2, -10);
+ const auto e4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto e5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0);
+ const auto e6 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 2, -5);
+ const auto e7 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 1, -5);
+ const auto e8 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 0, 4);
+ const auto e9 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 2, -10);
+ const auto e10 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+
+ Execution execution(PartialExecution{e0, e1, e2, e3, e4, e5, e6, e7, e8, e9, e10});
+
+ // Nothing comes before event 0
+ CHECK(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
+
+ // Events 0 and 1 are independent
+ CHECK(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
+
+ // Events 1 and 2 are executed by the same actor, even though they are dependent
+ CHECK(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{});
+
+ // Events 2 and 3 are independent while events 1 and 2 are dependent
+ CHECK(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{1});
+
+ // Event 4 is independent with everything so it can never be in a race
+ CHECK(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{});
+
+ // Event 5 is independent with event 4. Since events 2 and 3 are dependent with event 5,
+ // but are independent of each other, both events are in a race with event 5
+ CHECK(execution.get_racing_events_of(5) == std::unordered_set<Execution::EventHandle>{2, 3});
+
+ // Events 5 and 6 are dependent. Everyone before 5 who's dependent with 5
+ // cannot be in a race with 6; everyone before 5 who's independent with 5
+ // could not race with 6
+ CHECK(execution.get_racing_events_of(6) == std::unordered_set<Execution::EventHandle>{5});
+
+ // Same goes for event 7 as for 6
+ CHECK(execution.get_racing_events_of(7) == std::unordered_set<Execution::EventHandle>{6});
+
+ // Events 5 and 8 are both run by the same actor; events in-between are independent
+ CHECK(execution.get_racing_events_of(8) == std::unordered_set<Execution::EventHandle>{});
+
+ // Event 6 blocks event 9 from racing with event 6
+ CHECK(execution.get_racing_events_of(9) == std::unordered_set<Execution::EventHandle>{});
+
+ // Event 10 is independent with everything so it can never be in a race
+ CHECK(execution.get_racing_events_of(10) == std::unordered_set<Execution::EventHandle>{});
+ }
+
+ SECTION("Example with many races for one event")
+ {
+ const auto e0 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto e3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto e4 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 5);
+ const auto e5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 6);
+ const auto e6 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 7);
+
+ Execution execution(PartialExecution{e0, e1, e2, e3, e4, e5, e6});
+ REQUIRE(execution.get_racing_events_of(6) == std::unordered_set<Execution::EventHandle>{0, 1, 2, 3, 4, 5});
+ }
+}
+
+TEST_CASE("simgrid::mc::odpor::Execution: Independence Tests")
+{
+ SECTION("Complete independence")
+ {
+ // Every transition is independent with every other and run by different actors. Hopefully
+ // we say that the events are independent with each other...
+ const auto a0 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 5);
+ const auto a5 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 6);
+ const auto a6 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 7);
+ const auto a7 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 7);
+ Execution execution(PartialExecution{a0, a1, a2, a3});
+
+ REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a4, a5}, a6));
+ REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a6, a5}, a1));
+ REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a6, a1}, a0));
+ REQUIRE(Execution().is_independent_with_execution_of(PartialExecution{a7, a7, a1}, a3));
+ REQUIRE(Execution().is_independent_with_execution_of(PartialExecution{a4, a0, a1}, a3));
+ REQUIRE(Execution().is_independent_with_execution_of(PartialExecution{a0, a7, a1}, a2));
+
+ // In this case, we notice that `a6` and `a7` are executed by the same actor.
+ // Hence, a6 cannot be independent with extending the execution with a4.a5.a7.
+ // Notice that we are treating *a6* as the next step of actor 7 (that is what we
+ // supplied as an argument)
+ REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a4, a5, a7}, a6));
+ }
+
+ SECTION("Independence is trivial with an empty extension")
+ {
+ REQUIRE(Execution().is_independent_with_execution_of(
+ PartialExecution{}, std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1)));
+ }
+
+ SECTION("Dependencies stopping independence from being possible")
+ {
+ const auto a0 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto a4 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto a5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a6 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a7 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a8 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto indep = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ Execution execution(PartialExecution{a0, a1, a2, a3});
+
+ // We see that although `a4` comes after `a1` with which it is dependent, it
+ // would come before "a6" in the partial execution `w`, so it would not be independent
+ REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a5, a6, a7}, a4));
+
+ // Removing `a6` from the picture, though, gives us the independence we're looking for.
+ REQUIRE(execution.is_independent_with_execution_of(PartialExecution{a5, a7}, a4));
+
+ // BUT, we we ask about a transition which is run by the same actor, even if they would be
+ // independent otherwise, we again lose independence
+ REQUIRE_FALSE(execution.is_independent_with_execution_of(PartialExecution{a5, a7, a8}, a4));
+
+ // This is a more interesting case:
+ // `indep` clearly is independent with the rest of the series, even though
+ // there are dependencies among the other events in the partial execution
+ REQUIRE(Execution().is_independent_with_execution_of(PartialExecution{a1, a6, a7}, indep));
+
+ // This ensures that independence is trivial with an empty partial execution
+ REQUIRE(execution.is_independent_with_execution_of(PartialExecution{}, a1));
+ }
+
+ SECTION("More interesting dependencies stopping independence")
+ {
+ const auto e0 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 1, 5);
+ const auto e1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e4 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 3, 5);
+ const auto e5 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 4, 4);
+ Execution execution(PartialExecution{e0, e1, e2, e3, e4, e5});
+
+ SECTION("Action run by same actor disqualifies independence")
+ {
+ const auto w_1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto w_2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto w_3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto w_4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto w = PartialExecution{w_1, w_2, w_3};
+
+ const auto actor4_action = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto actor4_action2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+
+ // Action `actor4_action` is independent with everything EXCEPT the last transition
+ // which is executed by the same actor
+ execution.is_independent_with_execution_of(w, actor4_action);
+
+ // Action `actor4_action2` is independent with everything
+ // EXCEPT the last transition which is executed by the same actor
+ execution.is_independent_with_execution_of(w, actor4_action);
+ }
+ }
+}
+
+TEST_CASE("simgrid::mc::odpor::Execution: Initials Test")
+{
+ const auto a0 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto a4 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto a5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a6 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a7 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a8 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto indep = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ Execution execution(PartialExecution{a0, a1, a2, a3});
+
+ SECTION("Initials trivial with empty executions")
+ {
+ // There are no initials for an empty extension since
+ // a requirement is that the actor be contained in the
+ // extension itself
+ REQUIRE_FALSE(execution.is_initial_after_execution_of(PartialExecution{}, 0));
+ REQUIRE_FALSE(execution.is_initial_after_execution_of(PartialExecution{}, 1));
+ REQUIRE_FALSE(execution.is_initial_after_execution_of(PartialExecution{}, 2));
+ REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{}, 0));
+ REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{}, 1));
+ REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{}, 2));
+ }
+
+ SECTION("The first actor is always an initial")
+ {
+ // Even in the case that the action is dependent with every
+ // other, if it is the first action to occur as part of the
+ // extension of the execution sequence, by definition it is
+ // an initial (recall that initials intuitively tell you which
+ // actions can be run starting from an execution `E`; if we claim
+ // to witness `E.w`, then clearly at least the first step of `w` is an initial)
+ REQUIRE(execution.is_initial_after_execution_of(PartialExecution{a3}, a3->aid_));
+ REQUIRE(execution.is_initial_after_execution_of(PartialExecution{a2, a3, a6}, a2->aid_));
+ REQUIRE(execution.is_initial_after_execution_of(PartialExecution{a6, a1, a0}, a6->aid_));
+ REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a0, a1, a2, a3}, a0->aid_));
+ REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a5, a2, a8, a7, a6, a0}, a5->aid_));
+ REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a8, a7, a1}, a8->aid_));
+ }
+
+ SECTION("Example: Disqualified and re-qualified after switching ordering")
+ {
+ // Even though actor `2` executes an independent
+ // transition later on, it is blocked since its first transition
+ // is dependent with actor 1's transition
+ REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{a1, a5, indep}, 2));
+
+ // However, if actor 2 executes its independent action first, it DOES become an initial
+ REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a1, indep, a5}, 2));
+ }
+
+ SECTION("Example: Large partial executions")
+ {
+ // The record trace is `1 3 4 4 3 1 4 2`
+
+ // Actor 1 starts the execution
+ REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a1, a2, a3, a4, a6, a7, a8, indep}, 1));
+
+ // Actor 2 all the way at the end is independent with everybody: despite
+ // the tangle that comes before it, we can more it to the front with no issue
+ REQUIRE(Execution().is_initial_after_execution_of(PartialExecution{a1, a2, a3, a4, a6, a7, a8, indep}, 2));
+
+ // Actor 3 is eliminated since `a1` is dependent with `a2`
+ REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{a1, a2, a3, a4, a6, a7, a8, indep}, 3));
+
+ // Likewise with actor 4
+ REQUIRE_FALSE(Execution().is_initial_after_execution_of(PartialExecution{a1, a2, a3, a4, a6, a7, a8, indep}, 4));
+ }
+
+ SECTION("Example: Stress tests for initials computation")
+ {
+ const auto v_1 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 1, 3);
+ const auto v_2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto v_3 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 2, 3);
+ const auto v_4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto v_5 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 3, 8);
+ const auto v_6 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto v_7 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto v_8 = std::make_shared<DependentIfSameValueAction>(Transition::Type::UNKNOWN, 4, 3);
+ const auto v = PartialExecution{v_1, v_2, v_3, v_4};
+
+ // Actor 1 being the first actor in the expansion, it is clearly an initial
+ REQUIRE(Execution().is_initial_after_execution_of(v, 1));
+
+ // Actor 2 can't be switched before actor 1 without creating an trace
+ // that leads to a different state than that of `E.v := ().v := v`
+ REQUIRE_FALSE(Execution().is_initial_after_execution_of(v, 2));
+
+ // The first action of Actor 3 is independent with what comes before it, so it can
+ // be moved forward. Note that this is the case even though it later executes and action
+ // that's dependent with most everyone else
+ REQUIRE(Execution().is_initial_after_execution_of(v, 3));
+
+ // Actor 4 is blocked actor 3's second action `v_7`
+ REQUIRE_FALSE(Execution().is_initial_after_execution_of(v, 4));
+ }
+}
+
+TEST_CASE("simgrid::mc::odpor::Execution: SDPOR Backtracking Simulation")
+{
+ // This test case assumes that each detected race is detected to also
+ // be reversible. For each reversible
+ const auto e0 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto e3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto e4 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto e5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e6 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto e7 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+
+ Execution execution;
+
+ execution.push_transition(e0);
+ REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
+
+ execution.push_transition(e1);
+ REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
+
+ // Actor 3, since it starts the extension from event 1, clearly is an initial from there
+ execution.push_transition(e2);
+ REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{1});
+ CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{}) == std::unordered_set<aid_t>{3});
+ CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{4, 5}) ==
+ std::unordered_set<aid_t>{3});
+ CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{3}) == std::unordered_set<aid_t>{});
+
+ // e1 and e3 are in an reversible race. Actor 4 is not hindered from being moved to
+ // the front since e2 is independent with e3; hence, it is an initial
+ execution.push_transition(e3);
+ REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{1});
+ CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{}) == std::unordered_set<aid_t>{4});
+ CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{3, 5}) ==
+ std::unordered_set<aid_t>{4});
+ CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{4}) == std::unordered_set<aid_t>{});
+
+ // e4 is not in a race since e3 is run by the same actor and occurs before e4
+ execution.push_transition(e4);
+ REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{});
+
+ // e5 is independent with everything between e1 and e5, and `proc(e5) == 2`
+ execution.push_transition(e5);
+ REQUIRE(execution.get_racing_events_of(5) == std::unordered_set<Execution::EventHandle>{1});
+ CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{}) == std::unordered_set<aid_t>{2});
+ CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{4, 5}) ==
+ std::unordered_set<aid_t>{2});
+ CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{2}) == std::unordered_set<aid_t>{});
+
+ // Event 6 has two races: one with event 4 and one with event 5. In the latter race, actor 3 follows
+ // immediately after and so is evidently a source set actor; in the former race, only actor 2 can
+ // be brought to the front of the queue
+ execution.push_transition(e6);
+ REQUIRE(execution.get_racing_events_of(6) == std::unordered_set<Execution::EventHandle>{4, 5});
+ CHECK(execution.get_missing_source_set_actors_from(4, std::unordered_set<aid_t>{}) == std::unordered_set<aid_t>{2});
+ CHECK(execution.get_missing_source_set_actors_from(4, std::unordered_set<aid_t>{6, 7}) ==
+ std::unordered_set<aid_t>{2});
+ CHECK(execution.get_missing_source_set_actors_from(4, std::unordered_set<aid_t>{2}) == std::unordered_set<aid_t>{});
+ CHECK(execution.get_missing_source_set_actors_from(5, std::unordered_set<aid_t>{}) == std::unordered_set<aid_t>{3});
+ CHECK(execution.get_missing_source_set_actors_from(5, std::unordered_set<aid_t>{6, 7}) ==
+ std::unordered_set<aid_t>{3});
+ CHECK(execution.get_missing_source_set_actors_from(5, std::unordered_set<aid_t>{3}) == std::unordered_set<aid_t>{});
+
+ // Finally, event e7 races with e6 and `proc(e7) = 1` is brought forward
+ execution.push_transition(e7);
+ REQUIRE(execution.get_racing_events_of(7) == std::unordered_set<Execution::EventHandle>{6});
+ CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{}) == std::unordered_set<aid_t>{1});
+ CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{4, 5}) ==
+ std::unordered_set<aid_t>{1});
+ CHECK(execution.get_missing_source_set_actors_from(1, std::unordered_set<aid_t>{1}) == std::unordered_set<aid_t>{});
+}
+
+TEST_CASE("simgrid::mc::odpor::Execution: ODPOR Smallest Sequence Tests")
+{
+ const auto a0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a3 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+
+ Execution execution;
+ execution.push_transition(a0);
+ execution.push_transition(a1);
+ execution.push_transition(a2);
+ execution.push_transition(a3);
+ execution.push_transition(a4);
+ execution.push_transition(a5);
+
+ SECTION("Equivalent insertions")
+ {
+ SECTION("Example: Eliminated through independence")
+ {
+ // TODO: Is this even a sensible question to ask if the two sequences
+ // don't agree upon what each actor executed after `E`?
+ const auto insertion =
+ Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a2}, PartialExecution{a2, a5});
+ REQUIRE(insertion.has_value());
+ REQUIRE(insertion.value() == PartialExecution{});
+ }
+
+ SECTION("Exact match yields empty set")
+ {
+ const auto insertion =
+ Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a2}, PartialExecution{a1, a2});
+ REQUIRE(insertion.has_value());
+ REQUIRE(insertion.value() == PartialExecution{});
+ }
+ }
+
+ SECTION("Match against empty executions")
+ {
+ SECTION("Empty `v` trivially yields `w`")
+ {
+ auto insertion =
+ Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{}, PartialExecution{a1, a5, a2});
+ REQUIRE(insertion.has_value());
+ REQUIRE(insertion.value() == PartialExecution{a1, a5, a2});
+
+ insertion = execution.get_shortest_odpor_sq_subset_insertion(PartialExecution{}, PartialExecution{a1, a5, a2});
+ REQUIRE(insertion.has_value());
+ REQUIRE(insertion.value() == PartialExecution{a1, a5, a2});
+ }
+
+ SECTION("Empty `w` yields empty execution")
+ {
+ auto insertion =
+ Execution().get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a4, a5}, PartialExecution{});
+ REQUIRE(insertion.has_value());
+ REQUIRE(insertion.value() == PartialExecution{});
+
+ insertion = execution.get_shortest_odpor_sq_subset_insertion(PartialExecution{a1, a5, a2}, PartialExecution{});
+ REQUIRE(insertion.has_value());
+ REQUIRE(insertion.value() == PartialExecution{});
+ }
+ }
+}
--- /dev/null
+/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/explo/odpor/ReversibleRaceCalculator.hpp"
+#include "src/mc/explo/odpor/Execution.hpp"
+
+#include <functional>
+#include <unordered_map>
+#include <xbt/asserts.h>
+#include <xbt/ex.h>
+
+namespace simgrid::mc::odpor {
+
+bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution::EventHandle e1,
+ Execution::EventHandle e2)
+{
+ using Action = Transition::Type;
+ using Handler = std::function<bool(const Execution&, Execution::EventHandle, const Transition*)>;
+ using HandlerMap = std::unordered_map<Action, Handler>;
+
+ const static HandlerMap handlers =
+ HandlerMap{{Action::ACTOR_JOIN, &ReversibleRaceCalculator::is_race_reversible_ActorJoin},
+ {Action::BARRIER_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock},
+ {Action::BARRIER_WAIT, &ReversibleRaceCalculator::is_race_reversible_BarrierWait},
+ {Action::COMM_ASYNC_SEND, &ReversibleRaceCalculator::is_race_reversible_CommSend},
+ {Action::COMM_ASYNC_RECV, &ReversibleRaceCalculator::is_race_reversible_CommRecv},
+ {Action::COMM_TEST, &ReversibleRaceCalculator::is_race_reversible_CommTest},
+ {Action::COMM_WAIT, &ReversibleRaceCalculator::is_race_reversible_CommWait},
+ {Action::MUTEX_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock},
+ {Action::MUTEX_TEST, &ReversibleRaceCalculator::is_race_reversible_MutexTest},
+ {Action::MUTEX_TRYLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexTrylock},
+ {Action::MUTEX_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexUnlock},
+ {Action::MUTEX_WAIT, &ReversibleRaceCalculator::is_race_reversible_MutexWait},
+ {Action::OBJECT_ACCESS, &ReversibleRaceCalculator::is_race_reversible_ObjectAccess},
+ {Action::RANDOM, &ReversibleRaceCalculator::is_race_reversible_Random},
+ {Action::SEM_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_SemAsyncLock},
+ {Action::SEM_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_SemUnlock},
+ {Action::SEM_WAIT, &ReversibleRaceCalculator::is_race_reversible_SemWait},
+ {Action::TESTANY, &ReversibleRaceCalculator::is_race_reversible_TestAny},
+ {Action::WAITANY, &ReversibleRaceCalculator::is_race_reversible_WaitAny}};
+
+ const auto e2_action = E.get_transition_for_handle(e2);
+ if (const auto handler = handlers.find(e2_action->type_); handler != handlers.end()) {
+ return handler->second(E, e1, e2_action);
+ } else {
+ xbt_die("There is currently no specialized computation for the transition "
+ "'%s' for computing reversible races in ODPOR, so the model checker cannot "
+ "determine how to proceed. Please submit a bug report requesting "
+ "that the transition be supported in SimGrid using ODPPR and consider "
+ "using the other model-checking algorithms supported by SimGrid instead "
+ "in the meantime",
+ e2_action->to_string().c_str());
+ }
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_ActorJoin(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // ActorJoin races with another event iff its target `T` is the same as
+ // the actor executing the other transition. Clearly, then, we could not join
+ // on that actor `T` and then run a transition by `T`, so no race is reversible
+ return false;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // BarrierAsyncLock is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_BarrierWait(const Execution& E, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // If the other event is a barrier lock event, then we
+ // are not reversible; otherwise we are reversible.
+ const auto e1_action = E.get_transition_for_handle(e1)->type_;
+ return e1_action != Transition::Type::BARRIER_ASYNC_LOCK;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_CommRecv(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // CommRecv is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_CommSend(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // CommSend is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_CommWait(const Execution& E, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // If the other event is a communication event, then we
+ // are not reversible; otherwise we are reversible.
+ const auto e1_action = E.get_transition_for_handle(e1)->type_;
+ return e1_action != Transition::Type::COMM_ASYNC_SEND and e1_action != Transition::Type::COMM_ASYNC_RECV;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_CommTest(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // CommTest is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // MutexAsyncLock is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_MutexTest(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // MutexTest is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_MutexTrylock(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // MutexTrylock is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // MutexUnlock is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // TODO: Get the semantics correct here
+ const auto e1_action = E.get_transition_for_handle(e1)->type_;
+ return e1_action != Transition::Type::MUTEX_ASYNC_LOCK and e1_action != Transition::Type::MUTEX_UNLOCK;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // SemAsyncLock is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // SemUnlock is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // TODO: Get the semantics correct here
+ return false;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // Object access is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_Random(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // Random is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_TestAny(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // TestAny is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_WaitAny(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // TODO: We need to check if any of the transitions
+ // waited on occurred before `e1`
+ return false;
+}
+
+} // namespace simgrid::mc::odpor
\ No newline at end of file
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_ODPOR_REVERSIBLE_RACE_CALCULATOR_HPP
+#define SIMGRID_MC_ODPOR_REVERSIBLE_RACE_CALCULATOR_HPP
+
+#include "src/mc/explo/odpor/Execution.hpp"
+#include "src/mc/explo/odpor/odpor_forward.hpp"
+#include "src/mc/transition/Transition.hpp"
+#include "src/mc/transition/TransitionActorJoin.hpp"
+#include "src/mc/transition/TransitionAny.hpp"
+#include "src/mc/transition/TransitionComm.hpp"
+#include "src/mc/transition/TransitionObjectAccess.hpp"
+#include "src/mc/transition/TransitionRandom.hpp"
+#include "src/mc/transition/TransitionSynchro.hpp"
+
+#include <memory>
+
+namespace simgrid::mc::odpor {
+
+/**
+ * @brief Computes whether a race between two events
+ * in a given execution is a reversible race.
+ *
+ * @note: All of the methods assume that there is
+ * indeed a race between the two events in the
+ * execution; indeed, the question the method answers
+ * is only sensible in the context of a race
+ */
+struct ReversibleRaceCalculator final {
+ static bool is_race_reversible_ActorJoin(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_BarrierAsyncLock(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_BarrierWait(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_CommRecv(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_CommSend(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_CommWait(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_CommTest(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_MutexAsyncLock(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_MutexTest(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_MutexTrylock(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_MutexUnlock(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_MutexWait(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_SemUnlock(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_SemWait(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_Random(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_TestAny(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_WaitAny(const Execution&, Execution::EventHandle e1, const Transition* e2);
+
+public:
+ static bool is_race_reversible(const Execution&, Execution::EventHandle e1, Execution::EventHandle e2);
+};
+
+} // namespace simgrid::mc::odpor
+#endif
--- /dev/null
+/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/explo/odpor/WakeupTree.hpp"
+#include "src/mc/explo/odpor/Execution.hpp"
+#include "xbt/asserts.h"
+#include "xbt/string.hpp"
+
+#include <algorithm>
+#include <exception>
+#include <queue>
+
+namespace simgrid::mc::odpor {
+
+void WakeupTreeNode::add_child(WakeupTreeNode* node)
+{
+ this->children_.push_back(node);
+ node->parent_ = this;
+}
+
+PartialExecution WakeupTreeNode::get_sequence() const
+{
+ // TODO: Prevent having to compute this at the node level
+ // and instead track this with the iterator
+ PartialExecution seq_;
+ const WakeupTreeNode* cur_node = this;
+ while (cur_node != nullptr and !cur_node->is_root()) {
+ seq_.push_front(cur_node->action_);
+ cur_node = cur_node->parent_;
+ }
+ return seq_;
+}
+
+void WakeupTreeNode::detatch_from_parent()
+{
+ if (parent_ != nullptr) {
+ // TODO: There may be a better method
+ // of keeping track of a node's reference to
+ // its parent, perhaps keeping track
+ // of a std::list<>::iterator instead.
+ // This would allow us to detach a node
+ // in O(1) instead of O(|children|) time
+ parent_->children_.remove(this);
+ }
+}
+
+WakeupTree::WakeupTree() : WakeupTree(std::unique_ptr<WakeupTreeNode>(new WakeupTreeNode({}))) {}
+WakeupTree::WakeupTree(std::unique_ptr<WakeupTreeNode> root) : root_(root.get())
+{
+ this->insert_node(std::move(root));
+}
+
+std::vector<std::string> WakeupTree::get_single_process_texts() const
+{
+ std::vector<std::string> trace;
+ for (const auto* child : root_->children_) {
+ const auto t = child->get_action();
+ const auto message = xbt::string_printf("Actor %ld: %s", t->aid_, t->to_string(true).c_str());
+ trace.push_back(std::move(message));
+ }
+ return trace;
+}
+
+std::optional<aid_t> WakeupTree::get_min_single_process_actor() const
+{
+ if (const auto node = get_min_single_process_node(); node.has_value()) {
+ return node.value()->get_actor();
+ }
+ return std::nullopt;
+}
+
+std::optional<WakeupTreeNode*> WakeupTree::get_min_single_process_node() const
+{
+ if (empty()) {
+ return std::nullopt;
+ }
+ // INVARIANT: The induced post-order relation always places children
+ // in order before the parent. The list of children maintained by
+ // each node represents that ordering, and the first child of
+ // the root is by definition the smallest of the single-process nodes
+ xbt_assert(not this->root_->children_.empty(), "What the");
+ return this->root_->children_.front();
+}
+
+WakeupTree WakeupTree::make_subtree_rooted_at(WakeupTreeNode* root)
+{
+ // Perform a BFS search to perform a deep copy of the portion
+ // of the tree underneath and including `root`. Note that `root`
+ // is contained within the context of a *different* wakeup tree;
+ // hence, we have to be careful to update each node's children
+ // appropriately
+ auto subtree = WakeupTree();
+
+ std::list<std::pair<WakeupTreeNode*, WakeupTreeNode*>> frontier{std::make_pair(root, subtree.root_)};
+ while (not frontier.empty()) {
+ auto [node_in_other_tree, subtree_equivalent] = frontier.front();
+ frontier.pop_front();
+
+ // For each child of the node corresponding to that in `subtree`,
+ // make clones of each of its children and add them to `frontier`
+ // to that their children are added, and so on.
+ for (WakeupTreeNode* child_in_other_tree : node_in_other_tree->get_ordered_children()) {
+ WakeupTreeNode* child_equivalent = subtree.make_node(child_in_other_tree->get_action());
+ subtree_equivalent->add_child(child_equivalent);
+ frontier.push_back(std::make_pair(child_in_other_tree, child_equivalent));
+ }
+ }
+ return subtree;
+}
+
+void WakeupTree::remove_subtree_rooted_at(WakeupTreeNode* root)
+{
+ if (not contains(root)) {
+ throw std::invalid_argument("Attempting to remove a subtree pivoted from a node "
+ "that is not contained in this wakeup tree");
+ }
+
+ std::list<WakeupTreeNode*> subtree_contents{root};
+ std::list<WakeupTreeNode*> frontier{root};
+ while (not frontier.empty()) {
+ auto node = frontier.front();
+ frontier.pop_front();
+ for (const auto& child : node->get_ordered_children()) {
+ frontier.push_back(child);
+ subtree_contents.push_back(child);
+ }
+ }
+
+ // After having found each node with BFS, now we can
+ // remove them. This prevents the "joys" of iteration during mutation.
+ // We also remove the `root` from being referenced by its own parent (since
+ // it will soon be destroyed)
+ root->detatch_from_parent();
+ for (WakeupTreeNode* node_to_remove : subtree_contents) {
+ this->remove_node(node_to_remove);
+ }
+}
+
+void WakeupTree::remove_min_single_process_subtree()
+{
+ if (const auto node = get_min_single_process_node(); node.has_value()) {
+ remove_subtree_rooted_at(node.value());
+ }
+}
+
+bool WakeupTree::contains(WakeupTreeNode* node) const
+{
+ return std::find_if(this->nodes_.begin(), this->nodes_.end(), [=](const auto& pair) { return pair.first == node; }) !=
+ this->nodes_.end();
+}
+
+WakeupTreeNode* WakeupTree::make_node(std::shared_ptr<Transition> u)
+{
+ auto node = std::unique_ptr<WakeupTreeNode>(new WakeupTreeNode(std::move(u)));
+ auto* node_handle = node.get();
+ this->nodes_[node_handle] = std::move(node);
+ return node_handle;
+}
+
+void WakeupTree::insert_node(std::unique_ptr<WakeupTreeNode> node)
+{
+ auto* node_handle = node.get();
+ this->nodes_[node_handle] = std::move(node);
+}
+
+void WakeupTree::remove_node(WakeupTreeNode* node)
+{
+ this->nodes_.erase(node);
+}
+
+WakeupTree::InsertionResult WakeupTree::insert(const Execution& E, const PartialExecution& w)
+{
+ // See section 6.2 of Abdulla. et al.'s 2017 ODPOR paper for details
+
+ // Find the first node `v` in the tree such that
+ // `v ~_[E] w` and `v` is not a leaf node
+ for (WakeupTreeNode* node : *this) {
+ if (const auto shortest_sequence = E.get_shortest_odpor_sq_subset_insertion(node->get_sequence(), w);
+ shortest_sequence.has_value()) {
+ // Insert the sequence as a child of `node`, but only
+ // if the node is not already a leaf
+ if (not node->is_leaf() or node == this->root_) {
+ // NOTE: It's entirely possible that the shortest
+ // sequence we are inserting is empty. Consider the
+ // following two cases:
+ //
+ // 1. `w` is itself empty. Evidently, insertion succeeds but nothing needs
+ // to happen
+ //
+ // 2. a leaf node in the tree already contains `w` exactly.
+ // In this case, the empty `w'` returned (viz. `shortest_seq`)
+ // such that `w [=_[E] v.w'` would be empty
+ this->insert_sequence_after(node, shortest_sequence.value());
+ return node == this->root_ ? InsertionResult::root : InsertionResult::interior_node;
+ }
+ // Since we're following the post-order traversal of the tree,
+ // the first such node we see is the smallest w.r.t "<"
+ return InsertionResult::leaf;
+ }
+ }
+ xbt_die("Insertion should always succeed with the root node (which contains no "
+ "prior execution). If we've reached this point, this implies either that "
+ "the wakeup tree traversal is broken or that computation of the shortest "
+ "sequence to insert into the tree is broken");
+}
+
+void WakeupTree::insert_sequence_after(WakeupTreeNode* node, const PartialExecution& w)
+{
+ WakeupTreeNode* cur_node = node;
+ for (const auto& w_i : w) {
+ WakeupTreeNode* new_node = this->make_node(w_i);
+ cur_node->add_child(new_node);
+ cur_node = new_node;
+ }
+}
+
+} // namespace simgrid::mc::odpor
\ No newline at end of file
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_ODPOR_WAKEUP_TREE_HPP
+#define SIMGRID_MC_ODPOR_WAKEUP_TREE_HPP
+
+#include "src/mc/explo/odpor/WakeupTreeIterator.hpp"
+#include "src/mc/explo/odpor/odpor_forward.hpp"
+#include "src/mc/transition/Transition.hpp"
+
+#include <memory>
+#include <optional>
+#include <string>
+#include <unordered_map>
+#include <vector>
+
+namespace simgrid::mc::odpor {
+
+/**
+ * @brief A single node in a wakeup tree
+ *
+ * Each node in a wakeup tree contains
+ */
+class WakeupTreeNode {
+private:
+ explicit WakeupTreeNode(std::shared_ptr<Transition> u) : action_(u) {}
+
+ WakeupTreeNode* parent_ = nullptr;
+
+ /** An ordered list of children of for this node in the tree */
+ std::list<WakeupTreeNode*> children_;
+
+ /** @brief The contents of the node */
+ std::shared_ptr<Transition> action_;
+
+ /** @brief Removes the node as a child from the parent */
+ void detatch_from_parent();
+
+ /** Allows the owning tree to insert directly into the child */
+ friend WakeupTree;
+ friend WakeupTreeIterator;
+
+public:
+ ~WakeupTreeNode() = default;
+ WakeupTreeNode(const WakeupTreeNode&) = delete;
+ WakeupTreeNode(WakeupTreeNode&&) = default;
+ WakeupTreeNode& operator=(const WakeupTreeNode&) = delete;
+ WakeupTreeNode& operator=(WakeupTreeNode&&) = default;
+
+ auto begin() const { return this->children_.begin(); }
+ auto end() const { return this->children_.end(); }
+ auto rbegin() const { return this->children_.rbegin(); }
+ auto rend() const { return this->children_.rend(); }
+
+ bool is_leaf() const { return children_.empty(); }
+ bool is_root() const { return parent_ == nullptr; }
+ aid_t get_actor() const { return action_->aid_; }
+ PartialExecution get_sequence() const;
+ std::shared_ptr<Transition> get_action() const { return action_; }
+ const std::list<WakeupTreeNode*>& get_ordered_children() const { return children_; }
+
+ /** Insert a node `node` as a new child of this node */
+ void add_child(WakeupTreeNode* node);
+};
+
+/**
+ * @brief The structure used by ODPOR to maintains paths of execution
+ * that should be followed in the future
+ *
+ * The wakeup tree data structure is formally defined in the Abdulla et al.
+ * 2017 ODPOR paper. Conceptually, the tree consists of nodes which are
+ * mapped to actions. Each node represents a partial extension of an execution,
+ * the complete extension being the transitions taken in sequence from
+ * the root of the tree to the node itself. Leaf nodes in the tree conceptually,
+ * then, represent paths that are guaranteed to explore different parts
+ * of the search space.
+ *
+ * Iteration over a wakeup tree occurs as a post-order traversal of its nodes
+ *
+ * @note A wakeup tree is defined relative to some execution `E`. The
+ * structure itself does not hold onto a reference of the execution with
+ * respect to which it is a wakeup tree.
+ *
+ * @todo: If the idea of execution "views" is ever added -- viz. being able
+ * to share the contents of a single execution -- then a wakeup tree could
+ * contain a reference to such a view which would then be maintained by the
+ * manipulator of the tree
+ */
+class WakeupTree {
+private:
+ WakeupTreeNode* root_;
+
+ /**
+ * @brief All of the nodes that are currently are a part of the tree
+ *
+ * @invariant Each node event maps itself to the owner of that node,
+ * i.e. the unique pointer that manages the data at the address. The tree owns all
+ * of the addresses that are referenced by the nodes WakeupTreeNode.
+ * ODPOR guarantees that nodes are persisted as long as needed.
+ */
+ std::unordered_map<WakeupTreeNode*, std::unique_ptr<WakeupTreeNode>> nodes_;
+
+ void insert_node(std::unique_ptr<WakeupTreeNode> node);
+ void insert_sequence_after(WakeupTreeNode* node, const PartialExecution& w);
+ void remove_node(WakeupTreeNode* node);
+ bool contains(WakeupTreeNode* node) const;
+
+ /**
+ * @brief Removes the node `root` and all of its descendants from
+ * this wakeup tree
+ *
+ * @throws: If the node `root` is not contained in this tree, an
+ * exception is raised
+ */
+ void remove_subtree_rooted_at(WakeupTreeNode* root);
+
+ /**
+ * @brief Adds a new node to the tree, disconnected from
+ * any other, which represents the partial execution
+ * "fragment" `u`
+ */
+ WakeupTreeNode* make_node(std::shared_ptr<Transition> u);
+
+ /* Allow the iterator to access the contents of the tree */
+ friend WakeupTreeIterator;
+
+public:
+ WakeupTree();
+ explicit WakeupTree(std::unique_ptr<WakeupTreeNode> root);
+
+ /**
+ * @brief Creates a copy of the subtree whose root is the node
+ * `root` in this tree
+ */
+ static WakeupTree make_subtree_rooted_at(WakeupTreeNode* root);
+
+ auto begin() const { return WakeupTreeIterator(*this); }
+ auto end() const { return WakeupTreeIterator(); }
+
+ std::vector<std::string> get_single_process_texts() const;
+
+ /**
+ * @brief Remove the subtree of the smallest (with respect
+ * to the tree's "<" relation) single-process node.
+ *
+ * A "single-process" node is one whose execution represents
+ * taking a single action (i.e. those of the root node). The
+ * smallest under "<" is that which is continuously selected and
+ * removed by ODPOR.
+ *
+ * If the tree is empty, this method has no effect.
+ */
+ void remove_min_single_process_subtree();
+
+ /**
+ * @brief Whether or not this tree is considered empty
+ *
+ * @note Unlike other collection types, a wakeup tree is
+ * considered "empty" if it only contains the root node;
+ * that is, if it is "uninteresting". In such a case,
+ */
+ bool empty() const { return nodes_.size() == static_cast<size_t>(1); }
+
+ /**
+ * @brief Returns the number of *non-empty* entries in the tree, viz. the
+ * number of nodes in the tree that have an action mapped to them
+ */
+ size_t get_num_entries() const { return !empty() ? (nodes_.size() - 1) : static_cast<size_t>(0); }
+
+ /**
+ * @brief Returns the number of nodes in the tree, including the root node
+ */
+ size_t get_num_nodes() const { return nodes_.size(); }
+
+ /**
+ * @brief Gets the actor of the node that is the "smallest" (with respect
+ * to the tree's "<" relation) single-process node.
+ *
+ * If the tree is empty, returns std::nullopt
+ */
+ std::optional<aid_t> get_min_single_process_actor() const;
+
+ /**
+ * @brief Gets the node itself that is the "smallest" (with respect
+ * to the tree's "<" relation) single-process node.
+ *
+ * If the tree is empty, returns std::nullopt
+ */
+ std::optional<WakeupTreeNode*> get_min_single_process_node() const;
+
+ /** @brief Describes how a tree insertion was carried out */
+ enum class InsertionResult { leaf, interior_node, root };
+
+ /**
+ * @brief Inserts an sequence `seq` of processes into the tree
+ * such that that this tree is a wakeup tree relative to the
+ * given execution
+ *
+ * A key component of managing wakeup trees in ODPOR is
+ * determining what should be inserted into a wakeup tree.
+ * The procedure for implementing the insertion is outlined in section 6.2
+ * of Abdulla et al. 2017 as follows:
+ *
+ * | Let `v` be the smallest (w.r.t to "<") sequence in [the tree] B
+ * | such that `v ~_[E] w`. If `v` is a leaf node, the tree can be left
+ * | unmodified.
+ * |
+ * | Otherwise let `w'` be the shortest sequence such that `w [=_[E] v.w'`
+ * | and add `v.w'` as a new leaf, ordered after all already existing nodes
+ * | of the form `v.w''`
+ *
+ * This method performs the post-order search of part one and the insertion of
+ * `v.w'` of part two of the above procedure. Note that the execution will
+ * provide `v.w'` (see `Execution::get_shortest_odpor_sq_subset_insertion()`).
+ *
+ * @invariant: It is assumed that this tree is a wakeup tree
+ * with respect to the given execution `E`
+ *
+ * @return Whether a sequence equivalent to `seq` is already contained
+ * as a leaf node in the tree
+ */
+ InsertionResult insert(const Execution& E, const PartialExecution& seq);
+};
+
+} // namespace simgrid::mc::odpor
+#endif
--- /dev/null
+/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/explo/odpor/WakeupTreeIterator.hpp"
+#include "src/mc/explo/odpor/WakeupTree.hpp"
+
+namespace simgrid::mc::odpor {
+
+WakeupTreeIterator::WakeupTreeIterator(const WakeupTree& tree) : root_list{tree.root_}
+{
+ post_order_iteration.push(root_list.begin());
+ push_until_left_most_found();
+}
+
+void WakeupTreeIterator::push_until_left_most_found()
+{
+ // INVARIANT: Since we are traversing over a tree,
+ // there are no cycles. This means that at least
+ // one node in the tree won't have any children,
+ // so the loop will eventually terminate
+ auto* cur_top_node = *post_order_iteration.top();
+ while (not cur_top_node->is_leaf()) {
+ // INVARIANT: Since we push children in
+ // reverse order (right-most to left-most),
+ // we ensure that we'll always process left-most
+ // children first
+ auto& children = cur_top_node->children_;
+
+ for (auto iter = children.rbegin(); iter != children.rend(); ++iter) {
+ // iter.base() points one element past where we seek; hence,
+ // we move it over one position
+ post_order_iteration.push(std::prev(iter.base()));
+ }
+ cur_top_node = *post_order_iteration.top();
+ }
+}
+
+void WakeupTreeIterator::increment()
+{
+ // If there are no nodes in the stack, we've
+ // completed the traversal: there's nothing left
+ // to do
+ if (post_order_iteration.empty()) {
+ return;
+ }
+
+ auto prev_top_handle = post_order_iteration.top();
+ post_order_iteration.pop();
+
+ // If there are now no longer any nodes left,
+ // we know that `prev_top` must be the original
+ // root; that is, we were *just* pointing at the
+ // original root, so we're done
+ if (post_order_iteration.empty()) {
+ return;
+ }
+
+ // Otherwise, look at the next top node. If
+ // `prev_top` is that node's right-most child,
+ // then we don't attempt to re-add `next_top`'s
+ // children again for we would have already seen them.
+ // To actually determine "right-most", we check if
+ // moving over to the right one spot brings us to the
+ // end of the candidate parent's list
+ const auto* next_top_node = *post_order_iteration.top();
+ if ((++prev_top_handle) != next_top_node->get_ordered_children().end()) {
+ push_until_left_most_found();
+ }
+}
+
+} // namespace simgrid::mc::odpor
\ No newline at end of file
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef SIMGRID_MC_ODPOR_WAKEUP_TREE_ITERATOR_HPP
+#define SIMGRID_MC_ODPOR_WAKEUP_TREE_ITERATOR_HPP
+
+#include "src/mc/explo/odpor/odpor_forward.hpp"
+
+#include <boost/iterator/iterator_facade.hpp>
+#include <list>
+#include <stack>
+
+namespace simgrid::mc::odpor {
+
+/**
+ * @brief A forward-iterator that performs a postorder traversal
+ * of the nodes of a WakeupTree
+ *
+ * Inserting a sequence `w` into a wakeup tree `B` with respect to
+ * some execution `E` requires determining the "<-minimal" node `N`
+ * with sequence `v` in the tree such that `v ~_[E] w`. The "<" relation
+ * over a wakeup tree orders its nodes by first recursively ordering all
+ * children of a node `N` followed by the node `N` itself, viz. a postorder.
+ * This iterator provides such a postorder traversal over the nodes in the
+ * wakeup tree.
+ */
+struct WakeupTreeIterator
+ : public boost::iterator_facade<WakeupTreeIterator, WakeupTreeNode*, boost::forward_traversal_tag> {
+public:
+ WakeupTreeIterator() = default;
+ explicit WakeupTreeIterator(const WakeupTree& tree);
+
+private:
+ using node_handle = std::list<WakeupTreeNode*>::iterator;
+
+ /**
+ * @brief A list which is used to "store" the root node of the traversed
+ * wakeup tree
+ *
+ * The root node is, by definition, not the child of any other node. This
+ * means that the root node also is contained in any list into which the
+ * iterator can generate a pointer (iterator). This list takes the role
+ * of allowing the iterator to treat the root node like any other.
+ */
+ std::list<WakeupTreeNode*> root_list;
+
+ /**
+ * @brief The current "view" of the iteration in post-order traversal
+ */
+ std::stack<node_handle> post_order_iteration;
+
+ /**
+ * @brief Search the wakeup tree until a leaf node appears at the front
+ * of the iteration, pushing all children towards the top of the stack
+ * as the search progresses
+ */
+ void push_until_left_most_found();
+
+ // boost::iterator_facade<...> interface to implement
+ void increment();
+ bool equal(const WakeupTreeIterator& other) const { return post_order_iteration == other.post_order_iteration; }
+ WakeupTreeNode*& dereference() const { return *post_order_iteration.top(); }
+
+ // Allows boost::iterator_facade<...> to function properly
+ friend class boost::iterator_core_access;
+};
+
+} // namespace simgrid::mc::odpor
+#endif
--- /dev/null
+/* Copyright (c) 2017-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/3rd-party/catch.hpp"
+#include "src/mc/explo/odpor/Execution.hpp"
+#include "src/mc/explo/odpor/WakeupTree.hpp"
+#include "src/mc/explo/udpor/udpor_tests_private.hpp"
+#include "src/xbt/utils/iter/LazyPowerset.hpp"
+
+using namespace simgrid::mc;
+using namespace simgrid::mc::odpor;
+using namespace simgrid::mc::udpor;
+
+static void test_tree_iterator(const WakeupTree& tree, const std::vector<PartialExecution>& expected)
+{
+ uint64_t num_nodes_traversed = 0;
+ auto tree_iter = tree.begin();
+ for (auto expected_iter = expected.begin(); expected_iter != expected.end();
+ ++expected_iter, ++tree_iter, ++num_nodes_traversed) {
+ REQUIRE(tree_iter != tree.end());
+ REQUIRE((*tree_iter)->get_sequence() == *expected_iter);
+ }
+ REQUIRE(num_nodes_traversed == tree.get_num_nodes());
+}
+
+static void test_tree_empty(const WakeupTree& tree)
+{
+ REQUIRE(tree.empty());
+ REQUIRE(tree.get_num_entries() == 0);
+ REQUIRE(tree.get_num_nodes() == 1);
+ REQUIRE_FALSE(tree.get_min_single_process_node().has_value());
+ REQUIRE_FALSE(tree.get_min_single_process_actor().has_value());
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{}});
+}
+
+TEST_CASE("simgrid::mc::odpor::WakeupTree: Constructing Trees")
+{
+ SECTION("Constructing empty trees")
+ {
+ test_tree_empty(WakeupTree());
+ }
+
+ SECTION("Testing subtree creation and manipulation")
+ {
+ // Here, we make everything dependent. This will ensure that each unique sequence
+ // inserted into the tree never "eventually looks like"
+ const auto a0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a3 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 5);
+ const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 6);
+
+ Execution execution;
+ execution.push_transition(a0);
+ execution.push_transition(a1);
+ execution.push_transition(a2);
+ execution.push_transition(a3);
+ execution.push_transition(a4);
+ execution.push_transition(a5);
+
+ // The tree is as follows:
+ // {}
+ // / /
+ // a1 a4
+ // / / /
+ // a2 a3 a1
+ // / / / /
+ // a3 a2 a5 a2
+ // / / /
+ // a4 a4 a3
+ //
+ // Recall that new nodes (in this case the one with
+ // action `a2`) are added such that they are "greater than" (under
+ // the tree's `<` relation) all those that exist under the given parent
+ WakeupTree tree;
+ tree.insert(Execution(), {a1, a2, a3, a4});
+ tree.insert(Execution(), {a1, a3, a2, a4});
+ tree.insert(Execution(), {a1, a3, a2, a4, a5});
+ tree.insert(Execution(), {a1, a3, a5});
+ tree.insert(Execution(), {a4, a2, a1, a3});
+ REQUIRE(tree.get_num_nodes() == 13);
+ test_tree_iterator(tree, std::vector<PartialExecution>{
+ PartialExecution{a1, a2, a3, a4}, PartialExecution{a1, a2, a3},
+ PartialExecution{a1, a2}, PartialExecution{a1, a3, a2, a4},
+ PartialExecution{a1, a3, a2}, PartialExecution{a1, a3, a5}, PartialExecution{a1, a3},
+ PartialExecution{a1}, PartialExecution{a4, a2, a1, a3}, PartialExecution{a4, a2, a1},
+ PartialExecution{a4, a2}, PartialExecution{a4}, PartialExecution{}});
+
+ SECTION("Cloning a tree from the root produces the same tree")
+ {
+ // The root node is the last node
+ auto tree_root = tree.begin();
+ std::advance(tree_root, tree.get_num_nodes() - 1);
+
+ WakeupTree clone = WakeupTree::make_subtree_rooted_at(*tree_root);
+ REQUIRE(clone.empty() == tree.empty());
+ REQUIRE(clone.get_num_entries() == tree.get_num_entries());
+ REQUIRE(clone.get_num_nodes() == tree.get_num_nodes());
+
+ auto tree_iter = tree.begin();
+ for (auto clone_iter = clone.begin(); clone_iter != clone.end(); ++clone_iter, ++tree_iter) {
+ REQUIRE(tree_iter != tree.end());
+ REQUIRE((*tree_iter)->get_sequence() == (*clone_iter)->get_sequence());
+ }
+ }
+
+ SECTION("Cloning a subtree from a leaf gives an empty tree")
+ {
+ // Let's pick the first leaf
+ WakeupTree clone = WakeupTree::make_subtree_rooted_at(*tree.begin());
+ REQUIRE(clone.empty());
+ REQUIRE(clone.get_num_entries() == 0);
+ REQUIRE(clone.get_num_nodes() == 1);
+ }
+
+ SECTION("Cloning a subtree from an interior node gives the subtree underneath")
+ {
+ // Here, we pick the second-to-last node in the
+ // series, which is the right-most child of the root
+ auto right_most = tree.begin();
+ std::advance(right_most, tree.get_num_nodes() - 2);
+
+ WakeupTree clone = WakeupTree::make_subtree_rooted_at(*right_most);
+ REQUIRE_FALSE(clone.empty());
+ REQUIRE(clone.get_num_entries() == 3);
+ REQUIRE(clone.get_num_nodes() == 4);
+ // Importantly, note that action `a4` is not included in
+ // any of the executions; for in the subtree `clone` `a4`
+ // is now the root.
+ test_tree_iterator(clone, std::vector<PartialExecution>{PartialExecution{a2, a1, a3}, PartialExecution{a2, a1},
+ PartialExecution{a2}, PartialExecution{}});
+ }
+
+ SECTION("Removing the first single-process subtree")
+ {
+ // Prior to removal, the first `a1` was the first single-process node
+ REQUIRE(tree.get_min_single_process_node().has_value());
+ REQUIRE(tree.get_min_single_process_actor().has_value());
+ REQUIRE(tree.get_min_single_process_actor().value() == a1->aid_);
+
+ tree.remove_min_single_process_subtree();
+
+ // Now the first `a4` is
+ REQUIRE(tree.get_min_single_process_node().has_value());
+ REQUIRE(tree.get_min_single_process_actor().has_value());
+ REQUIRE(tree.get_min_single_process_actor().value() == a4->aid_);
+
+ REQUIRE(tree.get_num_nodes() == 5);
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a4, a2, a1, a3},
+ PartialExecution{a4, a2, a1}, PartialExecution{a4, a2},
+ PartialExecution{a4}, PartialExecution{}});
+ tree.remove_min_single_process_subtree();
+
+ // At this point, we've removed each single-process subtree, so
+ // the tree should be empty
+ REQUIRE(tree.empty());
+ }
+
+ SECTION("Removing the first single-process subtree from an empty tree has no effect")
+ {
+ WakeupTree empty_tree;
+ test_tree_empty(empty_tree);
+
+ empty_tree.remove_min_single_process_subtree();
+
+ // There should be no effect: the tree should still be empty
+ // and the function should have no effect
+ test_tree_empty(empty_tree);
+ }
+ }
+}
+
+TEST_CASE("simgrid::mc::odpor::WakeupTree: Testing Insertion for Empty Executions")
+{
+ SECTION("Following an execution")
+ {
+ // We imagine the following completed execution `E`
+ // consisting of executing actions a0-a3. Execution
+ // `E` is the first such maximal execution explored
+ // by ODPOR, which implies that a) all sleep sets are
+ // empty and b) all wakeup trees (i.e. for each prefix) consist of the root
+ // node with a single leaf containing the action
+ // taken, save for the wakeup tree of the execution itself
+ // which is empty.
+
+ // We first notice that there's a reversible race between
+ // events 0 and 3.
+
+ const auto a0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+
+ Execution execution;
+ execution.push_transition(a0);
+ execution.push_transition(a1);
+ execution.push_transition(a2);
+ execution.push_transition(a3);
+ execution.push_transition(a4);
+
+ REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{0});
+ REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{0});
+
+ WakeupTree tree;
+
+ SECTION("Attempting to insert the empty sequence into an empty tree should have no effect")
+ {
+ tree.insert(Execution(), {});
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{}});
+ }
+
+ // First, we initialize the tree to how it looked prior
+ // to the insertion of the race.
+ tree.insert(Execution(), {a0});
+
+ // Then, after insertion, we ensure that the node was
+ // indeed added to the tree.
+ tree.insert(Execution(), {a1, a3});
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a1, a3},
+ PartialExecution{a1}, PartialExecution{}});
+
+ SECTION("Attempting to re-insert the same EXACT sequence should have no effect")
+ {
+ tree.insert(Execution(), {a1, a3});
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a1, a3},
+ PartialExecution{a1}, PartialExecution{}});
+ }
+
+ SECTION("Attempting to re-insert an equivalent sequence should have no effect")
+ {
+ // a3 and a1 are interchangeable since `a1` is independent with everything.
+ // Since we found an equivalent sequence that is a leaf, nothing should result..
+ tree.insert(Execution(), {a3, a1});
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a1, a3},
+ PartialExecution{a1}, PartialExecution{}});
+ }
+
+ SECTION("Attempting to insert the empty sequence should have no effect")
+ {
+ tree.insert(Execution(), {});
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a1, a3},
+ PartialExecution{a1}, PartialExecution{}});
+ }
+
+ SECTION("Inserting an extension should create a branch point")
+ {
+ // `a1.a2` shares the same `a1` prefix as `a1.a3`. Thus, the tree
+ // should now look as follows:
+ //
+ // {}
+ // / /
+ // a0 a1
+ // / /
+ // a3 a4
+ //
+ // Recall that new nodes (in this case the one with
+ // action `a2`) are added such that they are "greater than" (under
+ // the tree's `<` relation) all those that exist under the given parent.
+ tree.insert(Execution(), {a1, a4});
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a1, a3},
+ PartialExecution{a1, a4}, PartialExecution{a1},
+ PartialExecution{}});
+ }
+
+ SECTION("Inserting an equivalent sequence to a leaf should preserve the tree as-is")
+ {
+ // `a1.a2` is equivalent to `a1.a3` since `a2` and `a3` are independent
+ // (`E ⊢ p ◊ w` where `p := proc(a2)` and `w := a3`). Thus, the tree
+ // should now STILL look as follows:
+ //
+ // {}
+ // / /
+ // a0 a1
+ // /
+ // a3
+ //
+ // Recall that new nodes (in this case the one with
+ // action `a2`) are added such that they are "greater than" (under
+ // the tree's `<` relation) all those that exist under the given parent.
+ tree.insert(Execution(), {a1, a3});
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a1, a3},
+ PartialExecution{a1}, PartialExecution{}});
+ }
+ }
+
+ SECTION("Performing Arbitrary Insertions")
+ {
+ const auto a0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a3 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a5 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+ WakeupTree tree;
+
+ SECTION("Attempting to insert the empty sequence into an empty tree should have no effect")
+ {
+ tree.insert(Execution(), {});
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{}});
+ }
+
+ SECTION("Attempting to re-insert the same sequence multiple times should have no extra effect")
+ {
+ tree.insert(Execution(), {a4});
+ tree.insert(Execution(), {a4});
+ tree.insert(Execution(), {a4});
+ REQUIRE(tree.get_num_nodes() == 2);
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a4}, PartialExecution{}});
+ }
+
+ SECTION("Attempting to insert an independent sequence same should have no extra effect")
+ {
+ // a4 and a1 are independent actions. Intuitively, then, we need only
+ // search one ordering of the two actions. The wakeup tree handles
+ // this by computing the `~` relation. The relation itself determines
+ // whether the `a1` is an initial of `a3`, which it is not. It then
+ // checks whether `a1` is independent with everything in the sequence
+ // (in this case, consisting only of `a1`) which IS true. Since `a4`
+ // is already a leaf node of the tree, it suffices to only have `a4`
+ // in this tree to guide ODPOR.
+ tree.insert(Execution(), {a4});
+ tree.insert(Execution(), {a1});
+ REQUIRE(tree.get_num_nodes() == 2);
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a4}, PartialExecution{}});
+ }
+
+ SECTION(
+ "Attempting to insert a progression of executions should have no extra effect when the first process is a leaf")
+ {
+ // All progressions starting with `a0` are effectively already accounted
+ // for by inserting `a0` since we `a0` "can always be made to look like"
+ // (viz. the `~` relation) `a0.*` where `*` is some sequence of actions
+ tree.insert(Execution(), {a0});
+ tree.insert(Execution(), {a0, a3});
+ tree.insert(Execution(), {a0, a3, a2});
+ tree.insert(Execution(), {a0, a3, a2, a4});
+ tree.insert(Execution(), {a0, a3, a2, a4});
+ REQUIRE(tree.get_num_nodes() == 2);
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{}});
+ }
+
+ SECTION("Stress test with multiple branch points: `~_E` with different looking sequences")
+ {
+ // After the insertions below, the tree looks like the following:
+ // {}
+ // / /
+ // a0 a2
+ // / | /
+ // a0 a3 a5
+ tree.insert(Execution(), {a0});
+ tree.insert(Execution(), {a2, a0});
+ tree.insert(Execution(), {a2, a3});
+ tree.insert(Execution(), {a2, a5});
+ REQUIRE(tree.get_num_nodes() == 6);
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a2, a0},
+ PartialExecution{a2, a3}, PartialExecution{a2, a5},
+ PartialExecution{a2}, PartialExecution{}});
+ SECTION("Adding more stress")
+ {
+ // In this case, `a2` and `a1` can be interchanged with each other.
+ // Thus `a2.a1 == a1.a2`. Since there is already an interior node
+ // containing `a2`, we attempt to add the what remains (viz. `a1`) to the
+ // series. HOWEVER: we notice that `a2.a5` is "eventually equivalent to"
+ // (that is `~` with) `a1.a2` since `a2` is an initial of the latter and
+ // `a1` and `a5` are independent of each other.
+ tree.insert(Execution(), {a1, a2});
+ REQUIRE(tree.get_num_nodes() == 6);
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a2, a0},
+ PartialExecution{a2, a3}, PartialExecution{a2, a5},
+ PartialExecution{a2}, PartialExecution{}});
+
+ // With a3.a0, we notice that starting a sequence with `a3` is
+ // always different than starting one with either `a0` or
+ //
+ // After the insertion, the tree looks like the following:
+ // {}
+ // / / /
+ // a0 a2 a3
+ // / | / |
+ // a0 a3 a5 a0
+ tree.insert(Execution(), {a3, a0});
+ REQUIRE(tree.get_num_nodes() == 8);
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a2, a0},
+ PartialExecution{a2, a3}, PartialExecution{a2, a5},
+ PartialExecution{a2}, PartialExecution{a3, a0},
+ PartialExecution{a3}, PartialExecution{}});
+ }
+ }
+ }
+
+ SECTION("Insertion with more subtle equivalents")
+ {
+ const auto cd_1 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto i_2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto i_3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto d_1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto d_2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+ WakeupTree complex_tree;
+ // After the insertions below, the tree looks like the following:
+ // {}
+ // / /
+ // cd_1 i_2
+ // / /
+ // i_2 d_2
+ // / /
+ // d_1 cd_1
+ // / / /
+ // i_3 d_1 i_3
+ // / / /
+ // d_2 i_3 d_2
+ // / / /
+ // d_2 d_2 d_1
+ //
+ // d_1.i_3.d_2 is equivalent to i_3.d_2.d_1
+ complex_tree.insert(Execution(), {cd_1, i_2, d_1, i_3, d_2, d_2});
+ complex_tree.insert(Execution(), {i_2, d_2, cd_1, d_1, i_3, d_2});
+ complex_tree.insert(Execution(), {i_2, d_2, cd_1, i_3, d_2, d_1});
+ REQUIRE(complex_tree.get_num_nodes() == 16);
+ test_tree_iterator(complex_tree, std::vector<PartialExecution>{{cd_1, i_2, d_1, i_3, d_2, d_2},
+ {cd_1, i_2, d_1, i_3, d_2},
+ {cd_1, i_2, d_1, i_3},
+ {cd_1, i_2, d_1},
+ {cd_1, i_2},
+ {cd_1},
+ {i_2, d_2, cd_1, d_1, i_3, d_2},
+ {i_2, d_2, cd_1, d_1, i_3},
+ {i_2, d_2, cd_1, d_1},
+ {i_2, d_2, cd_1, i_3, d_2, d_1},
+ {i_2, d_2, cd_1, i_3, d_2},
+ {i_2, d_2, cd_1, i_3},
+ {i_2, d_2, cd_1},
+ {i_2, d_2},
+ {i_2},
+ {}});
+ // Here we note that the sequence that we are attempting to insert, viz.
+ //
+ // i_3.i_2.d_2.cd_1.d_2.d_1
+ //
+ // is already equivalent to
+ //
+ // i_2.d_2.cd_1.i_3.d_2.d_1
+ complex_tree.insert(Execution(), {i_3, i_2, d_2, cd_1, d_2, d_1});
+ REQUIRE(complex_tree.get_num_nodes() == 16);
+
+ // Here we note that the sequence that we are attempting to insert, viz.
+ //
+ // i_2.d_2.cd_1.d_1.i_3
+ //
+ // is already equivalent to
+ //
+ // i_2.d_2.cd_1.i_3.d_2.d_1
+ complex_tree.insert(Execution(), {i_2, d_2, cd_1, d_1, i_3});
+ REQUIRE(complex_tree.get_num_nodes() == 16);
+
+ // Here we note that the sequence that we are attempting to insert, viz.
+ //
+ // i_2.d_2.cd_1
+ //
+ // is accounted for by an interior node of the tree. Since there is no
+ // "extra" portions that are different from what is already
+ // contained in the tree, nothing is added and the tree stays the same
+ complex_tree.insert(Execution(), {i_2, d_2, cd_1});
+ REQUIRE(complex_tree.get_num_nodes() == 16);
+ }
+}
\ No newline at end of file
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+/** @file odpor_forward.hpp
+ *
+ * Forward definitions for MC types specific to ODPOR
+ */
+
+#ifndef SIMGRID_MC_ODPOR_FORWARD_HPP
+#define SIMGRID_MC_ODPOR_FORWARD_HPP
+
+#include "src/mc/mc_forward.hpp"
+#include <list>
+#include <memory>
+#include <simgrid/forward.h>
+
+namespace simgrid::mc::odpor {
+
+using PartialExecution = std::list<std::shared_ptr<Transition>>;
+
+class Event;
+class Execution;
+class ReversibleRaceCalculator;
+class WakeupTree;
+class WakeupTreeNode;
+class WakeupTreeIterator;
+
+} // namespace simgrid::mc::odpor
+
+namespace simgrid::mc {
+
+// Permit ODPOR or SDPOR to be used as namespaces
+// Many of the structures overlap, so it doesn't
+// make sense to some in one and not the other.
+// Having one for each algorithm makes the corresponding
+// code easier to read
+namespace sdpor = simgrid::mc::odpor;
+
+} // namespace simgrid::mc
+
+#endif
--- /dev/null
+/* Copyright (c) 2007-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+/** @file odpor_tests_private.hpp
+ *
+ * A private header file for all ODPOR tests
+ */
+
+#ifndef SIMGRID_MC_ODPOR_TEST_PRIVATE_HPP
+#define SIMGRID_MC_ODPOR_TEST_PRIVATE_HPP
+
+#include "src/mc/explo/udpor/udpor_tests_private.hpp"
+#include "src/mc/transition/Transition.hpp"
+
+namespace simgrid::mc::odpor {
+
+struct DependentIfSameValueAction : public Transition {
+private:
+ const int value;
+
+public:
+ DependentIfSameValueAction() = default;
+ DependentIfSameValueAction(Type type, aid_t issuer, int value, int times_considered = 0)
+ : Transition(type, issuer, times_considered), value(value)
+ {
+ }
+ DependentIfSameValueAction(aid_t issuer, int value, int times_considered = 0)
+ : Transition(simgrid::mc::Transition::Type::UNKNOWN, issuer, times_considered), value(value)
+ {
+ }
+
+ // Dependent only with DependentAction (i.e. not itself)
+ bool depends(const Transition* other) const override
+ {
+ if (aid_ == other->aid_) {
+ return true;
+ }
+
+ if (const auto* same_value = dynamic_cast<const DependentIfSameValueAction*>(other); same_value != nullptr) {
+ return value == same_value->value;
+ }
+
+ // `DependentAction` is dependent with everyone who's not the `IndependentAction`
+ return dynamic_cast<const simgrid::mc::udpor::DependentAction*>(other) != nullptr;
+ }
+};
+
+} // namespace simgrid::mc::odpor
+
+#endif
#if SIMGRID_HAVE_STATEFUL_MC
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
- explo = std::unique_ptr<Exploration>(create_communication_determinism_checker(argv_copy, cfg_use_DPOR()));
+ explo = std::unique_ptr<Exploration>(
+ create_communication_determinism_checker(argv_copy, get_model_checking_reduction()));
else if (_sg_mc_unfolding_checker)
explo = std::unique_ptr<Exploration>(create_udpor_checker(argv_copy));
else if (not _sg_mc_property_file.get().empty())
explo = std::unique_ptr<Exploration>(create_liveness_checker(argv_copy));
else
#endif
- explo = std::unique_ptr<Exploration>(create_dfs_exploration(argv_copy, cfg_use_DPOR()));
+ explo = std::unique_ptr<Exploration>(create_dfs_exploration(argv_copy, get_model_checking_reduction()));
ExitStatus status;
try {
static simgrid::config::Flag<std::string> cfg_mc_reduction{
"model-check/reduction", "Specify the kind of exploration reduction (either none or DPOR)", "dpor",
[](std::string_view value) {
- if (value != "none" && value != "dpor")
- xbt_die("configuration option 'model-check/reduction' can only take 'none' or 'dpor' as a value");
+ if (value != "none" && value != "dpor" && value != "sdpor" && value != "odpor")
+ xbt_die("configuration option 'model-check/reduction' must be one of the following: "
+ " 'none', 'dpor', 'sdpor', or 'odpor'");
}};
simgrid::config::Flag<bool> _sg_mc_sleep_set{
"model-check/termination", "Whether to enable non progressive cycle detection", false,
[](bool) { _mc_cfg_cb_check("value to enable/disable the detection of non progressive cycles"); }};
-bool simgrid::mc::cfg_use_DPOR()
+simgrid::mc::ReductionMode simgrid::mc::get_model_checking_reduction()
{
- if (cfg_mc_reduction.get() == "dpor" && _sg_mc_max_visited_states__ > 0) {
+ if ((cfg_mc_reduction.get() == "dpor" || cfg_mc_reduction.get() == "sdpor" || cfg_mc_reduction.get() == "odpor") &&
+ _sg_mc_max_visited_states__ > 0) {
XBT_INFO("Disabling DPOR since state-equality reduction is activated with 'model-check/visited'");
- return false;
+ return simgrid::mc::ReductionMode::none;
+ }
+
+ if (cfg_mc_reduction.get() == "none") {
+ return ReductionMode::none;
+ } else if (cfg_mc_reduction.get() == "dpor") {
+ return ReductionMode::dpor;
+ } else if (cfg_mc_reduction.get() == "sdpor") {
+ return ReductionMode::sdpor;
+ } else if (cfg_mc_reduction.get() == "odpor") {
+ return ReductionMode::odpor;
+ } else if (cfg_mc_reduction.get() == "udpor") {
+ XBT_INFO("No reduction will be used: "
+ "UDPOR has a dedicated invocation 'model-check/unfolding-checker' "
+ "but is not yet fully supported in SimGrid");
+ return ReductionMode::none;
+ } else {
+ XBT_INFO("Unknown reduction mode: defaulting to no reduction");
+ return ReductionMode::none;
}
- return cfg_mc_reduction.get() == "dpor";
}
/********************************** Configuration of MC **************************************/
namespace simgrid::mc {
-bool cfg_use_DPOR(); // "model-check/reduction" == "DPOR"
+XBT_DECLARE_ENUM_CLASS(ReductionMode, none, dpor, sdpor, odpor);
XBT_DECLARE_ENUM_CLASS(ModelCheckingMode, NONE, APP_SIDE, CHECKER_SIDE, REPLAY);
+ReductionMode get_model_checking_reduction(); // "model-check/reduction" == "DPOR"
XBT_PUBLIC ModelCheckingMode get_model_checking_mode();
XBT_PUBLIC void set_model_checking_mode(ModelCheckingMode mode);
-};
+}; // namespace simgrid::mc
extern XBT_PUBLIC simgrid::config::Flag<std::string> _sg_mc_buffering;
extern XBT_PRIVATE simgrid::config::Flag<int> _sg_mc_checkpoint;
}
bool ActorJoinTransition::depends(const Transition* other) const
{
- // Joining is indep with any other transitions:
+ // Joining is dependent with any transition whose
+ // actor is that of the `other` action. , Join i
+ if (other->aid_ == target_) {
+ return true;
+ }
+
+ // Actions executed by the same actor are always dependent
+ if (other->aid_ == aid_)
+ return true;
+
+ // Otherwise, joining is indep with any other transitions:
// - It is only enabled once the target ends, and after this point it's enabled no matter what
// - Other joins don't affect it, and it does not impact on the enabledness of any other transition
return false;
}
bool TestAnyTransition::depends(const Transition* other) const
{
+ // Actions executed by the same actor are always dependent
+ if (other->aid_ == aid_)
+ return true;
+
return transitions_[times_considered_]->depends(other);
}
WaitAnyTransition::WaitAnyTransition(aid_t issuer, int times_considered, std::stringstream& stream)
}
bool WaitAnyTransition::depends(const Transition* other) const
{
+ // Actions executed by the same actor are always dependent
+ if (other->aid_ == aid_)
+ return true;
return transitions_[times_considered_]->depends(other);
}
if (other->type_ < type_)
return other->depends(this);
+ // Actions executed by the same actor are always dependent
+ if (other->aid_ == aid_)
+ return true;
+
if (const auto* wait = dynamic_cast<const CommWaitTransition*>(other)) {
if (timeout_ || wait->timeout_)
return true; // Timeouts are not considered by the independence theorem, thus assumed dependent
if (other->type_ < type_)
return other->depends(this);
+ // Actions executed by the same actor are always dependent
+ if (other->aid_ == aid_)
+ return true;
+
if (dynamic_cast<const CommTestTransition*>(other) != nullptr)
return false; // Test & Test are independent
if (other->type_ < type_)
return other->depends(this);
+ // Actions executed by the same actor are always dependent
+ if (other->aid_ == aid_)
+ return true;
+
if (const auto* recv = dynamic_cast<const CommRecvTransition*>(other))
return mbox_ == recv->mbox_;
if (other->type_ < type_)
return other->depends(this);
+ // Actions executed by the same actor are always dependent
+ if (other->aid_ == aid_)
+ return true;
+
if (const auto* other_isend = dynamic_cast<const CommSendTransition*>(other))
return mbox_ == other_isend->mbox_;
}
bool ObjectAccessTransition::depends(const Transition* o) const
{
+ if (o->type_ < type_)
+ return o->depends(this);
+
+ // Actions executed by the same actor are always dependent
+ if (o->aid_ == aid_)
+ return true;
+
if (const auto* other = dynamic_cast<const ObjectAccessTransition*>(o))
return objaddr_ == other->objaddr_; // dependent only if it's an access to the same object
return false;
public:
std::string to_string(bool verbose) const override;
RandomTransition(aid_t issuer, int times_considered, std::stringstream& stream);
- bool depends(const Transition* other) const override { return aid_ == other->aid_; } // Independent with any other transition
+ bool depends(const Transition* other) const override
+ {
+ if (other->type_ < type_)
+ return other->depends(this);
+
+ return aid_ == other->aid_;
+ } // Independent with any other transition
};
} // namespace simgrid::mc
if (o->type_ < type_)
return o->depends(this);
+ // Actions executed by the same actor are always dependent
+ if (o->aid_ == aid_)
+ return true;
+
// type_ <= other->type_ in MUTEX_LOCK, MUTEX_TEST, MUTEX_TRYLOCK, MUTEX_UNLOCK, MUTEX_WAIT,
if (auto* other = dynamic_cast<const MutexTransition*>(o)) {
> If this is too much, consider sharing allocations for computation buffers.
> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
>
-> [0.000000] [mc_dfs/INFO] DFS exploration ended. 635 unique states visited; 173 backtracks (3896 transition replays, 3088 states visited overall)
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed MPI handles:
+> [0.000000] [smpi_utils/WARNING] To get more information (location of allocations), compile your code with -trace-call-location flag of smpicc/f90
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Comm
+> [0.000000] [smpi_utils/INFO] 4 leaked handles of type MPI_Group
+> [0.000000] [smpi_utils/INFO] Probable memory leaks in your code: SMPI detected 8 unfreed buffers:
+> [0.000000] [smpi_utils/INFO] leaked allocations of total size 152, called 8 times, with minimum size 16 and maximum size 28
+> [0.000000] [smpi_utils/INFO] Memory Usage: Simulated application allocated 152 bytes during its lifetime through malloc/calloc calls.
+> Largest allocation at once from a single process was 28 bytes, at coll-allreduce-with-leaks.c:28. It was called 1 times during the whole simulation.
+> If this is too much, consider sharing allocations for computation buffers.
+> This can be done automatically by setting --cfg=smpi/auto-shared-malloc-thresh to the minimum size wanted size (this can alter execution if data content is necessary)
+>
+> [0.000000] [mc_dfs/INFO] DFS exploration ended. 1005 unique states visited; 276 backtracks (6560 transition replays, 5279 states visited overall)
set(MC_SRC_STATELESS
src/mc/api/ActorState.hpp
+ src/mc/api/ClockVector.cpp
+ src/mc/api/ClockVector.hpp
src/mc/api/State.cpp
src/mc/api/State.hpp
src/mc/api/RemoteApp.cpp
src/mc/explo/Exploration.cpp
src/mc/explo/Exploration.hpp
+ src/mc/explo/odpor/Execution.cpp
+ src/mc/explo/odpor/Execution.hpp
+ src/mc/explo/odpor/ReversibleRaceCalculator.cpp
+ src/mc/explo/odpor/ReversibleRaceCalculator.hpp
+ src/mc/explo/odpor/WakeupTree.cpp
+ src/mc/explo/odpor/WakeupTree.hpp
+ src/mc/explo/odpor/WakeupTreeIterator.cpp
+ src/mc/explo/odpor/WakeupTreeIterator.hpp
+ src/mc/explo/odpor/odpor_forward.hpp
+ src/mc/explo/odpor/odpor_tests_private.hpp
+
src/mc/remote/AppSide.cpp
src/mc/remote/AppSide.hpp
src/mc/remote/Channel.cpp
set(MC_UNIT_TESTS src/mc/sosp/Snapshot_test.cpp
src/mc/sosp/PageStore_test.cpp
+ src/mc/explo/odpor/ClockVector_test.cpp
+ src/mc/explo/odpor/Execution_test.cpp
+ src/mc/explo/odpor/WakeupTree_test.cpp
src/mc/explo/udpor/EventSet_test.cpp
src/mc/explo/udpor/Unfolding_test.cpp
src/mc/explo/udpor/UnfoldingEvent_test.cpp
