Align the behavior of MC and MC_replay in SMPI, so that replay actually works

[simgrid.git] / src / mc / transition / TransitionSynchro.cpp

diff --git a/src/mc/transition/TransitionSynchro.cpp b/src/mc/transition/TransitionSynchro.cpp
index 8813a15..09de8ee 100644 (file)
--- a/src/mc/transition/TransitionSynchro.cpp
+++ b/src/mc/transition/TransitionSynchro.cpp
@@ -13,8 +13,40 @@
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_trans_synchro, mc_transition, "Logging specific to MC synchronization transitions");
 
-namespace simgrid {
-namespace mc {
+namespace simgrid::mc {
+
+std::string BarrierTransition::to_string(bool verbose) const
+{
+  return xbt::string_printf("%s(barrier: %u)", Transition::to_c_str(type_), bar_);
+}
+BarrierTransition::BarrierTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream)
+    : Transition(type, issuer, times_considered)
+{
+  xbt_assert(stream >> bar_);
+}
+bool BarrierTransition::depends(const Transition* o) const
+{
+  if (o->type_ < type_)
+    return o->depends(this);
+
+  if (auto* other = dynamic_cast<const BarrierTransition*>(o)) {
+    if (bar_ != other->bar_)
+      return false;
+
+    // LOCK indep LOCK: requests are not ordered in a barrier
+    if (type_ == Type::BARRIER_ASYNC_LOCK && other->type_ == Type::BARRIER_ASYNC_LOCK)
+      return false;
+
+    // WAIT indep WAIT: requests are not ordered
+    if (type_ == Type::BARRIER_WAIT && other->type_ == Type::BARRIER_WAIT)
+      return false;
+
+    return true; // LOCK/WAIT is dependent because lock may enable wait
+  }
+
+  return false; // barriers are INDEP with non-barrier transitions
+}
+
 std::string MutexTransition::to_string(bool verbose) const
 {
   return xbt::string_printf("%s(mutex: %" PRIxPTR ", owner:%ld)", Transition::to_c_str(type_), mutex_, owner_);
@@ -40,12 +72,12 @@ bool MutexTransition::depends(const Transition* o) const
 
     // Theorem 4.4.11: LOCK indep TEST/WAIT.
     //  If both enabled, the result does not depend on their order. If WAIT is not enabled, LOCK won't enable it.
-    if (type_ == Type::MUTEX_LOCK && (other->type_ == Type::MUTEX_TEST || other->type_ == Type::MUTEX_WAIT))
+    if (type_ == Type::MUTEX_ASYNC_LOCK && (other->type_ == Type::MUTEX_TEST || other->type_ == Type::MUTEX_WAIT))
       return false;
 
     // Theorem 4.4.8: LOCK indep UNLOCK.
     //  pop_front and push_back are independent.
-    if (type_ == Type::MUTEX_LOCK && other->type_ == Type::MUTEX_UNLOCK)
+    if (type_ == Type::MUTEX_ASYNC_LOCK && other->type_ == Type::MUTEX_UNLOCK)
       return false;
 
     // TEST is a pure function; TEST/WAIT won't change the owner; TRYLOCK will always fail if TEST is enabled (because a
@@ -68,7 +100,7 @@ bool MutexTransition::depends(const Transition* o) const
 
 std::string SemaphoreTransition::to_string(bool verbose) const
 {
-  if (type_ == Type::SEM_LOCK || type_ == Type::SEM_UNLOCK)
+  if (type_ == Type::SEM_ASYNC_LOCK || type_ == Type::SEM_UNLOCK)
     return xbt::string_printf("%s(semaphore: %" PRIxPTR ")", Transition::to_c_str(type_), sem_);
   if (type_ == Type::SEM_WAIT)
     return xbt::string_printf("%s(semaphore: %" PRIxPTR ", granted: %s)", Transition::to_c_str(type_), sem_,
@@ -90,12 +122,12 @@ bool SemaphoreTransition::depends(const Transition* o) const
       return false;
 
     // LOCK indep UNLOCK: pop_front and push_back are independent.
-    if (type_ == Type::SEM_LOCK && other->type_ == Type::SEM_UNLOCK)
+    if (type_ == Type::SEM_ASYNC_LOCK && other->type_ == Type::SEM_UNLOCK)
       return false;
 
     // LOCK indep WAIT: If both enabled, ordering has no impact on the result. If WAIT is not enabled, LOCK won't enable
     // it.
-    if (type_ == Type::SEM_LOCK && other->type_ == Type::SEM_WAIT)
+    if (type_ == Type::SEM_ASYNC_LOCK && other->type_ == Type::SEM_WAIT)
       return false;
 
     // UNLOCK indep UNLOCK: ordering of two pop_front has no impact
@@ -115,5 +147,4 @@ bool SemaphoreTransition::depends(const Transition* o) const
   return false; // semaphores are INDEP with non-semaphore transitions
 }
 
-} // namespace mc
-} // namespace simgrid
+} // namespace simgrid::mc