Jade Alglave is a Professor of Computer Science at University College London, as well as a Senior Principal Engineer at Arm. She has developed models of the memory models used by hardware chips, together with a language for specifying these models (cat) and software tools (diy7 and herd7) for experimenting with and testing them.
As you read on, Professor Alglave explains how her work fits into our everyday digital lives.
The award is for your foundational work in concurrency - what do we need to know about that?
Concurrency is a term used to designate the behaviours of various agents which perform actions concurrently, or in parallel. In the case of multiprocessor chips, there are several processors running in parallel. In the case of an operating system such as Linux, there are several threads running in parallel. In all those cases, an agent’s actions can interfere with their neighbours’ actions.
What I try to do is to describe which interferences are allowed or forbidden.
What were your original motivations?
I do not design anything - that’s a misconception. Chip design would be the work of some of my Arm colleagues. They design the plans and blueprints to build the new Arm chips. Rather, I attempt to describe the behaviour of chips by trying to develop a formal and executable model of the behaviour of those chips.
Formal means that the models are underpinned by some mathematical constructs. Executable means that we can write those models as files which can be processed by a computer - the computer can then assist a user by running the model so that the user can experiment with it.
This work started when I was a PhD student - I studied with Luc Maranget at INRIA. Together we developed a tool called diy7 to test multiprocessor chips in a somewhat systematic way. Our original motivation for writing this tool was that we wanted to understand how certain chips behaved (it was IBM Power chips at the time) but we did not really understand what the accompanying documentation was saying. So, I thought: ‘Oh, we could ask the machines themselves what their behaviour is, by running tests on them.’
Later, we invented a language called cat. Cat is a domain-specific language, which is meant to describe the behaviours of concurrent systems in a concise manner. Our original motivation for inventing this language was very pragmatic, very much to make our daily lives easier. At the time, we had a prototype tool but each time we need to make a change to the model, we needed to dive into the entrails of the tool and modify the code there.
Then, I reflected on how we were communicating those changes to each other via email, by writing quite concise lines of maths. And I thought that if we could make the tool essentially understand those concise lines of maths, we wouldn’t have to change its code quite that much!
This tool is called herd7. It takes as input those ‘concise lines of maths’ written in a cat file, and a small program called a litmus test. The herd7 tool then runs the litmus test under the model and tells the user which outcomes of that litmus test are allowed by the model. More about herd7’s web interface
Although we started out using our models to explore the behaviour of chips after their creation, we now use our methodology and tools at Arm to not only test but also specify the designs before the chips are made. More about Arm
We’ve also worked with Linux developers to develop a formal model of the concurrency implemented by the Linux kernel, which is now distributed within the kernel.
Where does this fit into the technology we all live with and experience today? How might the person on the street experience your work as they go about their digital life?
So far, the application of our work has been at such a low, fundamental level in hardware and software that I am not entirely sure there’s been any visible impact to most people. However, I can try and give an illustration of the sort of behaviours I reason about daily.
An example of the sort of behaviours I try to describe may have happened to you when texting somebody. Imagine that a friend is writing a text to you to say: ‘Meet me at 1pm at the café.’ Then they change their mind and write: ‘Meet me at 2pm at mine.’
For some reason, their second text arrives to you first and you set out to meet them at 2pm at theirs. When their first text arrives (or indeed if it ever arrives), it may well look like they have changed their mind. As a consequence, you might change your course to meet them at the café and you may not manage to meet your friend today at all.
Some cases of ‘reordering of messages’ are allowed to happen in concurrent systems and are indeed desirable, because in some cases it allows for increased performance. I try to determine and record precisely when those reorderings are allowed or not. It sometimes involves discussing with the users of our systems to check whether certain reorderings are harmful, like in the case of the missed rendezvous.
In a nutshell, how do you sum up the work?
I try to describe how different agents (for example, two processors in a multiprocessor chip) communicate - more precisely, which communications are allowed.
Why is solving this problem so central to today’s world?
I don’t know whether it is central. However, I do believe it is somewhat fundamental in the following way: we need to understand and be able to describe how our systems behave so that we can make sure that they do behave the way in which we intended. Writing formal models is a step towards this.
Concurrency seems unavoidable as our systems continue to grow and interact in more complex ways. Correctness, reliability and security all depend on knowing that the combined behaviour of a world full of individual agents leads to the intended or expected result.
I hope that our work and tools allow people to reason about the endless combinations of possible actions without having to exhaustively consider each one.
Gazing into the crystal ball, how do you feel your work will change / influence tomorrow’s technology and our digital lives?
I believe it may influence tomorrow’s technology in the sense that we provide means to describe the behaviour of certain concurrent systems and to test those systems to an extent. This contributes, in a modest way, to making sure that our systems faithfully implement their designers’ intent.
The BCS mission is all about making IT good for society. Looking at your work through this prism, what would we see?
Our work is a small step towards making sure that our systems behave the way we intend them to and towards checking that our systems do not do bad things that were never intended.
It seems that our society is becoming ever more dependent on systems which have highly complex interactions. These systems are both difficult to design and expensive to run - and those concerns are driving more and more concurrency in both software and hardware.
I hope that our tools enable us to help to improve the performance and reliability of these systems which serve us all.
And finally - the award. What does it feel like to receive it? What does it mean to you?
I am honoured that our work is recognised in that way.
