Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version)

Armstrong, A; Campbell, B; Simner, B; Pulte, C; Sewell, P

Journal article

Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version)

Abstract:: Computing relies on architecture specifications to decouple hardware and software development. Historically these have been prose documents, with all the problems that entails, but research over the last ten years has developed rigorous and executable-as-test-oracle specifications of mainstream architecture instruction sets and 'user-mode' concurrency, clarifying architectures and bringing them into the scope of programming-language semantics and verification. However, the system semantics, of address translation and TLB maintenance, instruction-fetch and its required cache maintenance, and exceptions and interrupts, remains mostly obscure, leaving us without a solid foundation for verification of security-critical systems software. We develop precise mathematical models, for those aspects of the Arm A-class architecture. We implement these models as executable models, in both microarchitectural-flavoured operational and declarative axiomatic style formats. We validate these models, against currently available hardware through the production and evaluation of hardware test harnesses and test suites, and against the architectural intent through discussions with Arm architects. We give a variety of hand-written and machine-generated litmus tests, exercising parts of the architecture previously unexplored. We discuss the nature of developing such models, and the challenges that writing specifications of existing systems entails. We briefly touch on how these models have evolved over time, and how we imagine they will evolve in the future as the remaining questions are resolved

Publication status:: Published

Peer review status:: Peer reviewed

Actions

Email

Email this record

Send the bibliographic details of this record to your email address.

Your Email
Please enter the email address that the record information will be sent to.

-
Your message (optional)
Please add any additional information to be included within the email.
Share
Cite

Cite this record

APA Style

Armstrong, A., Campbell, B., Simner, B., Pulte, C., & Sewell, P. (2023). Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version). Formal Methods in System Design, 63(1-3), 110–133.

MLA Style

Armstrong, A, et al. “Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models (Extended Version).” Formal Methods in System Design, vol. 63, nos. 1-3, 2023, pp. 110–33.

Chicago Style

Armstrong, A, B Campbell, B Simner, C Pulte, and P Sewell. 2023. “Isla: Integrating Full-Scale ISA Semantics and Axiomatic Concurrency Models (Extended Version).” Formal Methods in System Design 63 (1-3): 110–33.
Print