Process Algebras for Locality

Introduction

Process algebras are formalisms for the specification and description of distributed, and in general, concurrent systems. Process algebras provide means to specify parallel composition (two processes operating at the same time), alternative composition (a choice between two processes) and sequential composition (a process operating after another process terminates) (Baeten et al. 2007).

Traditionally in process algebras, processes communicate with each other via channels. In a communication on a particular channel one of the processes writes to the channel and another process reads from the channel. Channels are a kind of a more general construct, called names. A name is an identifier, and it is only useful for comparing for identity with other names (Needham, 1989). In the area of process algebras, channel reads are referred to as abstractions, while channel writes are referred to as concretions.

Process algebras were conceived at the end of the 1970s (Milner, 1980, Antony and Hoare, 1978, Bergstra and Klop, 1985). Based on one of these early algebras, the Calculus of Communicating Systems (Milner, 1980), Robin Milner, Joachim Parrow, and David Walker developed the π-calculus (Milner et al., 1989). An extensively studied formalism, one of the main contributions of the π-calculus is the ability to establish and terminate communication channels dynamically. Process expressions in the π-calculus have the following syntax:

0 represents the null process. ā(ẽ).P represents a process writing names ẽ on channel a. In general, ẽ is used to indicate zero, or one or more names. After the names are read, the process continues as P. a(ẽ).P represents a process waiting for input on channel a. When the input is received, the process continues as P. P+Q, called summation of processes, represents a process that behaves either like P or Q. P|Q represents the parallel execution of processes P and Q. newa P, called restriction, is used to specify a private name a used in process P. P!, called replication, represents an infinite number of copies of P, running in parallel. Some variations of the π-calculus support recursive processes in-lieu of replication.

Because only names can be transmitted in channel communications, π-calculus is a first-order process algebra. Process algebras where names and processes can be transmitted as part of a channel communication are said to be higher-order algebras.

The asynchronous π-calculus was one of the first variations proposed of the π-calculus (Honda and Tokoro, 1991, Boudol, 1992). In the asynchronous π-calculus, outputs on channels cannot be followed by a process, and the summation of processes is eliminated from the algebra.

Some process algebras provide abstractions for modelling localities. A locality provides the ability to group, name, and transmit processes. Some process algebras allow locations to be transmitted as part of channel communications. The ability to associate a process with a location is of interest when formalizing and verifying locality-based processing. For example, one may be interested in formalizing that processing must occur at a certain location, or that a process may migrate from one location to another under certain conditions.