Book contents
- Frontmatter
- Preface
- Contents
- An introduction to process algebra
- Two simple protocols
- Proving mutual exclusion with process algebra
- Process algebra as a tool for the specification and verification of CIM-architectures
- A process creation mechanism in process algebra
- Correctness proofs for systolic algorithms: palindromes and sorting
- Verification of an algorithm for log-time sorting by square comparison
- On the Amoeba protocol
- Process algebra semantics of POOL
- Some observations on redundancy in a context
- A modular approach to protocol verification using process algebra
- Index of concepts
- Index of names
- Index of symbols and notation
Correctness proofs for systolic algorithms: palindromes and sorting
Published online by Cambridge University Press: 03 December 2009
- Frontmatter
- Preface
- Contents
- An introduction to process algebra
- Two simple protocols
- Proving mutual exclusion with process algebra
- Process algebra as a tool for the specification and verification of CIM-architectures
- A process creation mechanism in process algebra
- Correctness proofs for systolic algorithms: palindromes and sorting
- Verification of an algorithm for log-time sorting by square comparison
- On the Amoeba protocol
- Process algebra semantics of POOL
- Some observations on redundancy in a context
- A modular approach to protocol verification using process algebra
- Index of concepts
- Index of names
- Index of symbols and notation
Summary
In designing VLSI-circuits it is very useful, if not necessary, to construct the specific circuit by placing simple components in regular configurations. Systolic systems are circuits built up from arrays of cells and therefore very suitable for formal analysis and induction methods. In two examples correctness proofs are given using bisimulation semantics with asynchronous cooperation. These examples also have been worked out by Hennessy in a setting of failure semantics with synchronous cooperation. Finally the notion of process creation is introduced and used to construct machines with unbounded capacity.
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.
- Type
- Chapter
- Information
- Applications of Process Algebra , pp. 89 - 126Publisher: Cambridge University PressPrint publication year: 1990
- 1
- Cited by