next up previous contents
Next: Logics for Concurrency and Up: Calculi Previous: Bisimulations

Proofs of protocols and transformational rules

In [San97J], Sangiorgi applies the proof techniques developed in [San97a] to solve a problem submitted by Cliff Jones. Jones has proposed transformations between concrete programs and general transformation rules that increase concurrency in a system of objects, and has raised the challenge of how to prove their validity. A proof of correctness of the hardest of Jones's concrete transformations is presented.

In [PW97b], Philippou and Walker use the technique based on partial confluence of processes 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 rendez-vous 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 [PW97c] 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. In [I97] Ionitoiu begins to explore a new approach to modelling asynchronous communication and fault-tolerance in a process-calculus setting.

Another work on mobility [AmPra97] concerns the modelling of mobile hosts on a network in a simple name-passing process calculus. The protocol considered is a highly simplified version of proposals for mobility support in the version 6 of the Internet Protocols (IP). We concentrate on the issue of ensuring that messages to and from mobile agents are delivered without loss of connectivity. We provide three models of increasingly complex nature of a network of routers and computing agents that are interconnected via the routers: the first is without mobile agents and is treated as a specification for the next two; the second supports mobile agents, and the third additionally allows correspondent agents to cache the current location of a mobile agent. Following a detailed analysis of the three models to extract invariant properties, we show that the three models are related by a suitable notion of equivalence based on bisimulation.

[[AmPra97]] R. Amadio and S. Prasad.
Modelling IP mobility.
Technical Report TR 1997.244. Also RR-3301 INRIA, Université de Provence (LIM), 1997.

[[San97J]] D. Sangiorgi.
Typed $\pi$-calculus at work: a proof of Jones's parallelisation transformation on concurrent objects.
Presented at the Fourth Workshop on Foundations of Object-Oriented Languages (FOOL 4). To appear in Theory and Practice of Object-oriented Systems, 1997.

[[PW97b]] A. Philippou and D. Walker,
On transformations of concurrent object programs,
Theoretical Computer Science B, to appear.

[[PW97c]] A. Philippou and D. Walker,
Social confluence in client-server systems,
in Proceedings of Computer Science Logic, Utrecht, September 1996, Springer-Verlag Lecture Notes in Computer Science, vol. 1258, 385-398.

[[PW97d]] A. Philippou and D. Walker,
A rigorous analysis of concurrent operations on B-trees,
in Proceedings of Concurrency Theory, Warsaw, July 1997, Springer-Verlag Lecture Notes in Computer Science, vol. 1243, 361-375.

[[P97phd]] A. Philippou,
Reasoning about systems with evolving structure,
PhD thesis, University of Warwick, December 1996.

[[I97]] C. Ionitoiu,
An operational semantics for loosely coupled systems,
MSc dissertation, University of Warwick, September 1997.

next up previous contents
Next: Logics for Concurrency and Up: Calculi Previous: Bisimulations