- data Barrier : Type
A barrier enables multiple threads to synchronize the beginning of some
computation.
Totality: total- data Channel : Type -> Type
- Totality: total
- data Condition : Type
- Totality: total
- data Mutex : Type
- Totality: total
- data Semaphore : Type
- Totality: total
- barrierWait : HasIO io => Barrier -> io ()
Blocks the current thread until all threads have rendezvoused here.
Totality: total- channelGet : HasIO io => Channel a -> io a
Blocks until a sender is ready to provide a value through `chan`. The result
is the sent value.
Totality: total- channelPut : HasIO io => Channel a -> a -> io ()
CAUTION: Different behaviour under chez and racket:
- Chez: Puts a value on the channel. If there already is a value, blocks
until that value has been received.
- Racket: Blocks until a receiver is ready to accept the value `val` through
`chan`.
Totality: total- conditionBroadcast : HasIO io => Condition -> io ()
Releases all of the threads waiting for the condition identified by `cond`.
Totality: total- conditionSignal : HasIO io => Condition -> io ()
Releases one of the threads waiting for the condition identified by `cond`.
Totality: total- conditionWait : HasIO io => Condition -> Mutex -> io ()
Waits up to the specified timeout for the condition identified by the
condition variable `cond`. The calling thread must have acquired the mutex
identified by `mutex` at the time `conditionWait` is called. The mutex is
released as a side effect of the call to `conditionWait`. When a thread is
later released from the condition variable by one of the procedures
described below, the mutex is reacquired and `conditionWait` returns.
Totality: total- conditionWaitTimeout : HasIO io => Condition -> Mutex -> Int -> io ()
Variant of `conditionWait` with a timeout in microseconds.
When the timeout expires, the thread is released, `mutex` is reacquired, and
`conditionWaitTimeout` returns.
Totality: total- getThreadData : HasIO io => (a : Type) -> io a
- Totality: total
- makeBarrier : HasIO io => Int -> io Barrier
Creates a new barrier that can block a given number of threads.
Totality: total- makeChannel : HasIO io => io (Channel a)
Creates and returns a new channel. The channel can be used with channelGet
to receive a value through the channel. The channel can be used with
channelPut to send a value through the channel.
Totality: total- makeCondition : HasIO io => io Condition
Creates and returns a new condition variable.
Totality: total- makeMutex : HasIO io => io Mutex
Creates and returns a new mutex.
Totality: total- makeSemaphore : HasIO io => Int -> io Semaphore
Creates and returns a new semaphore with the counter initially set to `init`.
Totality: total- mutexAcquire : HasIO io => Mutex -> io ()
Acquires the mutex identified by `mutex`. The thread blocks until the mutex
has been acquired.
Mutexes are recursive in Posix threads terminology, which means that the
calling thread can use mutex-acquire to (re)acquire a mutex it already has.
In this case, an equal number of mutex-release calls is necessary to release
the mutex.
Totality: total- mutexRelease : HasIO io => Mutex -> io ()
Releases the mutex identified by `mutex`. Unpredictable behavior results if
the mutex is not owned by the calling thread.
Totality: total- semaphorePost : HasIO io => Semaphore -> io ()
Increments the semaphore's internal counter.
Totality: total- semaphoreWait : HasIO io => Semaphore -> io ()
Blocks until the internal counter for semaphore sema is non-zero. When the
counter is non-zero, it is decremented and `semaphoreWait` returns.
Totality: total- setThreadData : HasIO io => a -> io ()
- Totality: total