ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
Alasdair Armstrong, Thomas Bauereiss, Brian
Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth
Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark,
Neel Krishnaswami, and Peter Sewell
Architecture specifications notionally define the fundamental interface between
hardware and software: the envelope of allowed behaviour for processor
implementations, and the basic assumptions for software development and
verification. But in practice, they are typically prose and pseudocode
documents, not rigorous or executable artifacts, leaving software and
verification on shaky ground.
In this paper, we present rigorous semantic models for the sequential behaviour
of large parts of the mainstream ARMv8-A, RISC-V, and MIPS architectures, and
the research CHERI-MIPS architecture, that are complete enough to boot
operating systems, variously Linux, FreeBSD, or seL4. Our ARMv8-A models are
automatically translated from authoritative ARM-internal definitions, and (in
one variant) tested against the ARM Architecture Validation Suite.
We do this using a custom language for ISA semantics, Sail, with a lightweight
dependent type system, that supports automatic generation of emulator code in C
and OCaml, and automatic generation of proof-assistant definitions for
Isabelle, HOL4, and (currently only for MIPS) Coq. We use the former for
validation, and to assess specification coverage. To demonstrate the usability
of the latter, we prove (in Isabelle) correctness of a purely functional
characterisation of ARMv8-A address translation. We moreover integrate the
RISC-V model into the RMEM tool for (user-mode) relaxed-memory concurrency
exploration. We prove (on paper) the soundness of the core Sail type
We thereby take a big step towards making the architectural abstraction
actually well-defined, establishing foundations for verification and reasoning.
ISA Semantics for ARMv8-A, RISC-V, and
Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid,
Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon
French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and
In POPL 2019, Proc. ACM Program. Lang. 3, POPL, Article 71.
[ bib |
- Alasdair Armstrong, University of Cambridge
- Thomas Bauereiss, University of Cambridge
- Brian Campbell, University of Edinburgh
- Alastair Reid, ARM
- Kathryn E. Gray, University of Cambridge (formerly)
- Robert M. Norton, University of Cambridge
- Prashanth Mundkur, SRI International
- Mark Wassell, University of Cambridge
- Jon French, University of Cambridge
- Christopher Pulte, University of Cambridge
- Shaked Flur, University of Cambridge
- Ian Stark, University of Edinburgh
- Neel Krishnaswami, University of Cambridge
- Peter Sewell, University of Cambridge
- MiniSail core calculus
- Isabelle proof scripts about ARMv8-A address translation
- The Sail source code is available on GitHub.
Instructions for building Sail from source can be found here.
It is also possible to install Sail using the OPAM OCaml package manager by following these instructions.
A manual describing the Sail language and its usage is available here, including instructions on how to generate emulators from Sail models.
We are currently working on making the necessary steps and prerequisites for booting operating systems on our models publicly available, e.g. the private ARMv8-A specification.
For booting FreeBSD on MIPS, instructions are available here.
The following models discussed in the paper are publicly available:
ARM have agreed for us to release a version of the private model
discussed in the paper, for ARMv8.5-A. We plan to make this available shortly.
Snapshots of generated theorem prover definitions for these models are available here.