System.Concurrency

Concurrency primitives, e.g. threads, mutexes, etc.

N.B.: At the moment this is pretty fundamentally tied to the Scheme RTS.
Given that different back ends will have entirely different threading
models, it might be unavoidable, but we might want to think about possible
primitives that back ends should support.

Definitions

setThreadData : HasIO io => a -> io ()

  Set the data stored in a thread's parameter to the given value.
  Currently only supported under the scheme backends.

Totality: total
Visibility: export

getThreadData : HasIO io => (a : Type) -> io a

  Get the data stored in a thread's parameter.
  Currently only supported under the scheme backends.

Totality: total
Visibility: export

getThreadId : HasIO io => io Int

  Get the thread id of the current thread (chez backend).

Totality: total
Visibility: export

data Mutex : Type

Totality: total
Visibility: export

makeMutex : HasIO io => io Mutex

  Creates and returns a new mutex.

Totality: total
Visibility: export

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
Visibility: export

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
Visibility: export

data Condition : Type

Totality: total
Visibility: export

makeCondition : HasIO io => io Condition

  Creates and returns a new condition variable.

Totality: total
Visibility: export

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
Visibility: export

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
Visibility: export

conditionSignal : HasIO io => Condition -> io ()

  Releases one of the threads waiting for the condition identified by `cond`.

Totality: total
Visibility: export

conditionBroadcast : HasIO io => Condition -> io ()

  Releases all of the threads waiting for the condition identified by `cond`.

Totality: total
Visibility: export

data Semaphore : Type

Totality: total
Visibility: export

makeSemaphore : HasIO io => Int -> io Semaphore

  Creates and returns a new semaphore with the counter initially set to `init`.

Totality: total
Visibility: export

semaphorePost : HasIO io => Semaphore -> io ()

  Increments the semaphore's internal counter.

Totality: total
Visibility: export

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
Visibility: export

data Barrier : Type

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

Totality: total
Visibility: export

makeBarrier : HasIO io => Int -> io Barrier

  Creates a new barrier that can block a given number of threads.
  
  @ numThreads the number of threads to block

Totality: total
Visibility: export

barrierWait : HasIO io => Barrier -> io ()

  Blocks the current thread until all threads have rendezvoused here.

Totality: total
Visibility: export

data Channel : Type -> Type

Totality: total
Visibility: export

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
Visibility: export

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.
  
  @ chan the channel to receive on

Totality: total
Visibility: export

channelGetNonBlocking : HasIO io => Channel a -> io (Maybe a)

  Non-blocking version of channelGet (chez backend).
  
  @ chan the channel to receive on

Visibility: export

channelGetWithTimeout : HasIO io => Channel a -> Nat -> io (Maybe a)

  Timeout version of channelGet (chez backend).
  Clamps minimum timeout to 25 ms on windows.
  
  @ chan the channel to receive on
  @ milliseconds how many milliseconds to wait until timeout

Visibility: export

channelPut : HasIO io => Channel a -> a -> io ()

  Puts a value on the given channel.
  
  @ chan the `Channel` to send the value over
  @ val  the value to send

Totality: total
Visibility: export