On the Role of Prose in Specifications (Invited Talk)

Alglave, Jade

doi:10.4230/LIPIcs.CONCUR.2026.1

File

PDF

LIPIcs.CONCUR.2026.1.pdf

Filesize: 2.15 MB
15 pages

Document Identifiers

DOI: 10.4230/LIPIcs.CONCUR.2026.1
URN: urn:nbn:de:0030-drops-273326

Subject Classification

ACM Subject Classification

Theory of computation → Concurrency
Software and its engineering → Formal software verification
Computer systems organization → Architectures

Keywords

Arm Architecture
(prose
formal
executable
queryable
accessible) specifications
concurrency
herdtools
litmus tests
instruction set
Architecture Specification Language (ASL)
The Architecture Speaks
query interface

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

Document

0

Metadata

Abstract

Specifications should let users find answers to their questions. Those answers should be accessible, unambiguous, consensual, reproducible, auditable, and they should be traceable to the artefacts users actually read.
This paper uses work done by the Arm Architecture Formal Team as a case study in the tensions between those requirements.

Cite As Get BibTex

Jade Alglave. On the Role of Prose in Specifications (Invited Talk). In 37th International Conference on Concurrency Theory (CONCUR 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 391, pp. 1:1-1:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CONCUR.2026.1

Author Details

Jade Alglave

Arm, Cambridge, UK
University College London, UK

Acknowledgements

I would like to thank Nikos Nikoleris, Simon Peyton Jones and Daryl Stewart for taking the time to review various drafts and provide helpful feedback. I would like to give a big shout-out to the Arm Architecture Formal Team who works tiredlessly and with good cheer towards our ambition. I would like to thank Richard Grisenthwaite for giving the team the time and space needed to pursue our work and shape our vision.

References

Jade Alglave. Introducing "The Architecture Speaks", 2026. URL: https://developer.arm.com/community/arm-community-blogs/b/ai-blog/posts/introducing-the-architecture-speaks.
Jade Alglave, Richard Grisenthwaite, Artem Khyzha, Luc Maranget, and Nikos Nikoleris. Puss In Boots: On Formalizing Arm’s Virtual Memory System Architecture. IEEE MICRO, 2024. URL: https://doi.org/10.1109/MM.2024.3422668.
Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. Fences in Weak Memory Models. CAV, 2010.
Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. Litmus: running tests against hardware. TACAS, 2011.
Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding cats. TOPLAS, 2014.
Jade Alglave and Luc et al Maranget. herdtools7, 2026. URL: https://github.com/herd/herdtools7.
The Architecture Speaks chatbot. "what does an LDR do?", 2026. URL: https://developer.arm.com/architecture/the-architecture-speaks/?threadId=228d9997-7d58-4b2d-a1ce-2bfd6339aec3.
Arm. Arm Architecture Reference Manual for A-Profile Architecture. URL: https://developer.arm.com/documentation/ddi0487/mb/?lang=en.
Arm. ASL Reference, 2025. URL: https://developer.arm.com/architectures/architecture%20specification%20language.
Arm. ASL stdlib proofs, 2025. URL: https://github.com/herd/herdtools7/tree/master/acl2/asl/proofs/stdlib.
Arm. ASL1 code for LDR, 2025. URL: https://developer.arm.com/documentation/ddi0602/2025-12/Base-Instructions/LDR--immediate---Load-register--immediate--.
Arm. ASLRef tooling, 2025. URL: https://github.com/herd/herdtools7/tree/master/asllib.
Arm. The Architecture Speaks, 2026. URL: https://developer.arm.com/architecture/the-architecture-speaks/.
Arm. Web interface to ASLRef tooling, 2026. URL: https://developer.arm.com/architectures/tools/aslref.
Kathryn E. Gray, Peter Sewell, Christopher Pulte, Shaked Flur, and Robert Norton-Wright. The Sail instruction-set semantics specification language. URL: https://www.cl.cam.ac.uk/~pes20/sail/manual.pdf.
Alastair Reid. Trustworthy specifications of Arm v8-A and v8-M system level architecture. FMCAD, 2016.
Alastair Reid. ASL0 interpreter, 2020. URL: https://github.com/alastairreid/asl-interpreter.
Hadrien Renaud. Executable semantics of Arm’s Architecture Specification Language. JFLA, 2024. URL: https://hal.science/hal-04406399/document.
Dongjun Youn, Wonho Shin, Jaehyun Lee, Sukyoung Ryu, Joachim Breitner, Philippa Gardner, Sam Lindley, Matija Pretnar, Xiaojia Rao, Conrad Watt, and Andreas Rossberg. Bringing the WebAssembly Standard up to Speed with SpecTec. URL: https://dl.acm.org/doi/10.1145/3656440.