structure Control.Concurrent.QSemN : Type

A generalised quantity semaphore. Allows acquiring and releasing arbitrary amounts of the resource.

$$\text{QSemN.new} : \text{Nat} \to \text{BaseIO}\ \text{QSemN}$$

Modelled after Haskell's QSemN.

• state : Std.Mutex QSemNState

def Control.Concurrent.QSemN.new (initial : Nat) : BaseIO QSemN

Create a new semaphore with the given initial count.

$$\text{new} : \text{Nat} \to \text{BaseIO}\ \text{QSemN}$$

Equations

• Control.Concurrent.QSemN.new initial = do let __do_lift ← Std.Mutex.new { count := initial, waiters := ∅ } pure { state := __do_lift }

def Control.Concurrent.QSemN.wait (sem : QSemN) (n : Nat) : BaseIO (Task Unit)

Acquire $n$ units. If insufficient units are available, the caller becomes a dormant promise until enough are released.

$$\text{wait} : \text{QSemN} \to \text{Nat} \to \text{BaseIO}\ (\text{Task}\ \text{Unit})$$

Equations

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

def Control.Concurrent.QSemN.signal (sem : QSemN) (n : Nat) : BaseIO Unit

Release $n$ units. Wakes as many FIFO-ordered waiters as the available count allows.

$$\text{signal} : \text{QSemN} \to \text{Nat} \to \text{BaseIO}\ \text{Unit}$$

Equations

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

def Control.Concurrent.QSemN.withSemN {α : Type} (sem : QSemN) (n : Nat) (action : IO α) : IO α

Acquire $n$ units, run an action, then release $n$ — even if the action throws. Guarantees the semaphore is released via try/finally.

$$\text{withSemN} : \text{QSemN} \to \mathbb{N} \to \text{IO}\ \alpha \to \text{IO}\ \alpha$$

Equations

• sem.withSemN n action = do let __do_lift ← liftM (sem.wait n) liftM (IO.wait __do_lift) tryFinally action (liftM (sem.signal n))