Add debug log for ODPOR + required explaining comments

diff --git a/src/mc/explo/DFSExplorer.cpp b/src/mc/explo/DFSExplorer.cpp
index f82d8da..6fe0b46 100644 (file)
--- 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<odpor::Execution::EventHandle>(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 162425d..8b531ff 100644 (file)
--- a/src/mc/explo/odpor/Execution.cpp
+++ b/src/mc/explo/odpor/Execution.cpp
@@ -12,6 +12,8 @@
 #include <limits>
 #include <vector>
 
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_execution, mc_dfs, "ODPOR exploration algorithm of the model-checker");
+
 namespace simgrid::mc::odpor {
 
 std::vector<std::string> get_textual_trace(const PartialExecution& w)
@@ -64,18 +66,22 @@ std::vector<std::string> Execution::get_textual_trace() const
 std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
 {
   std::unordered_set<Execution::EventHandle> racing_events;
+  // This keep tracks of events that happens-before the target
   std::unordered_set<Execution::EventHandle> disqualified_events;
 
   // For each event of the execution
   for (auto e_i = target; e_i != std::numeric_limits<Execution::EventHandle>::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::EventHandle> 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::EventHandle> 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 947ccc0..f6007c2 100644 (file)
--- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
+++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
@@ -11,8 +11,18 @@
 #include <xbt/asserts.h>
 #include <xbt/ex.h>
 
+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 bd57886..5e7ded2 100644 (file)
--- 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<const SemaphoreTransition*>(o)) {
     if (sem_ != other->sem_)
       return false;