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 : IO (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 α → IO 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 : IO 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.β → IO (AsyncTask α)

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

• )

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

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.