Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Modernize simcall sem_acquire.
authorArnaud Giersch <arnaud.giersch@univ-fcomte.fr>
Sat, 13 Mar 2021 21:25:04 +0000 (22:25 +0100)
committerArnaud Giersch <arnaud.giersch@univ-fcomte.fr>
Sat, 13 Mar 2021 21:25:04 +0000 (22:25 +0100)
12 files changed:
include/simgrid/simix.h
src/kernel/activity/SemaphoreImpl.cpp
src/mc/checker/SimcallObserver.cpp
src/mc/checker/SimcallObserver.hpp
src/mc/mc_base.cpp
src/s4u/s4u_Semaphore.cpp
src/simix/libsmx.cpp
src/simix/popping_accessors.hpp
src/simix/popping_bodies.cpp
src/simix/popping_enum.hpp
src/simix/popping_generated.cpp
src/simix/simcalls.in

index b7efc34..87bdc50 100644 (file)
@@ -207,7 +207,7 @@ XBT_ATTRIB_DEPRECATED_v330("Please use sg_cond_init()") XBT_PUBLIC smx_cond_t si
 XBT_PUBLIC void simcall_cond_wait(smx_cond_t cond, smx_mutex_t mutex);
 XBT_PUBLIC int simcall_cond_wait_timeout(smx_cond_t cond, smx_mutex_t mutex, double max_duration);
 
-XBT_PUBLIC void simcall_sem_acquire(smx_sem_t sem);
+XBT_ATTRIB_DEPRECATED_v331("Please use sg_sem_acquire()") XBT_PUBLIC void simcall_sem_acquire(smx_sem_t sem);
 XBT_PUBLIC int simcall_sem_acquire_timeout(smx_sem_t sem, double max_duration);
 SG_END_DECL
 
index fbfffa1..ec75b82 100644 (file)
@@ -61,14 +61,6 @@ void SemaphoreImpl::unref()
 } // namespace simgrid
 
 // Simcall handlers:
-/**
- * @brief Handles a sem acquire simcall without timeout.
- */
-void simcall_HANDLER_sem_acquire(smx_simcall_t simcall, smx_sem_t sem)
-{
-  sem->acquire(simcall->issuer_, -1);
-}
-
 /**
  * @brief Handles a sem acquire simcall with timeout.
  */
index 3b7854c..3dd9d0e 100644 (file)
@@ -75,5 +75,25 @@ bool MutexLockSimcall::is_enabled() const
 {
   return not blocking_ || mutex_->get_owner() == nullptr || mutex_->get_owner() == get_issuer();
 }
+
+std::string SemAcquireSimcall::to_string(int time_considered) const
+{
+  return SimcallObserver::to_string(time_considered) + "Sem ACQUIRE";
+}
+
+std::string SemAcquireSimcall::dot_label() const
+{
+  return SimcallObserver::dot_label() + "Sem ACQUIRE";
+}
+
+bool SemAcquireSimcall::is_enabled() const
+{
+  static bool warned = false;
+  if (not warned) {
+    XBT_INFO("Using semaphore in model-checked code is still experimental. Use at your own risk");
+    warned = true;
+  }
+  return true;
+}
 } // namespace mc
 } // namespace simgrid
index 70efba4..2dec907 100644 (file)
@@ -88,6 +88,18 @@ public:
   std::string dot_label() const override;
   kernel::activity::MutexImpl* get_mutex() const { return mutex_; }
 };
+
+class SemAcquireSimcall : public SimcallObserver {
+  kernel::activity::SemaphoreImpl* const sem_;
+
+public:
+  SemAcquireSimcall(smx_actor_t actor, kernel::activity::SemaphoreImpl* sem) : SimcallObserver(actor), sem_(sem) {}
+  bool is_enabled() const override;
+  bool is_visible() const override { return false; }
+  std::string to_string(int times_considered) const override;
+  std::string dot_label() const override;
+  kernel::activity::SemaphoreImpl* get_sem() const { return sem_; }
+};
 } // namespace mc
 } // namespace simgrid
 
