Denotational Semantics of Mobility in Unifying Theories of Programming (UTP)

UTP promotes the unification of programming theories and has been used successfully
for giving denotational semantics to Imperative Programming, CSP process algebra,
and the Circus family of programming languages, amongst others.
In this thesis, we present an extension of UTP-CSP (the UTP semantics for CSP)
with the concept of mobility. Mobility is concerned with the movement of an entity
from one location (the source) to another (the target). We deal with two forms of
mobility:
• Channel mobility, concerned with the movement of links between processes,
models networks with a dynamic topology; and
• Strong process mobility, which requires to suspend a running process first, and
then move both its code and its state upon suspension, and finally resume the
process on the target upon reception.
Concerning channel mobility:
• We model channels as concrete entities in CSP, and show that it does not affect
the underlying CSP semantics.
• A requirement is that a process may not own a channel prior to receiving it. In
CSP, the set of channels owned by a process (called its interface) is static by
definition. We argue that making the interface variable introduces a paradox.
We resolve this by introducing a new concept: the capability of a process, and
show how it relates to the interface.
We then define channel mobility as the operation that changes the interface of a process,
but not its capability. We also provide a functional link between static CSP and its
mobile version.
Concerning strong mobility, we provide:
• The first extension of CSP with jump features, using the concept of continuations.
• A novel semantics for the generic interrupt (a parallel-based interrupt operator),
using the concept of Bulk Synchronous Parallelism.
We then define strong mobility as a specific interrupt operator in which the interrupt
routine migrates the suspended program.