#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");
}
/* 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:
+ */
+ execution_seq_.push_transition(executed_transition.get());
+
+ // 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
+ 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)) {
+ // 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 (not prev_state->is_actor_enabled(p)) {
+ continue;
+ }
+
+ // This is a reversible race! First, grab `E' := pre(e, E)`
+ // TODO: Instead of copying around these big structs, it
+ // would behoove us to incorporate some way to reference
+ // portions of an execution. For simplicity and for a
+ // "proof of concept" version, we opt to simply copy
+ // the contents instead of making a view into the execution
+ const sdpor::Execution E_prime_v = execution_seq_.get_prefix_up_to(racing_event_handle);
+
+ // The vector `v` is constructed as `v := notdep(e, E)
+ std::vector<sdpor::Execution::EventHandle> v(execution_seq_.size());
+ std::unordered_set<aid_t> disqualified_actors = state->get_todo_actors();
+
+ for (auto e_prime = racing_event_handle; e_prime <= next_E_p; ++e_prime) {
+ // Any event `e` which occurs after `racing_event_handle` but which does not
+ // happen after `racing_event_handle` is a member of `v`
+ if (not E_prime_v.happens_before(racing_event_handle, e_prime) or e_prime == next_E_p) {
+ v.push_back(e_prime);
+ }
+ const aid_t q = E_prime_v.get_actor_with_handle(e_prime);
+ if (disqualified_actors.count(q) > 0) {
+ continue;
+ }
+
+ const bool is_initial = std::none_of(v.begin(), v.end(), [&E_prime_v, e_prime](const auto& e_star) {
+ return E_prime_v.happens_before(e_star, e_prime);
+ });
+ if (is_initial) {
+ if (not prev_state->is_actor_done(q)) {
+ prev_state->consider_one(q);
+ opened_states_.emplace_back(std::move(prev_state));
+ }
+ break;
+ } else {
+ disqualified_actors.insert(q);
+ }
+ }
+ }
}
// 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
}
#endif
+ // Search how to restore the backtracking point
+ State* init_state = nullptr;
+ std::deque<Transition*> replay_recipe;
+ for (auto* s = backtracking_point.get(); s != nullptr; s = s->get_parent_state().get()) {
+#if SIMGRID_HAVE_STATEFUL_MC
+ if (s->get_system_state() != nullptr) { // Found a state that I can restore
+ init_state = s;
+ break;
+ }
+#endif
+ if (s->get_transition_in() != nullptr) // The root has no transition_in
+ replay_recipe.push_front(s->get_transition_in().get());
+ }
+
+ // Restore the init_state, if any
+ if (init_state != nullptr) {
+#if SIMGRID_HAVE_STATEFUL_MC
+ const auto* system_state = init_state->get_system_state();
+ system_state->restore(*get_remote_app().get_remote_process_memory());
+ on_restore_system_state_signal(init_state, get_remote_app());
+#endif
+ } else { // Restore the initial state if no intermediate state was found
+ get_remote_app().restore_initial_state();
+ on_restore_initial_state_signal(get_remote_app());
+ }
+
/* if no snapshot, we need to restore the initial state and replay the transitions */
- get_remote_app().restore_initial_state();
- on_restore_initial_state_signal(get_remote_app());
/* Traverse the stack from the state at position start and re-execute the transitions */
- for (auto& state : backtracking_point->get_recipe()) {
- state->replay(get_remote_app());
- on_transition_replay_signal(state, get_remote_app());
+ for (auto& transition : replay_recipe) {
+ transition->replay(get_remote_app());
+ on_transition_replay_signal(transition, get_remote_app());
visited_states_count_++;
}
this->restore_stack(backtracking_point);
}
DFSExplorer::DFSExplorer(const std::vector<char*>& args, bool with_dpor, bool need_memory_info)
- : Exploration(args, need_memory_info || _sg_mc_termination)
+ : Exploration(args, need_memory_info || _sg_mc_termination
+#if SIMGRID_HAVE_STATEFUL_MC
+ || _sg_mc_checkpoint > 0
+#endif
+ )
{
if (with_dpor)
reduction_mode_ = ReductionMode::dpor;
