Local Areas in the Pi-Calculus

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