2026-09-21T21:14:18Zhttps://api.repository.cam.ac.uk/server/oai/request

oai:www.repository.cam.ac.uk:1810/3894362025-09-24T01:42:49Zcom_1810_219481com_1810_256065col_1810_219482

Arm systems semantics https://doi.org/10.17863/CAM.121319 Simner, Ben 0009000084319577 Sewell, Peter 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. University of Cambridge 2025-04-15 Thesis Doctoral Doctor of Philosophy (PhD) eng Arm/EPSRC iCASE PhD studentship https://www.repository.cam.ac.uk/handle/1810/389436 https://www.repository.cam.ac.uk/bitstreams/b37a1aa9-354d-4d5e-8d80-3d10d5891ce8/download c0283494ff427dba080a059a64a4eb11 https://www.repository.cam.ac.uk/bitstreams/30b6133e-0a07-458c-b22f-22cc0a160146/download 87eda9de84448d1f82354d60eee3eb5f https://creativecommons.org/licenses/by/4.0/ computer architecture programming languages semantics