面向多核机器码的 SPARC TSO 内存模型形式化
计算机科学中的逻辑
2019-06-27 v1
摘要
SPARC 处理器在航空与航天工程等关键任务行业中有着广泛应用。因此，提供便于验证运行于这些处理器或与之交互的硬件与软件的形式化框架至关重要。本文提出了首个机械化的 SPARC 全序存储（TSO）内存模型，该模型运行于一个面向多核处理器的 SPARC 指令集架构（ISA）抽象模型之上。这两个模型均在定理证明器 Isabelle/HOL 中予以规约。我们形式化了两种 TSO 内存模型：一种是对公理化 SPARC TSO 模型的适配，另一种是新颖的操作性 TSO 模型，适用于验证执行结果。我们证明了该操作性模型相对于公理化模型是可靠且完备的。最后，我们以 SPARCv9 手册中的两个案例研究给出了验证示例。
关键词
引用
@article{arxiv.1906.11203,
title = {A formalisation of the SPARC TSO memory model for multi-core machine code},
author = {Zhe Hou and David Sanan and Alwen Tiu and Yang Liu and Jin Song Dong},
journal= {arXiv preprint arXiv:1906.11203},
year = {2019}
}
备注
15 pages + 2 pages of references