#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");
stack_.emplace_front(current_state);
}
XBT_DEBUG("Replaced stack by %s", get_record_trace().to_string().c_str());
+
+ if (reduction_mode_ == ReductionMode::sdpor) {
+ execution_seq_ = sdpor::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().get());
+ }
+ }
+ XBT_DEBUG("Additionally replaced corresponding SDPOR execution stack");
}
void DFSExplorer::log_state() // override
}
/* 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
}
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(executed_transition.get());
+
+ xbt_assert(execution_seq_.get_latest_event_handle().has_value(),
+ "No events are contained in the SDPOR/OPDPOR execution "
+ "even though one was just added");
+ const aid_t p = executed_transition->aid_;
+ const auto next_E_p = execution_seq_.get_latest_event_handle().value();
+
+ for (const auto racing_event_handle : execution_seq_.get_racing_events_of(next_E_p)) {
+ // To determine if the race is reversible, we have to ensure
+ // that actor `p` running `next_E_p` (viz. the event such that
+ // `racing_event -> (E_p) next_E_p` and no other event
+ // "happens-between" the two) is enabled in any equivalent
+ // execution where `racing_event` happens before `next_E_p`.
+ //
+ // 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 std::shared_ptr<State> prev_state = stack_[racing_event_handle];
+ if (prev_state->is_actor_enabled(p)) {
+ // 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
+ const std::optional<aid_t> q =
+ execution_seq_.get_first_sdpor_initial_from(racing_event_handle, prev_state->get_backtrack_set());
+ if (q.has_value()) {
+ prev_state->consider_one(q.value());
+ opened_states_.emplace_back(std::move(prev_state));
+ }
+ }
+ }
}
// 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
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 {
opened_states_.emplace_back(stack_.back());
}
-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
