}
void mark_done() { this->state_ = InterleavingType::done; }
- inline Transition* get_transition(unsigned times_considered) const
+ std::shared_ptr<Transition> get_transition() const { return get_transition(get_times_considered()); }
+
+ 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`, "
return strategy_->next_transition();
}
+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_sequence().front()->aid_;
+ }
+ return -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 actors;
}
+void State::seed_wakeup_tree_if_needed(const odpor::Execution& prior)
+{
+ // 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()) {
+ if (const aid_t next = std::get<0>(next_transition_guided()); next >= 0) {
+ wakeup_tree_.insert(prior, odpor::PartialExecution{strategy_->actors_to_run_.at(next).get_transition()});
+ }
+ }
+}
+
} // namespace simgrid::mc
#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
* transition */
std::map<aid_t, 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_;
+
public:
explicit State(RemoteApp& remote_app);
explicit State(RemoteApp& remote_app, std::shared_ptr<State> parent_state);
/* 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(); }
* 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 pseudcode in none of the above algorithms explicitly
+ * 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.
sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_));
}
+ /**
+ * @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);
+
/* Returns the total amount of states created so far (for statistics) */
static long get_expanded_states() { return expended_states_; }
};
}
XBT_DEBUG("Replaced stack by %s", get_record_trace().to_string().c_str());
- if (reduction_mode_ == ReductionMode::sdpor) {
- execution_seq_ = sdpor::Execution();
+ 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
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 dpor 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
+ 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(),
}
}
}
+ } 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(executed_transition.get());
}
// Before leaving that state, if the transition we just took can be taken multiple times, we
void DFSExplorer::backtrack()
{
+ if (reduction_mode_ == ReductionMode::odpor) {
+ // TODO: In the case of ODPOR, adding in backtrack points occurs
+ // only after a full execution has been realized
+ }
+
XBT_VERB("Backtracking from %s", get_record_trace().to_string().c_str());
XBT_DEBUG("%lu alternatives are yet to be explored:", opened_states_.size());
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()) {
+ if (not node->is_leaf() or node == this->root_) {
WakeupTreeNode* new_node = this->make_node(shortest_sequence.value());
node->add_child(new_node);
}
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 children_.size() == static_cast<size_t>(1); }
+ bool is_single_process() const { return seq_.size() == static_cast<size_t>(1); }
/** Insert a node `node` as a new child of this node */
void add_child(WakeupTreeNode* node) { this->children_.push_back(node); }
void insert_node(std::unique_ptr<WakeupTreeNode> node);
void remove_node(WakeupTreeNode* node);
+ bool contains(WakeupTreeNode* node) const;
/**
* @brief Adds a new node to the tree, disconnected from
*/
WakeupTreeNode* make_node(const PartialExecution& u);
- bool contains(WakeupTreeNode* node) const;
-
/* Allow the iterator to access the contents of the tree */
friend WakeupTreeIterator;
* considered "empty" if it only contains the root node;
* that is, if it is "uninteresting". In such a case,
*/
- bool is_empty() const { return nodes_.size() == static_cast<size_t>(1); }
+ bool empty() const { return nodes_.size() == static_cast<size_t>(1); }
/**
* @brief Inserts an sequence `seq` of processes into the tree
// 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 (!cur_top_node->is_leaf()) {
+ 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
auto& children = cur_top_node->children_;
for (auto iter = children.rbegin(); iter != children.rend(); ++iter) {
- post_order_iteration.push(iter.base());
+ // iter.base() points one element past where we seek; hence,
+ // we move it over one position
+ post_order_iteration.push((--iter.base()));
}
+ cur_top_node = *post_order_iteration.top();
}
}
} else if (cfg_mc_reduction.get() == "sdpor") {
return ReductionMode::sdpor;
} else if (cfg_mc_reduction.get() == "odpor") {
- XBT_INFO("No reduction will be used: ODPOR is not yet supported in SimGrid");
- return simgrid::mc::ReductionMode::none;
+ return simgrid::mc::ReductionMode::odpor;
} else if (cfg_mc_reduction.get() == "udpor") {
XBT_INFO("No reduction will be used: "
"UDPOR is has a dedicated invocation 'model-check/unfolding-checker' "
