Documentation

Init.System.Mutex

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

Mutual exclusion primitive (a lock).

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

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

      Creates a new BaseMutex.

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

      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")]

      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")]

      Condition variable.

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

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

          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")]

          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")]

          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 : TypeType u_1} [Monad m] [MonadLift BaseIO m] (condvar : Condvar) (mutex : BaseMutex) (pred : m Bool) :

          Waits on the condition variable until the predicate is true.

          Equations
            Instances For
              @[deprecated "Use Std.Mutex from Std.Sync.Mutex instead" (since := "2024-12-02")]
              structure IO.Mutex (α : 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.

              Instances For
                instance IO.instNonemptyMutex {α✝ : Type} [Nonempty α✝] :
                Nonempty (Mutex α✝)
                @[deprecated "Use Std.Mutex.new from Std.Sync.Mutex instead" (since := "2024-12-02")]
                def IO.Mutex.new {α : Type} (a : α) :

                Creates a new mutex.

                Equations
                  Instances For
                    @[reducible, inline, deprecated "Use Std.AtomicT from Std.Sync.Mutex instead" (since := "2024-12-02")]
                    abbrev IO.AtomicT (σ : Type) (m : TypeType) (α : 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
                      Instances For
                        @[deprecated "Use Std.Mutex.atomically from Std.Sync.Mutex instead" (since := "2024-12-02")]
                        def IO.Mutex.atomically {m : TypeType} {α β : 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
                          Instances For
                            @[deprecated "Use Std.Mutex.atomicallyOnce from Std.Sync.Mutex instead" (since := "2024-12-02")]
                            def IO.Mutex.atomicallyOnce {m : TypeType} {α β : 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
                              Instances For