{"id":{"repo_id":"cambridge","oai_identifier":"oai:www.repository.cam.ac.uk:1810/389436"},"canonical_url":"https://search.dev.ndltd.org/etd/cambridge/oai:www.repository.cam.ac.uk:1810/389436","repository":{"repo_id":"cambridge","name":"Cambridge University","base_url":"https://api.repository.cam.ac.uk/server/oai/request"},"display":{"title":"Arm systems semantics","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Simner, Ben"],"institution":"University of Cambridge","degree_name":"Doctor of Philosophy (PhD)","degree_level":"Doctoral","degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":["Sewell, Peter"],"committee_chairs":[],"committee_members":[],"year":2025,"date_issued":"2025-04-15","date_published":"2025-04-15","updated_at":"2026-07-22T22:24:24Z","subjects":["computer architecture","programming languages","semantics"],"languages":["eng"],"rights":[],"rights_urls":["https://www.repository.cam.ac.uk/bitstreams/30b6133e-0a07-458c-b22f-22cc0a160146/download","https://creativecommons.org/licenses/by/4.0/"],"identifier_entries":[{"key":"dc:creator.authoridentifier","label":"Author Identifier","values":["0009000084319577"],"render_values":[{"text":"0009-0000-8431-9577","href":"https://orcid.org/0009-0000-8431-9577","code":true}]}]},"links":{"outbound_url":"https://doi.org/10.17863/CAM.121319","outbound_label":"DOI","outbound_source":"dc:identifier.doi"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Sewell, Peter"]},{"key":"dc:contributor.sponsor","label":"Sponsor","values":["Arm/EPSRC iCASE PhD studentship"]},{"key":"dc:creator","label":"Author","values":["Simner, Ben"]},{"key":"dc:creator.authoridentifier","label":"Author Identifier","values":["0009000084319577"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.issued","label":"Date","values":["2025-04-15"]},{"key":"dc:publisher.institution","label":"Dc Publisher Institution","values":["University of Cambridge"]},{"key":"dc:relation.isreferencedby.uri","label":"Dc Relation Isreferencedby URI","values":["https://www.repository.cam.ac.uk/handle/1810/389436"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"dc:type.qualificationlevel","label":"Dc Type Qualificationlevel","values":["Doctoral"]},{"key":"dc:type.qualificationname","label":"Dc Type Qualificationname","values":["Doctor of Philosophy (PhD)"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["computer architecture","programming languages","semantics"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["https://www.repository.cam.ac.uk/bitstreams/30b6133e-0a07-458c-b22f-22cc0a160146/download","https://creativecommons.org/licenses/by/4.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.doi","label":"DOI","values":["https://doi.org/10.17863/CAM.121319"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://www.repository.cam.ac.uk/bitstreams/b37a1aa9-354d-4d5e-8d80-3d10d5891ce8/download"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:format.checksum.md5","label":"Dc Format Checksum Md5","values":["c0283494ff427dba080a059a64a4eb11","87eda9de84448d1f82354d60eee3eb5f"]},{"key":"dc:title","label":"Title","values":["Arm systems semantics"]}]}],"canonical_facts":{"dc:contributor.advisor":["Sewell, Peter"],"dc:contributor.sponsor":["Arm/EPSRC iCASE PhD studentship"],"dc:creator":["Simner, Ben"],"dc:creator.authoridentifier":["0009000084319577"],"dc:date.issued":["2025-04-15"],"dc:description.abstract":["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."],"dc:format.checksum.md5":["c0283494ff427dba080a059a64a4eb11","87eda9de84448d1f82354d60eee3eb5f"],"dc:identifier.doi":["https://doi.org/10.17863/CAM.121319"],"dc:identifier.uri":["https://www.repository.cam.ac.uk/bitstreams/b37a1aa9-354d-4d5e-8d80-3d10d5891ce8/download"],"dc:language":["eng"],"dc:publisher.institution":["University of Cambridge"],"dc:relation.isreferencedby.uri":["https://www.repository.cam.ac.uk/handle/1810/389436"],"dc:rights":["https://www.repository.cam.ac.uk/bitstreams/30b6133e-0a07-458c-b22f-22cc0a160146/download","https://creativecommons.org/licenses/by/4.0/"],"dc:subject":["computer architecture","programming languages","semantics"],"dc:title":["Arm systems semantics"],"dc:type":["Thesis"],"dc:type.qualificationlevel":["Doctoral"],"dc:type.qualificationname":["Doctor of Philosophy (PhD)"]},"updated_at":"2026-07-22T22:24:24Z"}