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

Clc Number:

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 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, and ARM, and plays an important role in chip memory consistency verification, system software, and parallel program development. As an open-source architectural specification, the memory consistency model of RISC-V 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 consistency 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 consistency 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.

    Reference
    Related
    Cited by
Get Citation

Xuezheng Xu, Deheng Yang, Lu Wang, Tao Wang, Anwen Huang, Qiong Li. Sequential Consistency Per Location Theorem Proving in RISC-V Memory Consistency Model. International Journal of Software and Informatics, 2025,15(3):283~305

Copy
Related Videos

Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:October 17,2023
  • Revised:
  • Adopted:September 19,2024
  • Online: September 30,2025
  • Published:
Article QR Code