source
def Std.BaseSharedMutex :
Type

An exclusion primitive that allows a number of readers or at most one writer.

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

Equations

- Std.BaseSharedMutex = Std.SharedMutexImpl✝.type

Instances For

source
instance Std.instNonemptyBaseSharedMutex :
Nonempty BaseSharedMutex
source
@[extern lean_io_basesharedmutex_new]
opaque Std.BaseSharedMutex.new :
BaseIO BaseSharedMutex

Creates a new `BaseSharedMutex`.

source
@[extern lean_io_basesharedmutex_write]
opaque Std.BaseSharedMutex.write (mutex : BaseSharedMutex) :
BaseIO Unit

Locks a `BaseSharedMutex` for exclusive write access. This function blocks until no other writers or readers have access to the lock.

The current thread must not have already locked the mutex. Reentrant locking is undefined behavior (inherited from the C++ implementation).

source
@[extern lean_io_basesharedmutex_try_write]
opaque Std.BaseSharedMutex.tryWrite (mutex : BaseSharedMutex) :
BaseIO Bool

Attempts to lock a `BaseSharedMutex` for exclusive write access. If the mutex is not available return `false`, otherwise lock it and return `true`.

The current thread must not have already locked the mutex. Reentrant locking is undefined behavior (inherited from the C++ implementation).

source
@[extern lean_io_basesharedmutex_unlock_write]
opaque Std.BaseSharedMutex.unlockWrite (mutex : BaseSharedMutex) :
BaseIO Unit

Unlocks a `BaseSharedMutex` write lock.

The current thread must have already locked the mutex for write access. Unlocking an unlocked mutex is undefined behavior (inherited from the C++ implementation).

source
@[extern lean_io_basesharedmutex_read]
opaque Std.BaseSharedMutex.read (mutex : BaseSharedMutex) :
BaseIO Unit

Locks a `BaseSharedMutex` for shared read access. This function blocks until there are no more writers which hold the lock. There may be other readers currently inside the lock when this method returns.

The current thread must not have already locked the mutex. Reentrant locking is undefined behavior (inherited from the C++ implementation).

source
@[extern lean_io_basesharedmutex_try_read]
opaque Std.BaseSharedMutex.tryRead (mutex : BaseSharedMutex) :
BaseIO Bool

Attempts to lock a `BaseSharedMutex` for shared read access. If the mutex is not available return `false`, otherwise lock it and return `true`.

The current thread must not have already locked the mutex. Reentrant locking is undefined behavior (inherited from the C++ implementation).

source
@[extern lean_io_basesharedmutex_unlock_read]
opaque Std.BaseSharedMutex.unlockRead (mutex : BaseSharedMutex) :
BaseIO Unit

Unlocks a `BaseSharedMutex` read lock.

The current thread must have already locked the mutex for read access. Unlocking an unlocked mutex is undefined behavior (inherited from the C++ implementation).

source
structure Std.SharedMutex (α : Type) :
Type

An exclusion primitive that allows a number of readers or at most one writer access to a shared state of type `α`.

- ref : IO.Ref α
- mutex : BaseSharedMutex

Instances For

source
instance Std.instNonemptySharedMutex {α✝ : Type} [Nonempty α✝] :
Nonempty (SharedMutex α✝)
source
instance Std.instCoeOutSharedMutexBaseSharedMutex {α : Type} :
CoeOut (SharedMutex α) BaseSharedMutex
Equations

- Std.instCoeOutSharedMutexBaseSharedMutex = { coe := Std.SharedMutex.mutex }

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

Creates a new shared mutex.

Equations

- Std.SharedMutex.new a = do let __do_lift ← IO.mkRef a let __do_lift_1 ← Std.BaseSharedMutex.new pure { ref := __do_lift, mutex := __do_lift_1 }

Instances For

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

`mutex.atomically k` runs `k` with read and write access to the mutex's state while locking the mutex for exclusive write access.

Calling `mutex.atomically` while already holding the underlying `BaseSharedMutex` in the same thread is undefined behavior.

Equations

- mutex.atomically k = tryFinally (do liftM mutex.mutex.write k (Std.SharedMutex.ref✝ mutex)) (liftM mutex.mutex.unlockWrite)

Instances For

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

`mutex.tryAtomically k` tries to lock `mutex` for exclusive write access and runs `k` with read and write access to the mutex's state if it succeeds. If successful, it returns the value of `k` as `some`, otherwise `none`.

Calling `mutex.tryAtomically` while already holding the underlying `BaseSharedMutex` in the same thread is undefined behavior.

Equations

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

Instances For

source
def Std.SharedMutex.atomicallyRead {m : Type → Type u_1} {α β : Type} [Monad m] [MonadLiftT BaseIO m] [MonadFinally m] (mutex : SharedMutex α) (k : ReaderT α m β) :
m β

`mutex.atomicallyRead k` runs `k` with read access to the mutex's state while locking the mutex for shared read access.

Calling `mutex.atomicallyRead` while already holding the underlying `BaseSharedMutex` in the same thread is undefined behavior.

Equations

- mutex.atomicallyRead k = tryFinally (do liftM mutex.mutex.read let state ← liftM (ST.Ref.get (Std.SharedMutex.ref✝ mutex)) k state) (liftM mutex.mutex.unlockRead)

Instances For

source
def Std.SharedMutex.tryAtomicallyRead {m : Type → Type u_1} {α β : Type} [Monad m] [MonadLiftT BaseIO m] [MonadFinally m] (mutex : SharedMutex α) (k : ReaderT α m β) :
m (Option β)

`mutex.tryAtomicallyRead k` tries to lock `mutex` for shared read access and runs `k` with read access to the mutex's state if it succeeds. If successful, it returns the value of `k` as `some`, otherwise `none`.

Calling `mutex.tryAtomicallyRead` while already holding the underlying `BaseSharedMutex` in the same thread is undefined behavior.

Equations

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

Instances For