Nomadic Pict: Programming Languages, Communication Infrastructure Overlays, and Semantics for Mobile Computation

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 netwo...

Full description

Saved in:
Bibliographic Details
Published in:ACM transactions on programming languages and systems 2010-04, Vol.32 (4), p.1-63
Main Authors: SEWELL, Peter, WOJCIECHOWSKI, Paweł T, UNYAPOTH, Asis
Format: Article
Language:English
Subjects:
Applied sciences
Calculi
Calculus
Computer science
control theory
systems
Computer systems and distributed systems. User interface
Design engineering
Exact sciences and technology
Mathematical analysis
Migration
Mobile computing
Networks
Semantics
Software
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0164-0925
1558-4593
DOI:10.1145/1734206.1734209