Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
The Nomadic Pict Page

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

Ken Moody
Peter Sewell
Benjamin Pierce (University of Pennsylvania)
Asis Unypoth
Pawel T. Wojciechowski (Poznan)

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.

Nomadic Pi Calculi: Expressing and Verifying Infrastructure for Mobile Computation, Asis Unyapoth, Ph.D. thesis. Appeared as Technical Report 514, Computer Laboratory, University of Cambridge, June 2001. Also in ps and pdf. Here is the abstract .
Algorithms for Location-Independent Communication between Mobile Agents. Pawel Wojciechowski. Technical Report 2001/13, Communication Systems Department, EPFL, March 2001. Abstract. In pdf. Here is a shorter version which appeared in the AISB'01 / Symposium on Software mobility and adaptive behaviour. These are copied in Cambridge: ps.gz, pdf, and abstract .
Nomadic Pict: Correct Communication Infrastructure for Mobile Computation, Asis Unypoth and Peter Sewell. In POPL 2001. Also in pdf, dvi, and ps.
Nomadic Pict: Language and Infrastructure Design for Mobile Computation . Pawel Wojciechowski, Ph.D. thesis. Appeared as Technical Report 492, Computer Laboratory, University of Cambridge, June 2000. Also in pdf. Here is the abstract . These are copied in Cambridge: ps.gz, pdf, and abstract .
Nomadic Pict: Language and Infrastructure Design for Mobile Agents, Pawel Wojciechowski and Peter Sewell. This appeared in ASA/MA'99 (First International Symposium on Agent Systems and Applications/Third International Symposium on Mobile Agents), October 1999. An extended version appeared in IEEE Concurrency vol 8 no 2, 2000.
Location-Independent Communication for Mobile Agents: a Two-Level Architecture, Peter Sewell, Pawel Wojciechowski and Benjamin Pierce. Technical Report 462, Computer Laboratory, University of Cambridge. A version of this appeared in Internet Programming Languages, LNCS 1686.
Location Independence for Mobile Agents, Peter Sewell, Pawel Wojciechowski and Benjamin Pierce. This appeared in the Workshop on Internet Programming Languages, 1998. It is largely superseded by Technical Report 462 above.

We are associated with the Opera and Theory and Semantics groups of the University of Cambridge Computer Laboratory.

opera
group theory and semantics

Copyright

The following IEEE notices apply to the ASA/MA 99 paper:

(c) 1999 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Peter.Sewell@cl.cam.ac.uk

[Validate this page.]