Jump Over Left Menu
DCS Projects: Edinburgh
A J R G MILNER
APPLICATIONS OF FLOW ALGEBRAS TO PROBLEMS IN CONCURRENT COMPUTATION
Jan 78 - Sept 79
This project takes as its starting point the work by Milne and Milner  on a process model of concurrent computation. This mathematical framework has been produced to enable a person to reason about computing systems in terms of the mathematical objects which model them. The question as to what is the most suitable framework to represent concurrent computation remains open but an apparently successful step has been made by the Flow Algebra of Processes. In  the process algebra is used in the construction of a model of a card reader and in the representation of communication scheduling. In both these examples correctness proofs have been found. As well as adopting an algebraic approach, the model uses the semantic concepts of Scott and Strachey  whereby the meaning of a system (or net) of communicating agents is an abstract object (a process). The meaning of such a system is constructed from the composition (via suitable operations) of the meanings of the system components.
The purpose of this project is to investigate the suitability of processes in particular, and other Flow Algebras in general, as models of concur computation. Application of the theory to real problems of concurrency should reveal those features of concurrency not suitably represented in the theory, and should also suggest changes to produce a better theory.
The first investigation has been in the area of distributed database systems. A real problem of such database systems arises when one wishes to keep copies of databases at various nodes (to minimise access delays). The problem is to produce a control algorithm to reside at each node of a computer network to control access to its own and to other databases. The protocols should control the communication and transfer of information between nodes in such a manner that the system does not deadlock, that the data remain consistent (at all times after the system has settled following an update all copies of a database are identical), that data accessing delays are minimised and that the system remains partially operable when one or more nodes has failed. Ellis  has produced a number of algorithms which aim to deal with these problems. The solution which he believes to be most satisfactory has been modelled using processes. By altering the definition of a process algebra slightly, a concise process formulation of Ellis algorithm was found. The alteration expresses, more naturally than using the previous process algebra, the notion of a simultaneous broadcast communication between one process and a number of others. The database network was modelled by combining a number of processes (each of which models a database manager) using a synchronising conjunction operator. A proof that the network is free from deadlock has been carried out but needs checking. Such a result gives some evidence that the model is on the right track.
Future work will be concerned not only with providing the consistency and partial operability of the above chosen example but also with examining a completely different level of concurrent computation - that of the problems of hardware representation and design. Many difficult problems exist concerning modelling of hardware and it needs to be seen whether the process algebra (or some similar Flow Algebra) can go some way towards satisfying them. An obvious problem is that of modelling an inherently continuous system by a discrete model. Also the present model assumes asynchronous communication, and it must be seen whether strongly synchronous communication can be suitably represented.
What has been achieved so far is not only a notation in which the behaviour of systems of communicating computing agents can be represented in a concise, intuitive manner as it evolves through time, but also a mathematical framework for formal reasoning about such systems. Certain proof techniques have already been developed but others need to be found. It has also become apparent that when modelling different concurrent systems and carrying out proofs on them, different algebras may need to be used. Guidelines governing the choice of algebra must be found. It must also be determined which properties of concurrency are preserved when mapping from one algebra into another.
PROGRESS TO SEPT 1979
This project is the work of one researcher, George Milne, under the direction of Robin Milner.
Many challenging examples of concurrency present problems which are mainly concerned with the control features of systems, rather than with the flow of data within. Syn algebras and Synchronised Behaviours were introduced to capture this pure synchronisation. This new framework is a natural variation of Flow Algebras, but does not model the passage of values between components of a system; on the other hand, it allows for multi-way synchronisation and does not restrict one to communications between two components as in Flow Algebra.
A major example tackled was that of a distributed database system. This system comprises a number of nodes containing databases, some of which hold identical copies. The investigators modelled the control portion of each node which controls access to its own and other databases. They in fact abstract away from the databases themselves, and use the models of the components to produce a model of the whole communicating control system, using their & combinator. Broadcasting of signals. which is inherent in this system, is easily represented by an n-way synchronisation between the sender and the n-l receivers, all n cooperating in this event. Once modelled, they use algebraic laws to prove a desired property of the system, namely, that it is free from deadlock.
At the other end of the spectrum they have also investigated some of the problems of modelling gate-level hardware using the Syn framework. There is a need for design and specification languages for representing the behavioural features of hardware components and not just their static features. Their investigation leads them to think that the Syn framework may be useful for this purpose, since it allows them to represent as primitive the rising and falling change on lines, together with the simultaneous effect of such a change upon possibly more than two components. Problems with this involve representing inherently continuous behaviour in a discrete model, and dealing with complicated behaviours. The latter means that the object representing this behaviour in their model is also very complex. Problems arise when combining such complex objects using the & combinator, and in carrying out proofs such as the equivalence of a composite system with its design specification. Some mechanisation of this part is probably necessary.
They investigated some standard concurrency problems to assess the flexibility of their model, including the Cigarette Smokers, and the Dining Philosophers problems. Using their model, various solutions to both problems can be produced. These are proved to satisfy the problem specification and thus to be equivalent with each other. This partly supports their claim that the algebraic method helps them to gain insight into different solutions to the same problem, and to compare them.
1. C. A. Ellis, Consistency and Correctness of Duplicate Database Systems, Sixth ACM Symposium on Operating Systems Principles, SIGOPS 11.5, Nov 1977.
2. G. Milne, R.Milner, Concurrent Processes and their Syntax. JACM 26, 2, pp 302-321, 1979.
3. G. Milne, A Mathematical Model of Concurrent Computation. Ph.D Thesis, Edinburgh, 1978.
4. D. Scott, C. Strachey, Towards a Mathematical Semantics for Computer Languages, Proceedings Symposium on Computers and Automata, Microwave Research Institute Symposia Series, Vol 21, Polytechnic Institute of Brooklyn, 1971.
5. G. Milne, Scheduling within a process model of computation, Proc. 1st European Conference on Parallel and Distributed Processing, Toulouse, France, February 1979.
6. G. Milne, Modelling distributed database protocols by synchronisation processes, Report CSR-34-78, Computer Science Department, University of Edinburgh.
DR G D PLOTKIN and A J R G MILNER
SEMANTICS OF A NON-DETERMINISTIC AND CONCURRENT COMPUTATION
Oct 81 - Sept 84
Background and Nature of Research
In the past five years, the focus of interest on distributed computing has led to tremendous interest in the design of concurrent programming languages, and in the need to describe and vigorously analyse the design of distributed hardware.
Concurrency is now no longer regarded as something to be grafted on to the classical sequential view of computation; it is rather seen as a basic idea, of which sequential computation is just a special case.
Like its predecessor, this project - which began at full strength in 1982 - concentrates upon the central concepts both of the computations and of incomplete (hence non-deterministic) descriptions of computations. The aim remains to isolate these concepts, to find suitable mathematical expressions for them. and to develop techniques for analysing systems and languages in terms of them.
The present focus of the project is on the mathematics of non-determinism, and on the relation between algebraic calculi for concurrency (developed in part by the preceding project) and methods of proof based upon suitable logics - in particular, temporal and tense logics.
Work in Hand
1. Modal and Tense Logic
In previous work, Hennessy and Milner defined an equivalence between processes called observational equivalence  . They showed that this equivalence can be characterised by a modal language. Colin Sterling has used this language to give complete modal proof theories for non-deterministic process languages .
Finer equivalences than observational equivalence have been defined between processes which take into account their liveness properties  . Joint work (between Colin Sterling and Matthew Hennessy) is in progress which has extended the modal characterisation result to these equivalences by using relativised branch time tense logics: logics where eventually operators are relativised to particular (general) paths into the future.
2. Operational semantics for "Liveness"
C Sterling and G Costa have been investigating a new way of handling the property of liveness (the assumption of unbounded but finite delay in computation) using variants of the operational semantic techniques employed by much work in Edinburgh projects. The problem arises when dealing with systems where (some) components evolve asynchronously. In modelling such systems. one usually considers languages in which there is a (binary) parallel operator. In the operational semantics for such languages. asynchrony is usually modelled by assuming rules which force interleaving of the actions of the operands of the parallel operator. The set of computation sequences produced by those rules then contains sequences which are "unfair". The aim is to find rules which will not produce unfair sequences, without enforcing synchrony. This has been achieved for a language which is a subset of Milner's CCS  .
The subset of CCS considered does not allow a distinction to be made between weak and strong fairness, whereas full CCS does. Work is in progress which extends the previous results to these notations of fairness. Further work in progress is the development of fair equivalences between process which do not appeal to infinite computations.
The research undertaken, however mathematically technical, is constantly guided by the need for good notations for expressing and analysing concurrent computations, and rigorous criteria by which to design articulate concurrent programming languages. Contacts with both ICL and STL (Harlow) have indicated that industry is interested in mathematical foundations, and is already willing to experiment with notations and techniques as they emerge.
1. G. Costa and C. Sterling, A Fair Calculus of Communicating Systems, Foundations of Computation Theory, 1983. Lecture Notes in Computer Science, Vol. 158, 1983, (and an extended version as internal report CSR-137-83).
2. M. Hennessy, Axiomatizing Finite Element Delay Operators, internal report CSR-124-82.
3. M. Hennessy and R. Milner, On Observing Nondeterminism and Concurrency, Lecture Notes in Computer Science, Vol. 85, pp. 299-309, 1980.
4. R. Milner, A Calculus of Communicating Systems, Lecture Notes in Lecture Notes in Computer Science, Vol. 92. 1980.
5. C. Sterling, A Proof Theoretical Characterization of Observational Equivalence, internal report CSR-132-83, (to appear in FCT and TCS, Bangalore, December 1983).
N H SHELNESS
AN ARCHITECTURE FOR A MULTIPLE COMPUTER SYSTEM
Oct 77 - Sept 80
This project commenced in 1973. It sprang from a supposition common to a number of other projects in the programme, that there exists a broad class of computer applications for which hardware containing more than one processor (CPU) would form a more effective base than hardware containing only a single processor. Increased effectiveness can be measured in terms of improved reliability, throughput, response, ease of growth or economy, the relative weighting of which will depend on the nature of the application.
An early study of how these various improvements could be effective in a system containing more than 2 or 3 processors led rapidly to a conclusion that such systems would need to make only minimal use of shared common memory and that this being the case, a more effective solution was to dispense with shared memory and to employ an inter-machine communications sub-system in its stead. An immediate result of dispensing with shared memory is that an application has to be programmed differently. The application requires a structure during execution that allows the code and data required by a sub-computation to be firstly identified and secondly transferred between and assigned to particular processors and their private memories.
From 1974-76 the group, especially Dr Laim Casey, devoted its efforts to developing and evaluating through simulation a structure (the distributed domain model) that would satisfy this requirement. During 1977 and early 1978 a number of improvements to this model were developed and evaluated. This led to the elaboration of a new. simpler and more powerful structure (the segment flow model) based on a generalisation of the distributed domain model.
In parallel with this latter effort. the group approached the SERC to fund the construction of a multi-computer test-bed on which the proposed models could be implemented and evaluated by successfully constructing a number of realistic pilot applications.
The test-bed which was installed in mid-1978. was built from Ferranti Argus 700 components. There are three identical computers or sites. Each site consists of an Argus 700 CPU which serves as the interface processor. The three sites are linked via the peripheral bus of each of the Argus 700Fs to a fast inter-site bus into which is also connected an Interdata 70 computer. This Interdata 70 which serves as a peripheral and maintenance processor for the entire system runs existing software and is linked through a high speed local network to standard peripherals and the Departments file processor.
The basic system was completed during 1980 but was still far from robust. However enough progress was made to produce some initial performance measures.
A segment transfer between two domains running on the same site took approximately 3 milliseconds of elapsed time. The same transfer between two domains running on different sites took approximately 25 milliseconds of elapsed time.
1. L. Casey and N.H.Shelness. A Domain Structure for Distributed Computing Systems, In ACM Operating Systems Review, Vol 11, No 5 and CSR-8-77 Edinburgh Computer Science Dept.
2. L. Casey. Structures for Distributed Computing Systems, Internal Report CST-2-77, Edinburgh Computer Science Dept.
3. L. Casey, On Kernels for Distributed Computing Systems, Internal Report CSR-27-78. Edinburgh Computer Science Dept.