University of Cambridge


Local Areas in the Pi-Calculus

By Tom Chothia and Ian Stark (Division of Informatics, University of Edinburgh).

In concurrent and distributed systems, it is common to find names that are widely known but always refer to local resources: for example, when a program connects to a well-known IP port, or makes library calls to operating system services. If we try to build a process calculus model of such systems in the pi-calculus, we meet a problem: the scope of a name is always identical to its reach; so for example a global name always represents a global service.

In this talk I shall present joint work with Tom Chothia on a local area pi-calculus which separates these issues, introducing areas stratified by levels. For example, a well-known name can now refer to a service that is local to the current application, a single host, or a network. Names and areas may be dynamically created, but with fixed rules for their interaction.

We have a type system that statically checks the correct use of names, and an encoding into the standard pi-calculus. The calculus is expressive enough to model success and failure in distributed protocols: for example, we use it to illustrate how FTP and Napster cope with firewalls based on network address translation (NAT).