skip to main content
research-article
Open access

Armed Cats: Formal Concurrency Modelling at Arm

Published: 23 July 2021 Publication History

Abstract

We report on the process for formal concurrency modelling at Arm. An initial formal consistency model of the Arm achitecture, written in the cat language, was published and upstreamed to the herd+diy tool suite in 2017. Since then, we have extended the original model with extra features, for example, mixed-size accesses, and produced two provably equivalent alternative formulations.
In this article, we present a comprehensive review of work done at Arm on the consistency model. Along the way, we also show that our principle for handling mixed-size accesses applies to x86: We confirm this via vast experimental campaigns. We also show that our alternative formulations are applicable to any model phrased in a style similar to the one chosen by Arm.

References

[1]
Arm Ltd. 2020. Arm released cat models. https://github.com/herd/herdtools7/tree/master/herd/libdir/arm-models.
[2]
Richard Gooch and Pekka Enberg. 2005. Linux Kernel Virtual File System (VFS). https://www.kernel.org/doc/html/latest/filesystems/vfs.html
[3]
RISC-V. 2019. The RISC-V Instruction Set Manual Volume I: Unprivileged ISA. https://content.riscv.org/wp-content/uploads/2019/12/riscv-spec-20191213.pdf.
[4]
Arm Ltd. 2020. Arm Memory Model. https://developer.arm.com/architectures/cpu-architecture/a-profile/memory-model-tool.
[5]
Arm Ltd. 2020. Armv8, for Armv8-A architecture profile. In Arm Architecture Reference Manual, Vol. ARM DDI 0487F.c. https://developer.arm.com/docs/ddi0487/latest/arm-architecture-reference-manual-armv8-for-armv8-a-architecture-profile.
[6]
Jade Alglave. 2019. Retrieved from https://github.com/herd/herdtools7/commit/95785c747750be4a3b64adfab9d5f5ee0ead8240.
[7]
Jade Alglave. 2020. https://github.com/herd/herdtools7/blob/master/herd/libdir/x86tso-mixed.cat.
[8]
Jade Alglave. 2010. A Shared Memory Poetics. PhD thesis.
[9]
Jade Alglave. 2019. Retrieved from Adding mixed-size accesses to Arm formal memory model. https://github.com/herd/herdtools7/commit/95785c747750be4a3b64adfab9d5f5ee0ead8240#diff-cc249d0a9116e1ab890d8b52586bc702.
[10]
Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen, and John Wickerson. 2015. GPU Concurrency: Weak behaviours and programming assumptions. In Proceedings of the 20th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS’15), Özcan Özturk, Kemal Ebcioglu, and Sandhya Dwarkadas (Eds.). ACM, 577–591.
[11]
Jade Alglave and Patrick Cousot. 2017. Ogre and Pythia: an invariance proof method for weak consistency models. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’17), Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 3–18.
[12]
Jade Alglave, Patrick Cousot, and Luc Maranget. 2016. Syntax and semantics of the weak consistency model specification language cat. CoRR abs/1608.07531. Retrieved from http://arxiv.org/abs/1608.07531.
[13]
Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli. 2009. The semantics of power and ARM multiprocessor machine code. In Proceedings of the POPL 2009 Workshop on Declarative Aspects of Multicore Programming (DAMP’09), Leaf Petersen and Manuel M. T. Chakravarty (Eds.). ACM, 13–24.
[14]
Jade Alglave and Luc Maranget. 2010-present. The herd+diy toolsuite. Retrieved from http://diy.inria.fr.
[15]
Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and Alan S. Stern. 2018. Frightening small children and disconcerting grown-ups: Concurrency in the linux kernel. In Proceedings of the 23rd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS’18), Xipeng Shen, James Tuck, Ricardo Bianchini, and Vivek Sarkar (Eds.). ACM, 405–418.
[16]
Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2010. Fences in weak memory models. In Proceedings of the 22nd International Conference on Computer Aided Verification (CAV’10), Tayssir Touili, Byron Cook, and Paul B. Jackson (Eds.), Lecture Notes in Computer Science, Vol. 6174. Springer, 258–272.
[17]
Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2011. Litmus: Running tests against hardware. In Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’11), Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS’11), Parosh Aziz Abdulla and K. Rustan M. Leino (Eds.), Lecture Notes in Computer Science, Vol. 6605. Springer, 41–44.
[18]
Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2012. Fences in weak memory models (extended version). Formal Methods Syst. Des. 40, 2 (2012), 170–205.
[19]
Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. Herding Cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst. 36, 2 (2014), 7:1–7:74.
[20]
Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ concurrency. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’11), Thomas Ball and Mooly Sagiv (Eds.). ACM, 55–66.
[21]
Nathan Chong and Samin Ishtiaq. 2008. Reasoning about the ARM weakly consistent memory model. In ACM SIGPLAN Workshop on Memory Systems Performance and Correctness.
[22]
Nathan Chong, Tyler Sorensen, and John Wickerson. 2018. The semantics of transactions and weak memory in x86, Power, ARM, and C++. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’18), Jeffrey S. Foster and Dan Grossman (Eds.). ACM, 211–225.
[23]
Will Deacon. 2017. Formal memory model for Armv8.0 application level. Retrieved from https://github.com/herd/herdtools7/commit/daa126680b6ecba97ba47b3e05bbaa51a89f27b7#diff-0461c726950c4454a08bd97fbfd49252.
[24]
Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. 2016. Modelling the ARMv8 architecture, operationally: concurrency and ISA. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’16), Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 608–621.
[25]
Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell. 2017. Mixed-size concurrency: ARM, POWER, C/C++11, and SC. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’17), Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 429–442.
[26]
C. A. R. Hoare and Peter E. Lauer. 1974. Consistent and complementary formal theories of the semantics of programming languages. Acta Inf. 3 (1974), 135–153.
[27]
Daniel Jackson. 2019. Alloy: A language and tool for exploring software designs. Commun. ACM 62, 9 (2019), 66–76.
[28]
Antoine Hacquard, Jade Alglave, and Luc Maranget. [n.d.]. Mixed-size experiments on AArch64 and x86. Retrieved from http://diy.inria.fr/mixed/.
[29]
Radha Jagadeesan, Alan Jeffrey, and James Riely. 2020. Pomsets with preconditions: A simple model of relaxed memory. Proc. ACM Program. Lang. 4, OOPSLA (2020).
[30]
Jeehoon Kang, Chung-Kil Hur, Ori Lahav, Viktor Vafeiadis, and Derek Dreyer. 2017. A promising semantics for relaxed-memory concurrency. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’17), Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 175–189.
[31]
Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. 2017. Repairing sequential consistency in C/C++11. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’17), Albert Cohen and Martin T. Vechev (Eds.). ACM, 618–632.
[32]
Leslie Lamport. 1979. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28, 9 (1979), 690–691.
[33]
Daniel Lustig, Sameer Sahasrabuddhe, and Olivier Giroux. 2019. A formal analysis of the NVIDIA PTX memory consistency model. In Proceedings of the 24th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS’19), Iris Bahar, Maurice Herlihy, Emmett Witchel, and Alvin R. Lebeck (Eds.). ACM, 257–270.
[34]
Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. 2018. Simplifying ARM concurrency: Multicopy-atomic axiomatic and operational models for ARMv8. PACMPL 2, POPL (2018), 19:1–19:29.
[35]
Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung Hwan Lee, and Chung-Kil Hur. 2019. Promising-ARM/RISC-V: a simpler and faster operational concurrency model. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’19), Kathryn S. McKinley and Kathleen Fisher (Eds.). ACM, 1–15.
[36]
Azalea Raad, John Wickerson, and Viktor Vafeiadis. 2019. Weak persistency semantics from the ground up: formalising the persistency semantics of ARMv8 and transactional models. PACMPL 3, OOPSLA (2019), 135:1–135:27.
[37]
Susmit Sarkar, Kayvan Memarian, Scott Owens, Mark Batty, Peter Sewell, Luc Maranget, Jade Alglave, and Derek Williams. 2012. Synchronising C/C++ and POWER. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’12), Jan Vitek, Haibo Lin, and Frank Tip (Eds.). ACM, 311–322.
[38]
Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. 2011. Understanding POWER multiprocessors. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’11), Mary W. Hall and David A. Padua (Eds.). ACM, 175–186.
[39]
Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, and Jade Alglave. 2009. The semantics of x86-CC multiprocessor machine code. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’09), Zhong Shao and Benjamin C. Pierce (Eds.). ACM, 379–391.
[40]
Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. 2010. x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM 53, 7 (2010), 89–97.
[41]
Ben Simner, Shaked Flur, Christopher Pulte, Alasdair Armstrong, Jean Pichon-Pharabod, Luc Maranget, and Peter Sewell. 2020. ARMv8-A system semantics: Instruction fetch in relaxed architectures (extended version). (2020).
[42]
Viktor Vafeiadis. 2021. Retrieved from https://github.com/vafeiadis/arm-model.
[43]
Conrad Watt, Christopher Pulte, Anton Podkopaev, Guillaume Barbier, Stephen Dolan, Shaked Flur, Jean Pichon-Pharabod, and Shu-yu Guo. 2020. Repairing and mechanising the JavaScript relaxed memory model. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI’20), Alastair F. Donaldson and Emina Torlak (Eds.). ACM, 346–361.

