structure Std.Semaphore : Type

Counting semaphore.

Semaphore.acquire returns a promise that is resolved once a permit is available. If a permit is currently available, the returned promise is already resolved. Semaphore.release either resolves one waiting promise or increments the available permits.

• lock : Std.Mutex SemaphoreState

def Std.Semaphore.new (permits : Nat) : BaseIO Semaphore

Creates a new semaphore with permits initially available permits.

Equations

• Std.Semaphore.new permits = do let __do_lift ← Std.Mutex.new { permits := permits } pure { lock := __do_lift }

def Std.Semaphore.acquire (sem : Semaphore) : BaseIO (IO.Promise Unit)

Requests one permit. Returns a promise that resolves once the permit is acquired.

Equations

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

def Std.Semaphore.tryAcquire (sem : Semaphore) : BaseIO Bool

Tries to acquire a permit without blocking. Returns true on success.

Equations

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

def Std.Semaphore.release (sem : Semaphore) : BaseIO Unit

Releases one permit and resolves one waiting acquirer, if any.

Equations

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

def Std.Semaphore.availablePermits (sem : Semaphore) : BaseIO Nat

Returns the number of currently available permits.

Equations

• sem.availablePermits = (Std.Semaphore.lock✝ sem).atomically do let __do_lift ← get pure (Std.SemaphoreState.permits✝ __do_lift)