aid_t State::next_odpor_transition() const
{
- const auto first_single_process_branch =
- std::find_if(wakeup_tree_.begin(), wakeup_tree_.end(),
- [=](const odpor::WakeupTreeNode* node) { return node->is_single_process(); });
- if (first_single_process_branch != wakeup_tree_.end()) {
- const auto* wakeup_tree_node = *first_single_process_branch;
- xbt_assert(wakeup_tree_node->get_sequence().size() == 1, "We claimed that the selected branch "
- "contained only a single process, yet more "
- "than one process was actually contained in it :(");
- return wakeup_tree_node->get_first_actor();
- }
- return -1;
+ return wakeup_tree_.get_min_single_process_actor().value_or(-1);
}
// This should be done in GuidedState, or at least interact with it
{
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 p = parent_state_->get_transition_out()->aid_;
- const auto branch = std::find_if(
- parent_state_->wakeup_tree_.begin(), parent_state_->wakeup_tree_.end(),
- [=](const odpor::WakeupTreeNode* node) { return node->is_single_process() && node->get_first_actor() == p; });
- xbt_assert(branch != parent_state_->wakeup_tree_.end(),
- "Attempted to create a subtree from the wakeup tree of the parent "
- "state using actor `%ld`, but no such subtree could be found. "
- "This implies that the wakeup tree management is broken, "
- "and more specifically that subtree formation is not working "
- "as intended; for if this state was generated by the parent "
- "having taken an action by actor `%ld`, this implies that "
- "ODPOR found `%ld` as a candidate branch prior",
- p, p, p);
- this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(*branch);
+ 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");
+
+ // TODO: This assert should even be bolstered to check that the
+ // the transitions themselves are identical -- not only just
+ // that the actors are the same. When we have to consider
+ // multiple paths for a transition, things get trickier
+ xbt_assert(parent_state_->get_transition_out()->aid_ == min_process_node.value()->get_actor(),
+ "We tried to make a subtree from a parent state who claimed to have executed %ld "
+ "but whose wakeup tree indicates it should have executed %ld. This indicates "
+ "that exploration is not following ODPOR. Are you sure you're choosing actors "
+ "to schedule from the wakeup tree?",
+ parent_state_->get_transition_out()->aid_, min_process_node.value()->get_actor());
+ this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(min_process_node.value());
}
-void State::remove_subtree_starting_with(aid_t p)
+void State::remove_subtree_using_current_out_transition()
{
- const auto branch = std::find_if(wakeup_tree_.begin(), wakeup_tree_.end(), [=](const odpor::WakeupTreeNode* node) {
- return node->is_single_process() && node->get_first_actor() == p;
- });
- xbt_assert(branch != wakeup_tree_.end(), "Attempted to remove a subtree of this state's "
- "wakeup tree that does not exist");
- this->wakeup_tree_.remove_subtree_rooted_at(*branch);
+ if (auto out_transition = get_transition_out(); out_transition != nullptr) {
+ // TODO: Add invariant check here
+ }
+
+ wakeup_tree_.remove_min_single_process_subtree();
}
void State::mark_path_interesting_for_odpor(const odpor::PartialExecution& pe, const odpor::Execution& E)
void State::do_odpor_backtrack_cleanup()
{
if (auto out_transition = get_transition_out(); out_transition != nullptr) {
- remove_subtree_starting_with(out_transition->aid_);
+ remove_subtree_using_current_out_transition();
add_sleep_set(std::move(out_transition));
}
}
* @brief Removes the subtree rooted at the single-process node
* `N` running actor `p` of this state's wakeup tree
*/
- void remove_subtree_starting_with(aid_t p);
+ void remove_subtree_using_current_out_transition();
bool has_empty_tree() const { return this->wakeup_tree_.empty(); }
/**
// Now we add `e_prime := <q, i>` to `E'.v` and repeat the same work
{
- 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);
-
if (not located_actor_in_initial) {
// It's possible `proc(e_prime)` is an initial
+ E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
v_handles.push_back(e_prime_in_E_prime_v);
- located_actor_in_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_loc) {
- return E_prime_v.happens_before(e_loc, e_prime_in_E_prime_v);
- });
+
+ const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v);
+ located_actor_in_initial = disqualified_actors.count(q) == 0 and
+ std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_loc) {
+ return E_prime_v.happens_before(e_loc, e_prime_in_E_prime_v);
+ });
}
}
// any of them are independent with this execution after `v`. This
// completes the check for weak initials
for (const auto& [aid, astate] : state_at_e.get_actors_list()) {
- if (sleeping_actors.count(astate.get_transition()->aid_) == 0 and
- pre_E_e.is_independent_with_execution(v, astate.get_transition())) {
+ // TODO: We have to be able to react appropriately here when adding new
+ // types of transitions (multiple choices can be made :( )
+ if (sleeping_actors.count(aid) == 0 and pre_E_e.is_independent_with_execution(v, astate.get_transition(0))) {
return v;
}
}
// Move one step forward in the direction of `v` and repeat
E_v.push_transition(next_E_p);
}
-
- // Construct, finally, v.w' by adding `v` to the front of
- // what remains of `w` after removing `v` as above
- for (auto it = v.rbegin(); it != v.rend(); ++it) {
- w_now.push_front(*it);
- }
-
return std::optional<PartialExecution>{std::move(w_now)};
}
* `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 `v.w'` that should be inserted
+ * @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,
#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>
namespace simgrid::mc::odpor {
-aid_t WakeupTreeNode::get_first_actor() const
-{
- if (seq_.empty()) {
- throw std::invalid_argument("Attempted to extract the first actor from "
- "a node in a wakeup tree representing the "
- "empty execution (likely the root node)");
- }
- return get_sequence().front()->aid_;
-}
-
void WakeupTreeNode::add_child(WakeupTreeNode* node)
{
this->children_.push_back(node);
node->parent_ = this;
}
-WakeupTreeNode::~WakeupTreeNode()
+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: We can probably be more clever here: when
- // we add the child to a node, we could perhaps
- // try instead to keep a reference to position of the
- // child in the list of the parent.
+ // 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);
}
}
this->insert_node(std::move(root));
}
-WakeupTree WakeupTree::make_subtree_rooted_at(WakeupTreeNode* root)
+std::vector<std::string> WakeupTree::get_single_process_texts() const
{
- if (not root->is_single_process()) {
- throw std::invalid_argument("Selecting subtrees is only defined for single-process nodes");
+ 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;
+}
- const aid_t p = root->get_first_actor();
+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;
// 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. Note that the subtree
- // **explicitly** removes the first process from each child
+ // to that their children are added, and so on.
for (WakeupTreeNode* child_in_other_tree : node_in_other_tree->get_ordered_children()) {
- auto p_w = child_in_other_tree->get_sequence();
- const auto p_again = p_w.front()->aid_;
-
- // INVARIANT: A nodes of a wakeup tree form a prefix-closed set;
- // this means that any child node `c` of a node `n` must contain
- // `n.get_sequence()` as a prefix of `c.get_sequence()`
- xbt_assert(p_again == p,
- "Invariant Violation: The wakeup tree from which a subtree with actor "
- "`%ld` is being taken is not prefix free! The child node starts with "
- "`%ld` while the parent is `%ld`! This indicates that there "
- "is a bug in the insertion logic for the wakeup tree",
- p, p_again, p);
- p_w.pop_front();
-
- WakeupTreeNode* child_equivalent = subtree.make_node(p_w);
+ 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));
}
}
}
// After having found each node with BFS, now we can
- // remove them. This prevents the "joys" of iteration during mutation
+ // 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(const PartialExecution& u)
+WakeupTreeNode* WakeupTree::make_node(std::shared_ptr<Transition> u)
{
- auto node = std::unique_ptr<WakeupTreeNode>(new WakeupTreeNode(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;
xbt_assert(!shortest_sequence.value().empty(), "A successful insertion into an interior"
"node of a wakeup tree should never involve "
"an empty sequence (yet here we are, with an empty sequence)");
- WakeupTreeNode* new_node = this->make_node(shortest_sequence.value());
- node->add_child(new_node);
+ this->insert_sequence_after(node, shortest_sequence.value());
}
// Since we're following the post-order traversal of the tree,
// the first such node we see is the smallest w.r.t "<"
"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
#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(const PartialExecution& u) : seq_(u) {}
- explicit WakeupTreeNode(PartialExecution&& u) : seq_(std::move(u)) {}
+ explicit WakeupTreeNode(std::shared_ptr<Transition> u) : action_(u) {}
WakeupTreeNode* parent_ = nullptr;
std::list<WakeupTreeNode*> children_;
/** @brief The contents of the node */
- PartialExecution seq_;
+ 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();
+ ~WakeupTreeNode() = default;
WakeupTreeNode(const WakeupTreeNode&) = delete;
WakeupTreeNode(WakeupTreeNode&&) = default;
WakeupTreeNode& operator=(const WakeupTreeNode&) = delete;
const auto rbegin() const { return this->children_.rbegin(); }
const auto rend() const { return this->children_.rend(); }
- const PartialExecution& get_sequence() const { return seq_; }
- const std::list<WakeupTreeNode*>& get_ordered_children() const { return children_; }
bool is_leaf() const { return children_.empty(); }
- bool is_single_process() const { return seq_.size() == static_cast<size_t>(1); }
- aid_t get_first_actor() const;
+ 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_;
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(const PartialExecution& u);
+ WakeupTreeNode* make_node(std::shared_ptr<Transition> u);
/* Allow the iterator to access the contents of the tree */
friend WakeupTreeIterator;
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(); }
- void remove_subtree_rooted_at(WakeupTreeNode* root);
- static WakeupTree make_subtree_rooted_at(WakeupTreeNode* root);
+ 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
*/
bool empty() const { return nodes_.size() == static_cast<size_t>(1); }
+ /**
+ * @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 Inserts an sequence `seq` of processes into the tree
* such that that this tree is a wakeup tree relative to the
* | and add `v.w'` as a new leaf, ordered after all already existing nodes
* | of the form `v.w''`
*
- * This method performs the postorder search of part one and the insertion of
+ * 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()`).
*
