Page 8 - 《软件学报》2025年第9期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
2025,36(9):3919−3936 [doi: 10.13328/j.cnki.jos.007292] [CSTR: 32375.14.jos.007292] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

*
RISC-V 内存一致性模型的同地址顺序一致性定理证明

徐学政, 杨德亨, 王 璐, 王 涛, 黄安文, 李 琼

(军事科学院 国防科技创新研究院, 北京 100071)
通信作者: 李琼, E-mail: qiong.li@nanhulab.ac.cn

摘 要: 内存一致性模型定义了并行程序在多核系统中的访存序约束, 是软硬件共同遵守的架构规范. 同地址顺序
一致性是内存一致性模型的经典公理之一, 它规定了多核系统中对于相同地址的所有访存操作遵循顺序一致性,
被广泛应用于 X86/TSO、Power、ARM 等经典架构的内存一致性模型中, 在芯片内存一致性验证及系统软件和并
行程序开发中发挥着重要作用. RISC-V 作为开源的架构规范, 其内存模型由全局访存序、保留程序序以及 3 条公理
(加载值公理、原子性公理和进度保证公理) 定义, 并未将同地址顺序一致性直接作为公理, 这给已有的内存模型
验证工具和系统软件开发带来了挑战. 面向 RISC-V 内存模型, 基于已定义的公理和规则, 将同地址顺序一致性作
为定理, 通过将任意同地址访存序列的构建抽象为确定有限状态自动机进行归纳证明. 该研究是对 RISC-V 内存一

致性相关形式化方法的一个理论补充.
关键词: RISC-V; 内存一致性; 定理证明
中图法分类号: TP302

中文引用格式: 徐学政, 杨德亨, 王璐, 王涛, 黄安文, 李琼. RISC-V内存一致性模型的同地址顺序一致性定理证明. 软件学报,
2025, 36(9): 3919–3936. http://www.jos.org.cn/1000-9825/7292.htm
英文引用格式: Xu XZ, Yang DH, Wang L, Wang T, Huang AW, Li Q. Sequential Consistency Per Location Theorem Proving in RISC-V
Memory Consistency Model. Ruan Jian Xue Bao/Journal of Software, 2025, 36(9): 3919–3936 (in Chinese). http://www.jos.org.cn/1000-
9825/7292.htm

Sequential Consistency Per Location Theorem Proving in RISC-V Memory Consistency Model

XU Xue-Zheng, YANG De-Heng, WANG Lu, WANG Tao, HUANG An-Wen, LI Qiong
(National Innovation Institute of Defense Technology, Academy of Military Sciences, Beijing 100071, China)
Abstract: The memory consistency model defines constraints on memory access orders for parallel programs in multi-core systems and is
an important architectural specification jointly followed by software and hardware. Sequential consistency (SC) per location is a classic
axiom of memory consistency models, which specifies that all memory access operations with the same address in a multi-core system
follow SC. Meanwhile, it has been widely employed in the memory consistency models of classic architectures such as X86/TSO, Power,
and ARM, and plays an important role in chip memory consistency verification, system software, and parallel program development. RISV
is an open-source architectural specification, and its memory model is defined by global memory orders, preserved program orders, and
three axioms (the load value axiom, atomicity axiom, and progress axiom). Additionally, it does not directly include SC per location as an
axiom, which poses challenges to existing memory model verification tools and system software development. This study formalizes the
SC per location as a theorem based on the defined axioms and rules in the RISC-V memory model. The proof process abstracts the
construction of memory access sequences with the same arbitrary address into deterministic finite automata for inductive proof. This study
is a theoretical supplement to the formal methods of RISC-V memory consistency.
Key words: RISC-V; memory consistency; theorem proving

* 基金项目: 国家自然科学基金 (62102439, 62402515)
收稿时间: 2023-10-17; 修改时间: 2024-02-21, 2024-08-15; 采用时间: 2024-09-19; jos 在线出版时间: 2024-12-10
CNKI 网络首发时间: 2025-05-15