Technical reports
Nomadic π-calculi: expressing and verifying communication infrastructure for mobile computation
Asis Unyapoth
June 2001, 316 pages
This technical report is based on a dissertation submitted March 2001 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Pembroke College.
DOI: 10.48456/tr-514
Abstract
This thesis addresses the problem of verifying distributed infrastructure for mobile computation. In particular, we study language primitives for communication between mobile agents. They can be classified into two groups. At a low level there are “location dependent” primitives that require a programmer to know the current site of a mobile agent in order to communicate with it. At a high level there are “location independent” primitives that allow communication with a mobile agent irrespective of any migrations. Implementation of the high level requires delicate distributed infrastructure algorithms. In earlier work of Sewell, Wojciechowski and Pierce, the two levels were made precise as process calculi, allowing such algorithms to be expressed as encodings of the high level into the low level; a distributed programming language “Nomadic Pict” has been built for experimenting with such encodings.
This thesis turns to semantics, giving a definition of the core language (with a type system) and proving correctness of an example infrastructure. This involves extending the standard semantics and proof techniques of process calculi to deal with the new notions of sites and agents. The techniques adopted include labelled transition semantics, operational equivalences and preorders (e.g., expansion and coupled simulation), “up to” equivalences, and uniform receptiveness. We also develop two novel proof techniques for capturing the design intuitions regarding mobile agents: we consider “translocating” versions of operational equivalences that take migration into account, allowing compositional reasoning; and “temporary immobility”, which captures the intuition that while an agent is waiting for a lock somewhere in the system, it will not migrate.
The correctness proof of an example infrastructure is non-trivial. It involves analysing the possible reachable states of the encoding applied to an arbitrary high-level source program. We introduce an intermediate language for factoring out as many ‘house-keeping’ reduction steps as possible, and focusing on the partially-committed steps.
Full text
BibTeX record
@TechReport{UCAM-CL-TR-514,
author = {Unyapoth, Asis},
title = {{Nomadic $\pi$-calculi: expressing and verifying
communication infrastructure for mobile computation}},
year = 2001,
month = jun,
url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-514.pdf},
institution = {University of Cambridge, Computer Laboratory},
doi = {10.48456/tr-514},
number = {UCAM-CL-TR-514}
}