source
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

Instances For

source
instance Std.instNonemptyBaseRecursiveMutex :
Nonempty BaseRecursiveMutex
source
@[extern lean_io_baserecmutex_new]
opaque Std.BaseRecursiveMutex.new :
BaseIO BaseRecursiveMutex

Creates a new `BaseRecursiveMutex`.

source
@[extern lean_io_baserecmutex_lock]
opaque Std.BaseRecursiveMutex.lock (mutex : BaseRecursiveMutex) :
BaseIO Unit

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

source
@[extern lean_io_baserecmutex_try_lock]
opaque Std.BaseRecursiveMutex.tryLock (mutex : BaseRecursiveMutex) :
BaseIO Bool

Attempts to lock a `BaseRecursiveMutex`. 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.

source
@[extern lean_io_baserecmutex_unlock]
opaque Std.BaseRecursiveMutex.unlock (mutex : BaseRecursiveMutex) :
BaseIO Unit

Unlocks a `BaseRecursiveMutex`. 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).

source
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

Instances For

source
instance Std.instNonemptyRecursiveMutex {α✝ : Type} [Nonempty α✝] :
Nonempty (RecursiveMutex α✝)
source
instance Std.instCoeOutRecursiveMutexBaseRecursiveMutex {α : Type} :
CoeOut (RecursiveMutex α) BaseRecursiveMutex
Equations

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

source
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 }

Instances For

source
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)

Instances For

source
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

- mutex.tryAtomically k = do let __do_lift ← liftM mutex.mutex.tryLock if __do_lift = true then tryFinally (some <$> k (Std.RecursiveMutex.ref✝ mutex)) (liftM mutex.mutex.unlock) else pure none

Instances For