article

Modelling the ARMv8 architecture, operationally: concurrency and ISA

Authors:

Kathryn E. Gray,

Christopher Pulte,

Peter SewellAuthors Info & Claims

ACM SIGPLAN Notices, Volume 51, Issue 1

Pages 608 - 621

https://doi.org/10.1145/2914770.2837615

Published: 11 January 2016 Publication History

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

References

[1]

J. Alglave and L. Maranget. The diy tool. http://diy.inria.fr/.

[2]

J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. Fences in weak memory models. In Proc. CAV, 2010.

Digital Library

[3]

J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. Litmus: running tests against hardware. In Proceedings of TACAS 2011: the 17th international conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 41–44, Berlin, Heidelberg, 2011. Springer-Verlag. ISBN 978-3-642-19834-2. URL http://dl.acm.org/citation.cfm?id=1987389.1987395.

Digital Library

[4]

J. Alglave, L. Maranget, and M. Tautschnig. Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory. ACM TOPLAS, 36(2):7:1–7:74, July 2014. ISSN 0164-0925.

Digital Library

[5]

R. M. Amadio, N. Ayache, F. Bobot, J. Boender, B. Campbell, I. Garnier, A. Madet, J. McKinna, D. P. Mulligan, M. Piccolo, R. Pollack, Y. Régis-Gianas, C. S. Coen, I. Stark, and P. Tranquilli. Certified complexity (cerco). In Foundational and Practical Aspects of Resource Analysis - Third International Workshop, FOPARA 2013, Bertinoro, Italy, August 29-31, 2013, Revised Selected Papers, pages 1–18, 2013.

[6]

. URL http://dx.doi.org/10.1007/978-3-319-12466-7_1.

[7]

ARM. Cortex-a57 processor. www.arm.com/products/processors/ cortex-a/cortex-a57-processor.php, Accessed 2015/07/06.

[8]

ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile). ARM Ltd., 2014.

[9]

W. W. Collier. Reasoning about parallel architectures. Prentice Hall, Englewood Cliffs, 1992.

Digital Library

[10]

ISBN 0-13-767187-3. URL http://opac.inria.fr/record=b1105256.

[11]

J. a. Dias and N. Ramsey. Automatically generating instruction selectors using declarative machine descriptions. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’10, pages 403–416, New York, NY, USA, 2010. ACM. ISBN 978-1-60558-479-9. URL http://doi.acm.org/10.1145/1706299.1706346.

Digital Library

[12]

A. C. J. Fox. Directions in ISA specification. In Interactive Theorem Proving – Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings, pages 338–344, 2012. URL http://dx.doi.org/10.1007/978-3-642-32347-8_23.

[13]

S. Goel, W. A. Hunt, M. Kaufmann, and S. Ghosh. Simulation and formal verification of x86 machine-code programs that make system calls. In Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, FMCAD ’14, pages 18:91–18:98, Austin, TX, 2014. FMCAD Inc. ISBN 978-0-9835678-4-4. URL http://dl.acm.org/citation.cfm?id=2682923.2682944.

Digital Library

[14]

K. E. Gray, G. Kerneis, D. Mulligan, C. Pulte, S. Sarkar, and P. Sewell. An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors. In Proc. MICRO-48, the 48th Annual IEEE/ACM International Symposium on Microarchitecture, Dec. 2015.

Digital Library

[15]

A. Kennedy, N. Benton, J. B. Jensen, and P.-E. Dagand. Coq: The world’s best macro assembler? In Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP ’13, pages 13–24, New York, NY, USA, 2013. ACM. ISBN 978-1-4503- 2154-9. URL http://doi.acm.org/10.1145/2505879.2505897.

Digital Library

[16]

R. Kumar, M. O. Myreen, M. Norrish, and S. Owens. Cakeml: A verified implementation of ml. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, pages 179–191, New York, NY, USA, 2014. ACM. ISBN 978-1-4503-2544-8. URL http://doi.acm.org/10.1145/2535838.2535841.

Digital Library

[17]

X. Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363–446, 2009. URL http://gallium.inria.fr/~xleroy/publi/compcert-backend.pdf.

Digital Library

[18]

L. Maranget, S. Sarkar, and P. Sewell. A tutorial introduction to the ARM and POWER relaxed memory models. Draft available from http://www.cl.cam.ac.uk/~pes20/ppc-supplemental/test7.pdf, 2012.

