This module contains the implementation of a fair and data-loss free IO multiplexing primitive. The main entrypoint for users is Selectable.one and the various functions to produce Selectors from other modules.

structure Std.Internal.IO.Async.Waiter (α : Type) : Type

The core data structure for racing on winning a Selectable.one if multiple event sources are ready at the same time. A Task can try to finish the waiter by calling Waiter.race.

• finished : IO.Ref Bool
• promise : IO.Promise (Except IO.Error α)

@[inline]

def Std.Internal.IO.Async.Waiter.withPromise {α β : Type} (w : Waiter α) (p : IO.Promise (Except IO.Error β)) : Waiter β

Swap out the IO.Promise within the Waiter. Note that the part which determines whether the Waiter is finished is not swapped out.

Equations

• w.withPromise p = { finished := Std.Internal.IO.Async.Waiter.finished✝ w, promise := p }

@[specialize #[]]

def Std.Internal.IO.Async.Waiter.race {m : Type → Type} {α β : Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (w : Waiter α) (lose : m β) (win : IO.Promise (Except IO.Error α) → m β) : m β

Try to atomically finish the Waiter. If the race for finishing it is won, win is executed with the internal IO.Promise of the Waiter. This promise must under all circumstances be resolved by win. If the race is lost some cleanup work can be done in lose.

Equations

• w.race lose win = do let first ← ST.Ref.modifyGet (Std.Internal.IO.Async.Waiter.finished✝ w) fun (s : Bool) => (s == false, true) if first = true then win w.promise else lose

@[inline]

def Std.Internal.IO.Async.Waiter.checkFinished {m : Type → Type} {α : Type} [Monad m] [MonadLiftT (ST IO.RealWorld) m] (w : Waiter α) : m Bool

Atomically checks whether the Waiter has already finished. Note that right after this function call ends this might have already changed.

Equations

• w.checkFinished = ST.Ref.get (Std.Internal.IO.Async.Waiter.finished✝ w)

structure Std.Internal.IO.Async.Selector (α : Type) : Type

An event source that can be multiplexed using Selectable.one, see the documentation of Selectable.one for how the protocol of communicating with a Selector works.

• tryFn : Async (Option α)

  Attempts to retrieve a piece of data from the event source in a non-blocking fashion, returning some if data is available and none otherwise.

• registerFn : Waiter α → Async Unit

  Registers a Waiter with the event source. Once data is available, the event source should attempt to call Waiter.race and resolve the Waiter's promise if it wins. It is crucial that data is never actually consumed from the event source unless Waiter.race wins in order to prevent data loss.

• unregisterFn : Async Unit

  A cleanup function that is called once any Selector has won the Selectable.one race.

structure Std.Internal.IO.Async.Selectable (α : Type) : Type 1

An event source together with a continuation to call on data obtained from that event source, usually used together in conjunction with Selectable.one.

• case :: (
• β : Type
• selector : Selector self.β

  The event source.

• cont : self.β → Async α

  The continuation that is called on results from the event source.

• )

def Std.Internal.IO.Async.Selectable.one {α : Type} (selectables : Array (Selectable α)) : Async α

Performs fair and data-loss free multiplexing on the Selectables in selectables.

The protocol for this is as follows:

1. The selectables are shuffled randomly.
2. Run Selector.tryFn for each element in selectables. If any succeed, the corresponding Selectable.cont is executed and its result is returned immediately.
3. If none succeed, a Waiter is registered with each Selector using Selector.registerFn. Once one of them resolves the Waiter, all Selector.unregisterFn functions are called, and the Selectable.cont of the winning Selector is executed and returned.

Equations

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

def Std.Internal.IO.Async.Selectable.tryOne {α : Type} (selectables : Array (Selectable α)) : Async (Option α)

Performs fair and data-loss free non-blocking multiplexing on the Selectables in selectables.

This function only tries the non-blocking tryFn for each Selectable without registering waiters or blocking. It returns some result if any Selectable is immediately available, or none if all would block.

The protocol for this is as follows:

1. The selectables are shuffled randomly for fairness.
2. Run Selector.tryFn for each element in selectables. If any succeed, the corresponding Selectable.cont is executed and its result is returned as some result.
3. If none succeed, none is returned immediately without blocking.

Equations

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

def Std.Internal.IO.Async.Selectable.combine {α : Type} (selectables : Array (Selectable α)) : IO (Selector α)

Creates a Selector that performs fair and data-loss free multiplexing on multiple Selectables. This allows the multiplexing operation to be composed with other selectors.

Equations

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