def Std.BaseMutex : Type

Mutual exclusion primitive (a lock).

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

Equations

• Std.BaseMutex = Std.BaseMutexImpl✝.type

instance Std.instNonemptyBaseMutex : Nonempty BaseMutex

@[extern lean_io_basemutex_new]

opaque Std.BaseMutex.new : BaseIO BaseMutex

Creates a new BaseMutex.

@[extern lean_io_basemutex_lock]

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

Locks a BaseMutex. Waits until no other thread has locked the mutex.

The current thread must not have already locked the mutex. Reentrant locking is undefined behavior (inherited from the C++ implementation). If this is unavoidable in your code, consider using BaseRecursiveMutex.

@[extern lean_io_basemutex_try_lock]

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

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

This function does not block.

The current thread must not have already locked the mutex. Reentrant locking is undefined behavior (inherited from the C++ implementation). If this is unavoidable in your code, consider using BaseRecursiveMutex.

@[extern lean_io_basemutex_unlock]

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

Unlocks a BaseMutex.

The current thread must have already locked the mutex. Unlocking an unlocked mutex is undefined behavior (inherited from the C++ implementation). If this is unavoidable in your code, consider using BaseRecursiveMutex.

def Std.Condvar : Type

Condition variable, a synchronization primitive to be used with a BaseMutex or Mutex.

The thread that wants to modify the shared variable must:

1. Lock the BaseMutex or Mutex
2. Work on the shared variable
3. Call Condvar.notifyOne or Condvar.notifyAll after it is done. Note that this may be done before or after the mutex is unlocked.

If working with a Mutex the thread that waits on the Condvar can use Mutex.atomicallyOnce to wait until a condition is true. If working with a BaseMutex it must:

1. Lock the BaseMutex.
2. Do one of the following:

• Use Condvar.waitUntil to (potentially repeatedly wait) on the condition variable until the condition is true.
• Implement the waiting manually by:
  1. Checking the condition
  2. Calling Condvar.wait which releases the BaseMutex and suspends execution until the condition variable is notified.
  3. Check the condition and resume waiting if not satisfied.

Equations

• Std.Condvar = Std.CondvarImpl✝.type

instance Std.instNonemptyCondvar : Nonempty Condvar

@[extern lean_io_condvar_new]

opaque Std.Condvar.new : BaseIO Condvar

Creates a new condition variable.

@[extern lean_io_condvar_wait]

opaque Std.Condvar.wait (condvar : Condvar) (mutex : BaseMutex) : BaseIO Unit

Waits until another thread calls notifyOne or notifyAll.

@[extern lean_io_condvar_notify_one]

opaque Std.Condvar.notifyOne (condvar : Condvar) : BaseIO Unit

Wakes up a single other thread executing wait.

@[extern lean_io_condvar_notify_all]

opaque Std.Condvar.notifyAll (condvar : Condvar) : BaseIO Unit

Wakes up all other threads executing wait.

def Std.Condvar.waitUntil {m : Type → Type u_1} [Monad m] [MonadLift BaseIO m] (condvar : Condvar) (mutex : BaseMutex) (pred : m Bool) : m Unit

Waits on the condition variable until the predicate is true.

Equations

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

structure Std.Mutex (α : Type) : Type

Mutual exclusion primitive (lock) guarding shared state of type α.

The type Mutex α is similar to IO.Ref α, except that concurrent accesses are guarded by a mutex instead of atomic pointer operations and busy-waiting.

• ref : IO.Ref α
• mutex : BaseMutex

instance Std.instNonemptyMutex {α✝ : Type} [Nonempty α✝] : Nonempty (Mutex α✝)

instance Std.instCoeOutMutexBaseMutex {α : Type} : CoeOut (Mutex α) BaseMutex

Equations

• Std.instCoeOutMutexBaseMutex = { coe := Std.Mutex.mutex }

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

Creates a new mutex.

Equations

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

def Std.Mutex.atomically {m : Type → Type} {α β : Type} [Monad m] [MonadLiftT BaseIO m] [MonadFinally m] (mutex : Mutex α) (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 BaseMutex in the same thread is undefined behavior. If this is unavoidable in your code, consider using RecursiveMutex.

Equations

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

def Std.Mutex.tryAtomically {m : Type → Type} {α β : Type} [Monad m] [MonadLiftT BaseIO m] [MonadFinally m] (mutex : Mutex α) (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 calling mutex.tryAtomically while already holding the underlying BaseMutex in the same thread is undefined behavior. If this is unavoidable in your code, consider using RecursiveMutex.

Equations

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

def Std.Mutex.atomicallyOnce {m : Type → Type} {α β : Type} [Monad m] [MonadLiftT BaseIO m] [MonadFinally m] (mutex : Mutex α) (condvar : Condvar) (pred : AtomicT α m Bool) (k : AtomicT α m β) : m β

mutex.atomicallyOnce condvar pred k runs k, waiting on condvar until pred returns true. Both k and pred have access to the mutex's state.

Calling mutex.atomicallyOnce while already holding the underlying BaseMutex in the same thread is undefined behavior. If this is unavoidable in your code, consider using RecursiveMutex.

Equations

• mutex.atomicallyOnce condvar pred k = mutex.atomically do condvar.waitUntil mutex.mutex pred k