Cited By

View all
  • (2025)Model Checking C/C++ with Mixed-Size AccessesProceedings of the ACM on Programming Languages10.1145/37049119:POPL(2232-2252)Online publication date: 9-Jan-2025
  • (2025)Monadic Interpreters for Concurrent Memory ModelsProceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3703595.3705890(283-298)Online publication date: 10-Jan-2025
  • (2024)CrossMappingProceedings of the 2024 USENIX Conference on Usenix Annual Technical Conference10.5555/3691992.3692054(1013-1028)Online publication date: 10-Jul-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems
ACM Transactions on Programming Languages and Systems  Volume 43, Issue 2
June 2021
197 pages
ISSN:0164-0925
EISSN:1558-4593
DOI:10.1145/3470134
Issue’s Table of Contents
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 July 2021
Accepted: 01 March 2021
Revised: 01 March 2021
Received: 01 August 2020
Published in TOPLAS Volume 43, Issue 2

Check for updates

Author Tags

  1. Concurrency Weak memory models
  2. arm architecture
  3. linux
  4. mixed-size accesses

Qualifiers

  • Research-article
  • Research
  • Refereed

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)833
  • Downloads (Last 6 weeks)80
Reflects downloads up to 20 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2025)Model Checking C/C++ with Mixed-Size AccessesProceedings of the ACM on Programming Languages10.1145/37049119:POPL(2232-2252)Online publication date: 9-Jan-2025
  • (2025)Monadic Interpreters for Concurrent Memory ModelsProceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3703595.3705890(283-298)Online publication date: 10-Jan-2025
  • (2024)CrossMappingProceedings of the 2024 USENIX Conference on Usenix Annual Technical Conference10.5555/3691992.3692054(1013-1028)Online publication date: 10-Jul-2024
  • (2024)Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO ArchitecturesProceedings of the ACM on Programming Languages10.1145/36897818:OOPSLA2(1982-2009)Online publication date: 8-Oct-2024
  • (2024)Toast: A Heterogeneous Memory Management SystemProceedings of the 2024 International Conference on Parallel Architectures and Compilation Techniques10.1145/3656019.3676944(53-65)Online publication date: 14-Oct-2024
  • (2024)How Hard Is Weak-Memory Testing?Proceedings of the ACM on Programming Languages10.1145/36329088:POPL(1978-2009)Online publication date: 5-Jan-2024
  • (2024)An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL LogicProceedings of the ACM on Programming Languages10.1145/36328638:POPL(604-637)Online publication date: 5-Jan-2024
  • (2024)Compiler Testing with Relaxed Memory Models2024 IEEE/ACM International Symposium on Code Generation and Optimization (CGO)10.1109/CGO57630.2024.10444836(334-348)Online publication date: 2-Mar-2024
  • (2024)Efficiently Adapting Stateless Model Checking for C11/C++11 to Mixed-Size AccessesProgramming Languages and Systems10.1007/978-981-97-8943-6_17(346-364)Online publication date: 23-Oct-2024
  • (2023)Static Analysis of Memory Models for SMT EncodingsProceedings of the ACM on Programming Languages10.1145/36228557:OOPSLA2(1618-1647)Online publication date: 16-Oct-2023
  • Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

HTML Format

View this article in HTML Format.

HTML Format

Login options

Full Access

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media