ISA语义规范_POPL19

1、ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPSPOPL19冯维直1OutlineMotivation: why we need formal semantics models for ISASail: an ISA semantics specification languageModels: RISC-VGeneration of Theorem Prover DefinitionsFormal Type System Generation of EmulatorsValidation2回顾上次报告最后的内容：RISC-V的形式语义3：RI

2、SC-V的形式语义4介绍最近在看的一个项目：/mit-plv/riscv-semanticsRISC-V的形式语义5代码结构：Src：SpecDecode.hs: 指令和参数, 如何提取指令ExecuteI.hs, ExecuteM.hs, ExecuteF.hs, ExecuteCSR.hs: 不同指令子集的执行 CSR.hs, CSRField.hs, CSRSpec.hs：读-写CSR的一些相关内容Spec.hs：描述一个cycle如何运行Machine.hs：定义基础操作，如setPCRISC-V的形式语义6Decode.hs:RISC-V的形式语义7Decode.hs:RISC-V的

3、形式语义8ExecuteI.hs:RISC-V的形式语义9ExecuteCSR.hs:Motivation：why we need formal semantics models for ISA10指令集架构的规范往往用文档的形式来描述指令的行为，如译码表、伪代码等，且往往非常复杂与庞大，如ARMv8-A的文档多达6000多页，包括：1. 单独描述每条指令的行为，2. 指令如何组合构成系统的并发模型和中断行为等.实现计算机系统的正确且鲁棒行为往往需要理解ISA的所有细节，而伪代码文档很难对其精确表述；规范文档（specification documents）无法作为test oracles来执

4、行 they do not allow one to compute the set of all architecturally allowed behaviour of hardware tests, or to test software above the entire architectural envelope rather than just some specific implementation and they do not support automatic test generation or test-suite specification coverage meas

5、urement.Programming languages, semantics, analysis and verification 领域的学者，越来越多致力于低至机器层面的正确性机械化推理（aim at mechanized reasoning about correctness down to the machine level），这也需要体系架构模型.Motivation：why we need formal semantics models for ISA11现有形式化模型的不足之处：Many groups have hand-written formal models of mod

6、est ISA fragments. These typically cover just enough of the instruction set, and in just enough detail, for their purpose往往只针对ISA的部分指令的顺序行为进行建模，或者只用于单个的定理证明工具（Coq, HOL4, Isabelle），这种每个小组对特定目的开发和优化的模型，不够完整，且难以用于其他任务。Motivation：why we need formal semantics models for ISA12本文的贡献：They present rigorous s

7、emantic models for the sequential behaviour of large parts of the mainstream ARMv8-A, RISC-V and MIPS architectures, that are complete enough to boot operating systems: Linux above the ARMv8-A model, and RISC-V.They achieve the models via a custom language for ISA semantics called Sail (extend Sail,

8、 formalize a core of Sails type system and prove its soundness).They provide automatic translations from Sail specifications to theorem prover definitions, for multiple provers.They provide automatic generation of emulators from Sail specifications that perform well enough to boot operating systems.

9、Sail：the instruction-set semantics specification language13Sail is a language for expressing the instruction-set architecture (ISA) semantics of processors.Sail aims to provide a engineer-friendly, vendor-pseudocode-like language for describing instruction semantics.Given a Sail definition, the tool

10、 will type-check it and generate executable emulators, theorem-prover definitions for Coq, HOL4 and Isabelle.Sail：the instruction-set semantics specification language14Sail supports various convenience features tuned for ISA specifications.Specifications are typically large and flat, so Sail support

11、s splitting functions and type definitions into multiple clauses which can be scattered throughout the file, interleaved with other definitions. (Sail 支持将函数和类型定义分散到不同的子句中，和其他定义交错排列)Example：multiple clauses for a load instruction from RISC-V formalized in Sail, group together in the way they would be

