2  Concurrency Model

We define our concurrency model with a set of primitive operations for running threads allowing communication and synchronization. We first define here informally these operations as their signatures will depend on each implementation.

2.1  Basic Operations

We define the following basic operations for running threads:

spawn takes a thunk and creates a new thread for executing it. The thread will actually start running only when the start operation is invoked.

yield suspends the calling thread, allowing other threads to execute.

halt terminates the calling thread. If the last thread terminates, start returns.

start starts all the threads created by spawn, and waits.

stop terminates all the threads. start returns, that is, control returns after the call to start.

Most systems providing threads do not include something like the start operation: threads start running as soon as they are spawned. In our model, the calling (“main”) code is not one of the threads but is suspended until all the threads have completed. It is then easy to spawn a set of threads to handle a specific task and resume to sequential operations when they are done. However, this choice has little impact on most of what we say in the following.

2.2  Communication

We allow threads to communicate through MVars and synchronous Fifos. Introduced in Haskell [20], MVars are shared mutable variables that provide synchronization. They can also be thought as one-cell synchronous channels. An MVar can contain a value or be empty. A tentative writer blocks if the MVar already contains a value, otherwise it writes the value and continues. A tentative reader blocks if it is empty, otherwise it takes (removes) the value and continues. Of course blocked readers or writers should be waken up when the MVar is written to or emptied.

We define α mvar as the type of MVars storing a value of type α. The following operations are defined:

make_mvar creates a fresh empty MVar.

put_mvar puts a value into the MVar.

take_mvar takes the value out of the MVar.

In the following we assume that only one thread wants to write and only one wants to read in a given MVar. This is not a necessary restriction, but does simplify the implementations a bit.

Contrary to an MVar, a synchronous Fifo can store an unlimited amount of values. Adding a value to the Fifo is a non blocking operation while taking one (the one at the head of queue) is blocking if the queue is empty. Operations are similar to MVar’s:

make_fifo creates a fresh empty Fifo.

put_fifo adds a value into the Fifo.

take_fifo takes the first value out of the Fifo.