Repository logo
 

ARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures

Simple item page
cam.issuedOnline2020-04-18
cam.orpheus.successThu Nov 05 11:55:58 GMT 2020 - Embargo updated
dc.contributor.authorSimner, B
dc.contributor.authorFlur, S
dc.contributor.authorPulte, C
dc.contributor.authorArmstrong, A
dc.contributor.authorPichon-Pharabod, J
dc.contributor.authorMaranget, L
dc.contributor.authorSewell, P
dc.contributor.orcidSewell, Peter [0000-0001-9352-1013]
dc.date.accessioned2020-02-24T14:49:37Z
dc.date.available2020-02-24T14:49:37Z
dc.date.issued2020
dc.description.abstract<jats:title>Abstract</jats:title><jats:p>Computing relies on <jats:italic>architecture specifications</jats:italic> 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 <jats:italic>system semantics</jats:italic>, of instruction-fetch and cache maintenance, exceptions and interrupts, and address translation, remains obscure, leaving us without a solid foundation for verification of security-critical systems software.</jats:p><jats:p>In this paper we establish a robust model for one aspect of system semantics: instruction fetch and cache maintenance for ARMv8-A. Systems code relies on executing instructions that were written by data writes, e.g. in program loading, dynamic linking, JIT compilation, debugging, and OS configuration, but hardware implementations are often highly optimised, e.g. with instruction caches, linefill buffers, out-of-order fetching, branch prediction, and instruction prefetching, which can affect programmer-observable behaviour. It is essential, both for programming and verification, to abstract from such microarchitectural details as much as possible, but no more. We explore the key architecture design questions with a series of examples, discussed in detail with senior Arm staff; capture the architectural intent in operational and axiomatic semantic models, extending previous work on “user-mode” concurrency; make these models executable as test oracles for small examples; and experimentally validate them against hardware behaviour (finding a bug in one hardware device). We thereby bring these subtle issues into the mathematical domain, clarifying the architecture and enabling future work on system software verification.</jats:p>
dc.description.sponsorshipThis work was partially supported by EPSRC grant EP/K008528/1 (REMS), ERC Advanced Grant 789108 (ELVER), an ARM iCASE award, and ARM donation funding. % This work is part of the CIFV project sponsored by the Defense Advanced Research Projects Agency (DARPA) and the Air Force Research Laboratory (AFRL), under contract FA8650-18-C-7809. The views, opinions, and/or findings contained in this paper are those of the authors and should not be interpreted as representing the official views or policies, either expressed or implied, of the Department of Defense or the U.S. Government.
dc.identifier.doi10.17863/CAM.49736
dc.identifier.eissn1611-3349
dc.identifier.isbn9783030449131
dc.identifier.issn0302-9743
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/302666
dc.language.isoeng
dc.publisherSpringer International Publishing
dc.publisher.urlhttp://dx.doi.org/10.1007/978-3-030-44914-8_23
dc.rightsAll rights reserved
dc.subject4613 Theory Of Computation
dc.subject46 Information and Computing Sciences
dc.subject4612 Software Engineering
dc.titleARMv8-A System Semantics: Instruction Fetch in Relaxed Architectures
dc.typeConference Object
dcterms.dateAccepted2019-12-23
prism.endingPage655
prism.publicationDate2020
prism.publicationNameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
prism.startingPage626
prism.volume12075 LNCS
pubs.conference-finish-date2020-04-30
pubs.conference-nameESOP 2020: European Symposium on Programming
pubs.conference-start-date2020-04-25
pubs.funder-project-idEngineering and Physical Sciences Research Council (EP/K008528/1)
pubs.funder-project-idEuropean Research Council (789108)
pubs.funder-project-idEPSRC (2097768)
rioxxterms.licenseref.startdate2020-01-01
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserved
rioxxterms.typeConference Paper/Proceeding/Abstract
rioxxterms.versionAM
rioxxterms.versionofrecord10.1007/978-3-030-44914-8_23

Files

Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
top-camera.pdf
Size:
474.42 KB
Format:
Adobe Portable Document Format
Description:
Accepted version
Licence
http://www.rioxx.net/licenses/all-rights-reserved
Download
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
DepositLicenceAgreementv2.1.pdf
Size:
150.9 KB
Format:
Adobe Portable Document Format
Download

Collections

Cambridge University Research Outputs