Note: the dissertation is available in physical form at the University Library; I hope also to make it available soon as a tech report.
This work describes a concurrent, distributed abstract machine for the pi calculus. It is relevant to researchers in the field of concurrency, and to working programmers looking for a better way to write interactive programs.
The pi calculus of Milner, Parrow and Walker [1989] is a widely studied formalism for describing interactive and concurrent systems. Its basic mechanism is synchronous message-passing over a channel: (1) One program signals its readiness to transmit some data over a channel; (2) Another program signals its readiness to receive over that channel; (3) When it has been established that two programs are ready to communicate, they do.
I introduce a new model for synchronous rendezvous — using explicit fusions. 'Fusion' means that, during communication, the data is temporarily shared between the two participating programs. 'Explicit' means that this fusion can persist in the program, allowing us to delay and control the effect of the communication. In this sense, explicit fusions do for the pi calculus what the explicit substitutions of Abadi, Cardelli, Curien and Lévy [1991] do for the lambda calculus.
The dissertation has two halves: theory and implementation. The theory introduces the explicit fusion calculus — a variant of the pi calculus that includes explicit fusions. I study its bisimulation, and relate it to the fusion calculus of Victor and Parrow [1998], the chi calculus of Fu [1997] and Sangiorgi's open bisimulation for the pi calculus [1996]. Fusions, although not explicit ones, were initially and independently discovered by Victor and Parrow and by Fu. A pi-calculus term called an equator, introduced by Honda and Yoshida [1995], behaves like an explicit fusion up to weak bisimulation. Merro [2000] has studied the connection between equators and the fusion calculus; I study their connection with explicit fusions. Some of the work here has already been published by Gardner and Wischik [2000].
For the implementation I introduce a distributed abstract machine for both the pi calculus and the explicit fusion calculus. I also introduce a technique called fragmentation which leads to more efficient operation of the machine, and show how fragmentation can be encoded in the explicit fusion calculus. This fragmentation is similar to the solos calculus of Laneve, Victor and Parrow [1999], in that it does not use syntactic guards. Now there have been implementations of the pi calculus before: PICT [1995-2001] by Pierce is the best known; Squeak [1985] based on a paper by Cardelli [1984]; Facile [1995]; and the Join Calculus [1996-2001]by Fournet, Lévy and others. What distinguishes my work is that it is an distributed virtual machine for the pi calculus which implements synchronous rendezvous without handshaking. The others implementations are either not distributed (PICT, Squeak), or use handshaking (Facile), or do not implement the pi calculus directly (Join). I discuss optimisations for when various agents share the same address space. In the degenerate case when the entire program occupies just a single address space, my implementation becomes essentially the same as PICT and Squeak.
Parts of the dissertation restate existing work [2000] done in collaboration with my supervisor Philippa Gardner. She has also contributed through extensive proofreading and advice. The machine calculus has been improved through the help of her and Cosimo Laneve.
@PhDThesis{wischik_thesis,
author = "Lucian Wischik",
title = "Explicit Fusions: Theory and Implementation",
school = "Computer Laboratory, University of Cambridge",
year = 2001,
url = "http://www.wischik.com/lu/research/efti.html",
}