ABSTRACTION AND SILENT STEP

As we argued in the previous chapter, we want to be able to abstract from certain actions, to hide them. It is important to note that it does not always work out well to simply remove steps (as what happens when we apply the operator θI; see for example exercise 4.6.7.2). This is because we want a process to behave precisely as it did before abstraction, apart from the actions abstracted from. For instance, a process having deadlock before abstraction, must still do so afterwards. As an example, consider the process a+bδ which has deadlock (see exercise 2.2.12.9), but after leaving out b by renaming it into θ, we obtain a+δ = a, which is without deadlock because of axiom A6 from BPAδ.

This is why we introduce the silent step τ, which can be removed in some cases, but in other cases it cannot. Abstraction now means renaming into τ. SO, abstracting from b in the process a+bδ, we obtain a+τδ, and in this case we cannot remove τ. We conclude that τa ≠ a (since τa+b ≠ a+b). However, abstracting from b in the process abc, we obtain aτc, and since this τ does not occur in a choice context, it can be removed: ac = ac.

COLOURED TRACES

Let us allow a new symbol τ to appear as a label. As mentioned earlier, this label τ refers to a silent step: by executing τ-steps the process proceeds but observers cannot record any visible actions.

HISTORICAL REMARKS

Process algebra, as described in this book, has for the most part been the work of people at the Centre of Mathematics and Computer Science in Amsterdam. There, J.A. Bergstra and J.W. Klop started with the theory PA in 1982, motivated by a question of J.W. de Bakker (see [BERGSTRA & KLOP [1982]). As a general reference to their work, see BERGSTRA & KLOP [1984b], in which a fairly detailed discussion of related work can be found as well. The most extensive treatment of their work can be found in the Dutch book BAETEN [1986], which was the starting point for this book.

Compared to other concurrency theories, this work is closely related to the work on CCS. The theory of CCS is briefly discussed in the following section 8.2. The seminal work of MlLNER [1980] in which CCS was introduced, clearly sets out the goals of algebraic concurrency theory. We may see the theory of ACPτ as a remodularization of CCS. CCS has been worked out and extended in the work of HENNESSY & PLOTKIN [1980] and HENNESSY [1983]. See also HENNESSY & MlLNER [1985], GRAF & SIFAKIS [1984] and BROOKES & ROUNDS [1981]. MILNE [1982] has the so-called ‘dot calculus’, with · as parallel composition, prefix multiplication, two operators for alternative composition (internal and external choice) and, in contrast with Milner, n-ary communication.

COMMUNICATION FUNCTION

A central issue in concurrency theory is that of modelling communication. The method that we present here yields synchronous communication. That is, the occurrence of communication between two processes is the result of the simultaneous performance of corresponding actions. For instance, one process may perform a send action, whereas the other performs a receive action, and if these actions take place simultaneously the result is a communicate action. Later on, we will also consider examples of asynchronous communication in process algebra.

In synchronous communication, every communication action has two parts. This can be enoted as follows: suppose an atomic action comm(5) represents the communication between send(5) and receive(5), then we write

If two actions do not communicate, then their communication is not defined. For example:

This will be formalized in the next paragraph.

DEFINITION

Let A be the set of atomic actions. A communication function on A is a partial binary function γ on A satisfying the following conditions:

1. for every a,b∈ A: γ(a,b) = γ(b,a), that is, communication is commutative;

2. for every a,b,c∈ A: γ(γ(a,b),c) = γ(aγ(b,C)): communication is associative.

When we write such an equation for a partial function, we also imply that one side of the equation is defined exactly when the other side is. Also, γ is not defined when one of its arguments is not defined or is not in A.

INTRODUCTION

One can speak of Computer Integrated Manufacturing (CIM) if the computer is used in all phases of the production of some industrial product. In this paper we will focus on the design of the product-flow and the information-flow, which occurs when products are actually produced. Topics like product-development, marketing and management are beyond the scope of this paper. The technique used in this paper is based on a theory for concurrency, called process algebra (see or). It can be used to describe the total phase of manufacturing, from the ordering of raw materials up to the shipping of the products which are made from this materials. During this process many machines are used, which can operate independently, but often depend on the correct operation of each other. Providing a correct functioning of the total of all machines, computers and transport-services is not a trivial exercise. Before actually building such a system (a CIM-architecture) there must be some design. Such a specification, when validated, describes a properly functioning system.

INTRODUCTION

At this moment there are a lot of programming languages which offer facilities for concurrent programming. The basic notions of some of these languages, for example CSP, occam and LOTOS, are rather close to the basic notions in ACP, and it is not very difficult to give semantics of these languages in the framework of ACP. Milner showed how a simple high level concurrent language can be translated into CCS. However, it is not obvious at first sight how to give process algebra semantics of more complex concurrent programming languages like Ada, Pascal-Plus or POOL. This is an important problem because of the simple fact that a lot of concurrent systems are specified in terms of these languages. In this article we will tackle the problem, and give process algebra semantics of the language POOL.

INTRODUCTION

Extension of process algebra

In this paper we extend process algebra with a new operator that will be helpful to describe process creation. From a methodological point of view the extension of process algebra with new operators is just the right way to incorporate new features. Only in a very rich calculus with many operators one may hope to be able to perform significant algebraic calculations on systems. In many cases a new feature requires new (additional) syntax and more equations, only in very rare circumstances the addition of equations alone suffices to obtain an appropriate model of some new system aspect. The core system ACP, see, describes asynchronous cooperation with synchronous communication.

On top of ACP various features can be added, for instance: asynchronous communication, cooperation in the presence of shared data, broadcasting, interrupts. This note adds process creation to the features that are compatible with process algebra.

For historical remarks and relations with previous literature we refer to.

Process creation

We start on basis of the axiom system ACP which is supposed to be known to the reader. We assume the presence of a finite set of data D and introduce for each d∈D an action cr(d). The action cr(d) stands for: create a process on basis of initial information d. Let cr(D) denote the set {cr(d)|d∈D}.

INTRODUCTION

Many authors have studied the concurrency aspects of sorting, and indeed the n-time bubblesort algorithm (using n processors) is rather thoroughly analyzed already (e.g. see: Hennessy, Kossen and Weijland). However, bubblesort is not the most efficient sorting algorithm in sequential programming, since it is n2-time and for instance heapsort and mergesort are n log n-time sorting algorithms. So, the natural question arises whether it would be possible to design an algorithm using even less than n-time.

In this paper we discuss a concurrent algorithm, capable of sorting n numbers in O(log n) time. This algorithm is based on the idea of square comparison: putting all numbers to be sorted in a square matrix, all comparisons can be made in O(1) time, using n2 processors (one for each cell of the matrix). Then, the algorithm only needs to evaluate the result of this operation.

The algorithm presented here, which is called ranksort, is not the only concurrent time-efficient sorting algorithm. Several sub n-time algorithms have been developed by others (see: Thompson).

One of the basic problems in protocol verification is the following: data are to be transmitted from A to B via some unreliable medium M. A protocol has been proposed for doing so correctly and perhaps efficiently. A rigorous mathematical proof of the correctness claim is desired.

Now protocol verification aims at providing the techniques for giving such a proof. Several formalisms have been advocated, but as yet none has been widely accepted.

The framework we adhere to is process algebra. The first protocol correctness proof by means of process algebra is in Bergstra and Klop, where a simple version of the Alternating Bit Protocol is verified.

We have tried our hands at a more complicated version, called the Concurrent Alternating Bit Protocol (CABP) and found that the number of possible state transitions was prohibitively large. In this article we propose a divide-and-conquer strategy. We group processes into modules, describe and verify their behaviour and finally combine them. For different approaches, see.

In Section 1 we deal with the Concurrent Alternating Bit Protocol (CABP). In Section 2 we present the modular approach. Modules are introduced in Section 3, whereas the verification of the CABP is given in Section 4.

It has been observed that formal verification methods for mathematical proofs, computer programs, communication protocols and the like are usually illustrated by ‘toy’ examples and that such proofs tend to be discouragingly long. In order to demonstrate that it is feasible to verify a ‘real-life’ communication protocol by means of process algebra, we picked one from the literature.

In his Ph.D. thesis, Mullender investigates issues he considered while developing the Amoeba distributed operating system. In Section 3.2.4 of a transaction protocol is described to which we will refer as the Amoeba protocol. In the preceding sections of the design goals are described that this protocol is supposed to satisfy. He does not give a formal verification that his protocol meets this criteria. In fact, it turns out that one of them is not met. Note that this only applies to the simplified version of the protocol that appears in, the actual implementation uses a much more complicated version in which this mistake is not found.

Section 1 of this article gives the minimum background information necessary for understanding the rest of the article.

In Section 2 the design goals are formulated in English and in terms of process algebra.

INTRODUCTION

In this article we will present simple descriptions of so-called systolic systems. Such systems can be looked at as a large integration of identical cells in such a way that the behaviour of the total system strongly resembles the behaviour of the individual cells. In fact the total system behaves like one of its individual cells ‘on a larger scale’.

For example one can think of a machine sorting arrays of numbers with a certain maximum length. Suppose we need a machine handling arrays that are much longer. A typical ‘systolic approach’ to this problem would be to try to interconnect the smaller machines such that the total circuit sorts arrays of a greater length. As a matter of fact this specific example will be worked out in the following sections. In designing VLSI-circuits (short for very large scale integrated circuits) it is very useful, if not necessary, to construct the specific circuit by placing simple components in regular configurations. Otherwise one looses all intuition about the behaviour of the circuit that is eventually constructed.