Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version)
Isla: integrating full-scale ISA semantics and axiomatic concurrency models (extended version)
复制标题
Isla：集成完整的 ISA 语义和公理并发模型（扩展版本）
DOI：
10.1007/s10703-023-00409-y
复制
发表时间：
2023
影响因子：
0.8
通讯作者：
Armstrong A
中科院分区：
文献类型：
--
作者：
Armstrong A
Armv 8-A和RISC-V等架构规范是软件验证的最终基础，也是硬件验证的正确性标准。它们应该定义程序的允许的顺序和松弛内存并发行为，但迄今为止，无论是在数学还是在工具中，都没有将全规模的并行集架构（伊萨）语义与公理化并发模型相结合。这些伊萨语义可以惊人地大和复杂，例如Armv 8-A的100 klines。在本文中，我们提出了一个工具，Isla，用于计算允许的行为的并发石蕊测试方面的全面伊萨定义，在帆船语言，和任意公理松弛内存并发模型，在猫语言。它是基于一个通用的符号引擎的帆船伊萨规范。我们为该工具配备了一个Web界面，使其可以广泛访问，并为Armv 8-A和RISC-V演示和评估它。符号执行引擎对其他验证任务也很有价值：它已被用于Arm Morello原型架构的自动伊萨测试生成，扩展了具有CHERI功能的Armv 8-A，以及针对Armv 8-A和RISC-V伊萨规范之上的二进制代码的Iris程序逻辑推理。通过使用全面和权威的伊萨语义，Isla让人们可以使用任意用户指令来评估石蕊测试。此外，由于这些伊萨规范提供了详细和验证的定义的顺序方面ofsystemsfunctionality，如所使用的虚拟机管理程序和操作系统，例如指令提取，异常和地址转换，我们的工具提供了一个基础，为这些开发并发语义。我们证明了这一点的Armv 8-A的自动提取和虚拟内存模型和Simner等人的例子。
Architecture specifications such as Armv8-A and RISC-V are the ultimate foundation for software verification and the correctness criteria for hardware verification. They should define the allowed sequential and relaxed-memory concurrency behaviour of programs, but hitherto there has been no integration of full-scale instruction-set architecture (ISA) semantics with axiomatic concurrency models, either in mathematics or in tools. These ISA semantics can be surprisingly large and intricate, e.g. 100klines for Armv8-A. In this paper we present a tool, Isla, for computing the allowed behaviours of concurrent litmus tests with respect to full-scale ISA definitions, in the Sail language, and arbitrary axiomatic relaxed-memory concurrency models, in the Cat language. It is based on a generic symbolic engine for Sail ISA specifications. We equip the tool with a web interface to make it widely accessible, and illustrate and evaluate it for Armv8-A and RISC-V. The symbolic execution engine is valuable also for other verification tasks: it has been used in automated ISA test generation for the Arm Morello prototype architecture, extending Armv8-A with CHERI capabilities, and for Iris program-logic reasoning about binary code above the Armv8-A and RISC-V ISA specifications. By using full-scale and authoritative ISA semantics, Isla lets one evaluate litmus tests using arbitrary user instructions with high confidence. Moreover, because these ISA specifications give detailed and validated definitions of the sequential aspects ofsystemsfunctionality, as used by hypervisors and operating systems, e.g. instruction fetch, exceptions, and address translation, our tool provides a basis for developing concurrency semantics for these. We demonstrate this for the Armv8-A instruction-fetch and virtual-memory models and examples of Simner et al.
登录
查看更多内容
DOI：
10.1145/2837614.2837615
发表时间：
2016-01
期刊：
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Shaked Flur;Kathryn E. Gray;Christopher Pulte;Susmit Sarkar;A. Sezgin;Luc Maranget;Will Deacon;Peter Sewell
通讯作者：
Shaked Flur;Kathryn E. Gray;Christopher Pulte;Susmit Sarkar;A. Sezgin;Luc Maranget;Will Deacon;Peter Sewell
多拷贝原子 ARMv8 和 RISC-V 的语义
DOI：
--
发表时间：
2019
期刊：
影响因子：
--
作者：
Christopher Pulte
通讯作者：
Christopher Pulte
影响因子：
1.8
作者：
Armstrong, Alasdair;Bauereiss, Thomas;Sewell, Peter
通讯作者：
Sewell, Peter
Morello 功能增强原型 Arm 架构的安全性经过验证
DOI：
10.1007/978-3-030-99336-8_7
发表时间：
2022
期刊：
2020 IEEE Symposium on Security and Privacy (SP)
影响因子：
--
作者：
Thomas Bauereiß;Brian Campbell;Thomas Sewell;A. Armstrong;Lawrence Esswood;I. Stark;Graeme Barnes;R. Watson;Peter Sewell
通讯作者：
Peter Sewell
针对 IBM POWER 多处理器的集成并发性和核心 ISA 架构包络定义以及测试预言机
DOI：
10.1145/2830772.2830775
发表时间：
2015
期刊：
2015 48th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO)
影响因子：
--
作者：
Kathryn E. Gray;Gabriel Kerneis;Dominic P. Mulligan;Christopher Pulte;Susmit Sarkar;Peter Sewell
通讯作者：
Peter Sewell