Research activity

Work has been done on theory of $\pi$-calculus, semantic definition of concurrent object-oriented programming languages, and correctness of transformation rules for programs and of concurrent algorithms on data structures.

In a process setting, the essence of confluence is that the occurrence of one action may not preclude others. In the case of $\pi$-calculus, where names may be extruded from their scopes, care is needed to find the right definition. Basic results on confluence in $\pi$-calculus are presented in [PW97]. In particular, conditions under which combinations of confluent, or almost-confluent, processes yield confluent systems are presented.

The view that general models of mobile processes, such as $\pi$-calculus and Higher-Order $\pi$-calculus, provide a good framework for the definition of a variety of concurrent object-oriented languages is illustrated in [LW97a]. A technique involving process continuations is used to give a natural and direct semantic definition for a language containing constructs for several kinds of inter-object communication. In the unpublished MSc dissertation [S97], an experimental extension of Pict with actor primitives is given semantic definition and implemented. Its author is now studying for a PhD at Cambridge.

In [LW97b], which was revised for publication this year, a theory of partial-confluence of processes is developed, in CCS and in $\pi$-calculus. The main theorem concerns systems which can be thought of as composed from two components: a questioner, and an answerer which may process questions concurrently. It gives conditions under which a system of this kind is behaviourally indistinguishable from the corresponding system in which the answerer may handle only one question at a time. This result, together with a semantic definition of the kind described above, is used to show the interchangeability in an arbitrary program context of two class definitions which prescribe binary-tree symbol-table data structures, one supporting concurrent operations, the other sequential.

In [PW97b], this work is extended to show the soundness of transformation rules for concurrent object-oriented programs which increase the scope for concurrent activity within the system prescribed by a program, without altering its observable behaviour. The rules allow one object to release another from a rendezvous before it has finished all the associated activity, and allow one object to delegate to a second object the responsibility for returning a result to a third object.

In [PW97c], the theory of [PW97b]is extended to encompass a larger class of answerers. Analogous behavioural indistinguishability results are obtained, for an appropriate class of questioners. The main advance is that whereas in the case of the symbol-table data structures, the answer to a question is determined at the moment the question is submitted, in [6] up to one state-changing internal action may occur in determining the answer.

This result is used in [PW97d] where algorithms for operating concurrently on a variant of the B-tree data structure are modelled and analysed using $\pi$-calculus. In this case the state-changing internal action is the act of locking the disk page in which the operation in question will take effect. Deficiences in and improvements to published algorithms were discovered.

The PhD thesis [P97phd] contains also other work on confluence of processes. The MSc dissertation [I97] begins to explore a new approach to modelling asynchronous communication and fault-tolerance in a process-calculus setting. Its author is now studying for a PhD at Edinburgh.