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

作者简介:

通讯作者:

中图分类号:

TP302

基金项目:

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


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

Fund Project:

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

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

    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.

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

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

复制
相关视频

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

京公网安备 11040202500063号