From: mlaurent Date: Wed, 8 Nov 2023 10:25:32 +0000 (+0100) Subject: Add debug log for ODPOR + required explaining comments X-Git-Tag: v3.35~88 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/ff4bc56d5d0d4b1bf3e5c83e5af51ac3cc119789 Add debug log for ODPOR + required explaining comments --- diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp index f82d8da149..6fe0b46ab4 100644 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@ -371,7 +371,8 @@ void DFSExplorer::backtrack() * relation) */ for (auto e_prime = static_cast(0); e_prime <= last_event.value(); ++e_prime) { - for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) { + XBT_DEBUG("ODPOR: Now considering all possible race with `%u`", e_prime); + for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) { XBT_DEBUG("ODPOR: Reversible race detected between events `%u` and `%u`", e, e_prime); State& prev_state = *stack_[e]; if (const auto v = execution_seq_.get_odpor_extension_from(e, e_prime, prev_state); v.has_value()) { diff --git a/src/mc/explo/odpor/Execution.cpp b/src/mc/explo/odpor/Execution.cpp index 162425d2f4..8b531ff7b0 100644 --- a/src/mc/explo/odpor/Execution.cpp +++ b/src/mc/explo/odpor/Execution.cpp @@ -12,6 +12,8 @@ #include #include +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_execution, mc_dfs, "ODPOR exploration algorithm of the model-checker"); + namespace simgrid::mc::odpor { std::vector get_textual_trace(const PartialExecution& w) @@ -64,18 +66,22 @@ std::vector Execution::get_textual_trace() const std::unordered_set Execution::get_racing_events_of(Execution::EventHandle target) const { std::unordered_set racing_events; + // This keep tracks of events that happens-before the target std::unordered_set disqualified_events; // For each event of the execution for (auto e_i = target; e_i != std::numeric_limits::max(); e_i--) { // We need `e_i -->_E target` as a necessary condition if (not happens_before(e_i, target)) { + XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` discarded because `%u` --\\-->_E `%u`", target, e_i, e_i, target); continue; } // Further, `proc(e_i) != proc(target)` if (get_actor_with_handle(e_i) == get_actor_with_handle(target)) { disqualified_events.insert(e_i); + XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` disqualified because proc(`%u`)=proc(`%u`)", target, e_i, e_i, + target); continue; } @@ -87,6 +93,8 @@ std::unordered_set Execution::get_racing_events_of(Execu // then e_i --->_E target indirectly (either through // e_j directly, or transitively through e_j) if (disqualified_events.count(e_j) > 0 && happens_before(e_i, e_j)) { + XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` disqualified because `%u` happens-between `%u`-->`%u`-->`%u`)", + target, e_i, e_j, e_i, e_j, target); disqualified_events.insert(e_i); break; } @@ -98,6 +106,9 @@ std::unordered_set Execution::get_racing_events_of(Execu // it (since this would transitively make it the event // which "happens-between" `target` and `e`) if (disqualified_events.count(e_i) == 0) { + XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` is a valid racing event", + target, e_i); + disqualified_events.insert(e_i); racing_events.insert(e_i); disqualified_events.insert(e_i); } diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp index 947ccc0903..f6007c27ff 100644 --- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp +++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp @@ -11,8 +11,18 @@ #include #include +XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_reversible_race, mc_dfs, "ODPOR exploration algorithm of the model-checker"); + namespace simgrid::mc::odpor { +/** + The reversible race detector should only be used if we already have the assumption + e1 <* e2 (see Source set: a foundation for ODPOR). In particular this means that : + - e1 -->_E e2 + - proc(e1) != proc(e2) + - there is no event e3 s.t. e1 --> e3 --> e2 +*/ + bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution::EventHandle e1, Execution::EventHandle e2) { @@ -141,8 +151,12 @@ bool ReversibleRaceCalculator::is_race_reversible_MutexUnlock(const Execution&, bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1, const Transition* /*e2*/) { - // TODO: Get the semantics correct here + // The only possibilities for e1 to satisfy the pre-condition are : + // - MUTEX_ASYNC_LOCK + + const auto e1_action = E.get_transition_for_handle(e1)->type_; + xbt_assert(e1_action == Transition::Type::MUTEX_UNLOCK); return e1_action != Transition::Type::MUTEX_ASYNC_LOCK && e1_action != Transition::Type::MUTEX_UNLOCK; } @@ -164,6 +178,10 @@ bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution&, Exec const Transition* /*e2*/) { // TODO: Get the semantics correct here + // Certainement qu'il suffit de considérer les SemUnlock. ⋀ a priori, + // il doit même suffir de considérer le cas où leur capacity après execution est <=1 + // ces cas disent qu'avant éxecution la capacity était de 0. Donc aucune chance de pouvoir + // wait avant le unlock. return false; } diff --git a/src/mc/transition/TransitionSynchro.cpp b/src/mc/transition/TransitionSynchro.cpp index bd5788665a..5e7ded2aed 100644 --- a/src/mc/transition/TransitionSynchro.cpp +++ b/src/mc/transition/TransitionSynchro.cpp @@ -128,11 +128,7 @@ bool SemaphoreTransition::depends(const Transition* o) const // Actions executed by the same actor are always dependent if (o->aid_ == aid_) return true; -<<<<<<< HEAD - -======= ->>>>>>> dfafe652e9ae62c35cd0fc084b117fc987b3e8dc if (const auto* other = dynamic_cast(o)) { if (sem_ != other->sem_) return false;