index d678be4..546b67e 100644 (file)
@@ -125,14 +125,6 @@ bool actor_is_enabled(smx_actor_t actor)
       return false;
     }
 
-    case Simcall::SEM_ACQUIRE: {
-      static bool warned = false;
-      if (not warned)
-        XBT_INFO("Using semaphore in model-checked code is still experimental. Use at your own risk");
-      warned = true;
-      return true;
-    }
-
     case Simcall::COND_WAIT: {
       static bool warned = false;
       if (not warned)
index b2482ed..908378c 100644 (file)
@@ -9,6 +9,7 @@
 #include "simgrid/forward.h"
 #include "simgrid/s4u/Semaphore.hpp"
 #include "src/kernel/activity/SemaphoreImpl.hpp"
+#include "src/mc/checker/SimcallObserver.hpp"
 
 namespace simgrid {
 namespace s4u {
@@ -21,7 +22,10 @@ SemaphorePtr Semaphore::create(unsigned int initial_capacity)
 
 void Semaphore::acquire()
 {
-  simcall_sem_acquire(pimpl_);
+  kernel::actor::ActorImpl* issuer = kernel::actor::ActorImpl::self();
+  mc::SemAcquireSimcall observer{issuer, pimpl_};
+  kernel::actor::simcall_blocking<void>([&observer] { observer.get_sem()->acquire(observer.get_issuer(), -1.0); },
+                                        &observer);
 }
 
 bool Semaphore::acquire_timeout(double timeout)
index 2e8c87d..cd8b9df 100644 (file)
@@ -18,6 +18,7 @@
 #include "src/kernel/activity/IoImpl.hpp"
 #include "src/kernel/activity/MailboxImpl.hpp"
 #include "src/kernel/activity/MutexImpl.hpp"
+#include "src/kernel/activity/SemaphoreImpl.hpp"
 #include "src/mc/checker/SimcallObserver.hpp"
 #include "src/mc/mc_replay.hpp"
 #include "src/plugins/vm/VirtualMachineImpl.hpp"
@@ -310,9 +311,9 @@ int simcall_cond_wait_timeout(smx_cond_t cond, smx_mutex_t mutex, double timeout
  * @ingroup simix_synchro_management
  *
  */
-void simcall_sem_acquire(smx_sem_t sem)
+void simcall_sem_acquire(smx_sem_t sem) // XBT_ATTRIB_DEPRECATD_v331
 {
-  simcall_BODY_sem_acquire(sem);
+  return sem->sem().acquire();
 }
 
 /**
index 091a7cc..6ee3f88 100644 (file)
@@ -758,19 +758,6 @@ static inline void simcall_cond_wait_timeout__set__result(smx_simcall_t simcall,
   simgrid::simix::marshal<int>(simcall->result_, result);
 }
 
-static inline smx_sem_t simcall_sem_acquire__get__sem(smx_simcall_t simcall)
-{
-  return simgrid::simix::unmarshal<smx_sem_t>(simcall->args_[0]);
-}
-static inline smx_sem_t simcall_sem_acquire__getraw__sem(smx_simcall_t simcall)
-{
-  return simgrid::simix::unmarshal_raw<smx_sem_t>(simcall->args_[0]);
-}
-static inline void simcall_sem_acquire__set__sem(smx_simcall_t simcall, smx_sem_t arg)
-{
-  simgrid::simix::marshal<smx_sem_t>(simcall->args_[0], arg);
-}
-
 static inline smx_sem_t simcall_sem_acquire_timeout__get__sem(smx_simcall_t simcall)
 {
   return simgrid::simix::unmarshal<smx_sem_t>(simcall->args_[0]);
@@ -847,5 +834,4 @@ XBT_PRIVATE void simcall_HANDLER_comm_test(smx_simcall_t simcall, simgrid::kerne
 XBT_PRIVATE void simcall_HANDLER_comm_testany(smx_simcall_t simcall, simgrid::kernel::activity::CommImpl** comms, size_t count);
 XBT_PRIVATE void simcall_HANDLER_cond_wait(smx_simcall_t simcall, smx_cond_t cond, smx_mutex_t mutex);
 XBT_PRIVATE void simcall_HANDLER_cond_wait_timeout(smx_simcall_t simcall, smx_cond_t cond, smx_mutex_t mutex, double timeout);
-XBT_PRIVATE void simcall_HANDLER_sem_acquire(smx_simcall_t simcall, smx_sem_t sem);
 XBT_PRIVATE void simcall_HANDLER_sem_acquire_timeout(smx_simcall_t simcall, smx_sem_t sem, double timeout);
index fc04c38..9f69d93 100644 (file)
@@ -118,13 +118,6 @@ inline static int simcall_BODY_cond_wait_timeout(smx_cond_t cond, smx_mutex_t mu
   return simcall<int, smx_cond_t, smx_mutex_t, double>(Simcall::COND_WAIT_TIMEOUT, cond, mutex, timeout);
 }
 
-inline static void simcall_BODY_sem_acquire(smx_sem_t sem)
-{
-  if (false) /* Go to that function to follow the code flow through the simcall barrier */
-    simcall_HANDLER_sem_acquire(&SIMIX_process_self()->simcall_, sem);
-  return simcall<void, smx_sem_t>(Simcall::SEM_ACQUIRE, sem);
-}
-
 inline static int simcall_BODY_sem_acquire_timeout(smx_sem_t sem, double timeout)
 {
   if (false) /* Go to that function to follow the code flow through the simcall barrier */
index 5e21f81..050d04c 100644 (file)
@@ -32,12 +32,11 @@ enum class Simcall {
   COMM_TESTANY,
   COND_WAIT,
   COND_WAIT_TIMEOUT,
-  SEM_ACQUIRE,
   SEM_ACQUIRE_TIMEOUT,
   RUN_KERNEL,
   RUN_BLOCKING,
 };
 
-constexpr int NUM_SIMCALLS = 16;
+constexpr int NUM_SIMCALLS = 15;
 } // namespace simix
 } // namespace simgrid
index 8f47b97..b3f1b8a 100644 (file)
@@ -40,7 +40,6 @@ constexpr std::array<const char*, simgrid::simix::NUM_SIMCALLS> simcall_names{{
     "Simcall::COMM_TESTANY",
     "Simcall::COND_WAIT",
     "Simcall::COND_WAIT_TIMEOUT",
-    "Simcall::SEM_ACQUIRE",
     "Simcall::SEM_ACQUIRE_TIMEOUT",
     "Simcall::RUN_KERNEL",
     "Simcall::RUN_BLOCKING",
@@ -106,10 +105,6 @@ void simgrid::kernel::actor::ActorImpl::simcall_handle(int times_considered_)
       simcall_HANDLER_cond_wait_timeout(&simcall_, simgrid::simix::unmarshal<smx_cond_t>(simcall_.args_[0]), simgrid::simix::unmarshal<smx_mutex_t>(simcall_.args_[1]), simgrid::simix::unmarshal<double>(simcall_.args_[2]));
       break;
 
-    case Simcall::SEM_ACQUIRE:
-      simcall_HANDLER_sem_acquire(&simcall_, simgrid::simix::unmarshal<smx_sem_t>(simcall_.args_[0]));
-      break;
-
     case Simcall::SEM_ACQUIRE_TIMEOUT:
       simcall_HANDLER_sem_acquire_timeout(&simcall_, simgrid::simix::unmarshal<smx_sem_t>(simcall_.args_[0]), simgrid::simix::unmarshal<double>(simcall_.args_[1]));
       break;
index d83300b..6ea13d2 100644 (file)
@@ -49,7 +49,6 @@ int            comm_testany(simgrid::kernel::activity::CommImpl** comms, size_t
 void       cond_wait(smx_cond_t cond, smx_mutex_t mutex) [[block]];
 int        cond_wait_timeout(smx_cond_t cond, smx_mutex_t mutex, double timeout) [[block]];
 
-void      sem_acquire(smx_sem_t sem) [[block]];
 int       sem_acquire_timeout(smx_sem_t sem, double timeout) [[block]];
 
 void       run_kernel(std::function<void()> const* code) [[nohandler]];