@[deprecated "Use Std.BaseMutex from Std.Sync.Mutex instead" (since := "2024-12-02")]

def IO.BaseMutex : Type

Mutual exclusion primitive (a lock).

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

Equations

• IO.BaseMutex = IO.BaseMutexImpl✝.type

instance IO.instNonemptyBaseMutex : Nonempty BaseMutex

@[extern lean_io_basemutex_new, deprecated "Use Std.BaseMutex.new from Std.Sync.Mutex instead" (since := "2024-12-02")]

opaque IO.BaseMutex.new : BaseIO BaseMutex

Creates a new BaseMutex.

@[extern lean_io_basemutex_lock, deprecated "Use Std.BaseMutex.lock from Std.Sync.Mutex instead" (since := "2024-12-02")]

opaque IO.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).

@[extern lean_io_basemutex_unlock, deprecated "Use Std.BaseMutex.unlock from Std.Sync.Mutex instead" (since := "2024-12-02")]

opaque IO.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).

@[deprecated "Use Std.Condvar from Std.Sync.Mutex instead" (since := "2024-12-02")]

def IO.Condvar : Type

Condition variable.

Equations

• IO.Condvar = IO.CondvarImpl✝.type

instance IO.instNonemptyCondvar : Nonempty Condvar

@[extern lean_io_condvar_new, deprecated "Use Std.Condvar.new from Std.Sync.Mutex instead" (since := "2024-12-02")]

opaque IO.Condvar.new : BaseIO Condvar

Creates a new condition variable.

@[extern lean_io_condvar_wait, deprecated "Use Std.Condvar.wait from Std.Sync.Mutex instead" (since := "2024-12-02")]

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

Waits until another thread calls notifyOne or notifyAll.

@[extern lean_io_condvar_notify_one, deprecated "Use Std.Condvar.notifyOne from Std.Sync.Mutex instead" (since := "2024-12-02")]

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

Wakes up a single other thread executing wait.

@[extern lean_io_condvar_notify_all, deprecated "Use Std.Condvar.notifyAll from Std.Sync.Mutex instead" (since := "2024-12-02")]

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

Wakes up all other threads executing wait.

@[deprecated "Use Std.Condvar.waitUntil from Std.Sync.Mutex instead" (since := "2024-12-02")]

def IO.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.

@[deprecated "Use Std.Mutex from Std.Sync.Mutex instead" (since := "2024-12-02")]

structure IO.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 IO.instNonemptyMutex {α✝ : Type} [Nonempty α✝] : Nonempty (Mutex α✝)

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

Equations

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

@[deprecated "Use Std.Mutex.new from Std.Sync.Mutex instead" (since := "2024-12-02")]

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

Creates a new mutex.

Equations

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

@[reducible, inline, deprecated "Use Std.AtomicT from Std.Sync.Mutex instead" (since := "2024-12-02")]

abbrev IO.AtomicT (σ : Type) (m : Type → Type) (α : Type) : Type

AtomicT α m is the monad that can be atomically executed inside a Mutex α, with outside monad m. The action has access to the state α of the mutex (via get and set).

Equations

• IO.AtomicT = StateRefT' IO.RealWorld

@[deprecated "Use Std.Mutex.atomically from Std.Sync.Mutex instead" (since := "2024-12-02")]

def IO.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.

Equations

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

@[deprecated "Use Std.Mutex.atomicallyOnce from Std.Sync.Mutex instead" (since := "2024-12-02")]

def IO.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.

Equations

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