Process Algebras for Locality

Process Algebras for Locality

Rolando Blanco (University of Waterloo, Canada) and Paulo Alencar (University of Waterloo, Canada)
DOI: 10.4018/978-1-61520-655-1.ch030
OnDemand PDF Download:
$37.50

Abstract

Several process algebras have been proposed in the literature to support the notion of locality. In this chapter the authors compare some of these process algebras, namely Distributed p, Ambient Calculus, Join Calculus, M-calculus, and Kell Calculus. Specifically, they look at the locality abstractions supported by the algebras and how these abstractions interact with the communication mechanisms in the algebras, higher-order constructs, and process passivation. The authors also look at the model checking support in the algebras that allow the verification of locality-based behaviour.
Chapter Preview
Top

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:

P0 |ā().P|a().P|P+Q| P|Q |newa P|P!

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.

Key Terms in this Chapter

Process Calculus: Another name for Process Algebra.

Higher-Order Process Algebra: A process algebra in which process expressions can be passed from one process to another in a communication on a channel.

First-Order Process Algebra: An algebra in which process expressions cannot be passed from one process to another in a communication on a channel.

Process Algebra: A formalism for the specification of concurrent systems by algebraic means. Each process algebra has a formal syntax that indicates which are valid expressions in the algebra, and a formal semantic that indicates how valid expressions evolve.

Name: A sequence of characters used to identify a channel or a locality.

Process: For a given process algebra, a process in the algebra is a valid expression according to the syntactic specification of the algebra. Processes are used to represent a system or part of a system.

Locality: A construct in a process algebra that allows the grouping and naming of processes. Processes grouped within a locality are said to be running at that locality. In some process algebras localities are themselves processes.

Channel: A communication mechanism in process algebras. Channels are identified by name. During a communication a process writes on a channel and another process reads from the channel.

Complete Chapter List

Search this Book:
Reset