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.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.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.Async.Waiter.finished✝ w, promise := p }

@[specialize #[]]

def Std.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.Async.Waiter.finished✝ w) fun (s : Bool) => (s == false, true) if first = true then win w.promise else lose

@[inline]

def Std.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.Async.Waiter.finished✝ w)

structure Std.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.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.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.

The returned Selector polls and registers the selectables in random order for fairness. If registering with one of them fails, the error is reported through the Waiter unless the race was already won, in which case the winner's result takes priority.

Equations

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

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

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

selectables is combined into a single Selector via Selectable.combine:

1. If Selector.tryFn immediately yields a value, the corresponding Selectable.cont is executed and its result is returned immediately.
2. Otherwise, a single Waiter is registered with the combined Selector using Selector.registerFn. Once the Waiter is resolved, Selector.unregisterFn is called unconditionally, cleaning up every entry of selectables, before the result (or error) is returned to the caller. This holds no matter how the race is decided: a winning result, an error raised while resolving the Waiter, or a registerFn that throws mid-registration.

Equations

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

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