[19]

P. McKenney. Validating memory barriers and atomic instructions. Linux Weekly News article, Dec. 2011.

[20]

https://lwn.net/Articles/470681/.

[21]

G. Morrisett, G. Tan, J. Tassarotti, J. Tristan, and E. Gan. Rocksalt: better, faster, stronger SFI for the x86. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’12, Beijing, China - June 11 - 16, 2012, pages 395–404, 2012. URL http://doi.acm.org/10.1145/2254064.2254111.

Digital Library

[22]

D. P. Mulligan, S. Owens, K. E. Gray, T. Ridge, and P. Sewell. Lem: reusable engineering of real-world semantics. In Proceedings of ICFP 2014: the 19th ACM SIGPLAN International Conference on Functional Programming, pages 175–188, 2014. URL http://doi.acm.org/10.1145/2628136.2628143.

Digital Library

[23]

S. Owens, S. Sarkar, and P. Sewell. A better x86 memory model: x86-TSO. In Proceedings of TPHOLs 2009: Theorem Proving in Higher Order Logics, LNCS 5674, pages 391–407, 2009.

Digital Library

[24]

S. Sarkar, P. Sewell, F. Zappa Nardelli, S. Owens, T. Ridge, T. Braibant, M. Myreen, and J. Alglave. The semantics of x86-CC multiprocessor machine code. In Proceedings of POPL 2009: the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pages 379–391, Jan. 2009. URL http://doi.acm.org/10.1145/1594834.1480929.

Digital Library

[25]

S. Sarkar, P. Sewell, J. Alglave, L. Maranget, and D. Williams. Understanding POWER multiprocessors. In Proceedings of PLDI 2011: the 32nd ACM SIGPLAN conference on Programming Language Design and Implementation, pages 175–186, 2011. URL http://doi.acm.org/10.1145/1993498.1993520.

Digital Library

[26]

S. Sarkar, K. Memarian, S. Owens, M. Batty, P. Sewell, L. Maranget, J. Alglave, and D. Williams. Synchronising C/C++ and POWER. In Proceedings of PLDI 2012, the 33rd ACM SIGPLAN conference on Programming Language Design and Implementation (Beijing), pages 311–322, 2012.

Digital Library

[27]

. URL http://doi.acm.org/10.1145/2254064.2254102.

[28]

P. Sewell, S. Sarkar, S. Owens, F. Zappa Nardelli, and M. O. Myreen. x86-TSO: A rigorous and usable programmer’s model for x86 multiprocessors. Communications of the ACM, 53(7):89–97, July 2010.

Digital Library

[29]

(Research Highlights).

[30]

X. Shi, J.-F. Monin, F. Tuong, and F. Blanqui. First steps towards the certification of an ARM simulator using Compcert. In J.-P. Jouannaud and Z. Shao, editors, Certified Programs and Proofs, volume 7086 of Lecture Notes in Computer Science, pages 346–361. Springer Berlin Heidelberg, 2011. ISBN 978-3-642-25378-2. URL http://dx.doi.org/10.1007/978-3-642-25379-9_25.

Digital Library

[31]

J. Ševˇcík, V. Vafeiadis, F. Zappa Nardelli, S. Jagannathan, and P. Sewell. CompCertTSO: A verified compiler for relaxed-memory concurrency. J. ACM, 60(3):22:1–22:50, June 2013. ISSN 0004-5411.

Digital Library

Cited By

Iorga DWickerson JDonaldson A(2023)Simulating Operational Memory Models Using Off-the-Shelf Program Analysis ToolsIEEE Transactions on Software Engineering10.1109/TSE.2023.332605649:12(5084-5102)Online publication date: 1-Dec-2023
https://dl.acm.org/doi/10.1109/TSE.2023.3326056
Moiseenko EPodkopaev AKoznov D(2021)A Survey of Programming Language Memory ModelsProgramming and Computing Software10.1134/S036176882106005047:6(439-456)Online publication date: 3-Dec-2021
https://dl.acm.org/doi/10.1134/S0361768821060050
Hóu ZSanan DTiu ALiu YHoa KDong J(2021)An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory ModelJournal of Automated Reasoning10.1007/s10817-020-09579-465:4(569-598)Online publication date: 1-Apr-2021
https://dl.acm.org/doi/10.1007/s10817-020-09579-4
Show More Cited By

