- mc::MutexLockSimcall observer{issuer, pimpl_};
- kernel::actor::simcall_blocking<void>([&observer] { observer.get_mutex()->lock(observer.get_issuer()); }, &observer);
+
+ if (MC_is_active() || MC_record_replay_is_active()) { // Split in 2 simcalls for transition persistency
+ kernel::actor::MutexObserver lock_observer{issuer, mc::Transition::Type::MUTEX_ASYNC_LOCK, pimpl_};
+ auto acquisition =
+ kernel::actor::simcall_answered([issuer, this] { return pimpl_->lock_async(issuer); }, &lock_observer);
+
+ kernel::actor::MutexObserver wait_observer{issuer, mc::Transition::Type::MUTEX_WAIT, pimpl_};
+ kernel::actor::simcall_blocking([issuer, &acquisition] { acquisition->wait_for(issuer, -1); }, &wait_observer);
+
+ } else { // Do it in one simcall only
+ kernel::actor::simcall_blocking([issuer, this] { pimpl_->lock_async(issuer)->wait_for(issuer, -1); });
+ }