ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS
复制标题
DOI：
10.1145/3290384
复制
发表时间：
2019-01-01
影响因子：
1.8
通讯作者：
Sewell, Peter
中科院分区：
文献类型：
--
作者：
Armstrong, Alasdair;Bauereiss, Thomas;Sewell, Peter
架构规范在概念上定义了硬件和软件之间的基本接口：处理器实现的允许行为的信封以及软件开发和验证的基本假设。但是实际上，它们通常是散文和伪代码文档，而不是严格或可执行的伪像，在摇摇欲坠的地面上留下软件和验证。在本文中，我们为主流ARMV8-A，RISC的大部分依次行为提出了严格的语义模型，RISC -v和MIPS架构以及研究Cheri-MIPS体系结构，它们完全可以启动操作系统，即不同的Linux，FreeBSD或SEL4。我们的ARMV8-A模型自动从权威的Arm-Internal定义转换，并且（在一个变体中）针对ARM Architecture验证套件进行了测试。我们使用ISA Sentics的自定义语言进行此操作，帆，具有轻巧的类型系统，该系统，该系统，该系统支持C和OCAML中自动生成的仿真器代码，以及自动生成Isabelle，Hol4和（目前仅用于MIPS）COQ的证明辅助定义。我们使用前者进行验证，并评估规范覆盖范围。为了证明后者的可用性，我们证明了ARMV8-A地址翻译的纯粹功能表征的（在Isabelle中）。此外，我们将RISC-V模型集成到（用户模式）放松的记忆并发探索的RMEM工具中。我们（在纸上）证明了核心帆类型系统的健全性。因此，我们朝着使建筑抽象真正定义明确的，为验证和推理建立基础迈出了重要一步。
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.