Show simple item record

dc.contributor.authorFlur, Shaked
dc.contributor.authorGray, KE
dc.contributor.authorPulte, Christopher
dc.contributor.authorSarkar, S
dc.contributor.authorSezgin, A
dc.contributor.authorMaranget, L
dc.contributor.authorDeacon, W
dc.contributor.authorSewell, Peter
dc.date.accessioned2018-11-20T00:30:58Z
dc.date.available2018-11-20T00:30:58Z
dc.date.issued2016-01
dc.identifier.issn1523-2867
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/285457
dc.description.abstractCopyright is held by the owner/author(s). In this paper we develop semantics for key aspects of the ARMv8 multiprocessor architecture: the concurrency model and much of the 64-bit application-level instruction set (ISA). Our goal is to clarify what the range of architecturally allowable behaviour is, and thereby to support future work on formal verification, analysis, and testing of concurrent ARM software and hardware. Establishing such models with high confidence is intrinsically difficult: it involves capturing the vendor's architectural intent, aspects of which (especially for concurrency) have not previously been precisely defined. We therefore first develop a concurrency model with a microarchitectural flavour, abstracting from many hardware implementation concerns but still close to hardware-designer intuition. This means it can be discussed in detail with ARM architects. We then develop a more abstract model, better suited for use as an architectural specification, which we prove sound w.r.t. the first. The instruction semantics involves further difficulties, handling the mass of detail and the subtle intensional information required to interface to the concurrency model. We have a novel ISA description language, with a lightweight dependent type system, letting us do both with a rather direct representation of the ARM reference manual instruction descriptions. We build a tool from the combined semantics that lets one explore, either interactively or exhaustively, the full range of architecturally allowed behaviour, for litmus tests and (small) ELF executables. We prove correctness of some optimisations needed for tool performance. We validate the models by discussion with ARM staff, and by comparison against ARM hardware behaviour, for ISA single-instruction tests and concurrent litmus tests.
dc.description.sponsorshipThis work was partly funded by the EPSRC Programme Grant REMS: Rigorous Engineering for Mainstream Systems, EP/K008528/1, the Scottish Funding Council (SICSA Early Career Industry Fellowship, Sarkar), an ARM iCASE award (Pulte), and ANR grant WMC (ANR-11-JS02-011, Maranget).
dc.publisherACM
dc.titleModelling the ARMv8 architecture, operationally: Concurrency and ISA
dc.typeArticle
prism.endingPage621
prism.issueIdentifier1
prism.publicationDate2016
prism.publicationNameACM SIGPLAN Notices
prism.startingPage608
prism.volume51
dc.identifier.doi10.17863/CAM.32815
dcterms.dateAccepted2015-12-04
rioxxterms.versionofrecord10.1145/2837614.2837615
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserved
rioxxterms.licenseref.startdate2016-04-08
dc.contributor.orcidSewell, Peter [0000-0001-9352-1013]
dc.identifier.eissn1558-1160
dc.publisher.urlhttps://dl.acm.org/doi/10.1145/2837614.2837615
rioxxterms.typeJournal Article/Review
pubs.funder-project-idEngineering and Physical Sciences Research Council (EP/K008528/1)
pubs.funder-project-idEngineering and Physical Sciences Research Council (EP/H027351/1)
pubs.funder-project-idEPSRC (1675850)
cam.issuedOnline2016-01-11
rioxxterms.freetoread.startdate2017-04-08


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record