wakeup_tree_.remove_min_single_process_subtree();
}
-void State::mark_path_interesting_for_odpor(const odpor::PartialExecution& pe, const odpor::Execution& E)
+odpor::WakeupTree::InsertionResult State::insert_into_wakeup_tree(const odpor::PartialExecution& pe,
+ const odpor::Execution& E)
{
- this->wakeup_tree_.insert(E, pe);
+ return this->wakeup_tree_.insert(E, pe);
}
-void State::do_odpor_backtrack_cleanup()
+void State::do_odpor_unwind()
{
if (auto out_transition = get_transition_out(); out_transition != nullptr) {
remove_subtree_using_current_out_transition();
/**
* @brief
*/
- void mark_path_interesting_for_odpor(const odpor::PartialExecution&, const odpor::Execution&);
+ odpor::WakeupTree::InsertionResult insert_into_wakeup_tree(const odpor::PartialExecution&, const odpor::Execution&);
- /** */
- void do_odpor_backtrack_cleanup();
+ /** @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_; }
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) {
- execution_seq_ = odpor::Execution();
-
// 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 = stack_.begin(); iter != stack_.end() - 1 and iter != stack_.end(); ++iter) {
- const auto& state = *(iter);
- execution_seq_.push_transition(state->get_transition_out());
+ 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");
}
- XBT_DEBUG("Additionally replaced corresponding SDPOR execution stack");
}
void DFSExplorer::log_state() // override
// 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());
- xbt_assert(!state->is_actor_sleeping(next),
- "We decided to schedule an actor (%ld) that is in the sleep set "
- "of the current state. By definition, this should be impossible; "
- "and yet it happened, somehow...",
- next);
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(),
{
for (auto iter = stack_.rbegin(); iter != stack_.rend(); ++iter) {
const auto& state = *iter;
- state->do_odpor_backtrack_cleanup();
+ state->do_odpor_unwind();
if (!state->has_empty_tree()) {
return state;
}
}
- xbt_die("There are no more states for ODPOR");
return nullptr;
}
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()) {
- XBT_DEBUG("ODPOR: Reversible race unaccounted for in the wakeup tree for "
- "the execution prior to event `%u`, inserting a sequence",
- e);
- prev_state.mark_path_interesting_for_odpor(v.value(), execution_seq_.get_prefix_before(e));
+ 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);
}
}
}
#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;
+}
+
void Execution::push_transition(std::shared_ptr<Transition> t)
{
if (t == nullptr) {
contents_.push_back(Event({std::move(t), max_clock_vector}));
}
+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;
namespace simgrid::mc::odpor {
+std::vector<std::string> get_textual_trace(const PartialExecution& w);
+
/**
* @brief The occurrence of a transition in an execution
*
Execution& operator=(Execution const&) = default;
Execution(Execution&&) = default;
+ 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(); }
this->nodes_.erase(node);
}
-void WakeupTree::insert(const Execution& E, const PartialExecution& w)
+WakeupTree::InsertionResult WakeupTree::insert(const Execution& E, const PartialExecution& w)
{
// See section 6.2 of Abdulla. et al.'s 2017 ODPOR paper for details
// 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;
+ return InsertionResult::leaf;
}
}
xbt_die("Insertion should always succeed with the root node (which contains no "
*/
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
*
* @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
*/
- void insert(const Execution& E, const PartialExecution& seq);
+ InsertionResult insert(const Execution& E, const PartialExecution& seq);
};
} // namespace simgrid::mc::odpor
