Six engineers from the Arm Architecture Formal Team have been awarded this year’s Colin Campbell Mitchell Award by the Royal Academy of Engineering. The team develops practical tools to model and test computer chips, paving the way for more reliable computing systems.
The Award is made annually to an engineer or small team of engineers who have made an outstanding contribution to the advancement of any field of UK engineering. Professor Jade Alglave FREng, Dr Artem Khyzha, Dr Roman Manevich, Dr Nikos Nikoleris, Hugo O’Keeffe, and Hadrien Renaud were presented with the Award at the Academy’s annual Fellows’ Day in London on 6 June 2024 (below).
Image credit: Rob Lacey
Efficient computing is enabled by multiprocessor chips, which feature several processing elements, performing tasks in parallel. These processing elements need to communicate with each other to perform their overall common task, and this may lead to subtle bugs.
Historically the interactions of concurrent processing elements have been described in an informal manner, complicating matters for both the hardware engineers designing chips and the software engineers programming them.
To address this issue, Professor Alglave and Luc Maranget created formal models of concurrent systems. Alglave and Maranget invented a language (cat) and software tools (herd, diy) for writing and experimenting with the models.
As part of the Arm Architecture Formal Team, Alglave and the team have enhanced the models and tools to encompass more features of the Arm® architecture. Furthermore, these models and tools are used to look for bugs in chip designs ahead of deployment, which is important since fixing hardware afterwards can be prohibitively expensive. The team is also developing a formal and executable definition of the Architecture Specification Language (ASL), used at Arm to describe how instructions operate.
The models are publicly available and the tools are open-source, allowing researchers to use industrial models and widen the impact of their work. Hardware and software vendors can also use the models and tools to check 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.”
Notes for editors
- The Colin Campbell Mitchell Award is given annually to an engineer, or team of engineers, who have made an outstanding contribution to the advancement of any field of UK engineering in the last four years.
- The Royal Academy of Engineering is harnessing the power of engineering to build a sustainable society and an inclusive economy that works for everyone. In collaboration with our Fellows and partners, we’re growing talent and developing skills for the future, driving innovation and building global partnerships, and influencing policy and engaging the public. Together we’re working to tackle the greatest challenges of our age.
For more information please contact: Jane Sutton at the Royal Academy of Engineering; Tel. +44 207 766 0636; email: [email protected].