X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/50753d5f8442a47c17c4035724201a18a7ff6146..1c27bfd8bf760d9b7f8220f17025acaf0da83cd2:/src/mc/explo/DFSExplorer.cpp diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index 187b9bb152..3afde709b6 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -62,9 +62,15 @@ void DFSExplorer::check_non_termination(const State* current_state) } RecordTrace DFSExplorer::get_record_trace() // override +{ + return get_record_trace_of_stack(stack_); +} + +/* Usefull to show debug information */ +RecordTrace DFSExplorer::get_record_trace_of_stack(stack_t stack) { RecordTrace res; - for (auto const& state : stack_) + for (auto const& state : stack) res.push_back(state->get_transition()); return res; } @@ -89,6 +95,18 @@ void DFSExplorer::log_state() // override Exploration::log_state(); } +/* Copy a given stack by deep-copying it at the State level : this is required so we can backtrack at different + * points without interacting with the stacks in the opened_states_ waiting for their turn. On the other hand, + * the exploration of one stack in opened_states_ could only slightly modify the sleep set of another stack in + * opened_states_, so it is only a slight waste of performance in the exploration. */ +void DFSExplorer::add_to_opened_states(stack_t stack) +{ + stack_t tmp_stack; + for (auto& state : stack) + tmp_stack.push_back(std::make_shared(State(*state))); + opened_states_.emplace(tmp_stack); +} + void DFSExplorer::run() { on_exploration_start_signal(get_remote_app()); @@ -129,7 +147,7 @@ void DFSExplorer::run() } // Search for the next transition - // next_transition returns a pair in case we want to consider multiple state + // next_transition returns a pair in case we want to consider multiple state (eg. during backtrack) auto [next, _] = state->next_transition_guided(); if (next < 0) { // If there is no more transition in the current state, backtrack. @@ -196,15 +214,16 @@ void DFSExplorer::run() if (prev_state->is_actor_enabled(issuer_id)) { if (not prev_state->is_actor_done(issuer_id)) { prev_state->consider_one(issuer_id); - opened_states.emplace_back(tmp_stack); + add_to_opened_states(tmp_stack); } else XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id); } else { XBT_DEBUG("Actor %ld is not enabled: DPOR may be failing. To stay sound, we are marking every enabled " "transition as todo", issuer_id); - prev_state->consider_all(); - opened_states.emplace_back(tmp_stack); + if (prev_state->consider_all() > + 0) // If we ended up marking at least a transition, explore it at some point + add_to_opened_states(tmp_stack); } break; } else { @@ -216,6 +235,11 @@ void DFSExplorer::run() } } + // Before leaving that state, if the transition we just took can be taken multiple times, we + // need to give it to the opened states + if (stack_.back()->count_todo_multiples() > 0) + add_to_opened_states(stack_); + if (_sg_mc_termination) this->check_non_termination(next_state.get()); @@ -232,8 +256,8 @@ void DFSExplorer::run() stack_.back()->consider_best(); // Take only one transition if DPOR: others may be considered later if required else { stack_.back()->consider_all(); - opened_states.emplace_back(stack_); } + dot_output("\"%ld\" -> \"%ld\" [%s];\n", state->get_num(), stack_.back()->get_num(), state->get_transition()->dot_string().c_str()); } else @@ -241,65 +265,46 @@ void DFSExplorer::run() visited_state_->original_num_ == -1 ? visited_state_->num_ : visited_state_->original_num_, state->get_transition()->dot_string().c_str()); } - log_state(); } void DFSExplorer::backtrack() { - backtrack_count_++; XBT_VERB("Backtracking from %s", get_record_trace().to_string().c_str()); + XBT_DEBUG("%lu alternatives are yet to be explored:", opened_states_.size()); + on_backtracking_signal(get_remote_app()); get_remote_app().check_deadlock(); // if no backtracking point, then set the stack_ to empty so we can end the exploration - if (opened_states.size() == 0) { + if (opened_states_.empty()) { stack_ = std::list>(); return; } - /* We may backtrack from somewhere either because it's leaf, or because every enabled process are in done/sleep set. - * In the first case, we need to remove the last transition corresponding to the Finalize */ - if (stack_.back()->get_transition()->aid_ == 0) - stack_.pop_back(); - - stack_t backtrack; - double min_dist = std::numeric_limits::infinity(); - aid_t min_aid = -1; - for (auto& stack : opened_states) { - auto [aid, dist] = stack.back()->next_transition_guided(); - if (aid == -1) - continue; - if (dist < min_dist) { - min_dist = dist; - min_aid = aid; - backtrack = stack; - } - } + stack_t backtrack = opened_states_.top(); // Take the point with smallest distance + opened_states_.pop(); - if (min_aid == -1) { - stack_ = std::list>(); + // if the smallest distance corresponded to no enable actor, remove this and let the + // exploration ask again for a backtrack + if (backtrack.back()->next_transition_guided().first == -1) return; - } - if (backtrack.back()->count_todo() <= 1) - opened_states.pop_back(); - XBT_VERB("%lu todo actors in last states of the next backtracking point %s (remaining %lu opened stacks)", - backtrack.back()->count_todo(), backtrack.back()->get_transition()->to_string().c_str(), - opened_states.size()); + // We found a real backtracking point, let's go to it + backtrack_count_++; /* If asked to rollback on a state that has a snapshot, restore it */ State* last_state = backtrack.back().get(); if (const auto* system_state = last_state->get_system_state()) { system_state->restore(*get_remote_app().get_remote_process_memory()); on_restore_system_state_signal(last_state, get_remote_app()); + stack_ = backtrack; return; } /* 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 (std::shared_ptr const& state : backtrack) { if (state == backtrack.back()) /* If we are arrived on the target state, don't replay the outgoing transition */ @@ -309,13 +314,11 @@ void DFSExplorer::backtrack() visited_states_count_++; } stack_ = backtrack; - XBT_VERB(">> Backtracked to %s", get_record_trace().to_string().c_str()); + XBT_DEBUG(">> Backtracked to %s", get_record_trace().to_string().c_str()); } -// DFSExplorer::DFSExplorer(const std::vector& args, bool with_dpor) : Exploration(args, _sg_mc_termination) // -// UNCOMMENT TO ACTIVATE REFORKS -DFSExplorer::DFSExplorer(const std::vector& args, bool with_dpor) - : Exploration(args, true) // This version does not use reforks as it breaks +DFSExplorer::DFSExplorer(const std::vector& args, bool with_dpor, bool need_memory_info) + : Exploration(args, need_memory_info || _sg_mc_termination) { if (with_dpor) reduction_mode_ = ReductionMode::dpor; @@ -344,8 +347,9 @@ DFSExplorer::DFSExplorer(const std::vector& args, bool with_dpor) stack_.back()->consider_best(); else { stack_.back()->consider_all(); - opened_states.emplace_back(stack_); } + if (stack_.back()->count_todo_multiples() > 1) + add_to_opened_states(stack_); } Exploration* create_dfs_exploration(const std::vector& args, bool with_dpor)