Skip to content

Research at St Andrews

Modelling the ARMv8 architecture, operationally: concurrency and ISA

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Author(s)

Shaked Flur, Kathryn Gray, Christopher Pulte, Susmit Sarkar, Luc Maranget, Ali Sezgin, Will Deacon, Peter Sewell

School/Research organisations

Abstract

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 represention 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.
Close

Details

Original languageEnglish
Title of host publicationProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Place of PublicationNew York
PublisherACM
Pages608-621
ISBN (Print)9781450335492
DOIs
StatePublished - 11 Jan 2016
EventPOPL '16 The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Hilton St Petersburg Bayfront, St Petersburg, Florida, United States
Duration: 20 Jan 201622 Jan 2016

Conference

ConferencePOPL '16 The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
CountryUnited States
CitySt Petersburg, Florida
Period20/01/1622/01/16

    Research areas

  • Relaxed Memory Models, Semantics, ISA

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by author

  1. Memory consistency models using constraints

    Akgün, Ö., Hoffmann, R. & Sarkar, S. 27 Aug 2018 The Seventeenth Workshop on Constraint Modelling and Reformulation (ModRef 2018), Proceedings. 16 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  2. Automatically deriving cost models for structured parallel processes using hylomorphisms

    Castro, D., Hammond, K., Sarkar, S. & Alguwaifli, Y. Feb 2018 In : Future Generation Computer Systems. 79, Part 2, p. 653-668

    Research output: Contribution to journalArticle

  3. Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8

    Pulte, C., Flur, S., Deacon, W., French, J., Sarkar, S. & Sewell, P. Jan 2018 Proceedings of the ACM on Programming Languages (POPL '18). New York: ACM, Vol. 2 Issue POPL, 29 p. 19

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  4. Verification of a lazy cache coherence protocol against a weak memory model

    Banks, C., Elver, M., Hoffmann, R., Sarkar, S., Jackson, P. & Nagarajan, V. 2 Oct 2017 Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD). ACM, p. 60-67

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  5. Mixed-size Concurrency: ARM, POWER, C/C++11, and SC

    Flur, S., Sarkar, S., Pulte, C., Nienhuis, K., Maranget, L., Gray, K., Sezgin, A., Batty, M. & Sewell, P. 1 Jan 2017 Proceedings of the 44th annual ACM-SIGPLAN Symposium on Principles of programming languages. ACM, p. 429-442

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

ID: 221642908