Tell the MC transition about the semaphore capacity and use it

This info is mandatory to compute the reversible race of SemWait in ODPOR

diff --git a/src/kernel/actor/SynchroObserver.cpp b/src/kernel/actor/SynchroObserver.cpp
index efe5bff..4382ec4 100644 (file)
--- a/src/kernel/actor/SynchroObserver.cpp
+++ b/src/kernel/actor/SynchroObserver.cpp
@@ -31,7 +31,8 @@ void MutexObserver::serialize(std::stringstream& stream) const
 std::string MutexObserver::to_string() const
 {
   return std::string(mc::Transition::to_c_str(type_)) + "(mutex_id:" + std::to_string(get_mutex()->get_id()) +
-         " owner:" + std::to_string(get_mutex()->get_owner()->get_pid()) + ")";
+         " owner:" +
+         (get_mutex()->get_owner() == nullptr ? "none" : std::to_string(get_mutex()->get_owner()->get_pid())) + ")";
 }
 
 bool MutexObserver::is_enabled()
@@ -48,7 +49,8 @@ SemaphoreObserver::SemaphoreObserver(ActorImpl* actor, mc::Transition::Type type
 
 void SemaphoreObserver::serialize(std::stringstream& stream) const
 {
-  stream << (short)type_ << ' ' << get_sem()->get_id() << ' ' << false /* Granted is ignored for LOCK/UNLOCK */;
+  stream << (short)type_ << ' ' << get_sem()->get_id() << ' ' << false /* Granted is ignored for LOCK/UNLOCK */ << ' '
+         << get_sem()->get_capacity();
 }
 std::string SemaphoreObserver::to_string() const
 {
@@ -66,7 +68,8 @@ bool SemaphoreAcquisitionObserver::is_enabled()
 }
 void SemaphoreAcquisitionObserver::serialize(std::stringstream& stream) const
 {
-  stream << (short)type_ << ' ' << acquisition_->semaphore_->get_id() << ' ' << acquisition_->granted_;
+  stream << (short)type_ << ' ' << acquisition_->semaphore_->get_id() << ' ' << acquisition_->granted_ << ' '
+         << acquisition_->semaphore_->get_capacity();
 }
 std::string SemaphoreAcquisitionObserver::to_string() const
 {

diff --git a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
index 947ccc0..b20ebaa 100644 (file)
--- a/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
+++ b/src/mc/explo/odpor/ReversibleRaceCalculator.cpp
@@ -5,6 +5,8 @@
 
 #include "src/mc/explo/odpor/ReversibleRaceCalculator.hpp"
 #include "src/mc/explo/odpor/Execution.hpp"
+#include "src/mc/transition/Transition.hpp"
+#include "src/mc/transition/TransitionSynchro.hpp"
 
 #include <functional>
 #include <unordered_map>
@@ -160,11 +162,15 @@ bool ReversibleRaceCalculator::is_race_reversible_SemUnlock(const Execution&, Ex
   return true;
 }
 
-bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution&, Execution::EventHandle /*e1*/,
+bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, Execution::EventHandle e1,
                                                           const Transition* /*e2*/)
 {
-  // TODO: Get the semantics correct here
-  return false;
+  // Reversible with everynbody but unlock which creates a free token
+  const auto e1_transition = E.get_transition_for_handle(e1);
+  if (e1_transition->type_ == Transition::Type::SEM_UNLOCK &&
+      static_cast<const SemaphoreTransition*>(e1_transition)->get_capacity() == 0)
+    return false;
+  return true;
 }
 
 bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle /*e1*/,

diff --git a/src/mc/transition/TransitionSynchro.cpp b/src/mc/transition/TransitionSynchro.cpp
index db97fb8..469c71c 100644 (file)
--- a/src/mc/transition/TransitionSynchro.cpp
+++ b/src/mc/transition/TransitionSynchro.cpp
@@ -109,16 +109,16 @@ bool MutexTransition::depends(const Transition* o) const
 std::string SemaphoreTransition::to_string(bool verbose) const
 {
   if (type_ == Type::SEM_ASYNC_LOCK || type_ == Type::SEM_UNLOCK)
-    return xbt::string_printf("%s(semaphore: %u)", Transition::to_c_str(type_), sem_);
+    return xbt::string_printf("%s(semaphore: %u, capacity: %u)", Transition::to_c_str(type_), capacity_, sem_);
   if (type_ == Type::SEM_WAIT)
-    return xbt::string_printf("%s(semaphore: %u, granted: %s)", Transition::to_c_str(type_), sem_,
-                              granted_ ? "yes" : "no");
+    return xbt::string_printf("%s(semaphore: %u, capacity: %u, granted: %s)", Transition::to_c_str(type_), capacity_,
+                              sem_, granted_ ? "yes" : "no");
   THROW_IMPOSSIBLE;
 }
 SemaphoreTransition::SemaphoreTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream)
     : Transition(type, issuer, times_considered)
 {
-  xbt_assert(stream >> sem_ >> granted_);
+  xbt_assert(stream >> sem_ >> granted_ >> capacity_);
 }
 bool SemaphoreTransition::depends(const Transition* o) const
 {

diff --git a/src/mc/transition/TransitionSynchro.hpp b/src/mc/transition/TransitionSynchro.hpp
index 66ed64c..a4ea7e3 100644 (file)
--- a/src/mc/transition/TransitionSynchro.hpp
+++ b/src/mc/transition/TransitionSynchro.hpp
@@ -37,11 +37,13 @@ public:
 class SemaphoreTransition : public Transition {
   unsigned int sem_; // ID
   bool granted_;
+  unsigned capacity_;
 
 public:
   std::string to_string(bool verbose) const override;
   SemaphoreTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream);
   bool depends(const Transition* other) const override;
+  int get_capacity() const { return capacity_; }
 };
 
 } // namespace simgrid::mc