RISC-V内存模型的同地址顺序一致性定理证明
CSTR:
作者:
作者单位:

作者简介:

通讯作者:

中图分类号:

TP302

基金项目:

国家自然科学基金(62102439, 62402515);


Proof of SC Per Location Theorem in RISC-V Memory Consistency Model
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

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

    Abstract:

    The memory consistency model defines constraints on memory access orders for parallel programs on multi-core systems and is an important architectural specification that is jointly followed by software and hardware. Sequential Consistency (SC) Per Location is one of the classic axioms of memory consistency model, which specifies that all memory operations with the same address in a multi-core system follow sequential consistency. It has been widely used in the memory consistency axiom model of classic architectures such as X86/TSO, Power, ARM, and plays an important role in chip memory consistency verification, system software, and parallel program development. As an open-source architectural specification, RISC-V's memory model is defined by global memory order, preserved program order, and three axioms (load value axiom, atomicity axiom, and progress axiom). It does not directly include SC Per Location as an axiom, which poses challenges for existing memory model verification tools and system software development. In this paper, we formalize 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 arbitrary same-address memory access sequences into deterministic finite automata for inductive proof. This research is a theoretical supplement to the formal methods of RISC-V memory consistency.

    参考文献
    相似文献
    引证文献
引用本文

徐学政,杨德亨,王璐,王涛,黄安文,李琼. RISC-V内存模型的同地址顺序一致性定理证明.软件学报,2025,36(9):1-18

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2023-10-17
  • 最后修改日期:2024-02-21
  • 录用日期:
  • 在线发布日期: 2024-12-10
  • 出版日期:
文章二维码
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号