X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/f5961f8e3a20cb943913a472ac8e11575470dab4..716c8e0b373bed43c35af2b35514f0b7a69b08a5:/src/mc/explo/UdporChecker.cpp diff --git a/src/mc/explo/UdporChecker.cpp b/src/mc/explo/UdporChecker.cpp index b29718331d..c8bac5bbd2 100644 --- a/src/mc/explo/UdporChecker.cpp +++ b/src/mc/explo/UdporChecker.cpp @@ -64,7 +64,12 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, Event // possibility is that we've finished running everything, and // we wouldn't be in deadlock then) if (enC.empty()) { - XBT_VERB("Maximal configuration detected. Checking for deadlock..."); + XBT_VERB("**************************"); + XBT_VERB("*** TRACE INVESTIGATED ***"); + XBT_VERB("**************************"); + XBT_VERB("Execution sequence:"); + for (auto const& s : get_textual_trace()) + XBT_VERB(" %s", s.c_str()); get_remote_app().check_deadlock(); } @@ -109,8 +114,8 @@ void UdporChecker::explore(const Configuration& C, EventSet D, EventSet A, Event // that we are searching again from `state(C)`. While the // stack of states is properly adjusted to represent // `state(C)` all together, the RemoteApp is currently sitting - // at some *future* state with resepct to `state(C)` since the - // recursive calls have moved it there. + // at some *future* state with respect to `state(C)` since the + // recursive calls had moved it there. restore_program_state_with_current_stack(); // Explore(C, D + {e}, J \ C) @@ -150,11 +155,22 @@ EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC, EventSet exC = prev_exC; exC.remove(e_cur); + // IMPORTANT NOTE: In order to have deterministic results, we need to process + // the actors in a deterministic manner so that events are discovered by + // UDPOR in a deterministic order. The processing done here always processes + // actors in a consistent order since `std::map` is by-default ordered using + // `std::less` (see the return type of `State::get_actors_list()`) for (const auto& [aid, actor_state] : stateC.get_actors_list()) { - for (const auto& transition : actor_state.get_enabled_transitions()) { - XBT_DEBUG("\t Considering partial extension for %s", transition->to_string().c_str()); - EventSet extension = ExtensionSetCalculator::partially_extend(C, &unfolding, transition); - exC.form_union(extension); + const auto& enabled_transitions = actor_state.get_enabled_transitions(); + if (enabled_transitions.empty()) { + XBT_DEBUG("\t Actor `%ld` is disabled: no partial extensions need to be considered", aid); + } else { + XBT_DEBUG("\t Actor `%ld` is enabled", aid); + for (const auto& transition : enabled_transitions) { + XBT_DEBUG("\t Considering partial extension for %s", transition->to_string().c_str()); + EventSet extension = ExtensionSetCalculator::partially_extend(C, &unfolding, transition); + exC.form_union(extension); + } } } return exC; @@ -163,7 +179,7 @@ EventSet UdporChecker::compute_exC(const Configuration& C, const State& stateC, EventSet UdporChecker::compute_enC(const Configuration& C, const EventSet& exC) const { EventSet enC; - for (const auto e : exC) { + for (const auto* e : exC) { if (C.is_compatible_with(e)) { enC.insert(e); } @@ -214,7 +230,7 @@ void UdporChecker::restore_program_state_with_current_stack() for (const std::unique_ptr& state : state_stack) { if (state == state_stack.back()) /* If we are arrived on the target state, don't replay the outgoing transition */ break; - state->get_transition()->replay(get_remote_app()); + state->get_transition_out()->replay(get_remote_app()); } } @@ -236,16 +252,23 @@ UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, con "empty before attempting to select an event from it?"); } + // UDPOR's exploration is non-deterministic (as is DPOR's) + // in the sense that at any given point there may + // be multiple paths that can be followed. The correctness and optimality + // of the algorithm remains unaffected by the route taken by UDPOR when + // given multiple choices; but to ensure that SimGrid itself has deterministic + // behavior on all platforms, we always pick events with lower id's + // to ensure we explore the unfolding deterministically. if (A.empty()) { - return const_cast(*(enC.begin())); - } - - for (const auto& event : A) { - if (enC.contains(event)) { - return const_cast(event); - } + const auto min_event = std::min_element(enC.begin(), enC.end(), + [](const auto e1, const auto e2) { return e1->get_id() < e2->get_id(); }); + return const_cast(*min_event); + } else { + const auto intersection = A.make_intersection(enC); + const auto min_event = std::min_element(intersection.begin(), intersection.end(), + [](const auto e1, const auto e2) { return e1->get_id() < e2->get_id(); }); + return const_cast(*min_event); } - return nullptr; } void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration& C, const EventSet& D) @@ -277,7 +300,7 @@ void UdporChecker::clean_up_explore(const UnfoldingEvent* e, const Configuration // "U (complicated expression)" portion const EventSet conflict_union = std::accumulate( - C_union_D.begin(), C_union_D.end(), EventSet(), [&](const EventSet acc, const UnfoldingEvent* e_prime) { + C_union_D.begin(), C_union_D.end(), EventSet(), [&](const EventSet& acc, const UnfoldingEvent* e_prime) { return acc.make_union(unfolding.get_immediate_conflicts_of(e_prime)); }); @@ -321,20 +344,10 @@ RecordTrace UdporChecker::get_record_trace() { RecordTrace res; for (auto const& state : state_stack) - res.push_back(state->get_transition()); + res.push_back(state->get_transition_out().get()); return res; } -std::vector UdporChecker::get_textual_trace() -{ - std::vector trace; - for (auto const& state : state_stack) { - const auto* t = state->get_transition(); - trace.push_back(xbt::string_printf("%ld: %s", t->aid_, t->to_string().c_str())); - } - return trace; -} - } // namespace simgrid::mc::udpor namespace simgrid::mc {