Colloquium d’Informatique de Sorbonne Université
C.A.R. (Tony) Hoare, Microsoft Research Cambridge

Tuesday, November 26, 2013 18:00
Amphi Durand, Esclangon Building Sorbonne University - Faculté des Sciences

Laws of concurrent system design

Tony Hoare is one of the founders of modern informatics. He invented pre/post-condition logic, Quicksort, monitors and CSP, and was a pioneer of concurrent programming. He is a Fellow of the Royal Society since 1982 and was awarded the ACM Alan Turing Prize in 1980, the Kyoto Prize in 2000, and the John von Neumann medal in 2011.

Abstract

The algebraic laws that govern the behaviour of concurrent systems, with both sequential and concurrent composition, are as simple as the familiar laws of arithmetic learnt at school. They are strong enough to derive the structural rules of Hoare logic, which were designed as a proof system for verification of programs. They also derive the rules of O'Hearn's separation logic. They also derive the rules of a structural operational semantics, such as those used by Milner to define validity of an implementation of CCS. The laws are simpler than each of these calculi separately, and stronger than both of them combined.
The laws are satisfied by a simple graph model of the behaviour of a concurrent system, in which basic actions are nodes, connected by arrows that represent dependency between actions. Such a graph might be produced by a testing tool to help reveal the causes of an error, and decide what to do about it. The model is highly generic, and can be used for systems with different basic actions, expressed in different languages, and at different levels of granularity and abstraction.
I speculate that one day algebraic laws such as these will be accepted as a scientific and semantic basis for a Design Automation toolkit for systems engineering. Its tools will include_once system verification, program analysis, program generation, compilation and optimisation, test case generation, and error analysis.