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
} // 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.
*/
{
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
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
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)
#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 {
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)
#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"
* @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();
}
/**
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]);
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);
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 */
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
"Simcall::COMM_TESTANY",
"Simcall::COND_WAIT",
"Simcall::COND_WAIT_TIMEOUT",
- "Simcall::SEM_ACQUIRE",
"Simcall::SEM_ACQUIRE_TIMEOUT",
"Simcall::RUN_KERNEL",
"Simcall::RUN_BLOCKING",
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;
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]];