Colloquium d'informatique

2012-2013 - Campus Jussieu

Séminaire de prestige en recherche informatique. Invitation de grands noms du domaine, visant un public large.

Tony Hoare: Laws of concurrent system design


Envie de télécharger cette vidéo sur votre ordinateur ? Cliquez ici (poids : 613 Mo)

Résumé

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 system verification, program analysis, program generation, compilation and optimisation, test case generation, and error analysis


Orateur(s) : Tony Hoare, Microsoft Research Cambridge
Public : Tous
Date : Tuesday 26 November 2013
Lieu : Amphithéâtre Durand, Campus Jussieu