Index Terms

Modelling the ARMv8 architecture, operationally: concurrency and ISA

Recommendations

Promising-ARM/RISC-V: a simpler and faster operational concurrency model
PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

For ARMv8 and RISC-V, there are concurrency models in two styles, extensionally equivalent: axiomatic models, expressing the concurrency semantics in terms of global properties of complete executions; and operational models, that compute incrementally. ...
Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8

ARM has a relaxed memory model, previously specified in informal prose for ARMv7 and ARMv8. Over time, and partly due to work building formal semantics for ARM concurrency, it has become clear that some of the complexity of the model is not justified by ...
Modelling the ARMv8 architecture, operationally: concurrency and ISA
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

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

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 51, Issue 1

POPL '16

January 2016

815 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2914770

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2016
815 pages
ISBN:9781450335492
DOI:10.1145/2837614
General Chair:
Rastislav Bodik
UC Berkeley, USA
,
Program Chair:
Rupak Majumdar
MPI-SWS, Germany

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2016

Published in SIGPLAN Volume 51, Issue 1

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

120
Total Citations
View Citations
770
Total Downloads

Downloads (Last 12 months)54
Downloads (Last 6 weeks)6

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Iorga DWickerson JDonaldson A(2023)Simulating Operational Memory Models Using Off-the-Shelf Program Analysis ToolsIEEE Transactions on Software Engineering10.1109/TSE.2023.332605649:12(5084-5102)Online publication date: 1-Dec-2023
https://dl.acm.org/doi/10.1109/TSE.2023.3326056
Moiseenko EPodkopaev AKoznov D(2021)A Survey of Programming Language Memory ModelsProgramming and Computing Software10.1134/S036176882106005047:6(439-456)Online publication date: 3-Dec-2021
https://dl.acm.org/doi/10.1134/S0361768821060050
Hóu ZSanan DTiu ALiu YHoa KDong J(2021)An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory ModelJournal of Automated Reasoning10.1007/s10817-020-09579-465:4(569-598)Online publication date: 1-Apr-2021
https://dl.acm.org/doi/10.1007/s10817-020-09579-4
Colvin R(2021)Parallelized Sequential Composition and Hardware Weak Memory ModelsSoftware Engineering and Formal Methods10.1007/978-3-030-92124-8_12(201-221)Online publication date: 3-Dec-2021
https://doi.org/10.1007/978-3-030-92124-8_12
Ben Yehuda RZaidenberg N(2020)Protection against reverse engineering in ARMInternational Journal of Information Security10.1007/s10207-019-00450-119:1(39-51)Online publication date: 1-Feb-2020
https://dl.acm.org/doi/10.1007/s10207-019-00450-1
de Putter SWijs A(2020)Lock and Fence When Needed: State Space Exploration + Static Analysis = Improved Fence and Lock InsertionIntegrated Formal Methods10.1007/978-3-030-63461-2_16(297-317)Online publication date: 13-Nov-2020
https://doi.org/10.1007/978-3-030-63461-2_16
Smith GGroves L(2020)Weakening Correctness and Linearizability for Concurrent Objects on Multicore ProcessorsFormal Methods. FM 2019 International Workshops10.1007/978-3-030-54997-8_22(342-357)Online publication date: 11-Aug-2020
https://doi.org/10.1007/978-3-030-54997-8_22
Tahat AJoshi SGoswami PRavindran B(2019)Scalable Translation Validation of Unverified Legacy OS Code2019 Formal Methods in Computer Aided Design (FMCAD)10.23919/FMCAD.2019.8894252(1-9)Online publication date: Oct-2019
https://doi.org/10.23919/FMCAD.2019.8894252
Winter KSmith GDerrick J(2019)Modelling concurrent objects running on the TSO and ARMv8 memory modelsScience of Computer Programming10.1016/j.scico.2019.102308(102308)Online publication date: Sep-2019
https://doi.org/10.1016/j.scico.2019.102308
Li KLi SHuang SChen YZhang Y(2019)FastNBL: fast neighbor lists establishment for molecular dynamics simulation based on bitwise operationsThe Journal of Supercomputing10.1007/s11227-019-02860-3Online publication date: 29-Apr-2019
https://doi.org/10.1007/s11227-019-02860-3
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents