Idris2Doc : System.Concurrency

System.Concurrency

dataBarrier : Type
  A barrier enables multiple threads to synchronize the beginning of some
computation.

Totality: total
dataChannel : Type -> Type
Totality: total
dataCondition : Type
Totality: total
dataMutex : Type
Totality: total
dataSemaphore : Type
Totality: total
barrierWait : HasIOio => Barrier -> io ()
  Blocks the current thread until all threads have rendezvoused here.

Totality: total
channelGet : HasIOio => Channela -> ioa
  Blocks until a sender is ready to provide a value through `chan`. The result
is the sent value.

Totality: total
channelPut : HasIOio => Channela -> 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 : HasIOio => Condition -> io ()
  Releases all of the threads waiting for the condition identified by `cond`.

Totality: total
conditionSignal : HasIOio => Condition -> io ()
  Releases one of the threads waiting for the condition identified by `cond`.

Totality: total
conditionWait : HasIOio => 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 : HasIOio => 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 : HasIOio => (a : Type) -> ioa
Totality: total
makeBarrier : HasIOio => Int -> ioBarrier
  Creates a new barrier that can block a given number of threads.

Totality: total
makeChannel : HasIOio => io (Channela)
  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 : HasIOio => ioCondition
  Creates and returns a new condition variable.

Totality: total
makeMutex : HasIOio => ioMutex
  Creates and returns a new mutex.

Totality: total
makeSemaphore : HasIOio => Int -> ioSemaphore
  Creates and returns a new semaphore with the counter initially set to `init`.

Totality: total
mutexAcquire : HasIOio => 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 : HasIOio => Mutex -> io ()
  Releases the mutex identified by `mutex`. Unpredictable behavior results if
the mutex is not owned by the calling thread.

Totality: total
semaphorePost : HasIOio => Semaphore -> io ()
  Increments the semaphore's internal counter.

Totality: total
semaphoreWait : HasIOio => 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 : HasIOio => a -> io ()
Totality: total