Concurrency

Concurrency in Nex is explicit and structured. A program does not manipulate threads or locks directly. It starts lightweight tasks and lets them communicate over typed channels. The model descends from Hoare’s Communicating Sequential Processes by way of the goroutine-and-channel discipline of Go.

This chapter extends the dynamic semantics of Chapter 5 to several tasks evaluating at once. Each task evaluates its own expressions and statements by the rules of Chapter 5, and all tasks share one store (Section 5.2). The rule that evaluation is sequential holds within each task, not across them.

The static typing of the concurrent forms is unremarkable, and was already given by the grammar of Chapter 2 and the classes of Appendix B.5. The interest here is all in their run-time behaviour.

6.1Tasks

The expression spawn do block end starts a new task that executes block concurrently with the task that created it. It immediately yields a task handle: a reference to a new object of class Task, or of class Task[T] when the block assigns a result of type T. The creator does not wait; the two tasks proceed in parallel. A rescue clause written before the closing end handles an exception raised by the block within the new task, as the handler of a scoped block does (Section 5.7).

The new task runs with the bindings in force at the spawn, so it can read the variables and reach the objects that were in scope where it was created. Because the store is shared, a task and its creator can see each other’s changes to objects. The language provides channels precisely so that such sharing need not be the means of communication.

A task handle supports the methods of the Task class (Appendix B.5).

• await waits until the task has finished, then yields the task’s result.
• await(ms) waits at most ms milliseconds. It yields the result if the task finishes in time, and nil otherwise.
• is_done reports, without waiting, whether the task has finished.
• cancel asks for the task to be cancelled, and reports whether the request took effect before the task finished. is_cancelled reports whether it was cancelled.
• The free functions await_any and await_all of the standard environment wait on an array of tasks, as in await_all([t1, t2]). await_any yields the result of whichever task finishes first, and await_all yields an array of all their results, in the order of the tasks.

let t: Task[Integer] := spawn do
  sleep(100)
  result := 7
end
print(t.is_done)
print(t.await)
print(t.is_done)

The spawn returns at once, so the first print shows false. await then waits for the task and prints 7, after which is_done is true.

A task that waits makes no progress until whatever it waits for happens. This Definition does not prescribe how tasks are scheduled. It requires only that a task which is able to make progress is not denied it for ever.

6.2Channels

A channel is a typed conduit between tasks: an object of class Channel[T], which carries values of type T.

• A channel made by create Channel[T] is unbuffered. A send waits until another task is ready to receive, and a receive waits until another task is ready to send. The two then meet: the value passes from sender to receiver in a single step, and both tasks continue.
• A channel made by create Channel[T].with_capacity(n) is buffered, and holds up to n values in the order they were sent. A send adds its value to the buffer, waiting only if the buffer is full. A receive removes and yields the oldest value, waiting only if the buffer is empty.

let r: Channel[Integer] := create Channel[Integer]
let sender: Task := spawn do
  r.send(99)
  print("sender resumed")
end
sleep(100)
print("receiving")
print(r.receive)
sender.await

The sender reaches send first and waits there. Only when the main task reaches receive do the two meet. The program prints "receiving", then 99, then "sender resumed".

Each operation also has variants that do not wait, or wait only for a limited time.

• try_send(v) sends v if that can be done at once, and yields true; otherwise it yields false. try_receive receives a value if one is available at once, and otherwise yields nil. On an unbuffered channel, these succeed only if another task is already waiting at the matching operation.
• send(v, ms) and receive(ms) wait at most ms milliseconds. If the operation cannot complete in that time, send yields false and receive yields nil.

A channel may be closed with close. After that:

• no further value may be sent: send and try_send raise an exception;
• values already in the buffer can still be received;
• once the buffer is empty, receive raises an exception rather than waiting, and try_receive yields nil.

The methods is_closed, size and capacity report a channel’s state. An unbuffered channel has capacity 0.

6.3Selective Communication

The select statement waits on several communications at once, and proceeds with whichever becomes ready first. Each clause names a channel operation or a task’s completion. An optional timeout clause gives up after an interval, and an optional else clause makes the select not wait at all.

select
  when jobs.receive as job then ...
  when results.send(value) then ...
  when worker.await as value then ...
  timeout 1000 then ...
  else ...
end

A clause is ready when its operation could complete at once:

• a receive clause, when try_receive would succeed;
• a send clause, when try_send would succeed;
• an await clause, when the task has finished (is_done holds).

The statement takes a ready clause, performs its operation, binds the clause’s as variable to the value obtained, and runs the clause’s block. Which clause it takes depends on what is ready:

• If several clauses are ready, one of them is taken. This Definition does not say which, only that a ready clause is taken.
• If none is ready and there is an else clause, the else block runs at once.
• If none is ready and there is a timeout clause, the statement waits. It takes the first clause that becomes ready within the interval, or runs the timeout block when the interval ends.
• If none is ready and there is neither an else nor a timeout, the statement waits until some clause becomes ready.

6.4The Model and Its Realisations

The semantics above is given in the style of CSP, in which communicating tasks meet at a channel, and it is the authoritative meaning of the concurrent forms. Each back end realises it in a different way, and a programmer should know where the realisations differ.

• On the JVM, tasks run on platform threads, and channels are concurrent queues with the waiting rules of Section 6.2. Tasks really do run in parallel.
• On a back end such as JavaScript, where the host has a single thread, tasks may become asynchronous computations and channels promise-based queues. The Nex source is unchanged: spawn becomes asynchronous task code, and await, send and receive become waits on a promise. Waiting in the sense of Section 6.2 becomes suspension of the waiting computation, and apparent parallelism is interleaving.

In both realisations, a well-synchronised program behaves as the semantics above says. A well-synchronised program is one whose tasks communicate through channels rather than through shared mutable objects.

Programs whose tasks instead race to read and change shared objects are outside the guarantees of this chapter, and this Definition gives them no determinate meaning.