Arm systems semantics

Computing relies on architecture specifications to decouple hardware and software development. Historically these have been prose documents, with all the problems that entails, but research over the last ten years has developed rigorous and executable-as-test-oracle specifications of mainstream architecture instruction sets and 'user-mode' concurrency, clarifying architectures and bringing them into the scope of programming-language semantics and verification. However, the system semantics, of address translation and TLB maintenance, instruction-fetch and its required cache maintenance, and exceptions and interrupts, remains mostly obscure, leaving us without a solid foundation for verification of security-critical systems software. We develop precise mathematical models, for those aspects of the Arm A-class architecture. We implement these models as executable models, in both microarchitectural-flavoured operational and declarative axiomatic style formats. We validate these models, against currently available hardware through the production and evaluation of hardware test harnesses and test suites, and against the architectural intent through discussions with Arm architects. We give a variety of hand-written and machine-generated litmus tests, exercising parts of the architecture previously unexplored. We discuss the nature of developing such models, and the challenges that writing specifications of existing systems entails. We briefly touch on how these models have evolved over time, and how we imagine they will evolve in the future as the remaining questions are resolved.

Name dc:type.qualificationname

Doctor of Philosophy (PhD)

Level dc:type.qualificationlevel

Doctoral

Grantor dc:publisher.institution

University of Cambridge

Year dc:date.issued

2025

Author dc:creator

• Simner, Ben

Advisor dc:contributor.advisor

• Sewell, Peter

• computer architecture
• programming languages
• semantics

Licence

• https://www.repository.cam.ac.uk/bitstreams/30b6133e-0a07-458c-b22f-22cc0a160146/download
• https://creativecommons.org/licenses/by/4.0/

Language dc:language

eng

Author Identifier

0009-0000-8431-9577

OAI identifier oai:identifier

oai:www.repository.cam.ac.uk:1810/389436