- mc::SemAcquireSimcall observer{issuer, pimpl_, timeout};
- return kernel::actor::simcall_blocking(
- [&observer] { observer.get_sem()->acquire(observer.get_issuer(), observer.get_timeout()); }, &observer);
+
+ if (MC_is_active() || MC_record_replay_is_active()) { // Split in 2 simcalls for transition persistency
+ kernel::actor::SemaphoreObserver lock_observer{issuer, mc::Transition::Type::SEM_ASYNC_LOCK, pimpl_};
+ auto acquisition =
+ kernel::actor::simcall_answered([issuer, this] { return pimpl_->acquire_async(issuer); }, &lock_observer);
+
+ kernel::actor::SemaphoreAcquisitionObserver wait_observer{issuer, mc::Transition::Type::SEM_WAIT, acquisition.get(),
+ timeout};
+ return kernel::actor::simcall_blocking([issuer, acquisition, timeout] { acquisition->wait_for(issuer, timeout); },
+ &wait_observer);
+
+ } else { // Do it in one simcall only and without observer
+ kernel::actor::SemaphoreAcquisitionObserver observer{issuer, mc::Transition::Type::SEM_WAIT, nullptr, timeout};
+ return kernel::actor::simcall_blocking(
+ [this, issuer, timeout] { pimpl_->acquire_async(issuer)->wait_for(issuer, timeout); }, &observer);
+ }