From: mlaurent Date: Wed, 8 Nov 2023 10:26:51 +0000 (+0100) Subject: Merge branch 'master' of https://framagit.org/simgrid/simgrid X-Git-Tag: v3.35~87 X-Git-Url: http://bilbo.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/eb115a05127cacf97d96dca1107ebfe60653e4bd Merge branch 'master' of https://framagit.org/simgrid/simgrid --- eb115a05127cacf97d96dca1107ebfe60653e4bd diff --cc src/mc/explo/DFSExplorer.cpp index 6fe0b46ab4,978cdfd1ef..033c525924 --- a/src/mc/explo/DFSExplorer.cpp +++ b/src/mc/explo/DFSExplorer.cpp @@@ -362,17 -348,13 +350,14 @@@ void DFSExplorer::backtrack( /** * ODPOR Race Detection Procedure: * - * For each reversible race in the current execution, we - * note if there are any continuations `C` equivalent to that which - * would reverse the race that have already either a) been searched by ODPOR or - * b) been *noted* to be searched by the wakeup tree at the - * appropriate reversal point, either as `C` directly or - * an as equivalent to `C` ("eventually looks like C", viz. the `~_E` - * relation) + * For each reversible race in the current execution, we note if there are any continuations `C` equivalent to that + * which would reverse the race that have already either a) been searched by ODPOR or b) been *noted* to be searched + * by the wakeup tree at the appropriate reversal point, either as `C` directly or an as equivalent to `C` + * ("eventually looks like C", viz. the `~_E` 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()) {