POSTPONED: Inaugural Lecture of Professor Jade Alglave: Herding Cats

Celebrating the Inaugural Lecture of Professor Jade Alglave - UCL Principal Supervisor & UCL Subsidiary Supervisor
PPLV (Programming Principles, Logic, and Verification)

 17.00 - 18.00: Inaugural Lecture (Gustave Tuck LT)

• Introduction to Proceedings  - Peter O'Hearn and Byron Cook
• Inaugural Lecture by Prof. Jade Alglave: 'Herding Cats'
• Vote of Thanks - Richard Grisenthwaite

18.00 - 19.30:  Drinks Reception. Jeremy Bentham Room (JBR) - Wilkins Building

Abstract

Concurrent programming is often reputed to be hard - think of a collection of musicians gathered into an auditorium and the possible interactions between them. How to orchestrate them?

The orchestration in the case of multiprocessor systems for example is given in the technical documents which accompany those systems. Unfortunately, most of those documents have historically been quite sparse in the area of concurrency, and relatively obscure. This is partly due to the fact that those documentations are written in prose, which sadly can be prone to ambiguity.

For the last decade we have been developing models of the concurrency aspects of CPUs, as well as GPUs and more recently operating systems. Along the way we have developed tools which have assisted and informed our understanding and the design of our models:

• the herd tool takes as input a concurrency model and a litmus test, and returns the architecturally permissible behaviors of that test under that model;
• the diy tool generates systematic families of litmus tests;
• the litmus tool runs those tests on hardware.

Those tools are driven by a domain-specific language called cat, whose semantics we have formalised. We initially developed cat to make communicating our models faster and easier. But to our delight it has grown into much more than a mere convenience. What makes cat powerful is two-fold:

• a syntax to describe concurrency models concisely and uniformly;
• a formal semantics which means that anyone writing a model in cat is assured that their model has a well defined and coherent meaning.

Additionally, the fact that the cat language is implemented within the herd tool ensures that a cat model is machine-readable and executable. In turn this means that one can check their understanding of the concurrency aspects of a given system, and generate tests to probe the differences between what the model prescribes and what the concrete systems exhibit.

In other words, we have come quite a long way from the prose definitions of ten years ago. Encouragingly, various organisations have now officially adopted cat as a mean to describe their concurrency model, including Arm and the Linux kernel.

During this lecture, I will reflect on this decade of work, as well as those more recent thrilling developments.

Photography and Filming Notice: Please note that the lecture may be recorded and photographs will be taken throughout the lecture and reception. These will be used by the UCL for marketing and publicity in our publications, on our website and in social media or in any third party publication. Please contact the event organiser if you have any concerns or if you wish to be exempted from this activity. Please also make yourself known to event staff when you arrive at the event: computerscience.comms@ucl.ac.uk