Meet Arm’s Jade Alglave, Honoree of the Prestigious Blavatnik Award for Young Scientists

Jade Alglave, Lead Concurrency Architect and Distinguished Engineer at Arm, has been announced as an honoree of the 2023 Blavatnik Award for Young Scientists. The prestigious award acknowledges promising young scientists and their outstanding achievements to the world of science and technology earlier in their careers.

Jade’s joint work with Luc Maranget has been distinguished for inventing a mathematical framework, embodied in a domain-specific language called ‘cat’. The cat language allows a user to list the general principles and rules of a concurrent system, such as the ones defined by the Arm architecture. These are built into the architecture of most of the world’s modern computing systems that are used across a variety of technologies, from smartphones right through to data centers. Together with Luc Maranget, she also designed publicly available practical open-source software tools to test whether various specifications are being correctly implemented in these concurrent systems.

The methodology and accompanying tools have been applied by several leading technology companies, including Arm and the Linux Foundation, and also helped uncover bugs in computer chips before, during and after deployment.

We sat down with Jade to talk about her work, her role at Arm and within academia, and her award win, as well as seeing how she first got into technology.

First question, how did you have the foresight and vision to see that the methodology you were developing 15 years ago would be so crucial now?

Jade: I didn’t know 15 years ago that what I was working on during my PhD would be that useful today. The overarching theme of my PhD research was: can we describe precisely what concurrent systems are supposed to do?

This is because 15 years ago there were small collections of tests or behaviors described as being allowed or forbidden with some informal argument as to why, but the specifications were either very parsimonious or, on the contrary, had long explanations that were very hard to follow – at least for me. So, we took an empirical approach, which was: if we can’t really get the answers we need from the specifications, can we approximate them from the machines themselves, since the machines that are supposed to be built in accord with the specifications?

Luc Maranget and I designed a tool called ‘diy’ that generates lots and lots of tests. Then we ran those tests on various machines. This was so we could obtain experimental models out of those vast experimental campaigns. When we wrote that tool, I was certain that we had just reproduced something that existed in the industry already, but it turned out that this was not the case.

Why do you think your methodology has been adopted in industry?  

Jade: I think that one of the appeals is it’s not just math on paper: our models can be executed. Users can query the herd7 tool, ask a question, such as “is this behavior forbidden or not?”, and it will provide a Yes or No answer and not confront users with pages and pages of math. Also, the model does not need to dive into implementation considerations at a micro-architectural level.

So, a designer can use the herd7 tool, and throw various situations against it? And the tool will say “yes, you can do that” or “no, you can’t”?

Jade: Yes, exactly. And the diy tool allows you to generate vast families of scenarios that the designer can use as tests for different designs. Then, you run these tests against the executable model in the herd7 tool and compare it with the behaviours observed on hardware.

You developed the cat language to write those executable models. Was there a possibility of using another language to develop the models? Or was cat just very efficiently built for the purpose at hand?  

Jade: When we first wrote cat, we didn’t know that there was another system that we could have used, which is called Alloy. This allows you to write a declarative description of a system much like cat does. Alloy is very general; on the other hand for cat we developed an ecosystem of tools built for a very specific purpose.

Can you explain a little more about concurrency and why it’s important to compute systems? Also how does it relate to your work?

Jade: At a high level, concurrency describes how different agents, for example processors, communicate amongst themselves and exchange information. Concurrency can enable high performance and processing efficiency because you can distribute tasks to different processors to carry them out in parallel.

What made you join Arm? And what does Arm give you as an employer?

Jade: Arm has given me access to valuable knowledge and insights from my colleagues, as well as partners through its ecosystem. This means that the impact of the work can go far wider. Within the company, Richard Grisenthwaite, Arm’s Chief Architect, has been a huge supporter of the work. Firstly, through technical conversations with my team to help us model correctly. And, secondly, towards the Arm executive team and our partners through communicating why the work my team does is worthwhile and important for the company and the wider ecosystem.

I’m privileged to have Jade as part of my team at Arm. Her work has been hugely influential across all of today’s modern computing systems. The methodology developed by Jade and her team is also integral to Arm’s technology that is used by over 70 percent of the world’s population. Jade being an honoree of the Blavatnik Award for Young Scientists is an outstanding achievement, and recognizes the significant impact of her work across the global technology landscape.

Richard Grisenthwaite, EVP and Chief Architect at Arm

What is your current role within Arm?

Jade: Currently, I’m leading a team that works on maintaining and evolving the memory model, as well as maintaining and updating the companion tools. This involves plenty of collaboration with Arm architects where we ask them how the model should behave in detail. We do the same with Arm’s partners. This all feeds into the evolution of the model and supporting tools.

You’re also a Professor of Computer Science at UCL (University College London). How do you combine your academic work with your work at Arm?

Jade: I think there’s nice synergy between both jobs. My background is academia, so I often wear a “research hat” for my work. However, my role at Arm means I can try to ensure that the work is applied in ways that are valuable to the company and the wider industry.

At the moment, what’s the most exciting thing you’re working on at Arm or within academia?

Jade: At the moment, I find it really interesting learning more about engineering processes and management, as these give me ideas on how to scale the impact of my team at Arm so we can continue to improve the model and supporting tools.

What do you love most about what you do at Arm?

Jade: I think, at the moment, it’s great seeing my team grow within Arm. Watching everyone work so well together is an immense source of pride. It’s not just me on my own developing those models and tools. People in my team are taking the existing knowledge and methodology further and this means that we can be more ambitious in what we reach.

Who nominated you for the Blavatnik award?

Jade: I was nominated by the Royal Academy of Engineering. As I’m a Fellow there, the institution was aware of me and my work, and contacted me to say that I met the requirements.

Thinking back to when you were younger, what was your first experience of technology?

Jade: I didn’t own a computer until I was 21. When I was a child, my home had a telephone and a TV, but nothing else really. My first proper experience with technology wasn’t until I was at university.

So, it was quite a leap from not owning a computer to doing a PhD in Computer Science. How did that happen?

Jade: I studied Maths and Physics first, but realised I wasn’t brilliant in either. However, I did like the rigour of both fields. I started wondering how I could exploit that elsewhere. I had limited knowledge of programming, but the curriculum I followed wasn’t just about that. It was a lot about semantics, which is what I do: modelling systems.

Further reading

Check out the links below for some further reading in relation to Jade’s work:

• How to use the herd7 simulator – link here.
• How to generate tests with the diy7 test generator (including a configuration file to feed to diy to generate interesting tests) – link here.
• How to run tests on silicon with the litmus7 tool – link here.
• How we have extended our testing and modelling to page table related concerns – link here.
• How we have extended our testing and modelling to Memory Tagging and Morello – link here.