def Std.BaseRecursiveMutex : Type

Recursive (or reentrant) exclusion primitive.

If you want to guard shared state, use RecursiveMutex α instead.

Equations

• Std.BaseRecursiveMutex = Std.RecursiveMutexImpl✝.type

instance Std.instNonemptyBaseRecursiveMutex : Nonempty BaseRecursiveMutex

@[extern lean_io_baserecmutex_new]

opaque Std.BaseRecursiveMutex.new : BaseIO BaseRecursiveMutex

Creates a new BaseRecursiveMutex.

@[extern lean_io_baserecmutex_lock]

opaque Std.BaseRecursiveMutex.lock (mutex : BaseRecursiveMutex) : BaseIO Unit

Locks a RecursiveBaseMutex. Waits until no other thread has locked the mutex. If the current thread already holds the mutex this function doesn't block.

@[extern lean_io_baserecmutex_try_lock]

opaque Std.BaseRecursiveMutex.tryLock (mutex : BaseRecursiveMutex) : BaseIO Bool

Attempts to lock a RecursiveBaseMutex. If the mutex is not available return false, otherwise lock it and return true.

This function does not block. Furthermore the same thread may acquire the lock multiple times through this function.

@[extern lean_io_baserecmutex_unlock]

opaque Std.BaseRecursiveMutex.unlock (mutex : BaseRecursiveMutex) : BaseIO Unit

Unlocks a RecursiveBaseMutex. The owning thread must make as many unlock calls as lock and tryLock calls in order to fully relinquish ownership of the mutex.

The current thread must have already locked the mutex at least once. Unlocking an unlocked mutex is undefined behavior (inherited from the C++ implementation).

structure Std.RecursiveMutex (α : Type) : Type

Recursive (or reentrant) mutual exclusion primitive (lock) guarding shared state of type α.

The type RecursiveMutex α is similar to IO.Ref α, except that concurrent accesses are guarded by a mutex instead of atomic pointer operations and busy-waiting. Additionally locking a RecursiveMutex multiple times from the same thread does not block, unlike Mutex.

• ref : IO.Ref α
• mutex : BaseRecursiveMutex

instance Std.instNonemptyRecursiveMutex {α✝ : Type} [Nonempty α✝] : Nonempty (RecursiveMutex α✝)

instance Std.instCoeOutRecursiveMutexBaseRecursiveMutex {α : Type} : CoeOut (RecursiveMutex α) BaseRecursiveMutex

Equations

• Std.instCoeOutRecursiveMutexBaseRecursiveMutex = { coe := Std.RecursiveMutex.mutex }

def Std.RecursiveMutex.new {α : Type} (a : α) : BaseIO (RecursiveMutex α)

Creates a new recursive mutex.

Equations

• Std.RecursiveMutex.new a = do let __do_lift ← IO.mkRef a let __do_lift_1 ← Std.BaseRecursiveMutex.new pure { ref := __do_lift, mutex := __do_lift_1 }

def Std.RecursiveMutex.atomically {m : Type → Type} {α β : Type} [Monad m] [MonadLiftT BaseIO m] [MonadFinally m] (mutex : RecursiveMutex α) (k : AtomicT α m β) : m β

mutex.atomically k runs k with access to the mutex's state while locking the mutex.

Calling mutex.atomically while already holding the underlying BaseRecursiveMutex in the same thread does not block.

Equations

• mutex.atomically k = tryFinally (do liftM mutex.mutex.lock k (Std.RecursiveMutex.ref✝ mutex)) (liftM mutex.mutex.unlock)

def Std.RecursiveMutex.tryAtomically {m : Type → Type} {α β : Type} [Monad m] [MonadLiftT BaseIO m] [MonadFinally m] (mutex : RecursiveMutex α) (k : AtomicT α m β) : m (Option β)

mutex.tryAtomically k tries to lock mutex and runs k on it if it succeeds. On success the return value of k is returned as some, on failure none is returned.

This function does not block on the mutex. Additionally mutex.tryAtomically, while already holding the underlying BaseRecursiveMutex in the same thread, does not block.

Equations

• One or more equations did not get rendered due to their size.