return actors;
}
+std::unordered_set<aid_t> State::get_sleeping_set() 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.
this->wakeup_tree_.remove_subtree_rooted_at(*branch);
}
+void State::mark_path_interesting_for_odpor(const odpor::PartialExecution& pe, const odpor::Execution& E)
+{
+ this->wakeup_tree_.insert(E, pe);
+}
+
} // namespace simgrid::mc
* 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_set() const;
+ std::unordered_set<aid_t> get_enabled_actors() const;
std::map<aid_t, Transition> const& get_sleep_set() const { return sleep_set_; }
void add_sleep_set(std::shared_ptr<Transition> t)
{
*/
void remove_subtree_starting_with(aid_t p);
+ /**
+ * @brief
+ */
+ void mark_path_interesting_for_odpor(const odpor::PartialExecution&, const odpor::Execution&);
+
/* Returns the total amount of states created so far (for statistics) */
static long get_expanded_states() { return expended_states_; }
};
// The latter evidently must be done BEFORE the former
next_state->sprout_tree_from_parent_state();
state->remove_subtree_starting_with(next);
+
+ // TODO: Consider what we have to do to handle transitions
+ // with multiple possible executions. We probably have to re-insert
+ // something into `state` and make note of that for later (opened_states_)
}
/* DPOR persistent set procedure:
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
+ 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; e_prime++) {
+ for (const auto e : execution_seq_.get_racing_events_of(e_prime)) {
+ // To determine if the race is reversible, we have to ensure
+ // that actor `p` running `e_i` (viz. the event such that
+ // `racing_event -> (E_p) e_i` and no other event
+ // "happens-between" the two) is enabled in any equivalent
+ // execution where `racing_event` happens before `e_i`.
+ //
+ // Importantly, it is equivalent to checking if in ANY
+ // such equivalent execution sequence where `racing_event`
+ // happens-before `next_E_p` that `p` is enabled in `pre(racing_event, E.p)`.
+ // Thus it suffices to check THIS execution
+ //
+ // If the actor `p` is not enabled at s_[E'], it is not a *reversible* race
+ const aid_t p = execution_seq_.get_actor_with_handle(e_prime);
+ const std::shared_ptr<State> prev_state = stack_[e];
+ if (prev_state->is_actor_enabled(p)) {
+ const std::optional<odpor::PartialExecution> v = execution_seq_.get_odpor_extension_from(
+ e, e_prime, prev_state->get_sleeping_set(), prev_state->get_enabled_actors());
+ if (v.has_value()) {
+ prev_state->mark_path_interesting_for_odpor(v.value(), execution_seq_.get_prefix_before(e));
+ }
+ }
+ }
+ }
}
XBT_VERB("Backtracking from %s", get_record_trace().to_string().c_str());
return racing_events;
}
-Execution Execution::get_prefix_up_to(Execution::EventHandle handle) const
+Execution Execution::get_prefix_before(Execution::EventHandle handle) const
{
return Execution(std::vector<Event>{contents_.begin(), contents_.begin() + handle});
}
// First, grab `E' := pre(e, E)` and determine what actor `p` is
const auto next_E_p = get_latest_event_handle().value();
- Execution E_prime_v = get_prefix_up_to(e);
+ Execution E_prime_v = get_prefix_before(e);
std::vector<sdpor::Execution::EventHandle> v;
// Note `e + 1` here: `notdep(e, E)` is defined as the
return std::nullopt;
}
+std::optional<PartialExecution> Execution::get_odpor_extension_from(EventHandle e, EventHandle e_prime,
+ std::unordered_set<aid_t> sleep_set,
+ std::unordered_set<aid_t> enabled_actors) const
+{
+ // TODO: Implement this :(
+ return std::nullopt;
+}
+
bool Execution::is_initial_after_execution(const PartialExecution& w, aid_t p) const
{
auto E_w = *this;
*/
class Execution {
private:
- /**
- * @brief The actual steps that are taken by the process
- * during exploration, relative to the
- */
std::vector<Event> contents_;
-
Execution(std::vector<Event>&& contents) : contents_(std::move(contents)) {}
public:
*/
std::optional<aid_t> get_first_sdpor_initial_from(EventHandle e, std::unordered_set<aid_t> backtrack_set) const;
- bool is_initial_after_execution(const PartialExecution& w, aid_t p) const;
- bool is_independent_with_execution(const PartialExecution& w, const Transition* next_E_p) 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 a WakeupTree for
std::optional<PartialExecution> get_shortest_odpor_sq_subset_insertion(const PartialExecution& v,
const PartialExecution& w) const;
+ /**
+ * @brief For a given reversible race
+ */
+ std::optional<PartialExecution> get_odpor_extension_from(EventHandle, EventHandle,
+ std::unordered_set<aid_t> sleep_set,
+ std::unordered_set<aid_t> enabled_actors) const;
+
+ bool is_initial_after_execution(const PartialExecution& w, aid_t p) const;
+ bool is_independent_with_execution(const PartialExecution& w, const Transition* next_E_p) const;
+
/**
* @brief Determines the event associated with
* the given handle `handle`
*/
aid_t get_actor_with_handle(EventHandle handle) const { return get_event_with_handle(handle).get_transition()->aid_; }
+ /**
+ * @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
*/
std::unordered_set<EventHandle> get_racing_events_of(EventHandle handle) const;
- /**
- * @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 Computes `pre(e, E)` as described in ODPOR [1]
*
* causes that permitted event `e` to exist (roughly
* speaking)
*/
- Execution get_prefix_up_to(EventHandle) const;
+ Execution get_prefix_before(EventHandle) const;
/**
* @brief Whether the event represented by `e1`
