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 96f19ca..246b3f0 100644 (file)
--- a/src/mc/transition/Transition.hpp
+++ b/src/mc/transition/Transition.hpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2015-2022. The SimGrid Team. All rights reserved.          */
+/* Copyright (c) 2015-2023. The SimGrid Team. All rights reserved.          */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
@@ -7,13 +7,13 @@
 #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>
 #include <string>
 
-namespace simgrid {
-namespace mc {
+namespace simgrid::mc {
 
 /** An element in the recorded path
  *
@@ -24,7 +24,7 @@ namespace mc {
  *  calls.
  */
 class Transition {
-  /* Textual representation of the transition, to display backtraces */
+  /* Global statistics */
   static unsigned long executed_transitions_;
   static unsigned long replayed_transitions_;
 
@@ -32,15 +32,30 @@ class Transition {
 
 public:
   /* Ordering is important here. depends() implementations only consider subsequent types in this ordering */
-  XBT_DECLARE_ENUM_CLASS(Type, RANDOM,     /* First because indep with anybody */
-                         TESTANY, WAITANY, /* high priority because they can rewrite themselves to *_WAIT */
-                         COMM_RECV, COMM_SEND, COMM_TEST, COMM_WAIT, /* Alphabetical ordering of COMM_* */
-                         MUTEX_LOCK, MUTEX_TEST, MUTEX_TRYLOCK, MUTEX_UNLOCK, MUTEX_WAIT, /* alphabetical */
-                         /* 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;
 
+  /** The user function call that caused this transition to exist. Format: >>filename:line:function()<< */
+  std::string call_location_ = "";
+
   /* Which transition was executed for this simcall
    *
    * Some simcalls can lead to different transitions:
@@ -63,11 +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 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() const;
+  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) */
@@ -77,7 +109,6 @@ public:
 /** Make a new transition from serialized description */
 Transition* deserialize_transition(aid_t issuer, int times_considered, std::stringstream& stream);
 
-} // namespace mc
-} // namespace simgrid
+} // namespace simgrid::mc
 
 #endif