The Arm Architecture Formal Team looks after the formalisation of a number of areas of the Arm Architecture.

Historically, the team has looked after the Concurrency Model, which determines which value a Load instruction is Architecturally Allowed to see. To do that, we develop, maintain and enhance a number of tools which allow us to propose, execute, test and amend formalisations of the prose in the Arm Architecture Reference Manual (Arm ARM). We discuss our proposals with stakeholders and ratify them, after which a (partially automated) transliteration of the formalisation lands back into the Arm ARM. The current scope of the model includes some aspects of virtual memory and instruction fetch, and we work assiduously to expand the scope to the entirety of the Architecture.

More recently, the team has looked into defining and formalising the Arm Architecture Specification Language (ASL), which is used to describe the behaviour of the instructions of the Arm Instruction Set Architecture (ISA). Originally this language was a pseudocode without well defined syntax and semantics, and the team has provided a formal definition of both, as well as a reference interpreter.

Jade Alglave is a Professor of Computer Science at University College London and a Fellow at Arm, where she leads the Architecture Formal Team. This team is responsible in particular for the maintenance and enhancement of the Arm memory model (https://developer.arm.com/herd7).