structure Control.Concurrent.QSem : Type

A quantity semaphore. Create with QSem.new n to allow up to $n$ concurrent acquisitions.

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

Modelled after Haskell's QSem.

• state : Std.Mutex QSemState

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

Create a new semaphore with the given initial count $n$.

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

Equations

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

def Control.Concurrent.QSem.wait (sem : QSem) : BaseIO (Task Unit)

Acquire one unit of the semaphore. If no units are available, the caller becomes a dormant promise until signal releases one.

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

Never blocks an OS thread. FIFO fairness.

Equations

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

def Control.Concurrent.QSem.signal (sem : QSem) : BaseIO Unit

Release one unit of the semaphore. If there are waiting tasks, the first one in FIFO order is woken.

$$\text{signal} : \text{QSem} \to \text{BaseIO}\ \text{Unit}$$

No-lost-wakeup guarantee: either a waiter is woken or the count is incremented. Both branches are mutually exclusive.

Equations

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

def Control.Concurrent.QSem.withSem {α : Type} (sem : QSem) (action : IO α) : IO α

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

$$\text{withSem} : \text{QSem} \to \text{IO}\ \alpha \to \text{IO}\ \alpha$$

Equations

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