软件学报

作者：徐学政，杨德亨，王璐，王涛，黄安文，李琼

单位：徐学政，军事科学院 国防科技创新研究院, 北京 10007111,杨德亨，军事科学院 国防科技创新研究院, 北京 10007102,王璐，军事科学院 国防科技创新研究院, 北京 10007103,王涛，军事科学院 国防科技创新研究院, 北京 10007104,黄安文，军事科学院 国防科技创新研究院, 北京 10007105,李琼，军事科学院 国防科技创新研究院, 北京 10007106

关键词：RISC-V;内存一致性;定理证明

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

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

来源：2025年第9期

《软件学报》期刊编辑部

查看软件学报杂志2025年第9期