Behaviour-oriented concurrency (BoC) is a novel concurrency paradigm which provides programmers with
expressive synchronisation whilst avoiding deadlocks and data-races. This thesis focuses on the design of
BoC and how it provides isolated and ordered behaviours.
BoC is based on behaviours and concurrent owners. Concurrent owners provide exclusive access to mu-
table resources. Behaviours are units of work and are dispatched based on the availability of one or more
concurrent owners, providing a simple mechanism to coordinate access to multiple resources. In this thesis,
I explore the design of BoC by way of examples, and establish an operational semantics which captures how
BoC can enrich an underlying language with concurrency.
BoC guarantees behaviours are deadlock free, data-race free and atomic through behaviour isolation;
to ensure this, the underlying language must satisfy key isolation properties. In this thesis, I define these
isolation properties which constitute the interface between BoC and the underlying language. Using these
properties, I prove that BoC provides atomic behaviours.
BoC behaviours are implicitly ordered based on spawn order and cown acquisition; if one behaviour is
spawned after another and the behaviours require any of the same cowns, then the behaviour spawned first
will execute first. This ordering allows programmers to construct ordered concurrency without introducing
their own control-flow constructs.
In this thesis, I construct an axiomatic model of BoC to explore the design of behaviour ordering. This
model allows us to judge the validity of candidate executions, independent of the intricacies of the mecha-
nisms used to execute a program (e.g., an operational semantics). I compare this axiomatic model and the
operational semantics to investigate the two models’ expressiveness, finding that the operational semantics
is slightly too restrictive.
To demonstrate the expressiveness and applicability of BoC, I have implemented well-known concur-
rency challenges and benchmarks using the paradigm.