Nomadic Pict

Implementation and Semantics of Mobile Agent Infrastructure

The Nomadic Pict project studied programming language design and communication primitives for mobile computation. Communication primitives for interaction between mobile agents can be classified into two levels of abstraction. At a low level there are location dependent primitives that require an 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 proposed a simple calculus of agents that allows implementations 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 for reasoning about their correctness and robustness.

We implemented a language, Nomadic Pict, based on the calculus to enable experiments with distributed algorithms and agent computing. Nomadic Pict is an extension of Pict with the notion of locations, agents, migration, distribution, and failures. At the same time we developed reasoning techniques for correctness and robustness proofs of these algorithms.

Those involved include

An alpha release of the implementation is available from the language web page. It includes a tutorial.

Some relevant papers are below; others can be found on the individual pages above.

Peter.Sewell@cl.cam.ac.uk

[Validate this page.]