White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

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

EKEMBE NGONDI, Gerard (2016) Denotational Semantics of Mobility in Unifying Theories of Programming (UTP). PhD thesis, University of York.

This is the latest version of this item.

Thesis_draft6_1.pdf - Examined Thesis (PDF)
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (1546Kb) | Preview


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.

Item Type: Thesis (PhD)
Related URLs:
Keywords: UTP, CSP, denotational semantics, dynamic network, channel mobility, strong process mobility, continuations, interrupt
Academic Units: The University of York > Computer Science (York)
Identification Number/EthosID: uk.bl.ethos.707143
Depositing User: Gerard EKEMBE NGONDI
Date Deposited: 31 Mar 2017 16:09
Last Modified: 24 Jul 2018 15:22
URI: http://etheses.whiterose.ac.uk/id/eprint/16525

Available Versions of this Item

  • Denotational Semantics of Mobility in Unifying Theories of Programming (UTP). (deposited 31 Mar 2017 16:09) [Currently Displayed]

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)