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