Six engineers from the Arm Architecture Formal Team have been honoured with this year’s Colin Campbell Mitchell Award by the Royal Academy of Engineering.
This team develops practical tools for modelling and testing computer chips, contributing to more reliable computing systems.
The Colin Campbell Mitchell Award is given annually to an engineer or a small team of engineers who have made an exceptional contribution to advancing any field of UK engineering. This year, the award was presented to Professor Jade Alglave FREng, Dr Artem Khyzha, Dr Roman Manevich, Dr Nikos Nikoleris, Hugo O’Keeffe, and Hadrien Renaud during the Academy’s annual Fellows’ Day in London on 6th June 2024.
Efficient computing relies on multiprocessor chips, which contain several processing elements that perform tasks in parallel. These elements must communicate with each other to complete their tasks, which can sometimes lead to subtle bugs.
Traditionally, the interactions of concurrent processing elements were described informally, posing challenges for both hardware engineers designing chips and software engineers programming them.
To address this, Professor Jade Alglave and Luc Maranget created formal models of concurrent systems. They developed a language called ‘cat’ and software tools named ‘herd’ and ‘diy’ for writing and experimenting with these models.
As part of the Arm Architecture Formal Team, Alglave and her colleagues have improved these models and tools to include more features of the Arm architecture. These enhanced models and tools are used to detect bugs in chip designs before deployment, which is crucial as fixing hardware post-production can be extremely costly. The team is also working on a formal and executable definition of the Architecture Specification Language (ASL), used by Arm to describe how instructions operate.
These models are publicly available, and the tools are open-source, enabling researchers to use industrial models and broaden the impact of their work. Additionally, hardware and software vendors can use these models and tools to verify their systems.
Luke Logan FREng, Chair of the Academy’s Awards Committee, said: “By taking a theoretical model and turning it into successful engineering practice, Professor Alglave and her team have developed formal, queryable models of the Arm architecture for the first time. More than 280 billion Arm chips have been manufactured for use around the world in sensors, wearables, smartphones and supercomputers and formal modelling is essential to ensure the robust operation of future generations of these increasingly complex processors. Congratulations to the Arm Architecture Formal Team – they are worthy winners of this year’s Colin Campbell Mitchell Award.”
Professor Jade Alglave, Lead Formal Architect and Fellow at Arm, said: “It is a great honour for our team to receive the Royal Academy of Engineering’s Colin Campbell Mitchell Award. We are delighted that our models and tools are seen to be useful.”
Richard Grisenthwaite, EVP and Chief Architect at Arm, said: “Knowing exactly how systems behave is of paramount importance in chip design. I’m extremely proud of the team’s achievement and this work will empower chip designers to detect bugs in their designs earlier, enabling more efficient and secure Arm-based computing systems, with device functionality being further enhanced.”
