Documentation

Std.Sync.SharedMutex

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
    Instances For
      @[extern lean_io_basesharedmutex_new]

      Creates a new BaseSharedMutex.

      @[extern lean_io_basesharedmutex_write]

      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]

      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]

      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]

      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]

      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]

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

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

      Instances For
        def Std.SharedMutex.new {α : Type} (a : α) :

        Creates a new shared mutex.

        Equations
          Instances For
            def Std.SharedMutex.atomically {m : TypeType} {α β : 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
              Instances For
                def Std.SharedMutex.tryAtomically {m : TypeType} {α β : 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
                  Instances For
                    def Std.SharedMutex.atomicallyRead {m : TypeType 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
                      Instances For
                        def Std.SharedMutex.tryAtomicallyRead {m : TypeType 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
                          Instances For