Concurrency — The Definition of Nex

Concurrency in Nex is explicit and structured. A program does not manipulate threads, locks, or shared mutable cells 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. The single-threaded judgement \(s, E \vdash e \Rightarrow v, s'\) now describes one task’s contribution to a configuration: a collection of tasks together with a shared store.

The static typing of the concurrent forms is unremarkable, and was already admitted by the grammar of Chapter 2. The interest here is all in the dynamics.

6.1Tasks

The expression spawn do \(\mathit{block}\) end starts a new task that evaluates \(\mathit{block}\) concurrently with its creator, and immediately yields a task handle: a reference to an object of class Task, or of Task[T] when the block assigns a result of type \(T\). The creator does not wait; the two proceed in parallel.

\[ \frac{\ell \;\text{fresh} \quad t \;\text{a new task evaluating}\; \mathit{block}\;\text{in}\; E}{s, E \vdash \texttt{spawn}\;\texttt{do}\;\mathit{block}\;\texttt{end} \Rightarrow \ell,\; s + \{\ell \mapsto \mathsf{task}(t)\}} \tag{6.1} \]

A task captures the bindings of its spawn, so it may read the variables and reach the objects in scope where it was created. Because the store is shared, a task and its creator may observe one another’s writes to objects. The language provides channels precisely so that such sharing need not be the means of communication.

A task handle supports the operations of the Task class (Appendix B). The chief one is await, which blocks the caller until the task has finished and then yields its result. await(ms) waits at most ms milliseconds and yields nil on timeout.

The predicate is_done reports completion without blocking. cancel requests cancellation and reports whether it took effect before completion. The class methods await_any and await_all wait on a collection of tasks.

\[ \frac{s(\ell) = \mathsf{task}(t) \quad t \;\text{has completed with result}\; v\; \text{in}\; s}{s, E \vdash \ell.\texttt{await} \Rightarrow v,\, s} \tag{6.2} \]

Rule (6.2) has a premise that a scheduler must eventually make true: the awaiting task makes no progress until the awaited task completes. The Definition does not prescribe a scheduling policy. It only requires that a task which can make progress is not forever denied it.

6.2Channels

A channel is a typed conduit between tasks, an instance of Channel[T]. By default it is unbuffered (synchronous): a send blocks until a receive is ready to take the value, and the two rendezvous — the value passes from sender to receiver in a single step.

A channel created with_capacity(n) is buffered: up to \(n\) values may be held. A send blocks only when the buffer is full, and a receive only when it is empty.

\[ \frac{\ell \;\text{fresh}}{s, E \vdash \texttt{create}\;\texttt{Channel}[T] \Rightarrow \ell,\; s + \{\ell \mapsto \mathsf{chan}(T, 0, \langle\,\rangle)\}} \tag{6.3} \]

We write a channel object \(\mathsf{chan}(T, c, q)\) with element type \(T\), capacity \(c\), and pending queue \(q\). The synchronous rendezvous is the simultaneous progress of a blocked sender and a blocked receiver:

\[ \frac{s(\ell) = \mathsf{chan}(T, 0, \langle\,\rangle) \quad t_1\;\text{at}\;\ell.\texttt{send}(v) \quad t_2\;\text{at}\;\ell.\texttt{receive}}{t_1\;\text{proceeds};\quad t_2\;\text{yields}\;v;\quad s\;\text{unchanged}} \tag{6.4} \]

For a buffered channel, send appends to \(q\) when \(|q| < c\), and otherwise blocks. receive removes the head of \(q\) when \(q\) is non-empty, and otherwise blocks.

The non-blocking variants try_send and try_receive never block: they perform the operation if it can proceed immediately, and otherwise report failure (false, or nil for a receive). The timed variants send(v, ms) and receive(ms) block for at most the given interval.

A channel may be closed. After closing, no further value may be sent, and a send on a closed channel is an error. Values already buffered may still be received; once they are exhausted, receive on a closed channel completes rather than blocking.

The predicates is_closed, size, and capacity report a channel’s state.

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 completion; an optional timeout clause fires after an interval; an optional else clause makes the select non-blocking.

select
  when jobs.receive as job then ...
  when worker.await as value then ...
  timeout 1000 then ...
  else ...
end

Operationally, select probes its clauses. A channel-receive clause is ready when try_receive would succeed, and a channel-send clause is ready when try_send would. A task clause when \(t\).await is ready exactly when is_done holds of \(t\).

The statement chooses a ready clause, binds its as variable to the value obtained, and runs that clause’s block.

If several clauses are ready, one is chosen; the Definition does not fix which, only that a ready clause is taken.
If none is ready and an else clause is present, the else block runs at once.
If none is ready and there is a timeout clause, the statement waits, taking a clause that becomes ready within the interval, or running the timeout block when the interval elapses.
If none is ready and there is neither else nor timeout, the statement blocks until some clause becomes ready.

Task clauses fire only on completion A when t.await clause does not itself wait: it is ready only if \(t\) has already completed, and it then yields \(t\)’s result without blocking. To wait for a task within a select, give the statement a timeout or combine it with channels; a bare task clause is a non-blocking test of completion.

6.4The Model and Its Realisations

The semantics above is given in the rendezvous style of CSP, and is the authoritative meaning of the concurrent forms. Each back end realises it on a different substrate, and a programmer should know where the realisations differ.

On the JVM, tasks are scheduled onto platform threads and channels are concurrent queues with the blocking discipline of Section 6.2; evaluation is genuinely parallel.
On a backend like JavaScript, where the host is single-threaded, tasks may be lowered to asynchronous computations and channels to promise-mediated queues. The Nex source is unchanged: spawn becomes asynchronous task code, and await, send, and receive lower to await on a promise. The blocking of Section 6.2 becomes suspension of the awaiting computation, and apparent parallelism is interleaving.

In both realisations, the observable behaviour of a well-synchronised program agrees with the rendezvous semantics — "well-synchronised" meaning one that communicates through channels rather than through shared mutable objects.

Programs that instead race on shared objects are outside the guarantees of this chapter, and the Definition assigns them no determinate meaning.