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

instance Std.instNonemptyBaseSharedMutex : Nonempty BaseSharedMutex

@[extern lean_io_basesharedmutex_new]

opaque Std.BaseSharedMutex.new : BaseIO BaseSharedMutex

Creates a new BaseSharedMutex.

@[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).

@[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).

@[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).

@[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).

@[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).

@[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).

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

instance Std.instNonemptySharedMutex {α✝ : Type} [Nonempty α✝] : Nonempty (SharedMutex α✝)

instance Std.instCoeOutSharedMutexBaseSharedMutex {α : Type} : CoeOut (SharedMutex α) BaseSharedMutex

Equations

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

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 }

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)

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.

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)

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.