Documentation

Init.System.Mutex

Mutual exclusion primitive (a lock).

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

Equations
Instances For
    @[extern lean_io_basemutex_new]

    Creates a new BaseMutex.

    @[extern lean_io_basemutex_lock]

    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]

    Unlocks a BaseMutex.

    The current thread must have already locked the mutex. Unlocking an unlocked mutex is undefined behavior (inherited from the C++ implementation).

    Condition variable.

    Equations
    Instances For
      @[extern lean_io_condvar_new]

      Creates a new condition variable.

      @[extern lean_io_condvar_wait]
      opaque IO.Condvar.wait (condvar : IO.Condvar) (mutex : IO.BaseMutex) :

      Waits until another thread calls notifyOne or notifyAll.

      @[extern lean_io_condvar_notify_one]

      Wakes up a single other thread executing wait.

      @[extern lean_io_condvar_notify_all]

      Wakes up all other threads executing wait.

      def IO.Condvar.waitUntil {m : TypeType u_1} [Monad m] [MonadLift BaseIO m] (condvar : IO.Condvar) (mutex : IO.BaseMutex) (pred : m Bool) :

      Waits on the condition variable until the predicate is true.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        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
          Equations
          • IO.instCoeOutMutexBaseMutex = { coe := IO.Mutex.mutex }
          def IO.Mutex.new {α : Type} (a : α) :

          Creates a new mutex.

          Equations
          Instances For
            @[inline, reducible]
            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
              def IO.Mutex.atomically {m : TypeType} {α : Type} {β : Type} [Monad m] [MonadLiftT BaseIO m] [MonadFinally m] (mutex : IO.Mutex α) (k : IO.AtomicT α m β) :
              m β

              mutex.atomically k runs k with access to the mutex's state while locking the mutex.

              Equations
              Instances For
                def IO.Mutex.atomicallyOnce {m : TypeType} {α : Type} {β : Type} [Monad m] [MonadLiftT BaseIO m] [MonadFinally m] (mutex : IO.Mutex α) (condvar : IO.Condvar) (pred : IO.AtomicT α m Bool) (k : IO.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