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

Clc Number:

TP302

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    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.

    Reference
    Related
    Cited by
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:October 17,2023
  • Revised:February 21,2024
  • Adopted:
  • Online: December 10,2024
  • Published: September 06,2025
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063