MC: move the reversible_race logic to the Transition class

[simgrid.git] / src / mc / transition / Transition.hpp

diff --git a/src/mc/transition/Transition.hpp b/src/mc/transition/Transition.hpp
index 6beb8af..246b3f0 100644 (file)
--- a/src/mc/transition/Transition.hpp
+++ b/src/mc/transition/Transition.hpp
@@ -7,6 +7,7 @@
 #define SIMGRID_MC_TRANSITION_HPP
 
 #include "simgrid/forward.h" // aid_t
+#include "xbt/ex.h"
 #include "xbt/utility.hpp"   // XBT_DECLARE_ENUM_CLASS
 
 #include <sstream>
@@ -23,21 +24,31 @@ namespace simgrid::mc {
  *  calls.
  */
 class Transition {
-  /* Textual representation of the transition, to display backtraces */
+  /* Global statistics */
   static unsigned long executed_transitions_;
   static unsigned long replayed_transitions_;
 
   friend State; // FIXME remove this once we have a proper class to handle the statistics
+
 public:
   /* Ordering is important here. depends() implementations only consider subsequent types in this ordering */
-  XBT_DECLARE_ENUM_CLASS(Type, RANDOM, ACTOR_JOIN, /* First because indep with anybody including themselves */
-                         OBJECT_ACCESS,            /* high priority because indep with almost everybody */
-                         TESTANY, WAITANY,         /* high priority because they can rewrite themselves to *_WAIT */
-                         BARRIER_ASYNC_LOCK, BARRIER_WAIT, /* BARRIER transitions sorted alphabetically */
-                         COMM_ASYNC_RECV, COMM_ASYNC_SEND, COMM_TEST, COMM_WAIT, /* Alphabetical ordering of COMM_* */
-                         MUTEX_ASYNC_LOCK, MUTEX_TEST, MUTEX_TRYLOCK, MUTEX_UNLOCK, MUTEX_WAIT, /* alphabetical */
-                         SEM_ASYNC_LOCK, SEM_UNLOCK, SEM_WAIT, /* alphabetical ordering of SEM transitions */
-                         /* UNKNOWN must be last */ UNKNOWN);
+  XBT_DECLARE_ENUM_CLASS(Type,
+                         /* First because indep with anybody including themselves */
+                         RANDOM, ACTOR_JOIN, ACTOR_SLEEP,
+                         /* high priority because indep with almost everybody */
+                         OBJECT_ACCESS,
+                         /* high priority because they can rewrite themselves to *_WAIT */
+                         TESTANY, WAITANY,
+                         /* BARRIER transitions sorted alphabetically */
+                         BARRIER_ASYNC_LOCK, BARRIER_WAIT,
+                         /* Alphabetical ordering of COMM_* */
+                         COMM_ASYNC_RECV, COMM_ASYNC_SEND, COMM_TEST, COMM_WAIT,
+                         /* alphabetical */
+                         MUTEX_ASYNC_LOCK, MUTEX_TEST, MUTEX_TRYLOCK, MUTEX_UNLOCK, MUTEX_WAIT,
+                         /* alphabetical ordering of SEM transitions */
+                         SEM_ASYNC_LOCK, SEM_UNLOCK, SEM_WAIT,
+                         /* UNKNOWN must be last */
+                         UNKNOWN);
   Type type_ = Type::UNKNOWN;
 
   aid_t aid_ = 0;
@@ -67,13 +78,28 @@ public:
   /** Returns something like >>label = "desc", color = c<< to describe the transition in dot format */
   virtual std::string dot_string() const;
 
-  std::string get_call_location() { return call_location_; }
+  std::string const& get_call_location() const { return call_location_; }
 
   /* Moves the application toward a path that was already explored, but don't change the current transition */
   void replay(RemoteApp& app) const;
 
   virtual bool depends(const Transition* other) const { return true; }
 
+  /**
+   The reversible race detector should only be used if we already have the assumption
+   this <* other (see Source set: a foundation for ODPOR). In particular this means that :
+   - this -->_E other
+   - proc(this) != proc(other)
+   - there is no event e s.t. this --> e --> other
+
+    @note: It is safe to assume that there is indeed a race between the two events in the execution;
+     indeed, the question the method answers is only sensible in the context of a race
+  */
+  virtual bool reversible_race(const Transition* other) const
+  {
+    xbt_die("%s unimplemented for %s", __func__, to_c_str(type_));
+  }
+
   /* Returns the total amount of transitions executed so far (for statistics) */
   static unsigned long get_executed_transitions() { return executed_transitions_; }
   /* Returns the total amount of transitions replayed so far while backtracing (for statistics) */