一句话：使用 Sail 语言为 ARMv8-A、RISC-V、MIPS 和 CHERI-MIPS 架构建立严谨的可执行语义模型，支持模拟器与证明助手代码生成。
架构规范通常以散文和伪代码形式存在，缺乏严谨性和可执行性，给软件开发和验证带来不确定性。本文使用自定义的 ISA 语义语言 Sail（具有轻量级依赖类型系统），为 ARMv8-A、RISC-V、MIPS 及研究性 CHERI-MIPS 架构的大型顺序行为片段建立了严谨语义模型。这些模型足以引导 Linux、FreeBSD 和 seL4 操作系统。Sail 支持自动生成 C 和 OCaml 模拟器代码，以及 Isabelle、HOL4、Coq 的证明助手定义。ARMv8-A 模型由 ARM 内部定义自动翻译而来，并通过 ARM 架构验证套件测试。我们还在 Isabelle 中证明了 ARMv8-A 地址翻译纯函数刻画的正确定性，将 RISC-V 模型集成到 RMEM 工具中，并在纸上证明了 Sail 核心类型系统的可靠性。
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 system. We thereby take a big step towards making the architectural abstraction actually well-defined, establishing foundations for verification and reasoning.
@article{paperbot639,
title = {ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS},
author = {Alasdair Armstrong and Thomas Bauereiss and Brian Campbell and Alastair Reid and Kathryn E. Gray and Robert M. Norton and Prashanth Mundkur and Mark Wassell and Jon French and Christopher Pulte and Shaked Flur and Ian Stark and Neel Krishnaswami and Peter Sewell},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290384}
}