一句话：提出 AxSL 分离逻辑族，为 Arm-A 等宽松内存模型提供模块化 Hoare 式推理，并在 Iris 中机器化证明其可靠性。
Arm-A、RISC-V 等宽松并发内存模型打破“语法程序序与 reads-from 关系总导出执行顺序”的直觉：除依赖、屏障或同步限制外允许乱序，因而不存在“当前”状态，使 Hoare 逻辑等语法导向的模块化推理困难，资源无法隐式跨程序点流动。本文提出 AxSL，一族面向宽松硬件内存模型的分离逻辑，并在顺序一致性与 Arm-A 上实例化；Arm-A 实例刻画高性能系统代码低开销同步惯用法所需的细粒度推理。作者在 Iris 中机器化 AxSL 并证明其相对 Arm-A 公理化内存模型可靠。不同内存模型的实例化显示该方法通用，且基本独立于具体公理模型与指令集语义，为其他模型及生产级并发模型与完整 ISA 的组合提供推理路径。
Very relaxed concurrency memory models, like those of the Arm-A, RISC-V and IBM Power hardware architectures, underpin much of computing but break a fundamental intuition about programs, namely that syntactic program order and the reads-from relation always both induce order in the execution. Instead, out-of-order execution is allowed except where prevented by certain pairwise dependencies, barriers, or other synchronisation. This means that there is no notion of the ‘current’ state of the program, making it challenging to design (and prove sound) syntax-directed, modular reasoning methods like Hoare logics, as usable resources cannot implicitly flow from one program point to the next. We present AxSL, a family of separation logics for relaxed hardware memory models, and instantiate it on sequential consistency and on the Arm-A memory model. The Arm-A instance captures the fine-grained reasoning underpinning the low-overhead synchronisation idioms used by high-performance systems code. We mechanise AxSL in the Iris separation logic framework, illustrate it on key examples, and prove it sound with respect to the axiomatic memory model of Arm-A. By instantiating AxSL on different memory models, we demonstrate the generality of our approach, and show that it is largely generic in the axiomatic model and in the instruction-set semantics, offering a potential way forward for compositional reasoning for other models, and for the combination of production concurrency models and full-scale ISAs.
@article{LiuHPSBP26,
title = {An Axiomatic Basis for Computer Programming on Relaxed Hardware Architectures: The AxSL Logics},
author = {Zongyuan Liu and Angus Hammond and Thibaut Pérami and Peter Sewell and Lars Birkedal and Jean Pichon-Pharabod},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {48},
number = {1},
year = {2026},
doi = {10.1145/3786762}
}