12、 in an ISA manual.Sail：the instruction-set semantics specification language15Sail supports various convenience features tuned for ISA specifications.Specifications are typically large and flat, so Sail supports splitting functions and type definitions into multiple clauses which can be scattered thr

13、oughout the file, interleaved with other definitions. (Sail 支持将函数和类型定义分散到不同的子句中，和其他定义交错排列)Sail：the instruction-set semantics specification language16Sail 的其他features：Lightweight dependent types for bitvector lengths and integer rangesISA通常是对bitvector操作进行描述，包括计算的indices和length，寄存器索引等，Sail使用一个类型系统去检查这

14、些，确保向量索引不越界. Example: assert 确保shift这个变量大于0, let语句令shift为S，范围为1到N（表示类型变量，ocaml的语法), 扩展x的长度为S+N，然后取slice，这里类型系统会证明N = S + N，来保证这个slice不会越界, 然后获取一个bit，这里类型系统通过S大于0来保证N是一个有效的index.Model：RISC-V17Implement the 64-bit (RV64) version of the ISA (integer, multiply-divide, atomic, and compressed instructions

15、), with user, machine, and supervisor modes, and the Sv39 address translation mode.User-space definitions, machine- and supervisor-mode parts, the physical memory interface, virtual memory and address translation, instruction definitions, and the fetch-execute-interrupt loop.Model：RISC-V18Implement

16、the 64-bit (RV64) version of the ISA (integer, multiply-divide, atomic, and compressed instructions), with user, machine, and supervisor modes, and the Sv39 address translation mode.User-space definitions, machine- and supervisor-mode parts, the physical memory interface, virtual memory and address

17、translation, instruction definitions, and the fetch-execute-interrupt loop.Model：RISC-V19Example: LOADA sail definition will typically define an abstract syntax type (AST) of machine instructions;A decode function takes binary values to AST valuesAnd an execute function that describes how each of th

18、ose behaves at runtime. Model：RISC-V20Sequential executionThe ISA semantics complete enough to boot an OS, rather than a user-mode fragment.The model supports: 1) trap 2) various control and status registers (CSRs) 3) memory model The Sail model implements a very simple platform based on the Spike (

19、一种RISC-V模拟器)The model builds Ocaml and C emulators that can execute RISC-V ELF files, and both emulators provide platform support sufficient to boot Linux, FreeBSD and seL4.Model：ARMv8-A21The ARM architecture specifications use a pseudocode meta-language ASL (Architecture Specification Language), to

20、 express instruction behaviour.The public release does not include tools for executing or reasoning about the ASL code, and it is not in a form usable for mechanized proof.This paper co-designed Sail and developed an asl-to-sail translation tool (将ASL specifications转为Sail)，and thence into multiple t

21、heorem-prover and emulator code targets.Generation of Theorem Prover Definitions & Emulators22This paper implements automatic translations from Sail code to definitions for different popular theorem provers (Isabelle. HOL4 and Coq).This paper implements a simple direct mapping from Sail into Ocaml,

22、and C. (生成emulator code)Mechanized Proof23This paper proved a nontrivial property of the ARMv8-A specification in Isabelle/HOL to evaluate the usability of the generated theorem prover definitions.Address translation from virtual to physical memory addresses.Structure of the C emulator24How the C em

23、ulator is built from the Sail model:It consists of the handwritten C files (not colored) and files generated by the Sail compiler (yellow).riscv-sim: command line options, initialization, loads the ELF program or OS image into raw memory.riscv_model_$ARCH: 基于RV32或RV64架构编译生成，包括对平台接口的调用等C library：prov

24、ides the low-level details of the implementation of raw memory and bitvectors Validation25This paper validated the RISC-V model with the seL4 (一种操作系统微内核) and Linux boots and against the Spike reference simulator.The Ocaml emulator runs against the tests in the test-suite repository, and passes all tests for integer and compressed instructions for the user, supervisor and