Nomadic Pict: Programming Languages, Communication Infrastructure Overlays, and Semantics for Mobile Computation . Peter Sewell, Pawel Wojciechowski, and Asis Unyapoth. ACM Transactions on Programming Languages and Systems (TOPLAS), 32(4):1--63 (and electronic appendix, 33pp), 2010. [ bib | doi | project page | pdf ]
Mobile computation, in which executing computations can move from one physical computing device to another, is a recurring theme: from OS process migration, to language-level mobility, to virtual machine migration. This article reports on the design, implementation, and verification of overlay networks to support reliable communication between migrating computations, in the Nomadic Pict project. We define two levels of abstraction as calculi with precise semantics: a low-level Nomadic π calculus with migration and location-dependent communication, and a high-level calculus that adds location-independent communication. Implementations of location-independent communication, as overlay networks that track migrations and forward messages, can be expressed as translations of the high-level calculus into the low. We discuss the design space of such overlay network algorithms and define three precisely, as such translations. Based on the calculi, we design and implement the Nomadic Pict distributed programming language, to let such algorithms (and simple applications above them) to be quickly prototyped. We go on to develop the semantic theory of the Nomadic π calculi, proving correctness of one example overlay network. This requires novel equivalences and congruence results that take migration into account, and reasoning principles for agents that are temporarily immobile (e.g., waiting on a lock elsewhere in the system). The whole stands as a demonstration of the use of principled semantics to address challenging system design problems.

 
Verifying Overlay Networks for Relocatable Computations (or: Nomadic Pict, relocated). Peter Sewell and Pawel Wojciechowski. In RRDD Workshop, 2008. [ bib | project page | pdf ]
In the late 1990s we developed a calculus, Nomadic Pict, in which to express and verify overlay networks, for reliable communication between relocatable computations. Then, efficient system support for relocation was rare, and the calculus was reified in a prototype high-level programming language. Now, relocatable computation is a pervasive reality, though at the level of virtual machines rather than high-level languages. One can ask whether the semantic theory and algorithms developed for Nomadic Pict can be applied (or adapted) to infrastructure for communication between these virtual machines.

 
Nomadic Pict: Correct Communication Infrastructure for Mobile Computation. Asis Unyapoth and Peter Sewell. In POPL 2001. [ bib | doi | project page | ps | pdf | http ]
This paper addresses the design and verification of 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 with Wojciechowski and Pierce we made the two levels precise as process calculi, allowing such algorithms to be expressed as encodings of the high level into the low level; we built Nomadic Pict, a distributed programming language for experimenting with such encodings. In this paper we turn to semantics, giving a definition of the core language and proving correctness of an example infrastructure. This requires novel techniques: we develop equivalences that take migration into account, and reasoning principles for agents that are temporarily immobile (eg. waiting on a lock elsewhere in the system).

 
Nomadic Pict: Language and Infrastructure Design for Mobile Agents. Pawel T. Wojciechowski and Peter Sewell. IEEE Concurrency, 8(2):42--52, April--June 2000. Invited submission for ASA/MA 99. [ bib | doi | project page | http ]
Location-independent communication between migrating agents requires a distributed infrastructure. The authors describe their Nomadic Pict distributed programming language and use it to develop an infrastructure for an example application.

 
Nomadic Pict: Language and Infrastructure Design for Mobile Agents. Pawel T. Wojciechowski and Peter Sewell. In ASA/MA 1999, Best paper award. [ bib | doi | project page | ps | pdf | http ]
We study the distributed infrastructures required for location-independent communication between migrating agents. These infrastructures are problematic: different applications may have very different patterns of migration and communication, and require different performance and robustness properties; algorithms must be designed with these in mind. To study this problem we introduce an agent programming language --- Nomadic Pict. It is designed to allow infrastructure algorithms to be expressed as clearly as possible, as translations from a high-level language to a low level. The levels are based on rigorously-defined process calculi, they provide sharp levels of abstraction. In this paper we describe the language and use it to develop an infrastructure for an example application. The language and examples have been implemented; we conclude with a description of the compiler and runtime.

 
Location-Independent Communication for Mobile Agents: a Two-Level Architecture, Peter Sewell, Pawel T. Wojciechowski, and Benjamin C. Pierce. pages 1--31. Springer-Verlag, October 1999. [ bib | doi | project page | ps | pdf | .html ]
We study communication primitives for interaction 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 its current site and of any migrations. Implementation of these requires delicate distributed infrastructure. We propose a simple calculus of agents that allows implementation of such distributed infrastructure algorithms to be expressed as encodings, or compilations, of the whole calculus into the fragment with only location dependent communication. These encodings give executable descriptions of the algorithms, providing a clean implementation strategy for prototype languages. The calculus is equipped with a precise semantics, providing a solid basis for understanding the algorithms and reasoning about their correctness and robustness. Two sample infrastructure algorithms are presented as encodings.

 
Location-Independent Communication for Mobile Agents: a Two-Level Architecture. Peter Sewell, Pawel T. Wojciechowski, and Benjamin C. Pierce. Technical Report UCAM-CL-TR-462, Computer Laboratory, University of Cambridge, April 1999. 31pp. [ bib | project page | ps | pdf | .html ]
We study communication primitives for interaction 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 its current site and of any migrations. Implementation of these requires delicate distributed infrastructure. We propose a simple calculus of agents that allows implementation of such distributed infrastructure algorithms to be expressed as encodings, or compilations, of the whole calculus into the fragment with only location dependent communication. These encodings give executable descriptions of the algorithms, providing a clean implementation strategy for prototype languages. The calculus is equipped with a precise semantics, providing a solid basis for understanding the algorithms and reasoning about their correctness and robustness. Two sample infrastructure algorithms are presented as encodings.

 
Location Independence for Mobile Agents. Peter Sewell, Pawel T. Wojciechowski, and Benjamin C. Pierce. In WIPL 1998, 6pp. [ bib | project page | ps | pdf ]