#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");
RecordTrace DFSExplorer::get_record_trace() // override
{
RecordTrace res;
- for (auto const& transition : stack_.back()->get_recipe())
- res.push_back(transition);
- res.push_back(stack_.back()->get_transition_out());
- return res;
-}
-std::vector<std::string> DFSExplorer::get_textual_trace() // override
-{
- std::vector<std::string> trace;
- for (auto const& transition : stack_.back()->get_recipe()) {
- trace.push_back(xbt::string_printf("%ld: %s", transition->aid_, transition->to_string().c_str()));
- }
- if (const auto* trans = stack_.back()->get_transition_out(); trans != nullptr)
- trace.push_back(xbt::string_printf("%ld: %s", trans->aid_, trans->to_string().c_str()));
- return trace;
+ if (const auto trans = stack_.back()->get_transition_out(); trans != nullptr)
+ res.push_back(trans.get());
+ for (const auto* state = stack_.back().get(); state != nullptr; state = state->get_parent_state().get())
+ if (state->get_transition_in() != nullptr)
+ res.push_front(state->get_transition_in().get());
+
+ return res;
}
void DFSExplorer::restore_stack(std::shared_ptr<State> state)
stack_.emplace_front(current_state);
}
XBT_DEBUG("Replaced stack by %s", get_record_trace().to_string().c_str());
+
+ if (reduction_mode_ == ReductionMode::sdpor) {
+ if (stack_.empty()) {
+ execution_seq_ = sdpor::Execution();
+ } else {
+ execution_seq_ = execution_seq_.get_prefix_up_to(stack_.size() - 1);
+ }
+ 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());
- on_transition_execute_signal(state->get_transition_out(), 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
// reached then perform one step of the exploration algorithm.
prev_state->get_transition_out()->to_string().c_str(), issuer_id);
tmp_stack.pop_back();
continue;
- } else if (prev_state->get_transition_out()->depends(state->get_transition_out())) {
+ } else if (prev_state->get_transition_out()->depends(state->get_transition_out().get())) {
XBT_VERB("Dependent Transitions:");
XBT_VERB(" %s (state=%ld)", prev_state->get_transition_out()->to_string().c_str(), prev_state->get_num());
XBT_VERB(" %s (state=%ld)", state->get_transition_out()->to_string().c_str(), state->get_num());
}
tmp_stack.pop_back();
}
+ } else if (reduction_mode_ == ReductionMode::sdpor) {
+ /**
+ * SDPOR Source Set Procedure:
+ *
+ * Find "reversible races" in the current execution 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` and then `p` to flip the race
+ */
+ 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 bes
+ const std::optional<aid_t> q =
+ execution_seq_.get_first_ssdpor_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
}
#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;
